OProver: Un Marco Unificado para la Demostración Formal de Teoremas Basada en Agentes

Resumen

El progreso reciente en la demostración formal de teoremas se ha beneficiado de la generación de pruebas a gran escala y del entrenamiento consciente del verificador, pero la demostración agente rara vez se integra en el entrenamiento del demostrador, apareciendo solo en el momento de la inferencia. Presentamos OProver, un marco unificado para la demostración formal de teoremas basada en agentes en Lean 4, en el que los intentos fallidos de prueba se revisan iterativamente utilizando pruebas verificadas por el compilador recuperadas y la retroalimentación del compilador de Lean. OProver se entrena mediante preentrenamiento continuado seguido de post-entrenamiento iterativo: cada iteración ejecuta la demostración agente, indexa las pruebas recién verificadas en OProofs y la memoria de recuperación, utiliza trayectorias de reparación como datos de ajuste fino supervisado (SFT), y utiliza casos difíciles no resueltos para el aprendizaje por refuerzo (RL). OProofs se construye a partir de recursos públicos de Lean, síntesis de pruebas a gran escala y trazas de demostración agente, conteniendo 1.77 millones de enunciados de Lean, 6.86 millones de pruebas verificadas por el compilador, y trayectorias serializadas con contexto recuperado, intentos fallidos, retroalimentación y reparaciones. En cinco puntos de referencia, OProver-32B obtiene el mejor Pass@32 en MiniF2F (93.3%), ProverBench (58.2%) y PutnamBench (11.3%), y ocupa el segundo lugar en MathOlympiad (22.8%) y ProofNet (33.2%), con más mejores posiciones que cualquier demostrador previo de pruebas completas de peso abierto.

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.