DeepTheorem团队 投稿 量子位 | 公众号 QbitAI 12.1万道IMO级难度数学"特训题"，让AI学会像人类一样 推导数学证明 ！ "特训"过后，模型定理证明性能大涨 ，7B模型性能比肩或超越现有的开源模型和Claude3.7等商业模型 。 "特训题"为 Deep Theore m ，是首个基于自然语言的数学定理证明框架与数据集，由腾讯AI Lab与上海交大团队联合推出。 团队表示，定理证明是数学前沿的重要组成部分，但当前大语言模型 （LLM） 在数学推理，特别是通过强化学习 （RL） 进行训练时，往往 需要可以自动验证的答案，导致大模型无法像数学家那样通过自然语言进行定理证明。 图（b）展示经过强化学习训练的DeepTheorem-7B模型性能，比肩或超越现有的开源模型和商业模型 （Gemini2.0-flash， Qwen2.5-72B- Instruct， Claude3.7 等 ） ，仅次于o1、o3以及Gemini2.5-pro强推理模型。 DeepTheorem-121K 1、规模与难度：专为"极限挑战"而生 DeepTheorem训练集的显著特点是其大规模与高难度。其包含121K ...

GitHub Copilot在数学定理证明中的应用 - 核心观点：GitHub Copilot在数学定理证明中主要起辅助作用，能快速生成代码框架和常见模式，但复杂数学细节和创造性解决方案仍需人工干预[5][6][7] - 陶哲轩演示了如何正确引导Copilot完成函数极限问题的求和、求差和求积定理证明[3][11][13][25][33] 具体证明过程 求和定理证明 - Copilot自动补全了ε-δ定义，但需手动调整绝对值符号表达[12] - 生成基本证明框架，但δ的正性验证和不等式处理不严谨，需人工修正绝对值符号、三角不等式应用和最终表达式[17][18][20] - 后期提示使用Lean内置的`add_sub_add_comm`引理简化步骤[23][24] 求差定理证明 - 沿用求和定理的框架，但虚构不存在的`sub_sub_anc`方法[27][28] - 处理代数表达式时不稳定，需手动完成恒等式证明[31][32] 求积定理证明 - 提出ε分配策略（ε/(2|M|+1)和ε/(2|L|+1)），但实现时出现正性验证和绝对值不等式错误[34][37][43] - 错误使用`add_lt_add`方法，需人工调整假设条件[37][39] - 建议复杂问题先用纸笔推导再形式化验证[41][42] Copilot的功能特点 - 优势：快速生成代码框架、提示库函数使用，对初学者友好[6][24] - 局限性：复杂数学细节可靠性低，易虚构方法或忽略适用条件[7][28][37][40]

模型性能突破 - DeepSeek-Prover-V2在普特南测试中刷新记录至49道题解答，远超当前第一名Kimi-Prover的10道题表现[2][3] - 在miniF2F测试中，671B参数的Prover-V2通过率达到88.9%，7B参数版本在非CoT模式下解决13个671B模型未能处理的问题[36][9] - 7B小模型展现出独特推理能力，在处理有限基数问题时使用Cardinal.toNat等671B模型未掌握的技巧[9][10] 技术架构创新 - 采用"形式化和非形式化数学证明统一模型"设计，整合DeepSeek-V3的高上下文窗口和自然语言推理能力[15] - 引入"子目标分解的强化学习"方法，通过递归证明搜索合成冷启动数据，使用70亿参数模型处理子目标证明[19][21] - 建立两阶段训练体系：第一阶段生成非CoT数据，第二阶段采用高精度CoT模式强化复杂问题推理能力[28][29] 训练方法论 - 采用GRPO算法进行强化学习，通过二元奖励机制（正确证明得1分）优化策略，避免使用单独裁判模型[32][33] - 监督微调数据包含两个来源：专家迭代收集的非CoT形式化验证数据，以及冷启动CoT结构化证明路径数据[31] - 对7B模型执行与671B相同的强化学习阶段，使其上下文窗口扩展至32768个token并融入非CoT证明数据[35] 行业影响与生态建设 - 推出ProverBench基准数据集，包含325个形式化数学问题（15道AIME竞赛题+310道教科书问题）[38][39] - GitHub仓库12小时内获350+星标，引发X/Twitter和Hugging Face社区热烈讨论，包括Kimina-Prover团队祝贺[51][52][59] - 普林斯顿教授评价miniF2F测试最后10%-20%问题的攻克标志着"能力重大飞跃"，显示行业竞争白热化[57] 团队与研发背景 - 18人团队包含DeepSeek-V3/R1/Prover系列前作核心成员，新增清华背景研究员Shirong Ma等资深成员[42][44][45] - 采用Fire-Flyer AI-HPC架构降低训练成本，但未披露具体基础设施优化细节[48][49] - 研究延续DeepSeek-Prover系列技术路线，从V1的合成数据微调演进至V2的子目标分解强化学习[12][13][14]

DeepSeek-Prover-V2-671B模型发布 - 公司于4月30日在Hugging Face平台开源了专注于数学定理证明的大语言模型DeepSeek-Prover-V2-671B [1] - 模型采用DeepSeek-V3架构，参数高达6710亿，采用MoE模式，具有61层Transformer层，7168维隐藏层 [3][6] - 模型最大位置嵌入达到16.38万，能够处理极其复杂的数学证明问题 [6] 模型技术细节 - 模型分为163个分片，每个分片大小约为4.3GB [4] - 使用safetensors文件格式，支持BF16、FP8、F32等多种计算精度 [4] - 采用FP8量化技术减小模型大小，提高推理效率 [8] - 结合合成数据、强化学习与蒙特卡洛树搜索等优化技术 [6] 模型性能提升 - 在高中数学题测试中，成功率从50%提高到了63.5% [12] - 相比V1.5版本7B参数的小模型，此次直接升级为大模型 [14] 公司发展动态 - 创始人梁文锋表示要将探索通用人工智能作为核心使命 [7] - 团队保持每季度重大更新的开发范式：2024年9月V2.5、12月V3、2025年3月V3-0324 [7] - 3月发布的V3-0324版本已被业内视为未来R2的基础模型 [5][7] 行业反响 - 在社交平台X上，网友对R2大模型发布表示期待 [7] - 有评论称"中国的AI初创公司正在改变整个游戏规则" [15] - 行业对"中国正在将一些功夫应用于AI"表示兴奋 [16]