OProver: Ein einheitliches Framework für agentisches formales Theorembeweisen

Zusammenfassung

Aktuelle Fortschritte im formalen Theorembeweisen profitieren von groß angelegter Beweiserzeugung und prüferbewusstem Training, jedoch wird agentisches Beweisen selten in das Training von Beweisern integriert und kommt nur zur Inferenzzeit zum Einsatz. Wir stellen OProver vor, ein einheitliches Framework für agentisches formales Theorembeweisen in Lean 4, bei dem fehlgeschlagene Beweisversuche iterativ mithilfe abgerufener, compiler-verifizierter Beweise und des Lean-Compiler-Feedbacks überarbeitet werden. OProver wird durch fortgesetztes Vortraining gefolgt von iterativem Nachtraining trainiert: Jede Iteration führt agentisches Beweisen durch, indexiert neu verifizierte Beweise in OProofs und den Abrufspeicher, nutzt Reparaturtrajektorien als SFT-Daten und verwendet ungelöste schwierige Fälle für RL. OProofs wird aus öffentlichen Lean-Ressourcen, groß angelegter Beweissynthese und agentischen Beweisspuren aufgebaut und enthält 1,77 Millionen Lean-Anweisungen, 6,86 Millionen compiler-verifizierte Beweise sowie serialisierte Trajektorien mit abgerufenem Kontext, fehlgeschlagenen Versuchen, Feedback und Reparaturen. Über fünf Benchmarks hinweg erzielt OProver-32B die beste Pass@32 auf MiniF2F (93,3 %), ProverBench (58,2 %) und PutnamBench (11,3 %) und belegt den zweiten Platz auf MathOlympiad (22,8 %) und ProofNet (33,2 %) – mit mehr Spitzenplatzierungen als jeder zuvor veröffentlichte Open-Weight-Ganzbeweis-Beweiser.

English

Recent progress in formal theorem proving has benefited from large-scale proof generation and verifier-aware training, but agentic proving is rarely integrated into prover training, appearing only at inference time. We present OProver, a unified framework for agentic formal theorem proving in Lean 4, in which failed proof attempts are iteratively revised using retrieved compiler verified proofs and Lean compiler feedback. OProver is trained through continued pretraining followed by iterative post-training: each iteration runs agentic proving, indexes newly verified proofs into OProofs and the retrieval memory, uses repair trajectories as SFT data, and uses unresolved hard cases for RL. OProofs is built from public Lean resources, large-scale proof synthesis, and agentic proving traces, containing 1.77M Lean statements, 6.86M compiler-verified proofs, and serialized trajectories with retrieved context, failed attempts, feedback, and repairs. Across five benchmarks, OProver-32B attains the best Pass@32 on MiniF2F (93.3%), ProverBench (58.2%), and PutnamBench (11.3%), and ranks second on MathOlympiad (22.8%) and ProofNet (33.2%) more top placements than any prior open-weight whole-proof prover.