EvolProver : Faire progresser la démonstration automatique de théorèmes en faisant évoluer les problèmes formalisés grâce à la symétrie et à la difficulté

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

October 1, 2025

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

cs.AI

papers.abstract

Les modèles de langage de grande taille (LLMs) pour la démonstration formelle de théorèmes ont montré un potentiel significatif, mais ils manquent souvent de généralisabilité et sont fragiles face à des transformations même mineures des énoncés de problèmes. Pour remédier à cette limitation, nous introduisons un nouveau pipeline d'augmentation de données conçu pour améliorer la robustesse du modèle sous deux angles : la symétrie et la difficulté. Du point de vue de la symétrie, nous proposons deux méthodes complémentaires : EvolAST, une approche basée sur les arbres de syntaxe abstraite (AST) qui cible la symétrie syntaxique pour générer des variantes de problèmes sémantiquement équivalentes, et EvolDomain, qui exploite les LLMs pour aborder la symétrie sémantique en traduisant des théorèmes entre différents domaines mathématiques. Du point de vue de la difficulté, nous proposons EvolDifficulty, qui utilise des instructions évolutives soigneusement conçues pour guider les LLMs dans la génération de nouveaux théorèmes avec une gamme de difficulté plus large. Nous utilisons ensuite les données évoluées pour entraîner EvolProver, un démonstrateur de théorèmes sans raisonnement de 7 milliards de paramètres. EvolProver établit un nouvel état de l'art (SOTA) sur FormalMATH-Lite avec un taux de réussite de 53,8 % pass@32, surpassant tous les modèles de taille comparable, y compris les modèles basés sur le raisonnement. Il établit également de nouveaux records SOTA pour les modèles sans raisonnement sur MiniF2F-Test (69,8 % pass@32), Ineq-Comp-Seed (52,2 % pass@32) et Ineq-Comp-Transformed (34,0 % pass@32). Les études d'ablation confirment en outre l'efficacité de notre pipeline d'augmentation de données sur plusieurs 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.