热点事件持续更新
研究团队推出形式化数学基准ReuF2F
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
2026年10月，研究人员推出了形式化数学评测基准 ReuF2F，旨在评估代码智能体的端到端解题能力。该基准包含源自本科科研项目的 244 个 Lean 4 形式化开放问题。评测将问题及其逻辑否定置于 Docker 容器内的 Lean 项目中，并基于 mini-SWE-agent 构建了统一评估框架 Leanimum-agent。测试结果显示，当前表现最佳的模型仅能解决其中约 40% 的问题。
AI 根据报道生成 · 1 小时前更新
最新进展10月21日 12:00
研究团队推出包含244个Lean 4问题的基准ReuF2F，最佳模型仅解决约40%。报道时间线
沿着报道，了解事件的不同侧面。
10月21日
- arXiv 人工智能ReuF2F：在形式化本科科研问题上评测代码智能体
研究人员推出形式化数学评测基准 ReuF2F，包含源自本科科研项目的 244 个 Lean 4 形式化开放问题，用于评估代码智能体的端到端解题能力。评测将问题及其逻辑否定置于 Docker 容器内的 Lean 项目中，并基于 mini-SWE-agent 构建了统一评估框架 Leanimum-agent。测试显示当前表现最佳的模型仅解决约 40% 的问题。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。