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.</p>\n","updatedAt":"2026-09-10T12:38:07.500Z","author":{"_id":"61deb0a302496c6d78da4ade","avatarUrl":"/avatars/1d31be74c0e6c983860d94846b4d3770.svg","fullname":"Debargha Ganguly","name":"Debargha","type":"user","isPro":false,"isHf":false,"isHfAdmin":false,"isMod":false,"followerCount":2,"isUserFollowing":false}},"numEdits":0,"identifiedLanguage":{"language":"en","probability":0.8706799149513245},"editors":["Debargha"],"editorAvatarUrls":["/avatars/1d31be74c0e6c983860d94846b4d3770.svg"],"reactions":[],"isReport":false}}],"primaryEmailConfirmed":false,"paper":{"id":"2609.09264","authors":[{"_id":"6aa2a443653f6b802b7e21ef","user":{"_id":"6a9f5f19a29092419a8eea99","avatarUrl":"/avatars/1878c59e0864189e24bbdcae136e72b4.svg","isPro":false,"fullname":"Idan Davidovich","user":"IdanDavidovich","type":"user","name":"IdanDavidovich"},"name":"Idan Davidovich","status":"claimed_verified","statusLastChangedAt":"2026-09-10T16:45:04.721Z","hidden":false},{"_id":"6aa2a443653f6b802b7e21f0","name":"Debargha Ganguly","hidden":false},{"_id":"6aa2a443653f6b802b7e21f1","name":"Vikash Singh","hidden":false},{"_id":"6aa2a443653f6b802b7e21f2","name":"Vipin Chaudhary","hidden":false}],"publishedAt":"2026-09-08T00:00:00.000Z","submittedOnDailyAt":"2026-09-10T00:00:00.000Z","title":"StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean","submittedOnDailyBy":{"_id":"61deb0a302496c6d78da4ade","avatarUrl":"/avatars/1d31be74c0e6c983860d94846b4d3770.svg","isPro":false,"fullname":"Debargha Ganguly","user":"Debargha","type":"user","name":"Debargha"},"summary":"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.","upvotes":4,"discussionId":"6aa2a443653f6b802b7e21f3","projectPage":"https://huggingface.co/datasets/IdanDavidovich/StochBench","ai_summary":"StochBench introduces 450 graduate-level stochastic processes problems in Lean 4 to benchmark formal theorem proving on domain-specific applied mathematics.","ai_keywords":["StochBench","Lean 4","formal theorem proving","stochastic processes","Markov chains","renewal processes","martingales","Brownian motion","stochastic calculus","weak convergence","Poisson processes"],"ai_summary_model":"thinkingmachines/Inkling-Small"},"canReadDatabase":false,"canManagePapers":false,"canSubmit":false,"hasHfLevelAccess":false,"upvoted":false,"upvoters":[{"_id":"61deb0a302496c6d78da4ade","avatarUrl":"/avatars/1d31be74c0e6c983860d94846b4d3770.svg","isPro":false,"fullname":"Debargha Ganguly","user":"Debargha","type":"user"},{"_id":"6a2da6c8ca070ee12c6e396c","avatarUrl":"/avatars/0355287dcabaa67dbc7f0b10b87451f9.svg","isPro":false,"fullname":"Joe Mama","user":"JoeMama123123123","type":"user"},{"_id":"6a9f5f19a29092419a8eea99","avatarUrl":"/avatars/1878c59e0864189e24bbdcae136e72b4.svg","isPro":false,"fullname":"Idan Davidovich","user":"IdanDavidovich","type":"user"},{"_id":"684d57f26e04c265777ead3f","avatarUrl":"https://cdn-avatars.huggingface.co/v1/production/uploads/no-auth/cuOj-bQqukSZreXgUJlfm.png","isPro":false,"fullname":"Joakim Lee","user":"Reinforcement4All","type":"user"}],"acceptLanguages":["en"],"dailyPaperRank":0,"markdownContentUrl":"https://huggingface.co/buckets/huggingchat/papers-content/resolve/2609/2609.09264.md","query":{}}">
StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
Abstract
StochBench introduces 450 graduate-level stochastic processes problems in Lean 4 to benchmark formal theorem proving on domain-specific applied mathematics.
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.
Community
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.
Upload images, audio, and videos by dragging in the text input, pasting, or clicking here.
Tap or paste here to upload images
Cite arxiv.org/abs/2609.09264 in a model README.md to link it from this page.
Cite arxiv.org/abs/2609.09264 in a dataset README.md to link it from this page.
Cite arxiv.org/abs/2609.09264 in a Space README.md to link it from this page.
Discussion (0)
Sign in to join the discussion. Free account, 30 seconds — email code or GitHub.
Sign in →No comments yet. Sign in and be the first to say something.