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

> STOCHBENCH, a 450-problem Lean 4 benchmark, shows proof agents solve only 34.9% of graduate stochastic processes problems, with rates varying 14-fold by topic.

- **Source:** [arXiv](https://arxiv.org/abs/2609.09264)
- **Published:** 2026-09-12
- **Permalink:** https://picx.dev/p/VFqX9d
- **Whiteboard:** https://picx.dev/p/VFqX9d/image

## Summary

## Summary

- **STOCHBENCH** is a new Lean 4 benchmark containing **450 graduate-level stochastic processes problems**, each paired with its natural-language source, spanning eight topics from Markov chains to stochastic calculus.
- The benchmark comprises **114 direct** (using Mathlib/shared definitions) and **336 abstracted** (properties taken as hypotheses) targets, addressing a field underrepresented in Mathlib.
- An **Opus 4.8-based proof agent** achieves a **34.9% clean proof rate (157/450)** under a 15-minute per-problem limit, with rates varying dramatically by topic (4.9% for renewal processes to 61.7% for martingales & stopping).
- The benchmark includes **shared mathematical definitions** for recurring concepts (matrix representations, hitting solutions, return times, etc.) and distinguishes between **marginal distributions** and **joint process laws** in problem representation.
- STOCHBENCH is released publicly with JSON records containing identifiers, informal statements, Lean targets, and representation labels, along with shared definitions and baseline proof attempts.

## Introduction and Theoretical Foundation

The paper addresses a gap in formal theorem proving benchmarks: existing benchmarks (MINIF2F, PROOFNET, PUTNAMBENCH, FORMALMATH) are dominated by competition math (IMO, Putnam) or broad textbook collections that **poorly represent field-specific applications**. The authors argue that aggregate scores across diverse problems can **obscure domain-specific strengths and failures** of automated provers.

The theoretical foundation rests on **Lean 4** and **Mathlib**, which provide an extensible proof environment with reusable mathematical abstractions. The field of stochastic processes was chosen because:
- It is **central to statistics and machine learning**
- It has **substantial but incomplete formalization** in Mathlib (e.g., Brownian motion, martingale convergence theorems, Itô integrals are formalized, but many graduate-level results are missing)
- It requires **recurring argument patterns** (first-step analysis, martingale arguments, coupling, etc.) that provide a meaningful test of proof automation

The benchmark design distinguishes between:
- **Direct targets**: use Mathlib objects or shared definitions directly
- **Abstracted targets**: take required properties as hypotheses when infrastructure is unavailable

This distinction addresses the reality that some problems require infrastructure not yet in Mathlib, while still allowing Lean to verify that conclusions follow from stated hypotheses.

## Methodology

### Problem Selection and Curation
The authors combined problems written specifically for the benchmark with exercises selected from:
- *Probability, Mathematical Statistics, and Stochastic Processes* (Siegrist, 2022)
- MIT course notes: *Introduction to Stochastic Processes* (Wu, 2015), *Advanced Stochastic Processes* (Gamarnik, 2013), *Discrete Stochastic Processes* (Gallager, 2011)

Problems were selected for **relevance to stochastic processes**; statements closer to general probability theory were excluded. All definitions, hypotheses, and questions are **human-written**, with an Opus 4.8-based formalizer assisting in expressing problems as Lean theorem statements.

### Shared Mathematical Definitions
Recurring concepts were formalized as shared abstractions:
- **Finite-state chains**: matrix representations for stochasticity, stationarity, irreducibility, aperiodicity, detailed balance, time reversal, total-variation distance
- **Hitting times**: `IsHittingSolution` and `returnTime` express first-step equations
- **Transition powers**: `nstep` defines powers through infinite sums for countable-state formulations
- **Stopping times**: `natStop` converts natural-valued stopping times to `WithTop`
- **Running maxima**: `runningMax` expresses finite running maxima
- **Conditional increments**: `IsConstDrift` states conditional increment identities

### Process Law Representations
The benchmark distinguishes two key representations:

**HasMatrixMarginals**: relates the distribution of $X_n$ to the corresponding row of $P^n$.

**HasChainLaw**: specifies finite-dimensional probabilities through:

$$
\mathbb{P}_\mu(X_0 = x_0, \ldots, X_n = x_n) = \nu(x_0) \prod_{i=0}^{n-1} P(x_i, x_{i+1})
$$

### Formalization Scope
- **Direct targets** use Mathlib objects or shared definitions
- **Abstracted targets** take required properties as hypotheses (e.g., memorylessness assumed rather than derived from continuous-time chain dynamics)

### Evaluation Setup
A multi-turn tool-using **Opus 4.8-based agent** using lean4skills and the Lean LSP MCP server was evaluated with:
- One run per target, capped at **15 minutes**
- Allowed: Lean-error inspection, library/shared-definition search, loogle and leansearch queries, proof revisions
- A proof is **clean** if Lean accepts it without `sorry`, `sorryAx`, or additional admitted facts

## Empirical Validation / Results

### Overall Performance

| Topic | Direct | Abstracted | Items | Clean Proofs (Direct) | Clean Proofs (Abstracted) | Total | Rate (%) |
|---|---|---|---|---|---|---|---|
| Poisson processes | 5 | 35 | 40 | 0 | 7 | 7 | 17.5 |
| Markov chains (finite & countable) | 23 | 73 | 96 | 15 | 22 | 37 | 38.5 |
| Renewal processes | 0 | 41 | 41 | 0 | 2 | 2 | 4.9 |
| Continuous-time Markov & queues | 1 | 54 | 55 | 1 | 22 | 23 | 41.8 |
| Random walks & large deviations | 9 | 53 | 62 | 6 | 10 | 16 | 25.8 |
| Martingales & stopping | 67 | 27 | 94 | 51 | 7 | 58 | 61.7 |
| Brownian motion & stochastic calculus | 0 | 45 | 45 | 0 | 8 | 8 | 17.8 |
| Weak convergence & functional limits | 9 | 8 | 17 | 6 | 0 | 6 | 35.3 |
| **All** | **114** | **336** | **450** | **79** | **78** | **157** | **34.9** |

**Clean-proof rates by target class**: Direct targets: **69.3%**, Abstracted targets: **23.2%**.

### Key Findings
1. **Direct targets are dramatically easier** (69.3% vs. 23.2% clean proof rate), though the authors note this comparison is descriptive, not a controlled causal effect—abstraction effects are confounded with problem difficulty and library support.
2. **Martingales & stopping** achieved the highest rate (61.7%), likely due to strong Mathlib support for martingale theory.
3. **Renewal processes** were the hardest (4.9%), reflecting poor library infrastructure.
4. **Brownian motion & stochastic calculus** also proved difficult (17.8%), despite existing formalizations, suggesting interface complexity.

### Qualitative Failure Analysis
The authors identified three categories of proof-search failures:
- **Plausible targets** where the agent failed to find proofs
- **Missing lemmas or difficult library interfaces**
- **Formalization defects**: missing measurability, integrability, or non-emptiness assumptions

## Theoretical and Practical Implications

### For Formal Proof Automation
- STOCHBENCH reveals that **domain-specific evaluation** uncovers performance patterns invisible in aggregate benchmarks—the 14× spread in proof rates across topics (4.9% to 61.7%) demonstrates this clearly.
- The large gap between direct and abstracted targets suggests that **library infrastructure quality is a primary bottleneck** for automated proving, not just reasoning ability.
- The benchmark provides **supervision data** (successfully checked baseline proofs) for training proof-generation models and autoformalization systems.

### For Mathlib Development
- The benchmark identifies **specific infrastructure gaps** in Mathlib for stochastic processes: renewal theory, continuous-time Markov chains, queueing theory, and stochastic calculus interfaces are underrepresented.
- The shared definitions (e.g., `IsHittingSolution`, `HasChainLaw`) represent reusable abstractions that could be integrated into Mathlib.

### For Benchmark Design
- The **direct/abstracted distinction** offers a principled way to benchmark problems whose infrastructure is incomplete, without excluding them entirely.
- The **informal–formal pairing** supports autoformalization research, addressing the semantic alignment problem highlighted by prior work (FORMALALIGN, MATHATLAS).

## Conclusion

STOCHBENCH provides a **focused testbed for evaluating proof agents on graduate stochastic processes**, a mathematically rich and practically important domain previously underrepresented in formal theorem-proving benchmarks. With 450 Lean 4 targets across eight topics at varying abstraction levels, it better represents domain-specific applied mathematics while remaining challenging: the best baseline achieves only 34.9% overall proof rate.

The authors acknowledge **limitations**: human curation introduces bias, faithfulness review could benefit from peer scrutiny, and the topic/abstraction classifications lack rigorous formal definitions. The direct/abstracted performance comparison is descriptive rather than causal.

**Future directions** implied by this work include:
- Developing stronger domain-specific provers trained on the released supervision data
- Using the informal–formal pairs for autoformalization training
- Continuing the formalization of stochastic processes in Lean, guided by the identified infrastructure gaps
- Expanding peer review of the benchmark's faithfulness to source problems

The benchmark is publicly available at https://huggingface.co/datasets/IdanDavidovich/StochBench.

---

_Markdown view of https://picx.dev/p/VFqX9d, served by PicX — AI-generated visual whiteboard summaries of research papers._