主要证据
- StochBench: A Domain-Specific Benchmark for Stochastic Processes in LeanS1 · 主要研究来源 · 论文 · 2026-09-08
- StochBench datasetS1 · 主要研究来源 · 数据集
StochBench 将研究生随机过程引入 Lean 定理证明评测
该基准覆盖马尔可夫链、更新过程、随机游走、鞅、停时、排队论、布朗运动、随机微积分、弱收敛、泊松过程与连续时间马尔可夫过程。公开数据集区分 114 个直接形式化目标与 336 个抽象化目标：当固定 Lean / Mathlib 环境缺少所需随机过程基础设施时，后者会把必要性质显式写入假设。
发生了什么？
StochBench 论文发布了 450 道研究生随机过程 Lean 4 问题，并与自然语言来源配对；作者报告一个基于 Opus 4.8 的证明 Agent 在每题 15 分钟预算下完成 157/450 个目标，证明率为 34.9%。
为什么重要？
如果形式定理证明基准主要集中在证明库已充分覆盖的领域，就可能高估系统对一般数学的覆盖能力。StochBench 把领域广度与形式库支持不足本身纳入评测面，为证明 Agent 能否在存在显著形式化缺口的应用数学中工作提供更严格的测试。
重要性说明：StochBench 是领域级基准里程碑，因为它把 Lean 定理证明评测从以竞赛题和教材型数学为主的场景扩展到广泛的研究生应用数学领域，并显式区分在形式库支持不足时所需的直接形式化与抽象化表达。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 一个基于 Opus 4.8 的形式化器协助把人工编写的基准问题表达为 Lean 命题，并结合 Lean 反馈与人工修订；另一个基于 Opus 4.8 的证明 Agent 生成论文报告的基线证明结果。
- 人类贡献
- 研究者选择并编写基准专用问题、定义、假设与评测协议，对照来源问题审查形式命题，固定 Lean / Mathlib 环境，并按主题和形式化表示分析基线结果。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-14
技术细节
- 系统
- stochbench, lean
- 机构
- case-western-reserve-university
- 数学问题
- stochastic-processes, graduate-applied-mathematics
- 方法
- benchmarking, lean-formalization, proof-agents, autoformalization
全部来源与工件
- StochBench: A Domain-Specific Benchmark for Stochastic Processes in LeanS1 · 主要研究来源 · 论文 · 访问于 2026-09-14
- StochBench datasetS1 · 主要研究来源 · 数据集 · 访问于 2026-09-14
验证历史
- 2026-09-08 · 论文已发布 · E2 · 研究记录
arXiv 研究记录定义了 450 题基准、随机过程覆盖范围，以及在每题 15 分钟预算下报告的 157/450 基线结果。
- 2026-09-14 · 论文已发布 · E3 · 可检查工件
StochBench 公开数据集提供自然语言陈述、Lean 命题、表示类别与已存储证明记录。E3 表示证据达到可检查 artifact 层级，并不表示完整基线评测已被独立重放。
更正
当前没有记录的更正。