热点事件持续更新
VeriSoftBench：仓库级 Lean 4 验证基准发布
1 篇报道1 个报道来源3 小时前更新
先了解这件事
AI 综述
2026 年 10 月，研究者在 COLM 会议上发布 VeriSoftBench，这是首个面向仓库规模 Lean 4 形式化验证的基准。该基准包含来自 23 个开源形式化方法仓库的 500 条证明义务，并保留真实仓库上下文与跨文件依赖，而非孤立的单文件题目。评测提供 Curated deps 与 Full repo context 两种模式，用以区分精选依赖与完整仓库上下文下的表现。结果显示前沿大模型成绩仍不理想，最佳成绩分别为 41.0% 与 34.8%，说明仓库级形式化验证对当前 LLM 仍是难题。
AI 根据报道生成 · 3 小时前更新
最新进展10月8日 00:11
VeriSoftBench 发布，含 23 个仓库的 500 条证明义务，最强 LLM 仅过 41.0%。报道时间线
沿着报道，了解事件的不同侧面。
10月8日
- AGI HuntVeriSoftBench 发布：仓库级 Lean 4 形式化验证，最强 LLM 仅过 41%
研究者在 COLM 会议上发布 VeriSoftBench，这是首个面向仓库规模 Lean 4 形式化验证的 benchmark，包含来自 23 个开源形式化方法仓库的 500 条证明义务，并保留真实仓库上下文与跨文件依赖。该基准提供 Curated deps 与 Full repo context 两种评测模式，前沿 LLM 表现仍不理想，最佳成绩仅为 41.0% 与 34.8%。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。