EvolProver: Avanzando en la Demostración Automática de Teoremas mediante la Evolución de Problemas Formalizados a través de Simetría y Dificultad

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

Resumen

Los Modelos de Lenguaje de Gran Escala (LLMs, por sus siglas en inglés) para la demostración formal de teoremas han mostrado un potencial significativo, aunque a menudo carecen de generalización y son frágiles ante incluso transformaciones menores de los enunciados de los problemas. Para abordar esta limitación, introducimos una novedosa canalización de aumento de datos diseñada para mejorar la robustez del modelo desde dos perspectivas: simetría y dificultad. Desde la perspectiva de la simetría, proponemos dos métodos complementarios: EvolAST, un enfoque basado en Árboles de Sintaxis Abstracta (AST, por sus siglas en inglés) que se enfoca en la simetría sintáctica para generar variantes semánticamente equivalentes de los problemas, y EvolDomain, que aprovecha los LLMs para abordar la simetría semántica mediante la traducción de teoremas a través de dominios matemáticos. Desde la perspectiva de la dificultad, proponemos EvolDifficulty, que utiliza instrucciones evolutivas cuidadosamente diseñadas para guiar a los LLMs en la generación de nuevos teoremas con un rango más amplio de dificultad. Luego, utilizamos los datos evolucionados para entrenar a EvolProver, un demostrador de teoremas sin razonamiento de 7 mil millones de parámetros. EvolProver establece un nuevo estado del arte (SOTA, por sus siglas en inglés) en FormalMATH-Lite con una tasa de 53.8% en pass@32, superando a todos los modelos de tamaño comparable, incluidos los modelos basados en razonamiento. También establece nuevos récords SOTA para modelos sin razonamiento en MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32) e Ineq-Comp-Transformed (34.0% pass@32). Los estudios de ablación confirman además la efectividad de nuestra canalización de aumento de datos en múltiples 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.