EvolProver: 대칭성과 난이도를 통해 형식화된 문제를 진화시켜 자동 정리 증명을 발전시키는 방법

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

October 1, 2025

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

cs.AI

초록

형식적 정리 증명을 위한 대형 언어 모델(LLMs)은 상당한 가능성을 보여주었지만, 종종 일반화 능력이 부족하고 문제 진술의 사소한 변형에도 취약한 경우가 많습니다. 이러한 한계를 해결하기 위해, 우리는 모델의 견고성을 두 가지 관점(대칭성과 난이도)에서 강화하기 위한 새로운 데이터 증강 파이프라인을 소개합니다. 대칭성 관점에서, 우리는 두 가지 상호 보완적인 방법을 제안합니다: EvolAST는 구문적 대칭성을 목표로 의미적으로 동등한 문제 변형을 생성하기 위한 추상 구문 트리(AST) 기반 접근법이며, EvolDomain은 LLMs를 활용하여 수학적 도메인 간 정리를 번역함으로써 의미적 대칭성을 다룹니다. 난이도 관점에서, 우리는 EvolDifficulty를 제안하며, 이는 신중하게 설계된 진화적 지침을 사용하여 LLMs가 더 넓은 범위의 난이도를 가진 새로운 정리를 생성하도록 유도합니다. 그런 다음, 우리는 진화된 데이터를 사용하여 7B 파라미터의 비추론적 정리 증명기인 EvolProver를 학습시킵니다. EvolProver는 FormalMATH-Lite에서 53.8%의 pass@32 비율로 모든 유사 크기의 모델(추론 기반 모델 포함)을 능가하며 새로운 최첨단(SOTA) 기록을 세웁니다. 또한, MiniF2F-Test(69.8% pass@32), Ineq-Comp-Seed(52.2% pass@32), Ineq-Comp-Transformed(34.0% pass@32)에서 비추론적 모델을 위한 새로운 SOTA 기록을 세웁니다. 추가 연구는 여러 벤치마크에서 우리의 데이터 증강 파이프라인의 효과를 더욱 확인시켜 줍니다.

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.