EvolProver: Vooruitgang in Automatisch Bewijzen door Geformaliseerde Problemen te Evolueren via Symmetrie en Moeilijkheidsgraad

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

October 1, 2025

Auteurs: Yuchen Tian, Ruiyuan Huang, Xuanwu Wang, Jing Ma, Zengfeng Huang, Ziyang Luo, Hongzhan Lin, Da Zheng, Lun Du

cs.AI

Samenvatting

Grote Taalmodellen (LLMs) voor formeel theorema bewijzen hebben aanzienlijke belofte getoond, maar ze missen vaak generaliseerbaarheid en zijn kwetsbaar voor zelfs kleine transformaties van probleemstellingen. Om deze beperking aan te pakken, introduceren we een innovatieve data-augmentatiepijplijn die is ontworpen om de robuustheid van het model vanuit twee perspectieven te verbeteren: symmetrie en moeilijkheidsgraad. Vanuit het symmetrieperspectief stellen we twee complementaire methoden voor: EvolAST, een Abstract Syntax Tree (AST) gebaseerde aanpak die syntactische symmetrie benut om semantisch equivalente probleemvarianten te genereren, en EvolDomain, dat gebruikmaakt van LLMs om semantische symmetrie aan te pakken door theorema's over verschillende wiskundige domeinen te vertalen. Vanuit het moeilijkheidsperspectief stellen we EvolDifficulty voor, dat zorgvuldig ontworpen evolutionaire instructies gebruikt om LLMs te begeleiden bij het genereren van nieuwe theorema's met een breder scala aan moeilijkheidsgraden. Vervolgens gebruiken we de geëvolueerde data om EvolProver te trainen, een 7B-parameter niet-redenerende theorema-bewijzer. EvolProver vestigt een nieuwe state-of-the-art (SOTA) op FormalMATH-Lite met een 53,8% pass@32-snelheid, waarmee het alle modellen van vergelijkbare grootte overtreft, inclusief redeneringsgebaseerde modellen. Het stelt ook nieuwe SOTA-records voor niet-redenerende modellen op MiniF2F-Test (69,8% pass@32), Ineq-Comp-Seed (52,2% pass@32) en Ineq-Comp-Transformed (34,0% pass@32). Ablatiestudies bevestigen verder de effectiviteit van onze data-augmentatiepijplijn over meerdere benchmarks.

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.