StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
StochBench puts 450 graduate stochastic-processes problems into Lean 4, with natural-language sources attached.
The benchmark is aimed at formal theorem proving systems that are not well tested by competition-math datasets. It covers Markov chains, renewal processes, martingales, queues, Brownian motion, stochastic calculus, weak convergence, and related stochastic topics. The authors say an Opus 4.8-based agent proved 157 of 450 problems, a 34.9% rate, with 15 minutes allowed per problem. HF Daily Papers' note
The benchmark is aimed at formal theorem proving systems that are not well tested by competition-math datasets. It covers Markov chains, renewal processes, martingales, queues, Brownian motion, stochastic calculus, weak convergence, and related stochastic topics. The authors say an Opus 4.8-based agent proved 157 of 450 problems, a 34.9% rate, with 15 minutes allowed per problem. HF Daily Papers' note
score 5