EAGER: Proof-Carrying Code Completions

University Of California-Davis, Davis CA

Investigators

Abstract

Today's programmers are using large language models (LLMs) to accelerate software development by automatically generating code suggestions and code completions. Widely used examples include GitHub Copilot and OpenAI ChatGPT. However, code generated by these tools can have bugs that are not caught by users, and this presents a serious safety risk. This project will leverage an idea called "proof-carrying code" where code suggestions are packaged together with a mathematical proof of their safety, allowing programmers to be confident that the program is safe to deploy. This project will develop tools, techniques, and empirical results for using LLMs to generate trustworthy code together with mathematical proofs. Project outcomes, including code, data sets and course materials, will be developed in the open and made available online to researchers working on LLMs, end users of LLM-based code generation, and early industry and open source adopters. In the 1990s, researchers in the programming languages community recognized a powerful idea known as proof-carrying code (PCC): they showed how code can be shipped together with a proof of its safety that could be vetted – efficiently – by an end user. LLMs can be viewed as high-resource computations, and LLM users as low-resource entities. Seen through this lens, PCC maps naturally to the safety problem for LLM-generated code. The technical aims of this project are divided into four thrusts: (1) Gather empirical data on code that is currently generated by LLMs, and to determine core safety risks, to enable building of a dataset that will be useful to other researchers; (2) Develop a framework for PCC, including enumeration of safety properties of interest and showing how to instantiate the framework with existing program verification, proof languages, and proof frameworks; (3) Implement new tools for verification condition generation from source code for popular programming languages and for specific safety properties; and (4) Evaluate the use of LLMs for generating proofs in this context, including developing new algorithms and proof sampling techniques to improve model effectiveness. The research will lead to new insights into the current capabilities of LLMs, to new relevant safety properties for code generation in a black-box setting, and to new techniques to generate verification conditions -- to bridge the gap in formal verification technology from special-purpose languages like Coq and Dafny to general-purpose programming languages in popular use. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.