Обучение исправлению доказательств в Lean на основе отклика компилятора
Learning to Repair Lean Proofs from Compiler Feedback
February 3, 2026
Авторы: Evan Wang, Simon Chess, Daniel Lee, Siyuan Ge, Ajit Mallavarapu, Vasily Ilin
cs.AI
Аннотация
По мере того как нейронные верификаторы теорем становятся все более автономными, способность интерпретировать и реагировать на обратную связь от компилятора становится критически важной. Однако существующие наборы данных для Lean почти исключительно содержат корректные доказательства, предлагая крайне мало примеров для обучения пониманию и исправлению ошибок. Мы исследуем исправление доказательств в Lean как задачу обучения с учителем: по ошибочному доказательству и отклику компилятора предсказать как исправленное доказательство, так и диагностику на естественном языке, основанную на этом же отклике. Мы представляем APRIL (Automated Proof Repair in Lean — автоматизированное исправление доказательств в Lean), набор данных из 260 000 размеченных кортежей, которые связывают систематически сгенерированные ошибочные доказательства с диагностикой компилятора, а также с соответствующими им целями по исправлению и объяснению. Обучение языковых моделей на APRIL существенно повышает точность исправления и способность к рассуждению с учетом обратной связи; в нашей настройке оценки с однократной попыткой исправления дообученная модель с 4 миллиардами параметров превосходит сильнейшую открытую модель-основу. Мы рассматриваем обучение с условием в виде диагностики как дополнительный сигнал для тренировки верификаторов, использующих обратную связь. Наш набор данных доступен по ссылке https://huggingface.co/datasets/uw-math-ai/APRIL{эта ссылка}.
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}.