AI enhances automatic conversion of math proofs into formal verification language
AIProver: Agentic Auto-Formalization of Mathematical Research via Certificate-Driven Evolving Harness
Logic in Computer ScienceArtificial IntelligenceMachine Learning
Summary
Translating complex math proofs written in everyday language into a formal language that computers can check is very hard, especially for new research with missing definitions and scarce training data. The authors present AIProver, a system that improves this translation by training a large language model together with a tool that evolves how it works based on feedback from verification checks. They introduce a new dataset of math theorems and proofs and show their system makes this translation much more accurate and cost-effective compared to existing methods.
What this means in practice
- •For software engineers: Automatically verify complex mathematical properties in software using improved translation of human-written proofs into formal code.
- •For automated theorem prover developers: Build more accurate agents that generate formally verified proofs by improving the interaction between language models and verification tools.
- •For financial model auditors: Assist in generating rigorously verified models by converting natural-language financial theorems into machine-checkable formal proofs.$Commercial implications: Enables selling formal verification services for financial modeling compliance and risk assessment using automated proof formalization.
Authors
Prithwish Jana, Viet Bach Hoang, Logan Luna, Viresh Pati, Akash Singirikonda, Cy Xie, Lisa Carbone, Wuyang Chen, Walter Moreira, Joe Stubbs, Sriram Vishwanath, Vijay Ganesh
Abstract
Proof auto-formalization translates natural-language (NL) theorems and proofs into a formal language (FL) such as Lean, enabling mechanical verification. Despite rapid progress, research-level proofs often depend on concepts missing from leading proof assistant libraries (e.g., Lean's Mathlib), and successful compilation does not guarantee that a translation preserves the theorem's meaning or the proof's reasoning. Furthermore, aligned NL-FL training data are scarce, and leading agents often rely on costly frontier models and manually engineered harnesses. To address the above issues, we present AIProver, an agentic framework for autonomous proof auto-formalization and proof synthesis (AFPS) that jointly post-trains a 119B open-weight language model and evolves its agentic, tool-calling harness with HarnessEvolve. Verifiers assess type correctness, proof completeness, and semantic correctness, returning rewards and diagnostic certificates that drive model fine-tuning and alternating reinforcement learning via symbolic feedback and HarnessEvolve, a certificate-driven evolutionary search over the whole harness control flow that re-tailors the harness to the updated model. For research-level training and evaluation, we introduce LoCoBench, 58.9k instances from Mathlib, CSLib, Mizar Math Library, and a bounded-arithmetic textbook, with a 771-instance validation split whose theorem-proof pairs have no public Lean formalization. Against 39 frameworks spanning AFPS agents, frontier LLMs, and coding agents, AIProver lifts pass@4 semantic correctness over its Leanstral-1.5 base from 15.7% to 36.7% and outperforms every other open-weight system and Aristotle. As a Claude Code and Codex skill, it lifts their semantic correctness from 41.9% and 34.1% to 79.8% and 62.4%, respectively. Further, it is also 24% cheaper than Numina-Lean-Agent, pushing the accuracy-cost frontier of research-level AFPS.