StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
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...
| Authors | Idan Davidovich, Debargha Ganguly, Vikash Singh et al. |
|---|---|
| Primary category | cs.CL |
| Published | 8 September 2026 |
| Last updated at source | 8 September 2026 |
Connected in the knowledge graph
- IdanDavidovich/StochBenchDataset · cited by
Models and datasets referencing this paper
- IdanDavidovich/StochBenchDataset
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.