SHF: Medium: Neurosymbolic Agents for Formal Theorem-Proving

SHF：介质：用于形式定理证明的神经符号代理

• 批准号: 2403211
• 负责人: Swarat Chaudhuri
• 金额: $ 120万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-06-01 至 2028-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2403211&HistoricalAwards=false
• 关键词: SHF; Medium; Neurosymbolic; Agents; Formal

This project studies artificial intelligence (AI)-powered techniques for enhancing the accessibility and efficiency of interactive formal theorem provers (ITPs). ITPs -- for example, Coq and Lean -- are a longstanding approach to the formal verification and are beginning to see uses in mathematics research as well. However, they tend to have a steep learning curve and require proofs to be spelled out in painful detail and are hence only accessible to a limited community of experts. The project's impact is to broaden the reach of ITPs by automating the low-level parts of theorem-proving, thereby paving the way to safer software, more robust hardware, and improved mathematical rigor in diverse applications. The project's novelties include introducing a category of "neurosymbolic agents" that enable such automation, and several new ways of implementing such agents. The PIs will be involved in training graduate and undergraduate students at University of Texas at Austin and help cultivate a new generation of researchers with dual expertise in formal methods and machine learning.Specifically, the project formulates formal theorem-proving as a control problem and approaches this problem through a combination of large language modeling, reinforcement learning, and symbolic analysis of proofs and theorems. Concrete research tasks include the development of new methods for training large language models on proof data, combining reinforcement learning and search for efficient inference, and the automatic discovery of proof tactics through proof compression. Collectively, the project's methods constitute a powerful toolkit that can automate many kinds of proofs that have traditionally been written by hand and have the potential to make ITPs significantly more usable.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.

该项目研究人工智能 (AI) 驱动的技术，以提高交互式形式定理证明器 (ITP) 的可访问性和效率。 ITP（例如 Coq 和 Lean）是一种长期存在的形式验证方法，并且也开始在数学研究中得到应用。然而，它们往往具有陡峭的学习曲线，并且需要以痛苦的细节阐明证明，因此只有有限的专家群体才能访问。该项目的影响是通过自动化定理证明的低级部分来扩大 ITP 的范围，从而为更安全的软件、更强大的硬件以及在不同应用中提高数学严谨性铺平道路。该项目的新颖之处包括引入一类能够实现这种自动化的“神经符号代理”，以及实现此类代理的几种新方法。 PI将参与德克萨斯大学奥斯汀分校研究生和本科生的培训，帮助培养具有形式方法和机器学习双重专业知识的新一代研究人员。具体来说，该项目将形式化定理证明制定为控制问题和方法通过结合大型语言建模、强化学习以及证明和定理的符号分析来解决这个问题。具体的研究任务包括开发在证明数据上训练大型语言模型的新方法，结合强化学习和搜索高效推理，以及通过证明压缩自动发现证明策略。总的来说，该项目的方法构成了一个强大的工具包，可以自动化传统上手工编写的多种证明，并有可能使 ITP 的可用性显着提高。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准。