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 transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.
@article{arxiv.2310.04870,
title = {Lemur: Integrating Large Language Models in Automated Program Verification},
author = {Haoze Wu and Clark Barrett and Nina Narodytska},
journal= {arXiv preprint arXiv:2310.04870},
year = {2024}
}