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的范围，从而为更安全的软件，更健壮的硬件和改进的数学严格性铺平了道路。该项目的新颖性包括引入一种“神经肯定代理”的类别，该类别能够实现这种自动化，以及几种实施此类代理的新方法。 PIS将在德克萨斯大学奥斯汀分校的培训研究生和本科生中，并帮助培养新一代的研究人员，具有正式方法和机器学习双重专业知识。特别是，该项目将正式的定理提供作为控制问题，并通过大型语言建模，强调模型，强化学习，证明和象征性分析和象征性分析和象征性的分析来解决此问题。具体的研究任务包括开发用于在证明数据上培训大语言模型的新方法，结合强化学习和寻找有效推理的方法，以及通过证明压缩自动发现证明策略。总的来说，该项目的方法构成了一个强大的工具包，可以自动化许多类型的证据，这些证明传统上是手工编写的，并有可能使ITP显着可用。该奖项反映了NSF的法定任务，并被认为是值得通过基金会的知识分子和更广泛影响的评估审查审查标准来通过评估来获得支持的。