In the past few years, Large Language Models (LLMs) have exploded in usefulness and popularity for code generation tasks. However, LLMs still struggle with accuracy and are unsuitable for high-risk applications without additional oversight and verification. In particular, they perform poorly at generating code for highly complex systems, especially with unusual or out-of-sample logic. For such systems, verifying the code generated by the LLM may take longer than writing it by hand. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis. We develop a benchmark to test our solution and show that our method allows the pipeline to solve problems previously intractable for LLM code generation.
@article{arxiv.2410.19736,
title = {Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis},
author = {William Murphy and Nikolaus Holzer and Feitong Qiao and Leyi Cui and Raven Rothkopf and Nathan Koenig and Mark Santolucito},
journal= {arXiv preprint arXiv:2410.19736},
year = {2024}
}