EvolProver: Fortschritt im automatischen Theorembeweis durch die Entwicklung formalisierter Probleme mittels Symmetrie und Schwierigkeitsgrad

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

Große Sprachmodelle (LLMs) für formales Theorembeweisen haben erhebliche Fortschritte gezeigt, jedoch mangelt es ihnen oft an Generalisierbarkeit und sie sind empfindlich gegenüber selbst geringfügigen Transformationen von Problemstellungen. Um diese Einschränkung zu überwinden, führen wir eine neuartige Datenaugmentationspipeline ein, die darauf abzielt, die Robustheit des Modells aus zwei Perspektiven zu verbessern: Symmetrie und Schwierigkeitsgrad. Aus der Symmetrieperspektive schlagen wir zwei komplementäre Methoden vor: EvolAST, einen auf abstrakten Syntaxbäumen (AST) basierenden Ansatz, der syntaktische Symmetrie nutzt, um semantisch äquivalente Problemvarianten zu erzeugen, und EvolDomain, das LLMs nutzt, um semantische Symmetrie durch die Übersetzung von Theoremen über mathematische Domänen hinweg zu adressieren. Aus der Schwierigkeitsperspektive schlagen wir EvolDifficulty vor, das sorgfältig gestaltete evolutionäre Anweisungen verwendet, um LLMs bei der Erzeugung neuer Theoreme mit einem breiteren Schwierigkeitsspektrum zu leiten. Anschließend verwenden wir die entwickelten Daten, um EvolProver, einen 7B-Parameter-Theorembeweiser ohne deduktive Fähigkeiten, zu trainieren. EvolProver erreicht einen neuen State-of-the-Art (SOTA) auf FormalMATH-Lite mit einer 53,8%igen pass@32-Rate und übertrifft damit alle Modelle vergleichbarer Größe, einschließlich deduktionsbasierter Modelle. Es setzt auch neue SOTA-Rekorde für nicht-deduktive Modelle auf MiniF2F-Test (69,8% pass@32), Ineq-Comp-Seed (52,2% pass@32) und Ineq-Comp-Transformed (34,0% pass@32). Ablationsstudien bestätigen weiterhin die Effektivität unserer Datenaugmentationspipeline über mehrere Benchmarks hinweg.

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.