03/21/24: How and Why to extend First Order Logic for Knowledge-Based Systems with Marc Denecker

Today Marc Denecker joined us to present How and Why to extend First Order Logic for Knowledge-Based Systems. This presentation provided the setup for a follow-on that Marc's student Simon Vandevelde is set to give on IDP-Z3, a formal reasoning machine that Marc and Simon have built. This was a really interesting talk touching on a variety of forms for formal logic, decision procedures, and industrial use-cases thereof, potentially with profound implications for the future and realizability of so-called AGI.

Today Daniel Melcer joined us to present Constrained Decoding for Code Language Models via Efficient Left and Right Quotienting of Context-Sensitive Grammars (https://arxiv.org/pdf/2402.17988). This is work he completed while at Amazon, and it's a really interesting project around how to constrain, guide, and check language models such that they generate valid code within a given context. We really appreciate that Daniel took the time to talk to us and hope you like the talk as much as we did!

Michael H. Borkowski is an Assistant Professor of Practice in the Department of Computer Science at Purdue University. Before joining Purdue, he earned his Ph.D. from the Department of Computer Science and Engineering at UC San Diego, where he was affiliated with the ProgSys Group. Today Michael joined us to discuss LiquidHaskell, a very cool project that incorporates a kind of refinement types, with SMT-based proofs, into Haskell. This was a really compelling talk and we hope you enjoy it as much as we did!

Today Brook Santangelo and John Sterrett

Gaspard Baye is a Cyber AI Ph.D. Candidate at the University of Massachusetts Dartmouth, where he researches AI-driven offensive and defensive security applications. Today Gaspard joined us to present "Hacking GenAI with LLM Red Teaming and Beyond" based on his recent DefCon talk. This was a really fun event with a great Q&A. Thanks to Jacob from the Trust Lab for hosting!

Navid Hashemi recently defended his PhD at USC and is about to begin a post-doc at Vanderbilt.  His research focuses on the intersection of Artificial Intelligence and Temporal Logics, with applications in Formal Verification of Learning Enabled Systems and Neurosymbolic Reinforcement Learning.  Today Navid joined us for a really exciting presentation about his work on metrizable logics for reinforcement learning, and a technique for verification thereof based on the over-approximation of reachable sets using ReLU.

Chengpeng Wangworking with Prof. Xiangyu Zhang. His research focuses on program analysis, especially software analysis, and in particular how existing analysis techniques intersect with emerging approaches from AI such as Large Language Models. Today Chengpeng joined us to talk about his recent NeurIPS paper proposing a novel static analysis technique based on LLMs. The technique is very interesting and highly informed by prior works in the static analysis space, but leverages LLMs as a kind of "oracle" to solve problems which, when handled statically, quickly become untenable. This was a really interesting talk and we're very greatful that Chengpeng took time out of his Sunday afternoon to talk to us!

Harry Eldridge is a Cryptography PhD student at Johns Hopkins, advised by Abhishek Jain and Matthew Green. His research (so far) touches on security and privacy implications of commodity hardware, which is a fascinating topic deserving of the mathematically disciplined, cryptographically informed approach his lab takes to such problems. Today Harry joined us to talk about his research into the problem of AirTag stalking, and how it can be ameliorated, while retaining acceptable performance, through cryptographic protocols. This was a very interesting talk with serious, real-world implications, and we hope you enjoy it as much as we did!

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 Mahmoudat 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.