# StochBench：面向 Lean 随机过程的领域专用基准

- 来源：HuggingFace Daily Papers（社区热门论文）
- 发布时间：2026-09-08 08:00
- AIHOT 分数：37
- AIHOT 链接：https://aihot.news/items/cmtvjb3b60axbronbsvrygpjm
- 原文链接：https://arxiv.org/abs/2609.09264

## AI 摘要

研究者推出 StochBench，一个包含 450 道研究生级随机过程问题的 Lean 4 基准，每题配有自然语言题面。基于 Opus 4.8 的智能体在每题 15 分钟限制下达到 34.9% 的证明率（157/450）。该基准覆盖马尔可夫链、鞅、布朗运动、随机微积分等方向，填补了 Mathlib 中随机过程领域代表性不足的空白。

## 正文

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 source. Addressing a field underrepresented in Mathlib, it covers finite and countable Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous-time Markov processes. Our Opus 4.8-based agent achieves a 34.9% proof rate (157/450) under a 15-minute per-problem limit. StochBench better represents domain-specific applied mathematics while remaining challenging for advanced provers.