Lemur: Integrating Large Language Models in Automated Program Verification
Abstract
The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that typically demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of derivation rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure, which led to practical improvements on a set of synthetic and competition benchmarks.
Cite
Text
Wu et al. "Lemur: Integrating Large Language Models in Automated Program Verification." NeurIPS 2023 Workshops: MATH-AI, 2023.Markdown
[Wu et al. "Lemur: Integrating Large Language Models in Automated Program Verification." NeurIPS 2023 Workshops: MATH-AI, 2023.](https://mlanthology.org/neuripsw/2023/wu2023neuripsw-lemur/)BibTeX
@inproceedings{wu2023neuripsw-lemur,
title = {{Lemur: Integrating Large Language Models in Automated Program Verification}},
author = {Wu, Haoze and Barrett, Clark and Narodytska, Nina},
booktitle = {NeurIPS 2023 Workshops: MATH-AI},
year = {2023},
url = {https://mlanthology.org/neuripsw/2023/wu2023neuripsw-lemur/}
}