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.