SHF: Medium: Neurosymbolic Agents for Formal Theorem-Proving

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

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.