StochBench：適用於 Lean 中隨機過程的領域特定基準測試
為何重要
這項研究對於評估 AI 的「事實驗證」與「邏輯推導」能力具有指標意義。透過引進工程與科學中常見的隨機過程與數學分析題材，StochBench 擴大了測試範疇，迫使模型從單純的競賽數學競爭中，轉向處理更具挑戰性的研究生級別應用數學，有助於追蹤模型在科學與工程領域的實際應用潛力。
現有的大型語言模型定理證明基準測試多取材於競賽數學（如 IMO 與 Putnam），難以反映具體領域的應用實況。為此，研究團隊推出 StochBench，這是一套基於 Lean 4 的基準測試，包含 450 道研究生等級的隨機過程難題，並附上對應的自然語言來源。
- 基準測試包含 450 道 Lean 4 編寫的研究生等級隨機過程問題。
- 覆蓽有限與計數馬可夫鍊、鞅、隨機微積分、布朗運動及連續時間馬可夫過程等主題。
- 基於 Claude Opus 4.8 的代理在每題 15 分鐘限制下，達到 34.9%（157/450）的證明成功率。