截至 2026-07-07T23:35:05Z UTC，BFS-Prover-V2 的有效信号集中在一个更具体的位置：字节跳动 Seed 正在把形式化数学当作执行问题处理。模型提出 Lean4 tactic，证明助手接受或拒绝这些 tactic，系统再把训练与推理预算投向那些实际能收束证明的搜索分支。[1][2][3]
这让本文成为另一类 AI-China 基准笔记。许多推理发布要求读者相信自然语言答案或基准打分器，BFS-Prover 和 BFS-Prover-V2 则更接近编译器式循环。一个候选 tactic 要么让 Lean 证明状态沿合法方向前进，要么报错失败，要么让搜索停住。它的评测面比通用推理窄，但更难用漂亮文本掩盖失败。在这一条线上，“推理”指的是在结构化证明空间里找到一条机器可检查的路线，而不是写出一段有说服力的文字。
封面图有意采用纪实照片：维基共享资源上一张北京字节跳动前总部建筑的真实照片。[6] 本文讨论的是字节跳动 Seed 的系统发布，核心问题是一个模型要成为有用的形式化证明组件，需要多少搜索、反馈与再训练。
为什么这个基准不同
最初的 BFS-Prover 论文于 2025 年 2 月提交，随后修订。它挑战了自动定理证明中的一个假设：大规模证明搜索一定要依赖蒙特卡洛树搜索或价值函数这类更重的方法。论文的核心动作更简单：使用 best-first tree search，把训练数据过滤到更难的样本上，用 Lean4 编译器反馈对 state-tactic 对做偏好优化，并归一化路径长度，让搜索避免过度偏向浅层证明尝试。[2]
字节跳动 Seed 在 2025 年 2 月 25 日的官方发布中，用操作层语言解释了这一点。形式化证明面对庞大的 tactic 空间、不断变化的合法动作、稀疏反馈，以及耗时很长的开放式尝试。因此，系统必须同时从失败和成功里学习：失败的 Lean tactic 变成负信号，成功的 tactic 变成证明路线数据，后续轮次减少在简单证明上的重复学习。[1]
因此，头部数字不能按聊天模型分数理解。BFS-Prover 在累积评测中报告 MiniF2F 为 72.95%，官方文章还给出固定预算对比，预算为 2048 x 2 x 600 次推理调用。[1][2] 预算本身就是主张的一部分。一个定理证明器若只靠消耗远多得多的搜索调用来解出更多题目，它对研究仍然有用，但和 Lean 编辑器里的快速交互助手属于不同产品形态。
V2 改了什么
BFS-Prover-V2 把第一版系统的重心明确到两类扩展：训练循环扩展，推理循环也扩展。2025 年 9 月的 V2 论文描述了用于训练的多轮离策略强化学习框架，以及用于推理的规划器增强多智能体树搜索架构。规划器把难定理拆成更简单的子目标，并行证明 agent 则共同使用共享证明缓存。[3]
公开 GitHub 仓库用更直接的工程语言给出了同一条边界。V2 是一个面向 Lean4 的开源步骤级定理证明系统，包含自适应 tactic 级数据过滤、周期性再训练，以及规划器引导的多智能体搜索。表格把无规划器和有规划器两种情况分开列出：BFS-Prover-V2-32B 在 MiniF2F-test 上为 86.1%，MiniF2F-valid 上为 85.5%，ProofNet-test 上为 41.4%；带规划器的 BFS-Prover-V2-32B 在 MiniF2F-test 上达到 95.08%。[4]
这个拆分很重要。规划器结果的含义更具体：外围推理系统提高了证明搜索效率，模型本体能力提升之外，系统工程承担了相当部分。对评估形式化证明模型的团队来说，正确单位是模型、搜索策略、证明缓存与预算的组合。把 95.08% 当成裸模型分数，会抹掉支撑这个数字的系统工作。
模型边界
Hugging Face 模型卡把组件边界展示得很清楚。BFS-Prover-V2-32B 是一个在 Apache-2.0 许可下发布的 33B 参数 safetensors 模型，标签指向 Lean4 与步骤证明，基座模型为 Qwen2.5-32B。模型卡列出的训练来源包括经 LeanDojo 使用的 Mathlib、Lean GitHub 仓库、自动形式化的 NuminaMath 数据集，以及 Goedel-Pset。[5]
它的使用格式也被限定得很窄。模型接收一个 Lean4 tactic state，后接 :::，再返回一个候选 tactic。这更接近验证过的证明状态中的代码补全，距离通用数学导师较远。模型卡里的示例采用一次 tactic 生成调用的形态，针对具体证明状态产出 Lean tactic；对话式推导留在范围之外。[5]
读者理解评测时要抓住这一边界。BFS-Prover-V2 有力表明，中国 AI 实验室正在发布严肃的形式化推理基础设施组件。若把它当作无约束数学发现、通用科学自主性或日常编码 agent 可靠性的证据，力度就弱得多。Lean 检查每一步，所以基准严谨；状态空间、语法、库和 tactic 又都属于 Lean4 形式化范围，所以它也高度专门化。
它在中国技术栈中的意义
中国 AI 叙事常被简化为模型规模、token 价格和消费者应用。BFS-Prover-V2 指向另一层：特定领域推理系统，模型只是其中一个活动部件。字节跳动 Seed 发布的是带有训练循环、推理循环、模型权重、代码和可复现形式化目标的证明搜索栈；聊天机器人式的数学示例只在外围。[3][4][5]
这对工程团队有意义，因为形式化证明是检验 agentic 主张的压力测试。系统要处理长程搜索、稀疏奖励、工具反馈、状态转移和严格正确性检查。这些成分同样出现在软件修复、芯片验证、符号规划、科学工作流等任务中；在这些任务里，模型要处理的远超过生成可信文本。迁移不会自动发生；但架构给出了清楚提示：把环境设得严格，把错误转成训练信号，并把基准结果绑定到真实搜索预算。
它在地缘技术层面的意义也比较低调。中国实验室的开放模型发布已经扩展到通用聊天与媒体生成之外，越来越多地包含基础设施组件：评测 harness、后训练系统、服务层、GUI agent 组件，以及现在的形式化证明系统。BFS-Prover-V2 属于这一类。它呈现为一个可检查、可 fork、可评测、可嵌入的研究与开发者制品，消费端热闹发布只是外围参照。
观察项
第一个观察项是预算透明度。只有在 tactic 生成预算、规划器使用、超时策略和缓存行为可见时，MiniF2F 与 ProofNet 结果才有用。缺少这些细节，团队就无法公平比较步骤证明器、整段证明生成器和交互助手。
第二个观察项是库依赖。一个在 Mathlib 和相关仓库上训练的 Lean 证明器，面对定理陈述、可用引理和 tactic 模式与语料相似的任务时表现较好。遇到不熟悉的局部定义、发展不足的库，或训练分布之外的领域形式化时，它会变得吃力。
第三个观察项是人类工作流适配。Hugging Face 与 GitHub 材料都指向 Lean 工作流中的使用方式，包括 tactic-state 输入和集成方式。[4][5] 实践问题在于，数学家或形式化方法工程师能否用这个模型缩短证明开发时间，而不只是看到离线基准提高。
证伪条件很直接。如果 V2 最强数字所需的搜索预算对真实 Lean 工作过于昂贵，如果离开基准式陈述后性能急剧下降，或者生成的 tactic 需要大量人工分拣以至于拖慢工作流，那么 BFS-Prover-V2 主要就是研究里程碑。如果规划器和证明器的组合能在明确预算下持续解出困难子目标，那就是更重要的信号：中国 AI 进展正从宽口径模型发布，进入由环境本身给工作打分的专门化推理系统。
来源
- ByteDance Seed, "Seed Research | New SOTA in Formal Mathematical Reasoning! BFS-Prover Model Now Open Sourced"（2025 年 2 月 25 日；BFS-Prover、Lean4 反馈、MiniF2F 结果和开源链接的官方概览）。
- Ran Xin et al., "BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving," arXiv:2502.03438（2025 年 2 月 5 日提交；2025 年 10 月 9 日修订）。
- Ran Xin et al., "Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers," arXiv:2509.06493（2025 年 9 月 8 日提交；2025 年 10 月 9 日修订）。
- ByteDance-Seed, "BFS-Prover-V2" GitHub repository（开源代码、技术概览、基准表和 Lean 使用说明）。
- ByteDance-Seed, "BFS-Prover-V2-32B" Hugging Face model card（模型元数据、Apache-2.0 许可、Qwen2.5-32B 基座、训练来源、基准表和使用格式）。
- Wikimedia Commons, "File:In-Do Mansion (20220411152216).jpg"（本文封面真实照片的来源页面）。