OProver: Een geünificeerd raamwerk voor agentisch formeel stellingbewijs

Samenvatting

Recent vooruitgang in formeel stellingen bewijzen heeft geprofiteerd van grootschalige bewijsgeneratie en verifier-bewuste training, maar agentisch bewijzen wordt zelden geïntegreerd in provertraining en verschijnt alleen tijdens inferentie. We presenteren OProver, een uniform raamwerk voor agentisch formeel stellingen bewijzen in Lean 4, waarin mislukte bewijspogingen iteratief worden herzien met behulp van opgehaalde compiler-geverifieerde bewijzen en Lean compiler-feedback. OProver wordt getraind door voortgezet voortrainen gevolgd door iteratief natrainen: elke iteratie voert agentisch bewijzen uit, indexeert nieuw geverifieerde bewijzen in OProofs en het retrievalgeheugen, gebruikt reparatietrajecten als SFT-data, en gebruikt onopgeloste moeilijke gevallen voor RL. OProofs is opgebouwd uit openbare Lean-bronnen, grootschalige bewijssynthese en agentische bewijssporen en bevat 1,77M Lean-verklaringen, 6,86M compiler-geverifieerde bewijzen en geserialiseerde trajecten met opgehaalde context, mislukte pogingen, feedback en reparaties. Over vijf benchmarks heen behaalt OProver-32B de beste Pass@32 op MiniF2F (93,3%), ProverBench (58,2%) en PutnamBench (11,3%), en staat het op de tweede plaats op MathOlympiad (22,8%) en ProofNet (33,2%), met meer topplaatsingen dan enige eerdere open-gewicht whole-proof prover.

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.