核心观点 - DeepTheorem是首个基于自然语言的数学定理证明框架与数据集，通过12.1万道IMO级难度数学题训练AI模型，使7B参数模型在定理证明性能上比肩或超越部分开源模型和商业模型（如Claude3.7）[1][2][4] 数据集特点 - 数据集规模达121K，难度等级为5-9级，显著大于现有数学定理数据集且难度更高，与国际数学奥赛级别测试集难度分布相似[6] - 数据经过严格五阶段去污染流程，包括嵌入相似性搜索和LLM-Judge消除与14个通用数学及STEM基准的重叠，确保评估完整性[9][11] - 每条数据包含问题、最终答案（真/假）、难度标注、分层主题分类及o3-mini生成的证明过程，支持监督微调与强化学习训练[15] 方法创新 - 引入可验证奖励强化学习（RLVR），通过自动化方法对每个定理生成可证明或证伪的变体，将原始121K定理扩展至242K变体[17][19] - 采用基于GRPO的RLVR训练，模型需判断定理真伪并通过二值奖励函数（正确得1分，错误得0分）优化性能[20][21] 评估框架 - 测试集整合FIMO（172题）、HMMT（205题）和PutnamBench（281题），通过手工扩展变体形成658个总测试样本[22][24] - 评估指标包含结果评价（模型需正确判断所有变体）和过程评价（GPT-4o从逻辑正确性等四个维度打分）[25][26] 性能表现 - DeepTheorem-7B模型在三个测试集上平均结果评价达47.22%，过程评价达34.04%，在18个模型中排名第五，超越Claude3.7-Sonnet（31.44%）等商业模型[28] - 模型性能仅次于o1系列、o3-mini及Gemini2.5-Pro等强推理模型，显著优于参数量相近的定理证明模型（如DeepSeek-Prover）和更大参数模型（如Qwen2.5-72B）[28] 行业意义 - 框架突破传统形式语言定理证明范式，充分利用大模型自然语言能力，为AI在数学推理领域应用开辟新思路[31] - 推动AI从封闭计算向复杂数学证明迈进，助力构建更通用、认知更复杂的智能系统[32]

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]