TLDR: PROOFBRIDGE is a novel AI framework designed to automatically translate entire mathematical theorems and their proofs from natural language into the formal language Lean 4. It achieves this by using a joint embedding model that aligns natural language and formal language proofs in a shared semantic space, enabling the retrieval of relevant formal examples. These examples then guide a large language model (LLM) during the translation process. The framework also incorporates an iterative repair loop that leverages Lean’s type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity of the generated formal proofs. Experiments show PROOFBRIDGE significantly outperforms existing methods in both semantic and type correctness.
The world of mathematics relies heavily on proofs to establish the truth of theorems. Traditionally, these proofs are written in natural language, which, while intuitive for humans, can sometimes be ambiguous and prone to subtle errors. To address this, computer-verifiable formal languages like Lean 4 have emerged, offering a way to create proofs with absolute certainty. However, translating complex human-written proofs into these strict formal languages is a monumental challenge, often requiring deep mathematical expertise and detailed knowledge of the formal system.
Current AI methods typically tackle this problem in two separate stages: first translating the theorem statement, and then attempting to generate the proof. This disconnected approach often falls short when it comes to fully automating the formalization of an entire natural language proof.
Introducing PROOFBRIDGE: A Unified Approach
A new framework called PROOFBRIDGE aims to bridge this gap by offering a unified solution for automatically translating complete natural language theorems and their proofs into Lean 4. Developed by researchers from Georgia Institute of Technology and Bogazici University, PROOFBRIDGE represents a significant step forward in the field of proof auto-formalization.
At its heart, PROOFBRIDGE employs a clever technique called a joint embedding model. This model learns to understand both natural language (NL) and formal language (FL) theorem-proof pairs, mapping them into a shared semantic space. Imagine this space as a conceptual map where similar mathematical ideas, regardless of whether they are expressed in English or Lean 4, are placed close together. This alignment enables the system to perform ‘cross-modal retrieval,’ meaning it can take a natural language proof and find semantically relevant formal Lean 4 examples from a vast database.
These retrieved formal examples act as crucial guides for the translation process. Instead of trying to generate a formal proof from scratch, which is incredibly difficult, the system learns from demonstrations of how similar mathematical concepts and proof strategies have been formalized before. This ‘learning from demonstrations’ approach helps the AI generate more accurate and verifiable Lean 4 proofs.
How PROOFBRIDGE Works
The framework integrates several key components:
- Joint Embedding Model: This model uses specialized encoders for natural language and formal language. The natural language encoder processes the human-written proof, while the formal language encoder analyzes the structured ‘tactic-style’ proofs in Lean 4, which are represented as Directed Acyclic Graphs (DAGs) of proof states and tactics. Through a process called contrastive learning, the model ensures that semantically equivalent NL and FL pairs are embedded closely in the shared space, while unrelated pairs are pushed apart.
- Retrieval-Augmented Fine-Tuning: Once the joint embedding model can effectively retrieve relevant formal proofs, a large language model (LLM), specifically a fine-tuned version of Kimina-Prover-RL-1.7B, is trained. This LLM learns to translate natural language inputs into Lean 4, but critically, it is conditioned on the top-K relevant formal proofs retrieved by the joint embedding model. This provides rich contextual information, guiding the LLM towards correct formalization patterns.
- Iterative Proof Repair: Even with retrieval augmentation, LLMs can sometimes produce errors. PROOFBRIDGE includes an iterative repair mechanism during the inference phase. This involves two types of verification: syntactic verification (using Lean’s type checker to ensure the proof is grammatically correct and valid within Lean) and semantic verification (using an LLM-based judge to confirm that the generated formal theorem accurately represents the original natural language theorem). If errors are found, the system generates feedback and attempts to repair the proof iteratively, ensuring both correctness and fidelity.
Also Read:
- ProofOptimizer: An AI System for Concise Formal Mathematics
- Peer Review for Large Language Models: A Game Theory Approach
New Datasets and Impressive Results
To facilitate this research, the team curated two new datasets: NUMINAMATH-LEAN-PF, a large-scale collection of 38.9k natural language and Lean 4 theorem-proof pairs, and MINIF2F-TEST-PF, a benchmark specifically tailored for proof auto-formalization in Lean v4.15.0.
Experiments show that PROOFBRIDGE significantly outperforms existing state-of-the-art LLMs and auto-formalization tools. For instance, its cross-modal retrieval quality improved Recall@1 by up to 3.28 times compared to previous methods. In terms of proof auto-formalization, PROOFBRIDGE achieved a remarkable +31.14% improvement in Semantic Correctness (SC) and +1.64% in Type Correctness (TC) over the strong baseline Kimina-Prover-RL-1.7B at pass@32 on the MINIF2F-TEST-PF benchmark.
This work demonstrates that by integrating structured embeddings, retrieval guidance, and verifier feedback, AI systems can achieve more reliable and accurate auto-formalization of mathematical proofs, moving closer to a future where the correctness of complex mathematical arguments can be routinely verified by computers. You can read the full research paper here.
