大模型证明随机过程仅34.9%！450道Lean 4研究生题新基准发布
StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean
📖 AI 总结
本文提出 StochBench，一个面向随机过程领域的 Lean 4 形式化定理证明基准。现有主流基准多取自 IMO、Putnam 等竞赛数学题目，规模小且难以反映特定学科的实际应用。StochBench 包含 450 道研究生水平的随机过程问题，每题均配有自然语言原文，覆盖有限与可数马尔可夫链、更新过程、随机游走、鞅、停时、排队论、布朗运动、随机微积分、弱收敛以及泊松过程与连续时间马尔可夫过程等主题，填补了 Mathlib 中该领域内容不足的空白。作者基于 Opus 4.8 构建的智能体在每题 15 分钟限制下达到 34.9% 的证明率（157/450）。该基准更好地代表了领域特定的应用数学，同时对先进证明系统仍具挑战性。
🔑 关键词速览
| Lean 4 | 一种交互式定理证明器与编程语言，用于形式化数学证明和验证。 |
| 随机过程 | 研究随时间演变的随机现象的概率论分支，如马尔可夫链、布朗运动等。 |
| Mathlib | Lean 的数学库，包含大量已形式化的数学定义、定理和证明。 |
| 形式化定理证明 | 使用计算机程序严格验证数学定理证明正确性的过程。 |
| 鞅 | 一种随机过程，其未来期望值等于当前值，常用于建模公平赌博。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅