StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
StochBench introduces 450 graduate-level stochastic-processes problems in Lean 4; an Opus 4.8-based agent proved 34.9% under a 15-minute limit.
StochBench is a Lean 4 benchmark of 450 graduate stochastic-processes problems, each paired with its natural-language source, covering Markov chains, renewal processes, martingales, Brownian motion, stochastic calculus, weak convergence, and Poisson and continuous-time Markov processes. The benchmark addresses field-specific applied mathematics underrepresented in Mathlib, unlike competition-math-dominated suites such as IMO and Putnam collections. An Opus 4.8-based agent achieved a 34.9% proof rate (157/450) under a 15-minute per-problem limit, showing the benchmark remains challenging for advanced provers.
- 450 graduate stochastic-processes problems formalized in Lean 4
- Covers martingales, Brownian motion, stochastic calculus, queues, and more
- Opus 4.8-based agent proved 34.9% of problems at 15 minutes each
- Addresses domain-specific gaps left by competition-math benchmarks
Full article110 words · extracted from huggingface.co · click to collapse
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.
Text extracted automatically; images, tables and formatting may be missing. Original: https://huggingface.co/papers/2609.09264