AIMing: A Neuro-Symbolic Approach to Mechanized Mathematical Reasoning

Neural and generative artificial intelligence (AI) is opening up vast new opportunities for mathematical reasoning. This project introduces novel approaches for developing AI for mathematics, combining neural networks with symbolic, logic-based methods. The project goals aim to achieve a deeper understanding of how AI can learn and reason, as well as how to best combine symbolic and neural approaches.

Additionally, the project involves the development of new practical tools that mathematicians can use to formalize mathematical definitions and proofs, enabling proofs to be represented in a digital format so that they can be processed and verified by a computer. The methods to be developed in this project are intended to make the digitization of mathematics easier and more accessible.

In turn, this is intended to lead to new paradigms for using, teaching, and learning mathematics, as well as a deeper understanding of mathematics itself. The project is designed to be translational through collaborations with Lean developers as well as with industry. Educational and outreach efforts include developing tutorials on this topic, training students who will contribute to this research, and integrating the proposed research into existing courses. Open-source course material and code will be made available.

The project aims to achieve these goals by pursuing three thematic lines of research. First, the investigators will develop novel techniques that synergistically combine the features of machine learning and symbolic AI. This includes using machine learning for tasks that symbolic methods are unable to achieve and using symbolic methods to produce data and signals that can be used to train neural systems effectively.

Second, the investigators will develop new ways of making mathematical understanding explicit with the goal of enabling AI to understand mathematical proofs as well as help humans understand proofs generated by AI. The team will develop novel methods for extracting and learning from symbolic information, inferring the informal reasoning underlying a formal proof, and working with new definitions and lemmas.

Finally, the investigators will explore mechanisms for training machine learning systems to carry out focused tasks requiring specific mathematical expertise. The mathematical focus will center on proving inequalities. Novel methods will be designed to learn on their own by exploring a space of actions and consequences.

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.