StochBench：精益随机过程的特定领域基准

使用 大语言模型 证明形式定理的主要基准是来自竞赛数学的小型集合，例如 IMO 和 Putnam，它们很难代表特定领域的应用。我们引入了 StochBench，这是一个 Lean 4 基准测试，包含 450 个不同抽象级别的研究生随机过程问题，每个问题都与其自然语言源配对。它针对 Mathlib 中代表性不足的领域，涵盖有限和可数马尔可夫链、更新过程、随机游走、鞅、停止时间、队列、布朗运动、随机微积分、弱收敛以及泊松和连续时间马尔可夫过程。我们基于 Opus 4.8 的代理在每个问题 15 分钟的限制下实现了 34.9% 的证明率 (157/450)。 StochBench 更好地代表了特定领域的应用数学，同时对高级证明者仍然具有挑战性。