SHF: Medium: Neurosymbolic Agents for Formal Theorem-Proving

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.