כתבה
arXiv cs.CL ·
StochBench: בנק איכותי לתהליכים סטוכסטיים בLean
StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
נחשף בנק איכותי חדש לתהליכים סטוכסטיים, המכיל 450 בעיות בLean 4. הבנק, הקרוי StochBench, כולל תהליכים סטוכסטיים שונים, כגון רצפי מרקוב, תהליכי תחזוקה, וכד'
תקציר מקורי באנגליתarXiv:2609.09264v1 Announce Type: new 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 b
קרא במקור המקורי
arxiv.org
פתח כתבה מקורית