StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
Idan Davidovich, Debargha Ganguly, Vikash Singh, Vipin Chaudhary
cs.CL · cs.LO
Quick verdict
StochBench: 450 Lean 4 graduate stochastic-process targets, 34.9% for an Opus 4.8 agent — valuable, though faithfulness and baseline rest on single-run self-review.
Summary
StochBench is a Lean 4 benchmark of 450 graduate-level stochastic-processes problems, each paired with its natural-language source, spanning eight topics from Markov chains and martingales to Brownian motion, stochastic calculus, and weak convergence. Targets are 114 direct statements that may use Mathlib or shared bespoke definitions, and 336 abstracted targets (74.7%) that state missing stochastic-process infrastructure as explicit hypotheses. All definitions and hypotheses are human-written; Claude Opus 4.8 assisted statement formalization until elaboration in Lean 4.30.0 with a fixed Mathlib. Evaluation used one multi-turn tool-using Opus 4.8 agent (lean4skills plus a Lean LSP MCP server) with a single 15-minute run per target, yielding 157 clean proofs (34.9%). Results vary sharply by topic: renewal processes are hardest (4.9%; 2/41) and martingales and stopping easiest (61.7%; 58/94); direct targets reach 69.3% versus 23.2% abstracted, although the paper labels this comparison descriptive. Authors cite proof-search failures, missing lemmas or library interfaces, and some formalization defects. The main weaknesses: faithfulness of formalization is self-reviewed without per-target audit, and all evaluation rests on one agent in one run, so variance and cross-model generalization remain unmeasured.
Review complete
Assessment at a glance
5
risk flags identified
● high 1
● medium 3
● low 1
4 strengths · 4 weaknesses · 5 author questions
AI text signal = Binoculars zero-shot detector score over 20 sampled passages (Fast-DetectGPT co-reported) — absence does not prove human authorship, and a flag does not imply misconduct.
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- StochBench is the first domain-focused Lean 4 benchmark dedicated to graduate stochastic processes, with 450 human-written targets paired with informal sources across eight topics.
- A multi-turn Opus 4.8-based tool-using agent solves 157 of 450 targets (34.9%) under a 15-minute per-problem cap, establishing a baseline that remains challenging.
- Abstracted targets (336 of 450) enable coverage of stochastic-process areas where Mathlib infrastructure is missing, while Lean kernel-checking guarantees every accepted proof follows from the stated hypotheses.
- Success rates differ sharply by representation: direct targets reach 69.3% clean-proof rate versus 23.2% for abstracted ones (descriptively), and by topic from 4.9% (renewal) to 61.7% (martingales and stopping).
Strengths
Genuine domain gap addressed
Section 2 documents that existing Lean benchmarks (miniF2F, ProofNet, PutnamBench, FormalProofBench) target competition or general curricular mathematics; a graduate stochastic-processes benchmark fills a real coverage hole, and Section 3 cites concrete Mathlib infrastructure that does not yet exist (Brownian-motion machinery, Ito-calculus tooling).
Honest scope and difficulty annotation
The direct/abstracted split (Table 1a: 114 vs 336) with per-topic breakdowns, and the explicit disclaimer that the class comparison (Table 1c: 69.3% vs 23.2%) is 'descriptive, not a controlled causal effect', is more careful reporting than most benchmark papers offer.
Transparent baseline protocol
Strong released artifacts
Weaknesses
No uncertainty quantification anywhere
Faithfulness is self-asserted, not audited
Potential construction-evaluation circularity
Single-model, single-run evaluation design
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
Report preview
Scope & Claims
StochBench (arXiv:2609.09264) is a Lean 4 benchmark of 450 graduate-level stochastic-processes theorem targets, each paired with its natural-language source, spanning eight topics from Markov chains (96 items) to weak convergence (17). The claims are two: the resource fills a documented domain gap in formal theorem-proving evaluation (Section 2 traces miniF2F, ProofNet, PutnamBench, FormalProofBench, FormalML, TaoBench — none dedicated to stochastic processes), and it is hard: a single-agent baseline solves 157/450 (34.9%) under a 15-minute cap. Targets split into 114 direct statements (Mathlib or shared bespoke definitions usable) and 336 abstracted ones (74.7%) where missing stochastic-process infrastructure is stated as explicit hypotheses. The paper is careful to claim a baseline, not a leaderboard: Section 4 states plainly this is 'a single-agent, single-budget baseline, not a model comparison or repeated-run evaluation.'
The remaining sections cover Methodology Assessment, Statistical Evidence, Results & Reproducibility, Limitations & Risks, and Verdict & Recommendations.
- All 4 strengths & 4 weaknesses, analyzed in detail
- 5 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is StochBench?
StochBench is a benchmark of 450 graduate-level stochastic-processes problems formalized in the Lean 4 theorem prover, each paired with its natural-language source statement. It spans eight topics (Markov chains, renewal processes, continuous-time Markov chains and queues, random walks, martingales and stopping times, Brownian motion and stochastic calculus, weak convergence, Poisson processes). Targets come in two flavors: 114 'direct' statements that may use Mathlib or shared definitions, and 336 'abstracted' statements that state the missing stochastic-process infrastructure as explicit hypotheses. The dataset is released on Hugging Face.
How well do AI models perform on StochBench?
The paper's single baseline is a Claude Opus 4.8-based agent using lean4skills and a Lean LSP MCP server, given one 15-minute run per problem. It produced 157 verified clean proofs out of 450 (34.9%). Difficulty varies sharply by topic: renewal processes were hardest (4.9% solved, 2/41) and martingales and stopping times easiest (61.7%, 58/94). Direct targets were solved far more often (69.3%) than abstracted targets (23.2%), though the authors note this comparison is descriptive rather than a controlled effect.
What are the main limitations of StochBench?
Per the paper itself: faithfulness of the formalization to the source problems was self-reviewed by the authors, not independently audited; curation and topic/representation labels involve human-curatorial bias; and the evaluation is a single agent with a single 15-minute run per problem, so there is no variance estimate and no cross-model comparison. The authors also report finding some formalization defects (e.g., missing measurability or integrability assumptions) during qualitative inspection.
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- PDF extraction strips Σ symbols in the appendix Lean code (summations render as blanks), but all prose, Table 1 numbers, and reference details are intact; judgments here rely on prose and tables, not Lean syntax.
- The paper references a Hugging Face dataset release but the text does not explicitly state whether the agent harness (prompts, tool budgets, scripts) is included; repro-readiness is judged accordingly.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.