EvolProver: Advancing Automated Theorem Proving by Evolving Formalized
  Problems via Symmetry and Difficulty
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.
68e0764f73e20ab577841bcb
Yuchen Tian
68e0764f73e20ab577841bcc
Ruiyuan Huang
68e0764f73e20ab577841bcd
Xuanwu Wang
68e0764f73e20ab577841bce
Jing Ma
68e0764f73e20ab577841bcf
Zengfeng Huang
68e0764f73e20ab577841bd0
Ziyang Luo
claimed_verified
2025-10-05T12:45:56.245Z
6090ff099a8bcaa437b234a4
https://cdn-avatars.huggingface.co/v1/production/uploads/6090ff099a8bcaa437b234a4/iUvw7JXT-ngI7rGk1x-io.jpeg
Ziyang Luo
user
Ziyang
68e0764f73e20ab577841bd1
Hongzhan Lin
claimed_verified
2025-10-05T12:45:53.371Z
6499466c7d1edf7cb612a9a6
/avatars/c2e18594aa0879db8226f2a04496fb0b.svg
Hongzhan Lin
user
danielhzlin
68e0764f73e20ab577841bd2
Da Zheng
68e0764f73e20ab577841bd3
Lun Du
EvolProver: Advancing Automated Theorem Proving by Evolving Formalized
  Problems via Symmetry and Difficulty
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.
A novel data augmentation pipeline enhances the robustness and generalizability of large language models for formal theorem proving by addressing syntactic and semantic symmetry and varying difficulty levels, leading to state-of-the-art performance on multiple benchmarks.
Large Language Models formal theorem proving data augmentation Abstract Syntax Tree EvolAST EvolDomain EvolDifficulty EvolProver FormalMATH-Lite MiniF2F-Test Ineq-Comp-Seed Ineq-Comp-Transformed