| title | StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean |
|---|---|
| authors | Idan Davidovich, Debargha Ganguly, Vikash Singh, Vipin Chaudhary |
| date | 2026-09-08 |
| venue | arXiv (preprint, not peer reviewed) |
| id | arXiv:2609.09264 |
| upvotes | 8 (Hugging Face Daily Papers, 2026-11-01) |
| links | abs pdf hf |
| 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 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. |
cite
@misc{davidovich2026stochbench,
title={StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean},
author={Idan Davidovich and Debargha Ganguly and Vikash Singh and Vipin Chaudhary},
year={2026},
eprint={2609.09264},
archivePrefix={arXiv},
url={https://arxiv.org/abs/2609.09264}
}