EvolProver: Развитие автоматического доказательства теорем через эволюцию формализованных задач с использованием симметрии и сложности

EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty

October 1, 2025

Авторы: Yuchen Tian, Ruiyuan Huang, Xuanwu Wang, Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, Lun Du

cs.AI

Аннотация

Крупные языковые модели (LLM) для формального доказательства теорем демонстрируют значительный потенциал, однако они часто страдают от недостатка обобщаемости и оказываются уязвимыми даже к незначительным изменениям формулировок задач. Чтобы устранить это ограничение, мы представляем новый конвейер аугментации данных, предназначенный для повышения устойчивости модели с двух перспектив: симметрии и сложности. С точки зрения симметрии мы предлагаем два взаимодополняющих метода: EvolAST, подход на основе абстрактного синтаксического дерева (AST), который нацелен на синтаксическую симметрию для генерации семантически эквивалентных вариантов задач, и EvolDomain, который использует LLM для работы с семантической симметрией путем перевода теорем между математическими областями. С точки зрения сложности мы предлагаем EvolDifficulty, который использует тщательно разработанные эволюционные инструкции для направления LLM в генерации новых теорем с более широким диапазоном сложности. Затем мы используем улучшенные данные для обучения EvolProver, 7-миллиардного параметрического нерассуждающего доказателя теорем. EvolProver устанавливает новый рекорд (SOTA) на FormalMATH-Lite с показателем 53,8% pass@32, превосходя все модели сопоставимого размера, включая модели, основанные на рассуждениях. Он также устанавливает новые рекорды SOTA для нерассуждающих моделей на MiniF2F-Test (69,8% pass@32), Ineq-Comp-Seed (52,2% pass@32) и Ineq-Comp-Transformed (34,0% pass@32). Абляционные исследования дополнительно подтверждают эффективность нашего конвейера аугментации данных на множестве бенчмарков.

English

Large Language Models (LLMs) for formal theorem proving have shown significant promise, yet they often lack generalizability and are fragile to even minor transformations of problem statements. To address this limitation, we introduce a novel data augmentation pipeline designed to enhance model robustness from two perspectives: symmetry and difficulty. From the symmetry perspective, we propose two complementary methods: EvolAST, an Abstract Syntax Tree (AST) based approach that targets syntactic symmetry to generate semantically equivalent problem variants, and EvolDomain, which leverages LLMs to address semantic symmetry by translating theorems across mathematical domains. From the difficulty perspective, we propose EvolDifficulty, which uses carefully designed evolutionary instructions to guide LLMs in generating new theorems with a wider range of difficulty. We then use the evolved data to train EvolProver, a 7B-parameter non-reasoning theorem prover. EvolProver establishes a new state-of-the-art (SOTA) on FormalMATH-Lite with a 53.8% pass@32 rate, surpassing all models of comparable size, including reasoning-based models. It also sets new SOTA records for non-reasoning models on MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32), and Ineq-Comp-Transformed (34.0% pass@32). Ablation studies further confirm our data augmentation pipeline's effectiveness across multiple benchmarks.