- 输入：大量的非正式数学问题（例如，来自高中和大学数学竞赛的问题）。
- 过程：使用一个基于深度学习的语言模型（如DeepSeekMath-Base 7B模型）将这些非正式问题转化为形式化的数学语句（Lean 4语言）。
- 输出
Quality Filtering（质量过滤）：
- 模型评分：使用一个评分模型对每个形式化语句进行评估，判断其质量（如“优秀”、“良好”、“一般”、“较差”、“差”）。
- 假设拒绝：通过尝试证明一个带有“False”结论的语句来检查原语句的假设是否一致。如果假设不一致，则排除该语句。
Statement Proving（语句证明）：
- 证明搜索：使用DeepSeek-Prover模型尝试为每个形式化语句找到证明。为了提高效率，同时证明原语句及其否定（即并行证明T ⊢ P和T ⊢ ¬P）。
- 验证
Iterative Enhancement（迭代增强）：
- 微调模型：使用新生成的证明数据对DeepSeek-Prover模型进行微调。
- 重复过程：使用微调后的模型进行下一轮的自动形式化、质量过滤和语句证明。
- 输入
- 过程
- 输出：不断提升性能的DeepSeek-Prover模型和更大规模的高质量形式化数学数据集。
ingFang SC", -apple-system, "system-ui", "Segoe UI", Roboto, Ubuntu, "Helvetica Neue", Helvetica, Arial, "Hiragino Sans GB", "Microsoft YaHei UI", "Microsoft YaHei", "Source Han Sans CN", sans-serif;font-optical-sizing: inherit;font-size-adjust: inherit;font-kerning: inherit;font-feature-settings: inherit;font-variation-settings: inherit;vertical-align: baseline;word-break: break-word;overflow-wrap: break-word;color: rgba(0, 0, 0, 0.9);letter-spacing: normal;orphans: 2;text-align: start;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(252, 252, 252);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">通过这些步骤，论文的方法能够有效地生成大规模的高质量形式化数学数据，并显著提升自动定理证明的性能。ingFang SC", -apple-system, "system-ui", "Segoe UI", Roboto, Ubuntu, "Helvetica Neue", Helvetica, Arial, "Hiragino Sans GB", "Microsoft YaHei UI", "Microsoft YaHei", "Source Han Sans CN", sans-serif;font-optical-sizing: inherit;font-size-adjust: inherit;font-kerning: inherit;font-feature-settings: inherit;font-variation-settings: inherit;vertical-align: baseline;word-break: break-word;overflow-wrap: break-word;color: rgba(0, 0, 0, 0.9);letter-spacing: normal;orphans: 2;text-align: start;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(252, 252, 252);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">以下是10个关于这篇论文的自问自答，用通俗易懂的方式阐述其价值：ingFang SC", -apple-system, "system-ui", "Segoe UI", Roboto, Ubuntu, "Helvetica Neue", Helvetica, Arial, "Hiragino Sans GB", "Microsoft YaHei UI", "Microsoft YaHei", "Source Han Sans CN", sans-serif;font-optical-sizing: inherit;font-size-adjust: inherit;font-kerning: inherit;font-feature-settings: inherit;font-variation-settings: inherit;vertical-align: baseline;color: rgba(0, 0, 0, 0.9);letter-spacing: normal;orphans: 2;text-align: start;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(252, 252, 252);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">1. 这篇论文主要解决了什么问题？ingFang SC", -apple-system, "system-ui", "Segoe UI", Roboto, Ubuntu, "Helvetica Neue", Helvetica, Arial, "Hiragino Sans GB", "Microsoft YaHei UI", "Microsoft YaHei", "Source Han Sans CN", sans-serif;font-optical-sizing: inherit;font-size-adjust: inherit;font-kerning: inherit;font-feature-settings: inherit;font-variation-settings: inherit;vertical-align: baseline;word-break: break-word;overflow-wrap: break-word;color: rgba(0, 0, 0, 0.9);letter-spacing: normal;orphans: 2;text-align: start;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(252, 252, 252);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">在数学定理证明领域，大型语言模型（LLMs）虽然有潜力，但缺乏训练数据，导致在形式化定理证明方面进展受限。这篇论文提出一种方法，通过从高中和大学本科数学竞赛问题生成大量Lean 4证明数据来解决这个数据缺乏的问题。ingFang SC", -apple-system, "system-ui", "Segoe UI", Roboto, Ubuntu, "Helvetica Neue", Helvetica, Arial, "Hiragino Sans GB", "Microsoft YaHei UI", "Microsoft YaHei", "Source Han Sans CN", sans-serif;font-optical-sizing: inherit;font-size-adjust: inherit;font-kerning: inherit;font-feature-settings: inherit;font-variation-settings: inherit;vertical-align: baseline;color: rgba(0, 0, 0, 0.9);letter-spacing: normal;orphans: 2;text-align: start;text-indent: 0px;text-transform: none;widows: 2;word-spacing: 0px;-webkit-text-stroke-width: 0px;white-space: normal;background-color: rgb(252, 252, 252);text-decoration-thickness: initial;text-decoration-style: initial;text-decoration-color: initial;">2. 它是怎么解决数据缺乏问题的？论文先从网上抓取高中和大学本科数学竞赛的自然语言问题，然后用一个大语言模型把这些自然语言问题转化为Lean 4的形式化语句。接着过滤掉质量低和无效的语句，再用模型生成证明，最后用这些数据来微调模型，不断迭代提升模型性能。
3. 这种方法效果如何？
在对Lean 4 miniF2F测试集的实验中，微调后的DeepSeek-Prover模型在使用64个样本时，完整证明生成准确率达到46.3%，累积达到52%，超过了基线模型GPT - 4的23.0%和一个树搜索强化学习方法的41.0%。在Lean 4 Formalized International Mathematical Olympiad (FIMO)基准测试中，该模型成功证明了148个问题中的5个，而GPT - 4一个都没证明出来。
4. 论文提出的方法有什么独特之处？
- 多步骤质量保证：通过质量评分模型和假设拒绝策略过滤低质量语句，还用迭代框架不断改进证明质量。
- 规模保障策略：通过并行证明原语句及其否定来加速证明过程，避免在不可证语句上浪费时间。
5. 这篇论文对数学领域有什么贡献？
它创建并开源了一个高质量的正式数学证明数据集，为数学和人工智能社区提供了更多资源，有助于进一步研究和发展自动定理证明，可能会让数学证明验证更可靠，也为学生和研究人员提供教育资源。
6. 对人工智能领域有什么意义？
展示了大型语言模型在自动定理证明方面的潜力，通过利用大规模合成数据提升了模型性能，为其他相关研究提供了新思路和方法，推动了人工智能在数学推理领域的发展。
7. 论文中的实验是如何设置的？
以DeepSeekMath - Base 7B模型为基础构建DeepSeek - Prover，使用1200亿数学相关标记预训练。在微调时，全局批量大小设为512，学习率设为1×10⁻⁴ ，包含6000个热身步骤。评估时与GPT - 3.5、GPT - 4、GPT - f等基线模型对比，使用pass@k指标衡量性能。
8. 实验结果除了证明准确率，还有其他发现吗？
通过消融实验发现：
- 大规模自动形式化有效，用自动生成数据训练的模型比仅用mathlib数据训练的模型性能更好。
- 模型在过滤低质量语句方面有效，用高质量证明数据训练的模型比用低质量数据训练的性能提升4.5%。
- 迭代增强策略有效，随着迭代次数增加，模型性能提升，定理证明能力增强。
- 合成定理证明数据规模与模型效果相关，数据量越大，模型在miniF2F基准测试上的性能越好。
9. 论文中的案例研究有什么作用？
展示了方法在实际应用中的效果，包括成功证明定理以及识别假设不一致的情况。比如在自动形式化定理时，能准确将自然语言描述的数学问题转化为Lean 4的形式化语句并证明；还能发现原自动形式化中的错误假设，并给出反例和修正版本。
10. 论文未来有什么展望？
目前主要关注中学和大学本科的代数和数论问题，未来计划扩大数学问题的多样性，提高方法在自动定理证明中的通用性，进一步推动自动定理证明领域的发展。
这篇文章的独特价值（打比方版）
1. 像“教AI做数学题”一样训练模型
想象一下，你要教一个AI做高中数学竞赛题，但你发现它连题目都看不懂，更别说解题了。以前的方法就像直接给AI一堆“标准答案”，让它死记硬背，但遇到新题就懵了。
这篇论文的做法是：先让AI学会把数学题翻译成“机器能看懂的语言”（Lean 4），再自己试着解题，最后用正确答案纠正它。就像你先教AI理解题目，再让它自己尝试解题，做错了就告诉它哪里错了，反复训练，直到它能独立解题。
2. 像“刷题库”一样提升AI的数学能力
以前的AI训练数据就像“几本薄薄的练习册”，题目太少，AI学得不够扎实。这篇论文生成了800万道数学题和答案，相当于给AI准备了一个“超级题库”，让它疯狂刷题，解题能力自然就提升了。
3. 像“错题本”一样优化训练
以前训练AI时，如果它做错了，可能就直接丢弃这个错误案例。但这篇文章的方法是：把错题整理出来，分析为什么错，再让AI重新学。比如，如果AI把“所有复数都满足某个错误条件”当成真命题，它会自己发现矛盾，并把这个错误案例剔除，避免下次再犯。
4. 像“双保险”一样提高解题效率
以前AI证明数学题时，只能一个一个试，效率很低。这篇论文的方法是同时证明原命题和它的反命题，就像“两条腿走路”：
这样就能快速排除错误命题，节省计算资源，提高效率。
作者为什么要做这篇论文？（打比方版）
1. 解决AI数学解题的“卡脖子”问题
现在的AI在数学推理上就像“小学生”，能做简单题，但遇到复杂的数学竞赛题就抓瞎。作者发现，数据不够是主要瓶颈——没有足够多的高质量数学题让AI学习。
于是，他们决定自己造数据，用自动方式生成800万道数学题，让AI有足够的“练习题”可以学，就像给AI请了一个“数学私教”，天天逼它刷题。
2. 让AI像数学家一样思考
以前的AI解题就像“暴力破解”，试遍所有可能，但效率极低。作者希望AI能像数学家一样，先理解题目，再有逻辑地推导。
他们的方法让AI先学会把数学题翻译成“机器语言”，再自己尝试证明，就像教一个人先学会读题，再自己思考解题步骤，而不是直接抄答案。
3. 推动AI自动定理证明的发展
自动定理证明（ATP）就像数学界的“自动驾驶”，如果能让AI自己证明数学定理，未来它就能帮数学家验证猜想、发现新定理。
但以前ATP的数据太少，AI学不会。这篇论文通过大规模合成数据，让AI的“数学驾驶技术”大幅提升，未来可能让AI在数学研究上发挥更大作用。
4. 让更多人能用上AI数学工具
作者开源了数据和模型，就像把“数学学习秘籍”公开，让全世界的研究者都能用。这样，更多人可以基于这个方法改进AI数学能力，甚至应用到教育、科研等领域。
总结（一句话版）
这篇论文的价值在于：用AI自动造了800万道数学题，让AI疯狂刷题，解题能力大幅提升，并开源数据和方法，推动数学+AI的跨界发展。作者做这件事，是因为数据不够是AI数学推理的瓶颈，而他们找到了高效造数据的方法，让AI离“数学专家”更近一步。