Syntax-Guided Synthesis (SyGuS) with LLM and Predicate Sub-Typing 

Syntax-Guided Synthesis (SyGuS) with LLM and Predicate Sub-Typing

Stéphane Graham-Lengrand, Formal Methods Group, CSL, SRI International

The emergence of generative AI, specifically LLMs, undoubtedly opens up exciting possibilities for the automated production of code.  It also raises new assurance challenges regarding the properties of the produced code, starting with the correctness of the code with respect to its intended purpose. We propose a code synthesis approach where Formal Methods guide the LLM output towards a provably correct code.

Dr Stéphane Graham-Lengrand is a Technical Director at SRI, where he heads the Formal Methods group within the Computer Science Laboratory. He graduated in 2007 with a joint Ph.D. from the University of St Andrews, U.K., and the University of Paris 7, France. His Ph.D. thesis on Computational Logic received the 2007 Ackermann award. Before joining SRI, Dr Graham-Lengrand was a tenured researcher at France's CNRS institute and served as a lecturer at École Polytechnique. His expertise in formal methods includes program verification, correct-by-construction software, type systems, and semantics for programs and proofs, with a primary focus on interactive and automated symbolic reasoning, specifically SMT-solving. Dr Graham-Lengrand drives the development of SRI's SMT-solver Yices. He leads the formal methods component of the STITCHES Air Force program of record and is currently the SRI principal investigator for the DARPA SIEVE program on Zero-Knowledge proofs and the DARPA IDAS program on adaptive software.