OProver : Un cadre unifié pour la preuve formelle de théorèmes par agents

Résumé

Les progrès récents en matière de démonstration formelle de théorèmes ont bénéficié de la génération de preuves à grande échelle et de l’entraînement sensible au vérificateur, mais la démonstration agentique est rarement intégrée à l’entraînement du prouveur, n’apparaissant qu’au moment de l’inférence. Nous présentons OProver, un cadre unifié pour la démonstration formelle agentique de théorèmes dans Lean 4, dans lequel les tentatives de preuve infructueuses sont révisées de manière itérative à l’aide de preuves vérifiées par compilateur et des retours du compilateur Lean. OProver est entraîné par pré-entraînement continu suivi d’un post-entraînement itératif : chaque itération exécute la démonstration agentique, indexe les preuves nouvellement vérifiées dans OProofs et la mémoire de récupération, utilise les trajectoires de réparation comme données SFT, et exploite les cas difficiles non résolus pour l’apprentissage par renforcement. OProofs est construit à partir de ressources Lean publiques, de synthèse de preuves à grande échelle et de traces de démonstration agentique, contenant 1,77 million d’énoncés Lean, 6,86 millions de preuves vérifiées par compilateur et des trajectoires sérialisées avec contexte récupéré, tentatives échouées, retours d’information et réparations. Sur cinq bancs d’essai, OProver-32B obtient le meilleur Pass@32 sur MiniF2F (93,3 %), ProverBench (58,2 %) et PutnamBench (11,3 %), et se classe deuxième sur MathOlympiad (22,8 %) et ProofNet (33,2 %), obtenant plus de premières places que tout autre prouveur de preuves complètes à poids ouverts antérieur.

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.