We are excited to announce one fully funded postdoctoral research position as part of our newly accepted project on AI-driven automated reasoning for higher-order logic and algebraic theories. The project builds on recent breakthroughs such as Enigma, Deepire, and Monte Carlo proof search, and aims to develop autonomous reasoning systems that combine symbolic and statistical guidance, applied to open research-level problems in algebraic domains (e.g., loop theory, AIM Conjecture) and large-theory interactive theorem proving.
[Read More]Deep Exploratory Engine for Precise Expert Reasoning
The project is concerned with developing machine learning guidance for modern state-of-the-art automatic theorem provers (ATPs) capable of generating correct proofs. In particular, it focuses on AI guidance for higher-order and dependently typed calculi, which are essential for directly addressing problems in the formalization of mathematics, as well as guidance for the Prover9 system, which plays a crucial role in the AIM project by Kinyon and Veroff. The approach combines neural and symbolic learning methods: deep learning for proof guidance is complemented by the hints method, which is critical in handling very large proofs of open conjectures.
Goals
To achieve the overall goal of powerful automated reasoning for mathematics, the project pursues the following four objectives:
-
Developing effective AI-based guidance for higher-order automated reasoning systems that can prove large numbers of goals in formalized mathematics libraries.
-
Designing proof advice and efficient automation for dependently typed proof foundations.
-
Integrating strong guided automated theorem provers into modern state-of-the-art proof assistants, including their hammer systems, and optimizing them for large proof libraries.
-
Advancing towards an autonomous reasoning system able to tackle open mathematical problems, using learning techniques such as conjecturing, reinforcement, and inspiration from existing proofs.
Partnership
The project is an international cooperation between
- 🇦🇺 University of Melbourne (UoM), Australia, and
- 🇨🇿 Czech Technical University in Prague (CTU), Czech Republic,
uniting complementary expertise to develop AI-guided automated reasoning systems.
