Spark-Prover-X1: Formal Theorem Proving Through Diverse Data Training

TL;DR

Spark-Prover-X1 is a 7B parameter language model trained through a multi-stage process, including broad mathematical pre-training, specialized fine-tuning, and policy optimization, achieving state-of-the-art results in formal theorem proving on challenging benchmarks.

Contribution

The paper introduces a novel multi-stage training framework for lightweight LLMs, combining diverse data, a new reasoning task, and policy optimization to enhance formal reasoning capabilities.

Findings

Achieves state-of-the-art performance among similar-sized models.

Solves 27 problems on PutnamBench (pass@32).

Scores 24.0% on CombiBench (pass@32).

Abstract

Large Language Models (LLMs) have shown significant promise in automated theorem proving, yet progress is often constrained by the scarcity of diverse and high-quality formal language data. To address this issue, we introduce Spark-Prover-X1, a 7B parameter model trained via an three-stage framework designed to unlock the reasoning potential of more accessible and moderately-sized LLMs. The first stage infuses deep knowledge through continuous pre-training on a broad mathematical corpus, enhanced by a suite of novel data tasks. Key innovation is a "CoT-augmented state prediction" task to achieve fine-grained reasoning. The second stage employs Supervised Fine-tuning (SFT) within an expert iteration loop to specialize both the Spark-Prover-X1-7B and Spark-Formalizer-X1-7B models. Finally, a targeted round of Group Relative Policy Optimization (GRPO) is applied to sharpen the prover's capabilities on the most challenging problems. To facilitate robust evaluation, particularly on problems from real-world examinations, we also introduce ExamFormal-Bench, a new benchmark dataset of 402 formal problems. Experimental results demonstrate that Spark-Prover achieves state-of-the-art performance among similarly-sized open-source models within the "Whole-Proof Generation" paradigm. It shows exceptional performance on difficult competition benchmarks, notably solving 27 problems on PutnamBench (pass@32) and achieving 24.0\% on CombiBench (pass@32). Our work validates that this diverse training data and progressively refined training pipeline provides an effective path for enhancing the formal reasoning capabilities of lightweight LLMs. We will release both Spark-Prover-X1-7B and Spark-Formalizer-X1-7B, along with the ExamFormal-Bench dataset, in the near future.