ICLR 2024poster30 citations
Lemur: Integrating Large Language Models in Automated Program Verification
Haoze Wu, Clark Barrett, Nina Narodytska
Abstract
The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that 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.
Large Language ModelsFormal verification
BibTeX
@inproceedings{
wu2024lemur,
title={Lemur: Integrating Large Language Models in Automated Program Verification},
author={Haoze Wu and Clark Barrett and Nina Narodytska},
booktitle={The Twelfth International Conference on Learning Representations},
year={2024},
url={https://openreview.net/forum?id=Q3YaCghZNt}
}