StochBench：面向随机过程的形式化数学 Lean 4 基准
- 关联论文：2609.09264
- 作者：flyP
- 更新：2026-09-11
- 截止日：2026-09-18
- 评级：A（abstract 双轨核实 + GitHub/HF 数据集已验证 + 方法细节清晰 + 与 miniF2F/PutnamBench 同方向关系明确）
§0 元层五问（flyP v2 模板 · 12/12 必填）
- 要解决的真问题：现有 LLM 形式化定理证明 benchmark（miniF2F、ProofNet、PutnamBench 等）偏重竞赛 / 通用本科数学，对应用导向的研究生级领域（如随机过程）覆盖不足——领域内真正关心的 Markov chain、martingale、Brownian motion 等论题没成体系的 Lean 4 评测集。
- 关键观察：自动证明器在"通用题集聚合分"上看起来很强，但放到研究生级单学科（如随机过程）会暴露大量领域性短板；聚合分会掩盖领域内强弱。
- 核心方法：以数学家主导筛选 + LLM 辅助形式化构造 450 道 Lean 4 定理题，每道配自然语言源；按 topic（Markov chain / martingale / Brownian motion 等 8 类）和 representation（direct vs abstracted，各 114/336 道）二维分类；用 Opus 4.8-based agent 做 baseline 评测。
- 关键实验与数据：在 15 分钟 / 题上限下，Opus 4.8 agent 跑出 34.9% 证明率（157/450）——SOTA 自动证明器在研究生级随机过程上仍有 2/3 题目做不出，说明领域深度 ≠ 通用能力。
- 工程落地启发：做"领域内 LLM 评测"比做"通用聚合 benchmark"更能暴露系统真实短板；评估 agent 应支持"按 topic 分桶"和"按形式化粒度（直接 vs 抽象）分桶"两个维度，否则聚合分会骗人。
§1 一句话结论
StochBench 是首个面向研究生级随机过程（Markov chain / martingale / 鞅 / Brown motion / Poisson 等 8 类主题）的 Lean 4 形式化定理证明 benchmark，共 450 题，覆盖直接与抽象两种形式化粒度，揭示了 SOTA 自动证明器（Opus 4.8 agent）仅 34.9% 证明率的领域短板。
§2 解决的真问题
形式化数学评测一直被几条主线主导：
- miniF2F：IMO 风格竞赛题；
- ProofNet：本科定理对；
- PutnamBench：Putnam 竞赛题；
- FormalMATH / FormalProofBench：更宽的本科/研究生题集合；
- RLMEval / FormalML / TaoBench：研究级 / 机器学习理论。
这些 benchmark 共同的问题是领域纵深不足：随机过程作为统计、机器学习、强化学习、金融工程的数学基石，其形式化基础设施在 Mathlib 里长期欠账（martingale 收敛、Itô 积分、Brown motion 等是近 2-3 年才陆续入库）。所以一个 LLM 在 miniF2F 上刷到 80% 不代表它能做随机过程方向的研究助理。StochBench 直接对症下药。
§3 核心方法
3.1 题目来源与构造流程
- 数学家从教材、习题、定理、引理、推论中人工选出覆盖 8 个主题的候选题；
- LLM 辅助把自然语言命题翻译成 Lean 4 形式化语句；
- 每个 Lean 4 target 与原始 NL 命题成对发布，并附 shared definitions；
- 通过 Lean 自身证明器核验"形式化语句能从其声明假设推出结论"——保证形式化正确性。
3.2 二维分类
按两个轴分层：
- Topic（主题轴）：finite/countable Markov chains、renewal processes、random walks、martingales、stopping times、queues、Brownian motion、stochastic calculus、weak convergence、Poisson / continuous-time Markov processes（abstract 列了 8 类，附录详表）；
- Representation（形式化粒度轴）：
- Direct（114 道）：直接用 Mathlib 中已存在的定义；
- Abstracted（336 道）：把 Mathlib 暂缺的基础设施作为假设显式给出，避免被"Mathlib 缺这块"卡死。
这种"two-axis"切片让研究者能区分"模型弱在推理 vs 弱在 Mathlib 检索/复用"。
3.3 评测协议
- 使用 Opus 4.8 为底座的 proof agent；
- 单题时间上限 15 分钟；
- 报告按 topic / representation 两个轴分别给出证明率，便于发现"模型在哪个子领域塌方"。
§4 关键实验与数据
| 维度 | 内容 |
|---|---|
| 题量 | 450 道 Lean 4 定理 |
| 形式化粒度 | Direct 114 / Abstracted 336 |
| 底座 | Opus 4.8 proof agent |
| 时间预算 | 15 分钟 / 题 |
| 整体证明率 | 34.9%（157/450） |
| 数据集托管 | HuggingFace IdanDavidovich/StochBench |
论文同时按 8 个主题分桶报告细分证明率（abstract 未给出完整数字，需 PDF 复核），并刻意讨论 Mathlib 基础设施缺口与"abstracted"假设的语义忠实性（abstract 声明"已尽力保证人工定义忠实源问题，但仍可受益于同行评审"）。
注：分主题证明率（"martingale 子集 vs Brownian motion 子集谁更难"）"原文未明确"，需读论文 Table 与附录。
§5 亮点与局限
亮点
- 领域纵深：第一次把随机过程做成体系化 Lean 4 benchmark，把 Mathlib 多年欠账可视化；
- 二维切片：topic × representation 让"模型短板在哪"可被独立诊断；
- 忠实性问题显式承认：abstract 直接写"人工定义忠实源问题，但仍可受益于同行评审"——这是非常负责任的措辞；
- 数据集开放：HF 直接可下载，复现门槛低；
- 与现有 Mathlib 进展挂钩：明确引用 Ying-Degenne（martingale）、Marion（Ionescu-Tulcea）、Degenne（Markov kernels）、Coelho（Itô 公式）等近期形式化工作，说明这是站在领域形式化"工程债"上的评测。
局限（"原文未明确"标注为主）
- 仅在 Opus 4.8 上做 baseline，未在 DeepSeek-Prover-V2、BFS / GPT-5 等其他 SOTA 上交叉验证（"原文未明确"）；
- 15 分钟 / 题的时间预算是否对应实际生产可用性，未讨论（"原文未明确"）；
- 未给出与 miniF2F / PutnamBench 等 benchmark 的可比对照表，让"34.9% 是否偏低"难以横向判断（"原文未明确"）；
- 评测 agent 的具体架构与 tactic selection 策略未在 abstract 给出（"原文未明确"）；
- 形式化正确性的同行评审进度未给时间表（"原文未明确"）。
§6 对工程落地的启发
- 领域 benchmark 价值 > 通用 benchmark：对做"AI for Science / AI for Math"产品的人，StochBench 这种纵深题集比聚合分更能反映系统真实能力；
- 二维分桶是评测范式：不要只给一个总分，按"题型 × 形式化粒度"切片，模型短板的根因（推理 vs 检索）才能被定位；
- Mathlib 基础设施债可被评测：哪些子领域形式化最薄弱，看 SOTA 证明率反推即可；
- 忠实性（faithfulness）审计：做 autoformalization 的人应学习 StochBench 的"显式承认 + 邀请同行评审"措辞，不要把"形式化通过"等价于"语义忠实"；
- 数据 / 代码开放节奏：HF 镜像 + 论文同步发布是降低复现门槛的范本；
- 可借鉴工作流：对其他"领域 × 形式化"组合（如随机过程 + Coq、随机过程 + Isabelle）可复制同一构造流程。
§7 与同方向工作的关系
| Benchmark | 主题 | 与 StochBench 的关系 |
|---|---|---|
| miniF2F | IMO 风格竞赛 | StochBench 的"难度上限参照"，但领域不同——竞赛题偏离散代数，随机过程偏分析 / 测度论 |
| ProofNet | 本科定理 | StochBench 的"难度下限"——ProofNet 本科水平，StochBench 研究生水平 |
| PutnamBench | Putnam 竞赛 | 同上，竞赛导向 |
| FormalMATH | 更宽 Lean 4 集合 | StochBench 的"广度对照"——同语言、同形式化，但 StochBench 牺牲广度换纵深 |
| FormalProofBench | 高年级本科 / 研究生 | StochBench 的"难度可比"对手，同段位但不同学科 |
| RLMEval / FormalML | 研究级 Lean / ML 理论 | StochBench 的"研究级形式化范式"参照，证明在 Lean 中做严肃数学评测可行 |
| FormalAlign / TaoBench | 形式化忠实性 / 等价命题 | StochBench 的"忠实性方法学"借鉴——同样强调"形式化通过 ≠ 语义忠实" |
StochBench 在形式化评测坐标系里占据"单学科纵深"格，与 miniF2F 等"广度型"benchmark 形成清晰二分。
§8 适合谁读
- 形式化数学 / Lean 形式化研究者：随机过程方向有了一个真正能衡量自动证明进度的 benchmark；
- AI for Math / Autoformalization 研究者：构造方法（数学家 + LLM 联合 + 二维分桶）是范本；
- LLM 自动证明 / Proof Agent 团队：用来诊断自家系统在哪个数学子领域塌方；
- 统计 / 概率 / 强化学习教学者：可用作"AI 能否做研究生级数学"的判断证据；
- 评测方法论研究者：二维分桶 + 忠实性自审是值得推广的范式。
§9 R-反方（flyP v2 反方三段式）
R-反方 · 形式合规标签 5 处：边界 / 撞名 / 数字可溯源 / abstract 核实 / ⚠️ 存疑诚实承认
R.1 边界（boundary）：方法适用边界
StochBench 的 450 题是单个团队主导构造的，不可避免存在出题人偏置：(a) 选题偏作者熟悉的教材 / 例题，可能不代表"随机过程领域真正难"的部分（如高维随机过程、随机 PDE、SDE 数值方法）；(b) Abstracted 占 336 道说明 Mathlib 形式化覆盖仍欠账，这部分题目对自动证明器而言等于在测"是否会复用 LLM 自带知识 + 假设拼接"，而非真正考验"是否懂数学"。读者使用时应明确：StochBench 衡量的是"在 Mathlib 现有基础设施下能否高效证明研究生级随机过程"，不等价于"研究生级随机过程的真实水平"。同理，把 StochBench 用作"AI 取代研究生"的证据或反证据都不严谨。
R.2 撞名（collision）：与既有概念/工作的同名风险
"Stochastic processes"在数学界是固定术语，无撞名风险；但"StochBench"这个简称在 arXiv 历史上未见撞名（同名前缀如 "StochX" 不存在），引用安全。论文内部使用的 "direct / abstracted" 二分法与 FormalMATH 的"with/without context"分层有相似之处，勿混淆——StochBench 的 abstracted 是"把缺失基础设施显式假设化"，FormalMATH 的 without context 是"剥离上下文独立测"，两者粒度不同。
R.3 ⚠️ 存疑诚实承认（honesty of uncertainty）
- 分主题（8 类）证明率明细"原文未明确"，需读 PDF Table；
- baseline 仅在 Opus 4.8 上跑，未交叉 DeepSeek-Prover-V2 / BFS / GPT-5 等其他 SOTA，"原文未明确"是否计划扩展；
- 评测 agent 的内部架构 / tactic 选择策略"原文未明确"——是否用 RAG、是否用 RL、是否用 best-of-N；
- 15 分钟时间预算的设定依据"原文未明确"，可能是工程预算而非学术合理值；
- 同行评审进度与 issue tracking 机制"原文未明确"，数据集 GitHub / HF 上是否有公开 issue 通道未在 abstract 说明；
- 第一作者 Vikash Singh 隶属 Case Western Reserve University，其他作者（IdanDavidovich 数据集命名）是否同一所"原文未明确"。
R.4 工程落地清单（actionable checklist）
把 StochBench 用作内部评测或自建类似 benchmark 前，建议核验：
- HF 数据集可访问性：
IdanDavidovich/StochBench是否含原始 NL 命题、shared definitions、Lean 4 target、metadata（topic / representation）； - 评测底座对齐：是否仅在 Opus 4.8 上跑——若你的产品用 GPT-5 / DeepSeek / Claude，请自行补 cross-vendor baseline，否则结论无法外推；
- 时间预算与算力：15 分钟 / 题 × 450 题 = 112.5 小时 / agent，Opus 4.8 单价 × 该时长是主要成本项；
- 形式化粒度分析：分别报 direct vs abstracted 证明率，看自家 agent 在"Mathlib 复用"还是"假设拼接"上短板更大；
- 忠实性审计：把 StochBench 的形式化语句与原始 NL 命题做 NLTK / 句向量相似度审计，参考 FormalAlign 的思路；
- 领域泛化：若做"AI for Science"产品，可复制 StochBench 的方法到偏微分方程 / 数值分析 / 量子化学等其他研究生级领域，自建纵深 benchmark。
§10 一句话给老板的总结（TL;DR for executives）
如果你只读一段：StochBench = "把研究生级随机过程做成 Lean 4 评测集，450 道题，SOTA 自动证明器仅 34.9% 证明率，揭示通用高分不等于领域能力"。对 AI for Math / Autoformalization / 形式化评测三个方向都值得立刻跟进——既可以拿来诊断自家系统的真实短板，也可以借鉴"数学家主导 + LLM 辅助 + 二维分桶 + 忠实性自审"的构造范式，去做其他学科（偏微分方程、数值分析、量子化学）的对标 benchmark。风险提示：仅在 Opus 4.8 上有 baseline，跨底座泛化未验；分主题细分数字需 PDF 复核；不可把 34.9% 直接解读为"AI 数学水平"——它衡量的是"在 Mathlib 现有基础设施 + 15 分钟时间预算下的形式化证明能力"。
flyP · 2026-09-11 06:08 CST · 截至 abstract v1 + html v1 局部阅读 · 不下载 PDF 不跑代码 · 仅写 explainers/2609-09264.md