ProofLoom automates formal proofs for complex stochastic optimization algorithms
ProofLoom: Proof-Obligation-Driven Theory Construction for Autoformalizing Research-Level Stochastic Optimization
Artificial Intelligence
Summary
Formalizing complex math proofs about algorithms that work with randomness is very hard and error-prone. The authors created ProofLoom, a system that uses AI to automatically build and check these formal proofs using a computer language called Lean. It reads published algorithms and proofs, then constructs detailed models and supporting math while catching mistakes or gaps in the original work. The system improves over time by reusing proven math and failed attempts from past tasks.
What this means in practice
- •For software verification engineers: Produce formally verified proofs of complex optimization algorithms to ensure mathematical correctness and identify hidden errors in published works.
- •For machine learning infrastructure teams: Integrate verified stochastic optimization methods into production systems with formal guarantees on algorithm behavior and convergence.
Authors
Feiming Wang, Daibo Li, Kun Yuan
Abstract
Formalizing research-level stochastic optimization in Lean requires both an algorithm model and domain theory connecting foundational libraries to convergence proofs. Revising a model to restore provability can change the mathematical claim. We introduce ProofLoom, a fully automated LLM-agent system for Proof-Obligation-Driven Theory Construction. Given a published algorithm, target theorem, and source proof, ProofLoom autonomously constructs the Lean model and supporting theory. Open proof obligations drive the development of definitions, interfaces, lemmas, and proof plans. Signature contracts record evidence and obligations for model revisions; an independent Judge rejects unsupported assumptions and weakened conclusions. Planner expands the published argument into intermediate claims, and Audit checks whether the Lean proof follows it. Across tasks, SOptLib accumulates verified mathematics and construction experience: reusable results are extracted, generalized, and verified, while modeling decisions and failed proof routes are recorded. Later tasks retrieve these results and records and contribute new developments, forming a cycle of construction, accumulation, and reuse. On fifteen textbook and research-paper tasks, ProofLoom obtains mean human ratings of 6.3/7 and 6.4/7, compared with 4.9/7 and 5.0/7 for the strongest of six baselines. Across 33 developments, it produces 490,693 lines of algorithm-local Lean code with no sorry. The formalizations also expose 28 incorrect formulas, proof gaps, and algorithm-analysis mismatches in published sources across 22 developments, each with checked evidence.