TLDR: EvolProver introduces a novel data augmentation pipeline to improve the generalizability and robustness of Large Language Models (LLMs) in formal theorem proving. It uses three methods: EvolAST for syntactic problem variations, EvolDomain for translating theorems across mathematical domains, and EvolDifficulty for generating problems with a wider range of complexity. Trained on this augmented data, EvolProver, a 7B-parameter non-reasoning model, achieves new state-of-the-art performance on multiple benchmarks like FormalMATH-Lite and MiniF2F-Test, demonstrating enhanced robustness and domain diversity.
Large Language Models (LLMs) have shown great potential in formal theorem proving, a field where mathematical proofs are represented as rigorous code that demands strict precision and logical soundness. However, a significant challenge for these models has been their lack of generalizability and fragility when faced with even minor changes to problem statements. This often stems from the scarcity of high-quality training data, as crafting formal proofs requires deep expertise and considerable time.
To tackle this limitation, a new research paper introduces an innovative data augmentation pipeline called EvolProver. This pipeline aims to enhance the robustness and generalizability of LLMs by evolving formalized problems from two key perspectives: symmetry and difficulty.
Enhancing Robustness Through Symmetry
The EvolProver pipeline addresses the concept of symmetry in mathematical problems, which refers to their invariance under certain transformations. The paper proposes two complementary methods:
-
EvolAST: This approach focuses on syntactic symmetry. It works by parsing a formal statement into an Abstract Syntax Tree (AST), applying equivalent transformations using a library of established axioms and theorems, and then converting the modified tree back into a new statement. This process generates problems that are semantically identical but syntactically diverse, making the model less sensitive to how a problem is phrased.
-
EvolDomain: This method tackles semantic symmetry. It uses LLMs to translate theorems across different mathematical domains. For example, a theorem originally stated in number theory could be reinterpreted and formalized in geometry, preserving its core logic. This expands the model’s understanding of how mathematical concepts apply across various fields.
Adjusting Difficulty for Better Generalization
The research also highlights that models trained on data with a narrow range of difficulty often struggle to generalize. To address this, EvolProver introduces:
-
EvolDifficulty: This method guides LLMs to adjust the difficulty of existing theorems. By using carefully designed evolutionary instructions, it generates new theorems with a broader spectrum of difficulty, from simpler variations to more complex ones. This discourages models from relying on shortcuts or mere memorization, promoting a deeper understanding of mathematical principles.
The entire data augmentation pipeline includes a stringent two-stage verification process. First, generated statements are checked for syntactic integrity using the Lean 4 compiler, with LLMs attempting repairs if errors are found. Second, an LLM-based judge evaluates the semantic consistency between formal and natural language versions, propositional correctness, and difficulty appropriateness.
Also Read:
- DIVER: A New Approach to Enhance LLM Reasoning Through Diverse Exploration
- HILBERT: Combining AI Intuition and Rigor for Advanced Math Proofs
Training and Performance of EvolProver
The researchers trained EvolProver, a 7-billion-parameter non-reasoning theorem prover, by fine-tuning an existing model (DeepSeekProver-V1.5-Base) on their augmented dataset. The training involved both Supervised Fine-Tuning (SFT) and Reinforcement Learning (RL).
EvolProver has achieved impressive results, setting new state-of-the-art (SOTA) records on several benchmarks:
-
On FormalMATH-Lite, it achieved a 53.8% pass@32 rate, outperforming all models of comparable size, including those that use reasoning-based approaches.
-
For non-reasoning models, it set new SOTA records on MiniF2F-Test (69.8% pass@32), Ineq-Comp-Seed (52.2% pass@32), and Ineq-Comp-Transformed (34.0% pass@32). The performance on Ineq-Comp-Transformed is particularly notable, demonstrating a significant boost in robustness against problem perturbations.
Ablation studies further confirmed the effectiveness of each component of the data augmentation pipeline, showing substantial performance gains. The research also found that directly evolving formal statements using EvolDomain and EvolDifficulty was more effective than evolving natural language problems first and then formalizing them.
This work represents a significant step forward in automated theorem proving, offering a robust and generalizable approach to training LLMs for complex mathematical tasks. The researchers plan to further enhance EvolProver’s reasoning capabilities by incorporating synthetically generated Chain-of-Thought data in future work. You can read the full paper here.
