Aprendiendo a Reparar Demostraciones Lean a partir de Retroalimentación del Compilador
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Autores: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Resumen
A medida que los demostradores de teoremas neuronales se vuelven más agentivos, la capacidad de interpretar y actuar sobre la retroalimentación del compilador es crucial. Sin embargo, los conjuntos de datos existentes para Lean consisten casi exclusivamente en demostraciones correctas, ofreciendo poca supervisión para comprender y reparar fallos. Estudiamos la reparación de demostraciones en Lean como un problema de aprendizaje supervisado: dada una demostración errónea y la retroalimentación del compilador, predecir tanto una demostración corregida como un diagnóstico en lenguaje natural basado en la misma retroalimentación. Presentamos APRIL (Reparación Automatizada de Demostraciones en Lean), un conjunto de datos de 260,000 tuplas supervisadas que emparejan fallos de demostración generados sistemáticamente con diagnósticos del compilador y objetivos alineados de reparación y explicación. Entrenar modelos de lenguaje en APRIL mejora sustancialmente la precisión de reparación y el razonamiento condicionado por la retroalimentación; en nuestro entorno de evaluación de reparación en un solo intento, un modelo de 4 mil millones de parámetros ajustado supera al baseline de código abierto más sólido. Consideramos la supervisión condicionada por diagnósticos como una señal de entrenamiento complementaria para demostradores que utilizan retroalimentación. Nuestro conjunto de datos está disponible en https://huggingface.co/datasets/uw-math-ai/APRIL{este enlace}.
English
As neural theorem provers become increasingly agentic, the ability to interpret and act on compiler feedback is critical. However, existing Lean datasets consist almost exclusively of correct proofs, offering little supervision for understanding and repairing failures. We study Lean proof repair as a supervised learning problem: given an erroneous proof and compiler feedback, predict both a corrected proof and a natural-language diagnosis grounded in the same feedback. We introduce APRIL (Automated Proof Repair in Lean), a dataset of 260,000 supervised tuples pairing systematically generated proof failures with compiler diagnostics and aligned repair and explanation targets. Training language models on APRIL substantially improves repair accuracy and feedback-conditioned reasoning; in our single-shot repair evaluation setting, a finetuned 4B-parameter model outperforms the strongest open-source baseline. We view diagnostic-conditioned supervision as a complementary training signal for feedback-using provers. Our dataset is available at https://huggingface.co/datasets/uw-math-ai/APRIL{this link}.