StochBench：面向随机过程的 Lean 4 领域专用定理证明基准 StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
450 道研究生随机过程 Lean 4 基准，最强智能体证明率 34.9%
前置知识
Lean 4 与 Mathlib
Lean 4 是交互式定理证明器兼编程语言：数学陈述写成类型论中的命题，证明是一段可被独立内核机械检查的程序。Mathlib 是其社区维护的大型数学库，收录大量已形式化的定义与定理。固定库版本下通过 elaboration（类型检查）可验证一个陈述是否良构；sorry 是“未证完”的占位符，含 sorry 的证明不算干净证明。
本文每道基准题都是一条 Lean 4 定理，评测判据（净证明 = Lean 接受且无 sorry/sorryAx/admitted 事实）完全建立在 Lean 内核检查之上，不懂这套机制就无法理解其评测协议。
随机过程核心对象
本文覆盖的教科书概念：马尔可夫链（状态转移只依赖当前状态的随机过程）、鞅（未来条件期望等于当前值的公平博弈过程）、停时（可由至今观测决定何时停止的随机时间）、首达时方程、布朗运动（增量服从高斯分布且路径几乎处处连续）、泊松过程、CTMC、全变差距离 $\|\mu-\nu\|_{TV}$ 与弱收敛。
基准题目全部取自研究生随机过程课程，若不清楚这些对象在数学上“要求证明什么”，就无法判断形式化是否忠实、抽象化假设给了证明器哪些便利。
自动形式化与语义对齐
自动形式化（autoformalization）指把自然语言数学陈述翻译成形式语言；难点在于语义对齐——形式陈述未必忠实表达原意（漏掉可测性、可积性假设等）。FormalAlign 专门评测非形式—形式对齐质量，MathAtlas 研究带依赖结构的研究生级形式化。
StochBench 的每条记录都是“非形式陈述 + Lean 目标”配对，作者坦承忠实性未经同行评审并接受内核验证的证伪；理解对齐风险才能正确使用这批数据做训练。
直接目标与抽象目标
本文的关键标注维度：直接目标（literal/direct）直接使用 Mathlib 对象或共享定义陈述；抽象目标（abstract）把证明所需的性质（如布朗运动的高斯增量、独立性与几乎处处连续，打包为局部 IsBM 定义）作为显式假设给出，由 Lean 保证结论确实由这些假设推出。
69.3% 对 23.2% 的证明率差距是全文最重要的实验发现，而这一差距的含义完全取决于对这两种表示方式的理解。
编译器反馈驱动的 LLM 证明智能体
多轮工具调用智能体：把 Lean 目标交给大模型生成证明策略，读取编译器/语言服务器返回的错误信息，检索库与共享定义（经 loogle、leansearch 查询），迭代修改证明直至通过或超时。本文用 lean4skills 与 Lean LSP MCP 服务器实现该循环，每题单次运行、上限 15 分钟。
34.9% 的基线成绩正是这套智能体栈跑出来的，其预算设置（单智能体、单次、15 分钟）直接决定了结果该作何解读。
研究动机
现有形式化定理证明基准几乎都集中在竞赛数学上：MiniF2F 以 Olympiad 风格题目为核心，PutnamBench 收录 Putnam 本科竞赛题，ProofNet 配对的是本科教材定理；后来的 FormalMath 扩大了规模和学科覆盖，FormalProofBench 触及研究生内容，但都不是针对单一应用数学领域的深度评测。这类集合规模小、领域窄，聚合分数会掩盖模型在具体分支上的强弱——一个在数论不等式上表现不错的证明器，可能在马尔可夫链或鞅论上完全失效，而总分完全看不出来。随机过程作为统计学与机器学习的核心数学工具，在 Mathlib 中的基础设施明显不足，许多教科书结论缺少现成引理，导致“想形式化也难以陈述”。结果是无法区分一次证明失败究竟源于模型能力不足、题目困难，还是库支持缺失。
本文的目标是本文要构建 STOCHBENCH：一个聚焦研究生随机过程的 Lean 4 定理证明基准，包含 450 道目标定理，每道都配有自然语言原始陈述，覆盖八个主题——马尔可夫链（有限与可数状态）、更新过程、随机游走与大偏差、鞅与停时、排队论与连续时间马尔可夫链、布朗运动与随机分析、弱收敛与泛函极限、泊松过程。作者为反复出现的概念构建共享 Lean 定义库，并对每道题标注形式化范围：直接目标使用 Mathlib 对象或共享定义，抽象目标把所需性质作为假设显式给出，使 Lean 能机械验证结论确实由所述假设推出。评测侧用编译器引导的 Opus 4.8 智能体在每题 15 分钟上限下做单次基线，按主题和表示方式分别报告成绩，为后续领域专用证明器提供可比较的测试床。
与已有工作不同的是，本文的独特切入是“领域内深度优先”：不像 MiniF2F 横跨多领域堆总量，而是把 450 道题集中在一个被忽视的分支上，让聚合分数能真实反映该领域的证明能力。第二，“范围感知”评测：每道题标注 direct/literal 或 abstract，把“Mathlib 缺基础设施”从混杂因素变成显式实验变量——直接使用 Mathlib 的 Martingale 接口与显式假设无记忆性，代表两类本质不同的任务。第三，区分“单时刻边际分布”与“过程联合律”两种表示：HasMatrixMarginals 只约束 $X_n$ 的分布等于转移矩阵幂的对应行，HasChainLaw 则规定有限维概率 $P_\mu(X_0{=}x_0,\dots,X_n{=}x_n)=\nu(x_0)\prod_{i=0}^{n-1}P(x_i,x_{i+1})$，显式控制证明器可获得的信息量。第四，考虑到形式化可能出错，作者接受“内核验证过的证伪”作为合法输出，这在基准设计中相当少见。
核心方法
整体思路是“数学家主导选题 + LLM 辅助形式化 + 编译器把关”的四阶段流水线：先从教材与课程笔记中选题，再由人类撰写全部定义、假设与问题陈述（Opus 4.8 形式化器辅助翻译为 Lean），接着为反复出现的概念构建共享定义库，最后产出 450 道 Lean 4 目标——114 道（25.3%）为直接目标、336 道（74.7%）为抽象目标。所有候选陈述在 Lean 4.30.0 与固定版本 Mathlib 下反复修订直至通过 elaboration 类型检查。共享定义层涵盖：随机矩阵的随机性、平稳性、不可约性、非周期性、转移幂的最终正性、细致平衡、时间反转与全变差距离的统一矩阵表示；首达时方程（IsHittingSolution、returnTime）；经无穷级数定义 n 步转移的 nstep；连接 Mathlib 的 natStop（自然数停时转 WithTop）、runningMax（有限运行最大值）、IsConstDrift（条件增量恒等式）。评测用 lean4skills 加 Lean LSP MCP 驱动的多轮 Opus 4.8 智能体，每题一次、上限 15 分钟。
核心创新是“范围感知的形式化”。随机过程的许多结论依赖 Mathlib 尚未提供的重型基础设施（如 Donsker 定理需要 $C([0,T],\mathbb{R})$ 上的测度与泛函分析工具），照搬教科书陈述根本无法在 Lean 中表述。作者的解法是把每道题分派为两种表示之一：直接目标使用 Mathlib 对象或共享定义；抽象目标把推导所需的性质作为显式假设给出——例如布朗运动目标以高斯增量分布、独立性与几乎处处路径连续为假设（打包为局部 IsBM 定义），而二次变差目标要求均方误差随分割网径趋零收敛。这些选择有实质差别：给出布朗运动性质并不预设二次变差结论，假设无记忆性则免去从连续时间链动力学推导它。本质区别在于：TaoBench 只用成对等价陈述孤立地研究表示问题，而本文在整个基准层面系统性标注范围，使“库支持缺口”成为可分析的变量，并以净证明判定（Lean 接受且无 sorry/sorryAx/admitted 事实）保证结果可信。
方法步骤详情
第一步（选题）：从 Siegrist 2022 教材与 MIT 三门课（Wu 2015 随机过程导论、Gamarnik 2013 高等随机过程、Gallager 2011 离散随机过程）的习题、引理与定理中挑选，剔除过于接近一般概率论的陈述（如全变差距离三角不等式），得到 450 道：马尔可夫链 96、鞅与停时 94、随机游走 62、CTMC 与排队 55、布朗运动 45、更新过程 41、泊松 40、弱收敛 17。第二步（形式化）：全部定义、假设与问题由人写，Opus 4.8 形式化器辅助表达，借 Lean 报错迭代修订，直到在 Lean 4.30.0 + 固定 Mathlib 下通过 elaboration；耦合界目标额外要求两过程在相遇时刻后一致，强平稳时间目标用联合律加停时条件联系停止时刻与之后确定时刻的状态。第三步（标注与发布）：每条 JSON 记录含标识符、题目名、非形式陈述、Lean 目标与 direct/abstract 标签，连同共享定义与基线证明尝试一起发布。第四步（评测）：单次运行 Opus 4.8 智能体（lean4skills + Lean LSP MCP），允许查看 Lean 报错、搜索库与共享定义、loogle/leansearch 查询与多轮改证明，每题 15 分钟；最后由 Lean 比较器验证证明不含任何被承认的事实。
技术新颖性
技术新颖性有三处。其一，这是随机过程方向的第一个 Lean 基准，把 Doob、Donsker 一脉的教科书结论系统搬进 Lean，八主题分布不均（鞅 94 道最多、弱收敛 17 道最少）忠实反映课程重心，而非刻意均衡采样。其二，共享定义层与表示学的设计：用统一矩阵表示承载有限链的全部性质，用 $P_\mu(X_0{=}x_0,\dots,X_n{=}x_n)=\nu(x_0)\prod_{i=0}^{n-1}P(x_i,x_{i+1})$ 这类联合律定义区分边际与过程律，使“证明器能看到哪些信息”成为受控变量；耦合界目标把矩阵边际与“相遇后过程一致”的显式条件结合，强平稳时间目标把联合律与停时条件结合。其三，评测协议上接受内核验证的证伪输出，为混入的形式化错误提供纠错通道。与 LeanDojo（证明搜索与检索）、FormalAlign（语义对齐评测）不同，本文把领域覆盖度与表示范围当作一等评测维度，这是与已有工作最本质的区别。
实验结果
基线评测核心数字：Opus 4.8 智能体在每题 15 分钟上限下完成 157/450 道净证明，总证明率 34.9%。按表示方式分层差异巨大：直接目标 79/114 = 69.3%，抽象目标仅 78/336 = 23.2%，相差 46.1 个百分点（作者强调这是描述性对比，不构成受控因果效应）。按主题看：鞅与停时最易，61.7%（58/94，其中 67 道直接题证出 51 道）；CTMC 与排队 41.8%（23/55）；马尔可夫链 38.5%（37/96）；弱收敛 35.3%（6/17，6 道全部来自直接题）；随机游走与大偏差 25.8%（16/62）；布朗运动与随机分析 17.8%（8/45，全部为抽象题）；泊松过程 17.5%（7/40，5 道直接题 0 通过）；更新过程最难，仅 4.9%（2/41）。定性检查发现三类失败模式：看似可行目标上的证明搜索失败、缺失引理或困难的库接口，以及少量形式化缺陷（缺可测性、可积性或非空性假设）。另值得注意：157 道净证明可作为证明生成的监督信号，450 组非形式—形式配对可用于自动形式化训练。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 随机过程定理证明（全部 450 题） | 净证明率（Lean 接受且无 sorry/sorryAx/admitted，每题 15 分钟上限，单次运行） | 34.9%（157/450） | 该领域首个 Lean 基准，无同分布基线；MiniF2F 等竞赛基准任务分布不同，不可直接对比 | —（建立首个领域基线） |
| 直接目标证明（direct/literal，114 题） | 净证明率 | 69.3%（79/114） | 抽象目标 23.2%（78/336） | 高出 46.1 个百分点（描述性对比，未控制题目难度与库支持差异） |
| 鞅与停时（94 题，67 直接 + 27 抽象） | 净证明率 | 61.7%（58/94） | 全基准平均 34.9% | 高出平均 26.8 个百分点，八主题中最易 |
| 更新过程（41 题，全部抽象） | 净证明率 | 4.9%（2/41） | 全基准平均 34.9% | 低于平均 30.0 个百分点，八主题中最难 |
| 布朗运动与随机分析（45 题，全部抽象） | 净证明率 | 17.8%（8/45） | 全基准平均 34.9% | 低于平均 17.1 个百分点，反映 Mathlib 随机分析基础设施缺口 |
局限与改进
作者明确承认：题目挑选、忠实性审查与主题/范围分类都由人工策展人决定，相关术语（如“何谓忠实形式化”）未严格定义，存在偏差；定义与假设虽经对照源题自查，仍需同行评审，可能混入形式化错误（他们为此接受内核验证的证伪，但这只是补救而非预防）。基线是单智能体、单预算、单次运行，不构成模型对比，也无法报告方差；主题率与类率是描述性统计，无法把抽象化效应与题目难度、库支持差异分离开。我的补充观察：15 分钟上限是任选的，可能系统性低估需要长程搜索的目标；形式化器与求解器同用 Opus 4.8 存在自我一致性偏好，也可能带来数据污染风险；抽象目标“赠送”的假设强弱不一（有的是完整中间引理，有的只是定义性条件），使 23.2% 这个数字难以精细解读；更新过程 4.9%、泊松 17.5% 的极低通过率到底是能力问题、题面问题还是共享定义接口问题，论文未做归因实验。
独立分析的弱点
第一，忠实性验证薄弱：450 道题的“Lean 陈述是否忠实于源题”只靠作者自查，论文坦承需要同行评审；一旦某题形式化有误，其“证明失败”就毫无意义。改进方向：公开每题源出处并组织社区审查，或训练自动忠实性评估器给出对齐分数。第二，类别对比混淆变量：abstracted 类占 74.7%，且各类假设的信息量差异极大，69.3% 对 23.2% 的差距无法归因于单一因素。改进：为每题标注假设的“馈赠强度”等级，并构造同一题的 direct/abstract 双版本做配对实验。第三，评测协议单薄：单次运行、单一模型、固定 15 分钟，无重复实验方差、无 pass@k 曲线，与主流代码生成评测实践脱节。改进：至少对代表性子集多次采样并报告 pass@k 与预算—性能曲线。第四，异常低分未归因：更新过程 4.9%（2/41）与泊松 17.5%（直接题 0/5）远低于平均，可能是共享定义接口不利或题面表述晦涩。改进：建立失败错误类型学，区分搜索失败、接口困难与题面缺陷。第五，工程复现摩擦：智能体栈需自行拼装 lean4skills 与 Lean LSP MCP，缺少一键评测脚本。
未来方向
作者提出的方向：利用新构造的非形式—形式配对做自动形式化训练；用 157 个通过内核检查的基线证明作为证明生成的监督信号；结合共享定义推动更强的领域专用证明器与随机过程在 Mathlib 中的持续形式化。基于成果可延伸的方向：其一，把 450 道题用作强化学习环境——Lean 编译器奖励信号天然干净，可训练专精随机过程的证明模型，并检验 abstract 训练能否迁移回 direct/Mathlib 真实基础设施。其二，开展范围感知的受控实验：同一题构造双版本，量化库支持缺口对证明率的因果影响，反哺 Mathlib 决定优先补哪些引理性价比最高。其三，横向扩展到相邻领域（统计推断、遍历理论、随机微分方程数值方法），纵向把 15 分钟预算扩展为预算扫描，刻画“花更多算力能买多少证明率”。其四，把证伪通道自动化：系统搜索能推翻形式化陈述的反例，形成形式化质量保障流水线，缓解人工评审瓶颈。
复现评估
复现基础较好：数据集已在 HuggingFace 公开（IdanDavidovich/StochBench），包含 450 条 JSON 记录（标识符、题目名、非形式陈述、Lean 目标、direct/abstract 标签）、共享定义文件与基线证明尝试；Lean 侧只需 Lean 4.30.0 加固定版本 Mathlib 即可编译验证，判定净证明完全确定且成本极低。难度较高的部分在智能体栈：需要自行组装 lean4skills 与 Lean LSP MCP 服务器并接入 Opus 4.8 API——按每题 15 分钟上限、450 题计，单次完整基线最多约 112.5 小时的模型调用时间，API 成本单个研究组可承受但不可忽略。主要不确定性在基线数字的可重复性：单次运行无方差报告，API 模型版本迭代后数字会漂移，建议复现者固定模型快照并在子集上多次采样。整体格局是“数据集高保真可复现、智能体分数仅供参考”，这也是此类 LLM 基准论文的常态。
论文图表
