EvolProver: Avançando a Prova Automática de Teoremas através da Evolução de Problemas Formalizados via Simetria e Dificuldade

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

October 1, 2025

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

cs.AI

Resumo

Modelos de Linguagem de Grande Escala (LLMs) para prova formal de teoremas têm demonstrado um potencial significativo, mas frequentemente carecem de generalização e são frágeis a transformações mínimas nos enunciados dos problemas. Para abordar essa limitação, introduzimos um novo pipeline de aumento de dados projetado para aprimorar a robustez do modelo a partir de duas perspectivas: simetria e dificuldade. Da perspectiva da simetria, propomos dois métodos complementares: EvolAST, uma abordagem baseada em Árvore de Sintaxe Abstrata (AST) que visa a simetria sintática para gerar variantes semanticamente equivalentes de problemas, e EvolDomain, que utiliza LLMs para tratar da simetria semântica ao traduzir teoremas entre domínios matemáticos. Da perspectiva da dificuldade, propomos EvolDifficulty, que usa instruções evolutivas cuidadosamente projetadas para orientar LLMs na geração de novos teoremas com uma gama mais ampla de dificuldade. Em seguida, usamos os dados evoluídos para treinar o EvolProver, um provador de teoremas sem raciocínio com 7 bilhões de parâmetros. O EvolProver estabelece um novo estado da arte (SOTA) no FormalMATH-Lite com uma taxa de 53,8% pass@32, superando todos os modelos de tamanho comparável, incluindo modelos baseados em raciocínio. Ele também define novos recordes SOTA para modelos sem raciocínio no MiniF2F-Test (69,8% pass@32), Ineq-Comp-Seed (52,2% pass@32) e Ineq-Comp-Transformed (34,0% pass@32). Estudos de ablação confirmam ainda mais a eficácia do nosso pipeline de aumento de dados em múltiplos 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.