Boston Computation Club

Ian Bicking is an engineer at Brilliant, which is also what he is. (Sorry, dad joke). Ian joined us today to talk about his super charming (and extremely interesting) weekend of experiments hacking various LLMs to solve puzzles using z3. The presentation was roughly the first 2/3 of the event and the remaining third presented a fantastic conversation about the future of AI, tool use, chain and tree of thought, o1, and more. Thanks again for joining us Ian!

Dhekra Mahmoud
at LIMOS in Clermont-Ferrand, France, where she researches the formal analysis of cryptographic protocols under the supervision of Pascal Lafoucade and Jannik Dreier. Today Dhekra joined us to present her recent USENIX paper Shaken, not Stirred -- Automated Discovery of Subtle Attacks on Protocols using Mix-Nets. This was a really interesting presentation with a good conversation afterword touching on some subtler points around the Dolev-Yao threat model, the limitations of ProVerif, and proof optimization.

Matej Panciak holds a PhD in mathematics and is a software engineer at the Argument Computer Corporation, where among other things, he works on Lurk. Lurk is a LISP for defining computations that can prove (in the ZKP sense) that they ran, which is probably useful for all sorts of cool things we haven't thought of yet, but right now, is pretty important for doing stuff on-chain. (I can easily imagine this being applicable to building something like a dweb version of AWS ... in some theoretical future where FHE is so good that you can just trust randos to run code for you). Anyway, Matej presented a super rad intro to Lurk, gave us a code demo (it worked!) and then enjoyed our usual über-nerd conversational segment at the end.

Derek Egolf is a PhD student (since 2021) at Northeastern University, advised by Stavros Tripakis. His primary research focus is the automatic generation of correct-by-construction systems from high-level specifications (synthesis). Today Derek talked about his recent paper in this vein, Efficient Synthesis of Symbolic Distributed Protocols by Sketching, to appear in FMCAD. This was a very interesting talk with a technical conversation afterword. We hope you enjoy it as much as we did!

Joshua Ramette (https://x.com/RametteJoshua) recently completed a PhD in physics at Mass Tech, and today he joined us to talk about his new project, Undermind. Josh and his friend Tom Hartke (https://www.tomhartke.com/) founded Undermind (YC S24) to radically improve academic literature search using a mixture of AI techniques. Their system is slow, deliberate, and very high quality. You can check out Undermind at www.undermind.ai , or peruse the query I did during the Q&A section here: https://www.undermind.ai/query_app/display_one_search/c743b66ee4378b12ae8bad1fe58975ba95da71e7f7a1d5c2f0c6973c677648cc/

Evan Pu ( https://evanthebouncy.github.io/ , @evanthebouncy on X ) is a senior research scientist at Autodesk AI Lab, working on code-generation for human-machine collaboration in CAD, and industry scale instruction-following dataset annotation. Today Evan joined us from a toilet (with the lid closed) so as not to wake up his wife due to a rather large time-zone delta, which was hilarious and a first for the Boston Computation Club. Anyway, this was a really fun talk with excellent Q&A and we hope you enjoy it as much as we did!

Arthur O’Dwyer is a C++ programmer and blogger who today joined us to talk about his musings on the algebraic structure of the popular web-game Infinite Craft. Infinite Craft is a clever little experiment in sandboxed exploration, and it turns out to give rise to a rather complex mathematical structure with some interesting background in theoretical CS. Arthur covered all this and more in his presentation, which was super interesting and a lot of fun to watch.

Check out Arthur's original blog post here: https://quuxplusone.github.io/blog/2024/03/03/infinite-craft-theory/

Check out Arthur's slides here: https://bstn.cc/artifacts/arthurODwyer/infiniteCraft.pdf

Evan Boehs is a HIGH SCHOOL STUDENT who broke the freaking internet.  What more do I need to say?  Hire this kid.  Maybe I will.  It's a race.  

Evan made an npm package called everything which installs everything.  Then he got stuck in a dependency loop when someone tried to delete something.  It turns out this is a nearly impossible problem to solve and he totally broke npm.  Then a bunch of adults got made at him, when really, they should have been mad at themselves for building a bad system.  

You can read Evan's full story here: https://boehs.org/node/npm-everything

June Marcuse

Adam Karvonen was my coworker at Galois and is a bright guy doing really interesting stuff in the ML interpretability space. Today he joined us to present his work on Chess-GPT, you guessed it, a GPT model that can play chess. The punchline isn't so much how good the model is as it is how the model "thinks" -- Adam provides compelling evidence that the model internally reasons about an actual board state, and learns to make legal moves. The discussion on this one was great and we really appreciate that Adam took the time to talk to us! Also -- you should hire him! He's doing MATS but will be on the job market at the end of the Summer.