EAGER: Proof-Carrying Code Completions

EAGER：携带证明的代码完成

• 批准号: 2403762
• 负责人: Caleb Stanford
• 金额: $ 30万
• 依托单位: University of California-Davis
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-02-15 至 2025-07-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2403762&HistoricalAwards=false
• 关键词: EAGER; Proof; Carrying; Code; Completions

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.

当今的程序员正在使用大型语言模型 (LLM) 通过自动生成代码建议和代码完成来加速软件开发，广泛使用的示例包括 GitHub Copilot 和 OpenAI ChatGPT，但是这些工具生成的代码可能存在用户无法发现的错误。这带来了严重的安全风险，该项目将利用一种称为“携带证明的代码”的想法，其中代码建议与其安全性的数学证明打包在一起，使程序员能够确信该程序是安全的。该项目将开发工具、技术和经验结果，以使用法学硕士生成值得信赖的代码以及数学证明。项目成果（包括代码、数据集和课程材料）将公开开发并在线提供给研究人员。在 20 世纪 90 年代，编程语言社区的研究人员认识到了一个强大的想法，称为证明代码（PCC）：他们展示了代码如何可以一起运送通过最终用户可以有效审查的安全性证明，LLM 可以被视为高资源计算，而 LLM 用户则可以被视为低资源实体，从这个角度来看，PCC 自然地映射到了安全问题。该项目的技术目标分为四个主旨：（1）收集目前由法学硕士生成的代码的经验数据，并确定核心安全风险，以构建对以下有用的数据集。其他研究人员；（2）开发 PCC 框架，包括枚举感兴趣的安全属性并展示如何使用现有程序验证、证明语言和证明框架实例化该框架；（3）实现从源代码生成验证条件的新工具对于流行的编程语言和特定的安全属性；以及（4）评估在这种情况下使用法学硕士生成证明，包括开发新的算法和证明采样技术以提高模型的有效性。法学硕士当前的能力，到新的黑盒设置中代码生成的相关安全属性，以及生成验证条件的新技术——弥合形式验证技术从 Coq 和 Dafny 等专用语言到通用编程语言的差距​​该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。