EvolProver: Avanzare nel Teorema Automatico Evolvendo Problemi Formalizzati attraverso Simmetria e Difficoltà

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

October 1, 2025

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

cs.AI

Abstract

I Large Language Model (LLM) per il teorema dimostrativo formale hanno dimostrato un potenziale significativo, ma spesso mancano di generalizzabilità e sono fragili anche rispetto a trasformazioni minime degli enunciati dei problemi. Per affrontare questa limitazione, introduciamo una nuova pipeline di data augmentation progettata per migliorare la robustezza del modello da due prospettive: simmetria e difficoltà. Dal punto di vista della simmetria, proponiamo due metodi complementari: EvolAST, un approccio basato sugli Abstract Syntax Tree (AST) che mira alla simmetria sintattica per generare varianti semanticamente equivalenti dei problemi, e EvolDomain, che sfrutta i LLM per affrontare la simmetria semantica traducendo teoremi tra diversi domini matematici. Dal punto di vista della difficoltà, proponiamo EvolDifficulty, che utilizza istruzioni evolutive accuratamente progettate per guidare i LLM nella generazione di nuovi teoremi con un intervallo più ampio di difficoltà. Utilizziamo quindi i dati evoluti per addestrare EvolProver, un dimostratore di teoremi non basato sul ragionamento con 7 miliardi di parametri. EvolProver stabilisce un nuovo stato dell'arte (SOTA) su FormalMATH-Lite con un tasso pass@32 del 53,8%, superando tutti i modelli di dimensioni comparabili, inclusi quelli basati sul ragionamento. Stabilisce inoltre nuovi record SOTA per i modelli non basati sul ragionamento su MiniF2F-Test (69,8% pass@32), Ineq-Comp-Seed (52,2% pass@32) e Ineq-Comp-Transformed (34,0% pass@32). Studi di ablazione confermano ulteriormente l'efficacia della nostra pipeline di data augmentation su più benchmark.

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.