Large Language Models for Verified Programs

Background

Static program verification tools allow establishing formal guarantees for important program properties such as correctness and memory safety. Such tools usually compromise between the level of automation and the significance of the results. A common middle ground is to automate the proof but requires developers to manually provide specifications. Providing these specifications can be expensive and difficult, limiting the popularity and the practicality of such verification tools. Therefore, it is a key research challenge to ease the burden of manually constructing specifications.

Automated program synthesis has recently seen major advancements through the use of machine learning techniques. Large language models (LLMs) such as external page Codex are capable of generating functional code from natural language prompts. However, LLMs are probabilistic and lack formal guarantees on the correctness and the safety of generated code.

An LLM augmented with the understanding of verification could help to improve both aspects mentioned above. Such a model can be used to automatically infer specifications for existing code to reduce the overhead of manually providing specifications. Moreover, it can also be used to directly generate verifying code with specifications, potentially from natural language prompts. As a result, the trust in code synthesized by LLMs can be greatly improved.