StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean

AI summary

Overview

Research area: Formal theorem proving with large language models; autoformalization and proof automation in Lean 4, applied to graduate-level probability and stochastic processes.

Technical level: Advanced. The paper assumes familiarity with Lean 4, Mathlib, tactic-based proof scripts, and graduate stochastic-processes material.

Scope: The authors introduce and evaluate StochBench, a Lean 4 benchmark of 450 graduate stochastic-processes theorem targets paired with natural-language statements, and report a baseline proof rate of 34.9% (157/450) for a tool-using Opus 4.8-based agent under a 15-minute per-problem limit.

What This Paper Is About

Leading benchmarks for formal theorem proving with large language models are small collections drawn from competition mathematics, such as the IMO and Putnam, which the authors argue poorly represent field-specific applications. The paper's goal is to build a domain-focused alternative: a Lean 4 benchmark of 450 graduate stochastic-processes problems, each paired with its natural-language source statement, covering a field the authors describe as underrepresented in Mathlib. The benchmark is accompanied by shared mathematical definitions, a size- and scope-aware baseline evaluation, and baseline proof attempts.

Key Contributions

1. A domain-focused benchmark. The authors release 450 Lean 4 theorem targets paired with informal statements, alongside shared definitions and baseline proof attempts. The corpus spans eight topics and comprises 114 direct and 336 abstracted statements.

2. A scope-aware baseline evaluation. They annotate formalization scope (direct versus abstracted) and evaluate a compiler-guided proof agent under a 15-minute per-problem cap (recorded proving time of at most 900 seconds), reporting results by topic and by representation.

3. Shared mathematical abstractions. They build reusable definitions for recurring stochastic-process concepts, including finite-state chain properties (stochasticity, stationarity, irreducibility, aperiodicity, eventual positivity of transition powers, detailed balance, time reversal, total-variation distance), first-step-equation and return-time notions via IsHittingSolution and returnTime, transition powers via nstep, plus natStop, runningMax, and IsConstDrift.

4. Distinguishing marginal from joint process laws. They separate HasMatrixMarginals (relating the distribution of time-(n) state to row (n) of a matrix power) from HasChainLaw (finite-dimensional joint probabilities specified through an initial law and products of transition probabilities), so each target states explicitly which information about the process is available to the prover.

Main Findings

• Overall baseline proof rate. The Opus 4.8-based agent produced 157 clean proofs out of 450 targets, a 34.9% proof rate under a 15-minute per-problem limit. A proof counts as clean if Lean accepts it without sorry, sorryAx, or additional admitted facts, checked by Lean comparator.

• Direct targets are proved far more often than abstracted ones. Clean-proof rates by target class are 69.3% for direct targets (79 clean proofs from 114 items) and 23.2% for abstracted targets (78 clean proofs from 336 items). The paper labels this comparison descriptive, not a controlled causal effect.

• Large variation across the eight topics. Reported topic rates using all items in the topic: martingales and stopping 61.7% (58/94), continuous-time Markov and queues 41.8% (23/55), Markov chains (finite and countable) 38.5% (37/96), weak convergence and functional limits 35.3% (6/17), random walks and large deviations 25.8% (16/62), Brownian motion and stochastic calculus 17.8% (8/45), Poisson processes 17.5% (7/40), and renewal processes 4.9% (2/41).

• Topics with no direct targets. Poisson processes (5 direct, 35 abstracted), renewal processes (0 direct, 41 abstracted), and Brownian motion and stochastic calculus (0 direct, 45 abstracted). Only 1 item out of 55 in the continuous-time Markov and queues topic is direct.

• Direct successes cluster in two topics. Martingales and stopping supplies 51 of the 79 clean direct proofs; Markov chains supplies 15, random walks and large deviations 6, weak convergence and functional limits 6, and continuous-time Markov and queues 1.

• Qualitative failure causes. Inspection found proof-search failures on plausible targets, missing lemmas or difficult library interfaces, and a smaller group of formalization defects, including missing measurability, integrability, or non-emptiness assumptions.

• A worked abstracted example exceeds the baseline budget. Target Q361, asking for a hitting-time bound, was proved in a separate run lasting more than 30 minutes, outside the 15-minute baseline protocol. The generated proof develops nine auxiliary theorems, including nonnegativity of matrix powers and hitting-time solutions, forward-closure reachability, a maximum-principle propagation lemma, a return-time identity, harmonicity and constancy of Kemeny's function, and a hitting-time triangle inequality.

• Scope labels are recorded per target. The JSON records the direct/abstracted distinction as literal and abstract, respectively. Each JSON record contains an identifier, a problem name, an informal statement, a Lean target, and a representation label.

Methodology in Plain English

The authors assembled 450 graduate stochastic-processes theorem targets by combining problems written specifically for the benchmark with exercises, lemmas, theorems, and corollaries selected from Probability, Mathematical Statistics, and Stochastic Processes (Siegrist, 2022) and from MIT course notes and assignments for Introduction to Stochastic Processes (Wu, 2015), Advanced Stochastic Processes (Gamarnik, 2013), and Discrete Stochastic Processes (Gallager, 2011). Problems closer to general probability theory, such as the triangle inequality for total variation distance, were excluded.

All benchmark-specific definitions, hypotheses, and questions were human-written. An Opus 4.8-based formalizer assisted with expressing the problems as Lean theorem statements, and candidate statements were revised using Lean feedback until they elaborated in Lean 4.30.0 with a fixed Mathlib version. Because some problems require infrastructure unavailable in Mathlib, the authors split targets into direct targets, which use Mathlib objects or shared definitions, and abstracted targets, which take the required properties as hypotheses. Lean verifies that each proved conclusion follows from its stated hypotheses; human review assesses whether the definitions and hypotheses faithfully represent the source problem. The authors state the definitions and hypotheses would benefit from further peer review.

For evaluation, they ran a multi-turn tool-using Opus 4.8-based agent using lean4skills and the Lean LSP MCP server. Each target received one run capped at 15 minutes, allowing Lean-error inspection, library and shared-definition search, loogle and leansearch queries, and proof revisions. The same model family assisted with statement construction.

Why This Matters

Impact on research. StochBench shifts evaluation of formal provers from competition-style breadth toward within-domain depth. It targets a discipline the authors describe as underrepresented in Mathlib, and it separates two things that aggregate benchmark scores typically conflate: whether a theorem is provable with available library infrastructure (direct) and whether it is provable once the required properties are supplied as hypotheses (abstracted). The direct-versus-abstracted gap of 69.3% versus 23.2% is presented as a diagnostic for library coverage and abstraction effects rather than as a controlled measurement. The newly constructed informal–formal pairs can support autoformalization training, and the checked baseline proofs can provide supervision for proof generation.

Real-world applications. The paper does not report deployed applications or industry case studies; the relevance below follows from the mathematical content the benchmark covers.

• Queueing systems: the continuous-time Markov and queues topic covers queue models used in service, network, and operations settings.
• Sequential decision-making and statistics: the Markov-chain, martingale, and stopping-time material underlies models in statistics and machine learning, which the authors identify as fields where stochastic processes are central.
• Financial and probabilistic modeling: Brownian motion, stochastic calculus, and martingales are the standard mathematical vocabulary for continuous-time random models.
• Engineering and reliability analysis: renewal processes are covered as a benchmark topic, though it is the weakest-performing topic at a 4.9% proof rate.

Industry relevance. The paper does not report industry deployments or cost figures. Its practical relevance is as infrastructure: a curated set of machine-checkable targets, shared definitions, and baseline proofs that teams building proof agents or autoformalization pipelines can use to measure progress on applied probability mathematics. Because every proof is kernel-checked, results are mechanically verifiable rather than dependent on informal grading.

Future Directions

• Peer review of definitions and hypotheses. The authors state that their human-written definitions and hypotheses were reviewed against the source problems but would benefit from further peer review, and they note that if a formalization error has crept in, they nonetheless accept a kernel-checked proof of the theorem being incorrect.

• Closing the abstraction gap. The gap between direct (69.3%) and abstracted (23.2%) clean-proof rates raises the question of how much comes from abstraction itself and how much from differences in problems or library support, which the paper explicitly says its descriptive comparison does not separate.

• Extending Mathlib infrastructure for stochastic processes. The weakest topics (renewal processes at 4.9%, Poisson processes at 17.5%, Brownian motion and stochastic calculus at 17.8%) correspond to areas where the paper reports missing lemmas, difficult library interfaces, and a reliance on abstracted rather than direct targets.

• Moving beyond a single-agent, single-budget baseline. The evaluation is one run per target with one agent and one 15-minute cap; the paper describes it as not a model comparison and not a repeated-run evaluation, leaving room for multi-model, multi-budget, and repeated-run studies. The Q361 example, proved in over 30 minutes outside the protocol, indicates that budget is a live variable.

• Reducing curator bias. The authors note that question curation, faithfulness review, and the topic and direct/abstracted classifications are decided by human curators and that the corresponding terminologies were not rigorously defined within the scope of the work.

Target Audience

Researchers and engineers working on formal theorem proving, autoformalization, and Lean 4 proof agents, especially those focused on applied mathematics rather than competition problems. It is also relevant to mathematicians and probabilists interested in the state of stochastic-process formalization in Mathlib, and to machine-learning researchers studying domain-specific evaluation benchmarks and semantic faithfulness between informal and formal statements. Readers without Lean 4 and graduate probability background will find the technical content, including the appendix proof of Q361, difficult to follow.

Authors’ 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.