StochBench：面向 Lean 随机过程的领域专用基准
原标题：StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
AI 摘要
研究者发布 StochBench，一个基于 Lean 4 的随机过程领域基准，包含 450 道研究生水平的随机过程题目，每题配有自然语言原题。该基准覆盖马尔可夫链、鞅、布朗运动、随机微积分等 Mathlib 中覆盖不足的主题。基于 Opus 4.8 的智能体在每题 15 分钟限制下达到 34.9% 的证明率（157/450），表明该基准对先进证明器仍具挑战性。
正文节选
The 6th Workshop on Mathematical Reasoning and AI StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean Abstract Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition math, such as the IMO and Putnam, that poorly represent field-specific applications. We introduce StochBench, a Lean 4 benchmark of 450 graduate stochastic-processes problems at varying abstraction levels, each paired with its natural-language sourc