Summary of AIPROVER: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness

Summary (Overview)

• AIPROVER is a novel agentic framework that jointly post-trains a 119B open-weight language model (Leanstral-1.5) and evolves its agentic tool-calling harness via HarnessEvolve, a certificate-driven evolutionary search algorithm, for research-level proof auto-formalization.
• The framework introduces SAM (Semantic Alignment Model) fine-tuning, which uses contrastive learning to align natural language (NL) and formal language (FL) representations in the LLM, treating an NL theorem-proof pair and its Lean counterpart as the same mathematical object.
• LoCoBench is introduced as a new benchmark: 58.9k instances (18.8k labeled NL–Lean pairs, 40.1k unlabeled NL–Mizar pairs) with a 771-instance validation split containing theorem–proof pairs with no public Lean formalization.
• AIPROVER improves pass@4 semantic correctness from 15.7% to 36.7% over its base model, outperforming all other open-weight systems and Aristotle (18.4%). As a skill for Claude Code and Codex, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively.
• The system is cost-efficient: 24% cheaper than Numina-Lean-Agent while achieving higher accuracy, establishing a new accuracy–cost Pareto frontier for research-level AFPS.

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses proof auto-formalization: translating natural-language (NL) theorems and proofs into formal language (FL) counterparts (e.g., Lean) for mechanical verification. While recent breakthroughs (Navier–Stokes conjecture, Fermat's Last Theorem formalization) demonstrate progress, five critical limitations plague existing systems:

1. Cost: Frontier model formalization can take 11 days and 6 billion output tokens
2. Human-in-the-loop dependence: Mathematicians must supply target statements and stay involved
3. Jagged intelligence: Frontier models excel at familiar tasks but falter on unfamiliar ones
4. Semantic drift: Compilation success doesn't guarantee the formalization preserves the theorem's meaning
5. Lack of accessibility: Headline results rely on non-public models, preventing cross-checking

Theoretical Foundation

The problem is formally defined as: Given an NL passage $M_{NL} = \langle T_{NL}, P_{NL} \rangle$ (theorem + proof), learn a map to an equivalent FL pair $\widehat{M}_{FL} = \langle \widehat{T}_{FL}, \widehat{P}_{FL} \rangle$ in Lean satisfying four properties:

• (a) Type-correctness: Lean's kernel accepts $\widehat{M}_{FL}$
• (b) Completeness: No placeholders (sorry, admit) are used
• (c) Semantic correctness: $\widehat{T}_{FL}$ states exactly theorem $T_{NL}$ under the same definitions
• (d) Proof faithfulness: $\widehat{P}_{FL}$ follows the proof strategy of $P_{NL}$

Properties (a) and (b) are mechanically certified by Lean; (c) and (d) are undecidable (Church, 1936; Turing, 1937) and require a judge.

Key insight: The authors hypothesize that an LLM that internalizes the NL–FL equivalence (rather than relying on external retrieval encoders, critics, or scorers) will formalize more accurately. Additionally, they argue that an agent's performance depends as much on its harness as on the model, motivating joint model–harness co-evolution.

Methodology

1. Semantic Alignment Model (SAM) Fine-Tuning

SAM is a decoder-only LLM fine-tuned to represent $M_{NL}$ and $M_{FL}$ as the same mathematical object. Two views are created:

• NL view: $h_{NL} \in \mathbb{R}^d$ — the hidden state at the [PRED] token when running on $u = M_{NL} \parallel [PRED] \parallel M_{FL}$
• FL view: $h_{FL} \in \mathbb{R}^d$ — the final hidden state when running on $M_{FL}$ alone

The training objective combines cross-entropy loss on the FL tokens with a contrastive InfoNCE loss:

$$\mathcal{L}_{\mathrm{CE}} = -\frac{1}{|F|} \sum_{t \in F} \log P_{\theta,\Delta}(u_t \mid u_{<t}), \qquad \mathcal{L}_{\mathrm{align}} = -\frac{1}{2B} \sum_{i=1}^{B} \left[ \log \frac{e^{S_{ii}}}{\sum_j e^{S_{ij}}} + \log \frac{e^{S_{ii}}}{\sum_j e^{S_{ji}}} \right]$$

where $S_{ij} = z_{NL,i}^\top z_{FL,j}/\tau$ is the cosine similarity of unit-normalized projected views, scaled by temperature $\tau$. The full objective is $\mathcal{L} = \mathcal{L}_{\mathrm{CE}} + \lambda \mathcal{L}_{\mathrm{align}}$ with $\lambda > 0$.

2. Reward Design (Reward Ladder)

A four-check reward ladder evaluates candidates, with each check presupposing the preceding one:

The four checks are: Type-correctness (TC) — Lean accepts the file; Completeness (CP) — no sorry/axiom bypass; Semantic correctness (SC) — logical equivalence via extended BEq$^{+}$ testing both directions ($T_{FL} \Rightarrow \widehat{T}_{FL}$ and $\widehat{T}_{FL} \Rightarrow T_{FL}$); Length fidelity (LF) — $v_{LF} = \exp\left(-\left|\ln\frac{|\widehat{P}_{FL}| + c}{|P_{FL}| + c}\right|\right)$ with $c = 60$ characters of slack.

3. HarnessEvolve: Certificate-Driven Evolutionary Search

HarnessEvolve evolves harness control flow while the model stays frozen. It maintains a search memory tree where:

• Each node stores a harness, its fitness, per-instance rewards/certificates, and verdict
• All evaluated harnesses are retained (accepted or rejected), enabling the mutator to learn from both successes and failures (inspired by conflict-driven clause learning in SAT solvers)
• Parent selection uses UCB1/UCT-style exploration: $Q(h) + c\sqrt{\ln(1 + t)/(1 + k(h))}$ where $Q(h) = 1 - \min(1, (f^* - f(h))/3\sigma)$
• A frontier coding agent mutates the parent harness using read, write, search, and bash tools
• Fitness is computed as $f(h) = \frac{1}{k|\mathcal{D}|} \sum_{d \in \mathcal{D}} \sum_{j \leq k} r_j(d)$

4. Agentic RLSF (Reinforcement Learning via Symbolic Feedback)

RLSF post-trains the model inside the frozen harness using GRPO (Group-Relative Policy Optimization):

• $K$ episodes per training instance yield rewards $r_1, \ldots, r_K$ from the verifier
• Advantage for rollout $k$: $A_k = r_k - \bar{r}$ (group mean baseline, no standard deviation normalization)
• The fine-grained reward ladder is essential: under binary verification rewards, groups where all rollouts fail or succeed yield $A_k = 0$ for all $k$ and no gradient

5. LoCoBench Benchmark Construction

LoCoBench comprises 58.9k instances from four sources:

Validation instances are out-of-distribution: Mizar theorems with the longest proofs from papers disjoint from training, plus 71 bounded-arithmetic textbook theorems. NL content is generated via informalization (FL-to-NL) using coding agents with CriticLeanGPT feedback loops.

Empirical Validation / Results

Main Results on LoCoBench-Val (Pass@4, %)

Key Findings

1. Open-weight models without Lean-tailored harnesses stay below 3.9% TC+SC; AIPROVER raises this nearly tenfold to 36.7%
2. AIPROVER outperforms frontier LLMs: GPT-5.6-Sol (25.2%), Aristotle (18.4%), Codex (34.1%); only Claude Code alone (41.9%) is higher
3. As a skill for coding agents: AIPROVER adds +28.3% to Codex and +37.9% to Claude Code, vs. +10.4%/+30.6% for Numina-Lean-Agent and +7.8%/+12.4% for OpenGauss

Ablation Insights

• Seed harness: Wrapping the base model raises TC from 27.4% to 57.6%
• HarnessEvolve alone: Lifts TC to 84.4% but full proofs only to 22.6% (harness fixes compilation, not semantics)
• SAM: Raises matched NL–FL cosine similarity from 0.11 to 0.75; RLSF mostly preserves it (0.64)
• Interleaved RLSF + HarnessEvolve: Full proofs reach 36.7%

Cost Analysis

AIPROVER forms the accuracy–cost Pareto frontier: higher accuracy at 14–24% lower cost than alternatives.

Theoretical and Practical Implications

Theoretical Contributions

• Semantic alignment as a training signal: AIPROVER is the first to make semantic alignment a training objective rather than a post-hoc filter, building NL–FL equivalence directly into the model via contrastive learning
• Certificate-driven co-evolution: The framework demonstrates that harness and model can be mutually optimized, with verifier certificates guiding both evolutionary search and reinforcement learning
• Fine-grained reward design: The reward ladder shows that graded rewards (distinguishing ill-typed, incomplete, and complete proofs) are essential for effective RL in formal mathematics, where binary rewards yield no gradient signal

Practical Implications

• Accessibility: AIPROVER makes research-level formalization accessible with open-weight models on local GPUs, removing the dependency on costly frontier APIs
• Human-in-the-loop reduction: The system runs unattended, addressing the human-dependence limitation of prior approaches
• Skill integration: AIPROVER can be deployed as a Lean-specialist sub-agent within frontier coding agents, improving both accuracy and cost-efficiency of existing systems
• Benchmark contribution: LoCoBench provides the first large-scale research-level benchmark with Mizar-to-Lean transfer, enabling standardized evaluation of AFPS systems

Conclusion

AIPROVER demonstrates that an open-weight LLM can achieve research-level proof auto-formalization through three synergistic innovations: (1) SAM fine-tuning that aligns NL and FL representations in the model, (2) a fine-grained verifier reward ladder that provides learning signal from partial successes, and (3) HarnessEvolve, which adapts the harness control flow to the evolving model while learning from both accepted and rejected designs.

The framework establishes a new state-of-the-art for open-weight AFPS systems (36.7% vs. 21.5% for the best prior open-weight system) and pushes the accuracy–cost frontier when integrated with frontier coding agents. Key future directions include: extending to additional proof assistants (Isabelle/HOL, Rocq), developing reliable proof-faithfulness checks (currently not scored due to lack of reliable judges), and scaling the co-evolution framework to even larger models and more diverse mathematical domains.