OpenFrontiers 用 Lean 4 形式化基准衡量 LLM 的科学再发现能力。
资讯摘要
论文提出 OpenFrontiers，一个跨学科资源，包含记录 12,151 个开放研究问题陈述、背景与进展的语料库，以及数学领域近期已解决问题的回顾性基准。基准含 200 道题（110 道 2026 年已解决、90 道仍开放），每题附经自动探针与两次独立评审校验的 Lean 4 陈述，并从中筛出 HQ-50 子集。评测在隔离沙箱中用两个独立检查器评分，设闭卷、冻结检索与实时联网三种条件；作者报告七个 LLM 智能体在标准化预算下闭卷再发现很少，最多 40 道中解出 7 道，联网成功多来自检索已发表解法。
要点速读
- 语料库收录 12,151 个开放研究问题的陈述、背景与进展信息。
- 基准含 200 道数学题，110 道 2026 年已解决、90 道仍开放，均配 Lean 4 陈述并经自动探针和两次独立评审。
- 作者报告七个 LLM 智能体在 HQ-50 上闭卷最多解出 40 道中的 7 道，联网成功多源于检索已发表解法。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/31 08:00:18（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。