核心发现
方法论
本文提出了Spark-Prover-X1，一个7B参数模型，通过三阶段框架进行训练。第一阶段是持续预训练，利用广泛的数学语料库和新颖的数据任务注入深度知识。第二阶段采用专家迭代循环中的监督微调，专门化Spark-Prover-X1-7B和Spark-Formalizer-X1-7B模型。最后，通过群体相对策略优化（GRPO）进一步提高模型在复杂问题上的证明能力。
关键结果
- Spark-Prover在Whole-Proof Generation范式中表现优异，在PutnamBench上解决了27个问题（pass@32），在CombiBench上达到了24.0%的通过率（pass@32）。
- 在ExamFormal-Bench基准测试中，Spark-Prover-X1-7B和Spark-Formalizer-X1-7B在同类开源模型中表现出色，前者的平均通过率为37.0%，后者在ProofNet-test中达到了78.85%。
- 通过数据增强和逐步优化的训练管道，模型在形式推理能力上取得了显著提升。
研究意义
本研究通过多样化的训练数据和逐步优化的训练管道，显著提升了轻量级大语言模型在形式推理任务中的表现。它不仅在学术界提供了新的研究路径，还为工业界的自动化推理和验证工具带来了潜在的应用价值。通过引入ExamFormal-Bench数据集，研究者们可以更好地评估模型在真实世界考试问题上的表现。
技术贡献
技术贡献包括提出了一种新的数据增强方法，即CoT增强状态预测任务，使模型能够实现细粒度的推理。此外，通过GRPO算法的应用，模型在解决复杂问题上的能力得到了显著提升。与现有方法相比，本文的方法在数据多样性和训练策略上具有显著的创新性。
新颖性
Spark-Prover-X1首次通过多样化数据和逐步优化的训练管道，显著提升了轻量级大语言模型在形式定理证明中的表现。与现有方法相比，本文在数据增强和训练策略上具有显著的创新性。
局限性
- 模型在处理极其复杂的定理证明时仍存在局限性，可能需要更多的计算资源和时间。
- 当前的训练数据集可能不够全面，无法涵盖所有可能的数学领域。
未来方向
未来的研究方向包括扩展训练数据集的多样性和规模，以覆盖更多的数学领域。此外，进一步优化模型的计算效率和推理能力也是一个重要的研究方向。
AI 总览摘要
自动定理证明是人工智能领域的一个重大挑战，现有方法常因缺乏多样化和高质量的形式语言数据而受限。Spark-Prover-X1通过三阶段训练框架，旨在释放中等规模大语言模型的推理潜力。第一阶段通过广泛的数学语料库和新颖的数据任务进行持续预训练，第二阶段在专家迭代循环中进行监督微调，第三阶段通过群体相对策略优化提高模型在复杂问题上的证明能力。
实验结果显示，Spark-Prover在Whole-Proof Generation范式中表现优异，特别是在PutnamBench和CombiBench等困难竞赛基准测试中取得了显著成绩。通过引入ExamFormal-Bench数据集，研究者们可以更好地评估模型在真实世界考试问题上的表现。
尽管取得了显著进展，模型在处理极其复杂的定理证明时仍存在局限性，未来的研究方向包括扩展训练数据集的多样性和规模，以及进一步优化模型的计算效率和推理能力。
深度分析
研究背景
自动定理证明（ATP）是人工智能领域的一个重要研究方向，近年来随着大语言模型（LLM）的兴起，ATP迎来了新的发展机遇。形式语言提供了严格的逻辑框架和机器可验证性，使其成为探索高级机器推理能力的理想试验场。然而，由于高质量形式训练数据的稀缺，LLM在形式证明生成中的进展受到限制。
核心问题
现有的自动定理证明方法常因缺乏多样化和高质量的形式语言数据而受限。获取高质量的形式定理证明数据既昂贵又困难，现有数学库与常见基准测试中的问题存在分布差异，限制了模型的泛化能力。
核心创新
Spark-Prover-X1的核心创新在于其三阶段训练框架。首先，通过广泛的数学语料库和新颖的数据任务进行持续预训练，注入深度知识。其次，在专家迭代循环中进行监督微调，专门化Spark-Prover-X1-7B和Spark-Formalizer-X1-7B模型。最后，通过群体相对策略优化提高模型在复杂问题上的证明能力。
方法详解
- �� 持续预训练：利用广泛的数学语料库和新颖的数据任务注入深度知识。
- �� 监督微调：在专家迭代循环中专门化模型。
- �� 群体相对策略优化：提高模型在复杂问题上的证明能力。
实验设计
实验设计包括在多个基准测试上评估模型性能，如miniF2F、ProofNet、PutnamBench和CombiBench。通过引入ExamFormal-Bench数据集，研究者们可以更好地评估模型在真实世界考试问题上的表现。
结果分析
实验结果显示，Spark-Prover在Whole-Proof Generation范式中表现优异，特别是在PutnamBench和CombiBench等困难竞赛基准测试中取得了显著成绩。
应用场景
该模型可用于自动化推理和验证工具，特别是在需要形式证明生成的场景中，如数学教育和科学研究。
局限与展望
尽管取得了显著进展，模型在处理极其复杂的定理证明时仍存在局限性，可能需要更多的计算资源和时间。
通俗解读 非专业人士也能看懂
想象你在厨房里做一道复杂的菜肴。首先，你需要收集所有的食材，这就像我们的模型在第一阶段收集数学数据一样。接下来，你需要按照食谱一步步地准备食材，这就像我们的模型在第二阶段进行监督微调一样。最后，你需要根据自己的口味调整调料，这就像我们的模型在第三阶段进行策略优化一样。通过这三个步骤，你最终可以做出一道美味的菜肴，而我们的模型则可以生成高质量的形式定理证明。
简单解释 像给14岁少年讲一样
想象一下，你在玩一个超级复杂的拼图游戏。首先，你需要找到所有的拼图块，这就像我们的模型在第一阶段收集数学数据一样。然后，你需要按照图案一步步地拼接这些拼图块，这就像我们的模型在第二阶段进行监督微调一样。最后，你需要根据整体效果调整一些拼图块的位置，这就像我们的模型在第三阶段进行策略优化一样。通过这些步骤，你最终可以完成这个拼图，而我们的模型则可以生成高质量的形式定理证明。
术语表
大语言模型 (Large Language Model)
一种基于深度学习的模型，能够处理和生成自然语言文本。
在本文中用于自动定理证明。
自动定理证明 (Automated Theorem Proving)
使用计算机程序自动证明数学定理的过程。
本文的核心研究领域。
监督微调 (Supervised Fine-tuning)
在特定任务上使用标注数据对预训练模型进行进一步训练。
用于专门化模型。
群体相对策略优化 (Group Relative Policy Optimization)
一种用于强化学习的优化算法，旨在提高策略的性能。
用于提高模型在复杂问题上的证明能力。
ExamFormal-Bench
一个包含402个形式问题的新基准数据集。
用于评估模型在真实世界考试问题上的表现。
开放问题 这项研究留下的未解疑问
- 1 如何进一步扩展训练数据集的多样性和规模，以覆盖更多的数学领域。
- 2 如何提高模型在极其复杂定理证明任务中的计算效率。
应用场景
近期应用
数学教育
可用于自动化生成数学证明，帮助学生理解复杂的数学概念。
科学研究
在科学研究中自动验证和生成复杂的数学证明。
远期愿景
自动化推理工具
开发更强大的自动化推理和验证工具，支持更广泛的应用场景。
原文摘要
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.