Source-linked AI summary
StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
Idan Davidovich, Debargha Ganguly, Vikash Singh, Vipin Chaudhary
TL;DR
Existing formal theorem-proving benchmarks provide limited domain-specific coverage for stochastic processes. STOCHBENCH introduces 450 Lean 4 stochastic-process targets with varying formalization scope and evaluates an Opus 4.8-based agent, which produces 157 clean proofs under a 15-minute limit.
Problem
Existing competition and broad textbook benchmarks can obscure domain-specific strengths and failures, while stochastic processes remain underrepresented in the benchmark scope addressed here.
Method
STOCHBENCH combines human-written stochastic-process statements, shared mathematical definitions, and direct or abstracted Lean targets, then evaluates a tool-using Opus 4.8-based agent.
Results
157 clean proofs were produced out of 450 targets under the 15-minute-per-problem evaluation protocol.
Takeaways & Limitations
STOCHBENCH provides a focused testbed for evaluating proof agents on graduate stochastic processes and resources for autoformalization training and proof generation.
Takeaways & Limitations
The benchmark’s curation, faithfulness review, and topic and representation classifications are decided by human curators and may introduce bias, while the evaluation is a single-agent, single-budget baseline.
Abstract
from arXiv · showhide
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.
1 Introduction
STOCHBENCH addresses the limits of broad formal-mathematics benchmarks by introducing a domain-focused Lean 4 benchmark for graduate stochastic processes. It contains 450 theorem targets built through mathematician-led curation, LLM-assisted formalization, and shared definitions.
- Competition and broad textbook benchmarks can obscure domain-specific strengths and failures through aggregate scores.
- STOCHBENCH provides a Lean 4 benchmark focused on graduate stochastic processes, a field central to statistics and machine learning.
- The benchmark releases 450 theorem targets paired with informal statements, shared definitions, and baseline proof attempts.
- Its construction combines mathematician-led curation, LLM-assisted formalization, and shared definitions across eight topics.
2 Related Work
Prior Lean benchmarks span competition difficulty, curricular coverage, and research context, while related infrastructure supports automated reasoning and formal stochastic mathematics. STOCHBENCH builds on these developments with domain-specific stochastic-process evaluation.
- MINIF2F, PROOFNET, PUTNAMBENCH, and FORMALMATH broaden Lean evaluation across competition difficulty, curricular coverage, scale, and disciplinary coverage.
- Lean 4 and Mathlib provide extensible proof environments and reusable abstractions for automated mathematical reasoning.
- Proof systems such as LeanDojo, Lean Copilot, Lean-Star, and DeepSeek-Prover combine interaction, retrieval, tactic suggestion, or proof search.
- Existing formalizations cover martingale convergence, trajectory-space probability measures, Markov kernels, Brownian motion, and stochastic integration.
3 The STOCHBENCH Benchmark
STOCHBENCH contains 450 curated stochastic-process theorem targets sourced from textbooks, course materials, and benchmark-written problems. Human-written statements are formalized with shared abstractions and explicitly labeled direct or abstracted scope.
- Sources and selection: The corpus contains 450 stochastic-process targets selected from benchmark problems, textbooks, exercises, lemmas, theorems, and course materials.
- Sources and selection: The corpus covers eight topics and excludes claims closer to general probability theory, such as the triangle inequality for total variation distance.
- Statement construction: All benchmark-specific definitions, hypotheses, and questions are human-written, while an Opus 4.8-based formalizer assisted with Lean theorem statements.
- Shared mathematical definitions: Shared definitions encode recurring concepts including finite-state chain properties, first-step equations, stopping-time conversion, running maxima, and conditional drift.
- Marginals and joint process laws: The benchmark distinguishes one-time marginals from joint process laws to specify which process information is available to the prover.
- Formalization scope: Direct targets use Mathlib objects or shared definitions, whereas abstracted targets take required properties as hypotheses.
- Path properties and convergence: Path and convergence targets state requirements explicitly, including Gaussian increments, independence, path continuity, mean-square convergence, and convergence of bounded continuous expectations.
- Human review and release: The release includes theorem records, shared definitions, and baseline proof attempts, but not complete proofs for all targets.
4 Evaluation
The evaluation uses a single Opus 4.8-based tool-using agent with one 15-minute run per target. It produced 157 clean proofs out of 450, while failures included proof-search, library, and formalization issues.
- The Opus 4.8-based agent received one tool-using run per target capped at 15 minutes.
- The baseline is a single-agent, single-budget evaluation rather than a model comparison or repeated-run study.
- 157 clean proofs were produced out of 450 targets.Clean proofs were accepted by Lean without sorry, sorryAx, or additional admitted facts.
- Observed failures involved proof search, missing lemmas or difficult library interfaces, and formalization defects such as missing measurability or integrability assumptions.
5 Limitations and Conclusion
STOCHBENCH offers a focused testbed for graduate stochastic-process proof agents, but human decisions about curation, faithfulness, and classifications introduce bias.
- Human curators decide question curation, faithfulness review, and topic and direct/abstracted classifications, introducing some bias.
- The corresponding terminologies were not rigorously defined within the scope of this work.
- The benchmark’s informal–formal pairs can support autoformalization training, while checked baseline proofs can supervise proof generation.
- Shared definitions and benchmark resources support developing domain-specific provers and continuing stochastic-process formalization in Lean.
A.1 An abstracted proof example - SOTA Prover
The Q361 example shows an abstracted proof that builds reusable finite-state Markov-chain lemmas before composing them into a global hitting-time bound.
- The agent-generated proof was obtained in a separate run lasting more than 30 minutes, outside the 15-minute baseline protocol.
- The target supplies first-step equations through IsHittingSolution rather than constructing hitting-time random variables.
- The generated Q361 proof develops nine auxiliary theorems across multiple abstraction levels for a single inequality.
- The proof establishes nonnegativity, positive-reachability closure, and a maximum-principle propagation lemma for finite-state transition matrices.
- A return-time identity yields harmonicity of Kemeny’s function, whose constancy follows from irreducibility and the maximum principle.
- The same propagation lemmas establish a hitting-time triangle inequality, and stationary averaging combines these results into a pointwise bound.
- The example tests hierarchical proof search by requiring reusable intermediate statements and coordinated auxiliary-theorem dependencies beyond local tactic selection.
A.2 A direct proof example - Opus Prover
The Q222 direct proof constructs a positive stationary distribution by averaging transition iterates, extracting a compactness-based subsequential limit, and using irreducibility for strict positivity.
- The direct proof was obtained in a separate run lasting less than 15 minutes.
- The Q222 target asks for a stationary probability measure π with strictly positive mass on every state of an irreducible finite chain.
- The proof represents the chain with a real transition matrix whose stochasticity and irreducibility encode nonnegative entries, unit row sums, and positive-power reachability.
- Transition iterates and their Cesàro averages remain in the standard simplex.
- A telescoping identity shows that applying the transition map to a Cesàro average differs from it by a term tending to zero.
- Compactness supplies a convergent subsequence of the averages, and the vanishing difference identifies its limit as stationary.
- Irreducibility and stationarity under matrix powers then show that every coordinate of the stationary distribution is strictly positive.
A.3 An abstracted proof example - Opus Prover
The Q128 abstracted proof derives martingale identities for drifted Brownian motion from supplied increment laws and independence assumptions, using conditional-expectation algebra and integrability conditions.
- The example’s agent-generated proof was obtained in a separate run lasting less than 15 minutes.
- Q128 asks to show that removing drift from Brownian motion yields a martingale and that its variance-corrected square is also a martingale.
- The Lean statement models a real-valued process on a probability space with filtration, adaptedness, and first- and second-moment integrability assumptions.
- For 0 ≤ s ≤ t, the abstraction supplies Gaussian increments with law N(0,t−s) and independence from the earlier filtration.
- The proof derives the conditional-expectation identity for the drift-removed process from the zero conditional increment mean.
- The squared-process identity additionally uses the conditional second moment and integrability of the cross term before deterministic scaling and subtraction.