形式化定理证明新范式发布 - 阶跃星辰正式发布并开源形式化定理证明大模型StepFun-Prover-Preview-7B和StepFun-Prover-Preview-32B [1] - 模型采用基于环境反馈的强化学习训练流程，模拟人类推理过程中的实时交互与修正 [2] - 模型在基准测试集miniF2F-test上表现优异，32B版本pass@1通过率达70%，领先已知模型4%以上 [9][10] 技术架构与训练方法 两阶段监督微调 - 分阶段微调策略使模型获得工具使用基础能力 [4] - 第一阶段利用开源Lean 4数据建立代码补全能力 [5] - 第二阶段通过高质量冷启动数据训练模型理解数学题求解与Lean验证的交互 [5] 工具集成强化学习 - 采用GRPO算法进行强化学习训练，赋予模型自然语言解题能力 [5] - 模型可主动插入<sketch>标签生成Lean 4代码并执行，通过<REPL>反馈实现调试式修正 [5][6] - 奖励函数设计为REPL验证通过得1分，失败得0分 [7] 迭代优化机制 - 采用"RL-SFT-RL"循环优化方法，逐步提升模型推理能力 [8] - 筛选强化学习中成功的高难度样本重新用于监督微调，增强推理鲁棒性 [12] 性能表现与案例 - StepFun-Prover-Preview-7B以66% pass@1准确率超越DeepSeek-Prover-V2-671B(61.9%)和Kimina-Prover-72B(63.9%) [10] - 案例显示模型能主动去除冗余证明步骤、根据超时反馈调整结构、基于环境反馈有效改错 [10][13][15] 资源与后续计划 - 模型已开源在GitHub和Huggingface平台，技术报告发布于arXiv [17] - 团队将持续探索形式化推理模型方向 [16]

核心观点 - 大语言模型（LLM）与形式化数学结合正推动数学领域的范式变革，解决传统人工验证的瓶颈问题 [1][4] - 形式化数学通过严格逻辑和计算机辅助验证提升数学证明的可靠性和效率 [4][7] - 从Theorem Prover向Proof Engineering Agent转型是形式化数学的未来趋势 [11][17] - APE-Bench作为自动化证明工程基准，支持形式化数学的长期动态演进 [12][16] - LLM与形式化方法的结合将催生Certified AI，提升知识生产的可信度和效率 [17] 形式化数学的背景与挑战 - 现代数学证明规模庞大（如300页的开普勒猜想证明），传统人工验证效率低且易出错 [6] - 形式化数学通过公理系统和逻辑语言表达数学内容，借助计算机工具实现自动化验证 [8] - LLM的"幻觉"问题在数学领域尤为突出，需结合形式化方法确保生成内容的逻辑严密性 [6] 形式化定理证明的应用 - 典型案例包括Flyspeck项目（验证开普勒猜想）、液体张量实验（验证凝聚态数学引理）、PFR猜想众包验证 [13] - 形式化方法适用于数学理论证明和软件工程验证，确保逻辑一致性 [9] LLM驱动的最新进展 - AlphaProof在国际数学奥林匹克题目证明中达到银牌水平，DeepSeek-Prover V2在miniF2F基准成功率近90% [10] - LEGO-Prover项目利用LLM构建可复用的数学知识库，推动形式化数学向库级理论构建转型 [10] - 前沿研究探索LLM主动提出数学猜想和发现抽象结构的潜力 [10] Proof Engineering Agent转型 - 当前形式化工具面临人工成本高、协作效率低等问题（如Flyspeck项目耗费数十人年） [11] - 下一代工具需具备自我规划、修复和知识积累能力，支持大规模跨模块协作 [11] APE-Bench的设计与实施 - 分为三个阶段：单文件局部修改（APE-Bench I）、跨文件一致性维护（APE-Bench II）、完全自主Agent模式（APE-Bench III） [19] - 基于真实数学库（如Mathlib4）的历史修改记录，模拟实际Proof Engineering场景 [12] 未来影响与展望 - 数学领域：提升验证效率，推动理论创新和概念探索 [17] - 工业领域：应用于高安全系统（如操作系统内核、智能合约），提升安全性与可靠性 [17] - Certified AI将结合形式化验证与动态学习，成为可信的知识生产伙伴 [17]

DeepSeek-Prover-V2发布 - 公司发布DeepSeek-Prover-V2模型，包含7B和671B两个参数版本，专注于形式化定理证明，专为数学AI编程语言Lean 4打造 [3] - DeepSeek-Prover-V2-671B基于DeepSeek-V3-Base训练，7B版本基于DeepSeek-Prover-V1.5-Base构建，支持32K tokens上下文长度 [3] - 模型在MiniF2F测试中达到88.9%通过率，解决PutnamBench数据集中658道题中的49道，性能达到业内最佳 [15] 技术实现 - 采用递归定理证明流程，使用DeepSeek-V3分解复杂问题为子目标并生成形式化推理步骤，融合非形式化与形式化数学推理 [9][4] - 通过7B模型完成子目标证明以降低计算开销，整合子目标证明与DeepSeek-V3生成的思维链构建冷启动数据 [11] - 采用两阶段训练：非思维链（non-CoT）模式优化快速生成Lean代码，思维链（CoT）模式强调透明推理步骤 [17] 性能与基准测试 - DeepSeek-Prover-V2-671B在ProofNet-test上通过率37.1%（1024样本），PutnamBench解决49/658题，显著优于Goedel-Prover-SFT和STP等竞品 [23] - 7B版本在ProofNet-test通过率29.6%（1024样本），PutnamBench解决11/658题，展示小模型的高效性能 [23] - 发布ProverBench基准数据集，包含325道题目，涵盖AIME竞赛题及本科数学内容，支持高中至本科难度评估 [25][26] 行业影响 - 模型开源并公开技术细节，HuggingFace平台提供7B和671B版本下载链接，推动数学AI领域发展 [6][16] - 用户实测显示模型效果优于o4-mini和Grok-3，尤其在数学奥林匹克问题解决中表现突出 [31] - 子目标分解与推理融合的设计被类比为初级工程师问题解决技巧，潜在适用于代码生成等场景 [32]