TLDR: Ax-Prover is a new multi-agent system that combines large language models (LLMs) with Lean proof assistant tools to perform automated theorem proving. It addresses limitations of specialized provers by offering generalizability across scientific domains like mathematics and quantum physics, enabling human-AI collaboration, and simplifying deployment. The system, composed of an Orchestrator, Prover, and Verifier, iteratively generates and verifies formal proofs. Evaluations show Ax-Prover outperforms baselines on new datasets and is competitive on public benchmarks, demonstrating its potential as a robust and accessible tool for formal verification in scientific research.
A new research paper introduces Ax-Prover, an innovative framework designed to tackle the complex challenge of automated theorem proving in diverse scientific fields, including mathematics and quantum physics. This system aims to bridge the gap between the broad reasoning capabilities of large language models (LLMs) and the strict formal verification required in scientific proofs.
Traditional LLMs, while powerful in general reasoning, often struggle with the precise, step-by-step formalization needed for theorem proving. On the other hand, specialized theorem provers are highly effective within their specific domains, primarily mathematics, but lack the flexibility to generalize to new areas or adapt to evolving proof libraries. They also tend to be resource-intensive and difficult to deploy.
Ax-Prover addresses these limitations by employing a multi-agent system that integrates general-purpose LLMs with Lean tools through a mechanism called the Model Context Protocol (MCP). This setup allows LLMs to leverage their vast knowledge and problem-solving skills while ensuring formal correctness by interacting with the Lean proof assistant environment.
The framework operates with three specialized agents: the Orchestrator, the Prover, and the Verifier. The Orchestrator manages the overall workflow, assigning tasks, routing feedback, and determining when a proof is complete. The Prover is the core constructive agent, responsible for generating proof sketches, formalizing them into Lean code, and iteratively refining them using Lean tools. These tools allow the Prover to inspect goals, search for relevant theorems, identify errors, and verify each step. Finally, the Verifier acts as a gatekeeper, independently compiling the generated proof and reporting any errors or incompleteness back to the Orchestrator.
A key advantage of Ax-Prover is its generalizability. Unlike specialized provers that are often trained on fixed versions of mathematical libraries like Mathlib, Ax-Prover can work with any recent version of Mathlib without needing retraining. This flexibility allows it to adapt to new scientific domains beyond traditional mathematics, such as abstract algebra and quantum theory.
The researchers evaluated Ax-Prover on several benchmarks, including existing public datasets like NuminaMath-LEAN and PutnamBench, and two new datasets they introduced: AbstractAlgebra and QuantumTheorems. The AbstractAlgebra dataset focuses on graduate-level algebraic structures, while QuantumTheorems explores foundational quantum mechanics. Ax-Prover demonstrated competitive performance on public datasets and significantly outperformed state-of-the-art specialized provers on the new, more diverse benchmarks.
The analysis of tool usage within Ax-Prover revealed that the Prover agent makes extensive and reliable use of Lean tools for tasks such as editing files, diagnosing messages, inspecting proof goals, and searching for theorems. This tight feedback loop of reasoning and tool interaction is crucial for building high-quality, formally verified proofs.
From a practical standpoint, Ax-Prover offers significant deployment advantages. It relies on API calls to existing frontier LLMs, eliminating the need for users to host or deploy specialized, high-spec machines. This makes it more accessible and cost-effective compared to specialized provers, which often require substantial computational resources and MLOps expertise.
Beyond autonomous proving, Ax-Prover also excels as a collaborative assistant. In a compelling use case, an expert mathematician collaborated with Ax-Prover to formalize and verify the proof of a complex cryptography theorem. The system not only helped structure the proof and validate lemmas but also identified an error in the original informal reasoning, showcasing its potential to advance scientific knowledge. This collaborative effort, resulting in over 2000 lines of Lean code, was completed in just two working days on a laptop, highlighting the efficiency and accessibility of the framework. You can read the full research paper for more details: Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics.
Also Read:
- Smart Logic: How LLMs Can Pick the Best Language for Complex Reasoning
- Audit-of-Understanding: A New Framework for Reliable Mathematical Reasoning in Language Models
The development of Ax-Prover represents a significant step towards verifiable scientific artificial intelligence, where AI systems can contribute to scientific discovery through formally validated reasoning. Future plans include enhancing the framework with parallelized agents for exploring multiple proof paths and integrating a long-term memory module for sustained collaborative research.
