核心观点 - 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]