OpenFrontiers：用形式化证明检验AI能否真正重发现科学问题

导语

大语言模型正在从“回答问题”走向“参与研究”，但研究级能力一直缺少足够严格、可复现的测试。OpenFrontiers试图补上这一缺口：它不只收集开放问题，还把其中一部分转化为能够由Lean 4检查的数学任务，用统一协议检验模型是否真的找到了证明。

一个连接“问题库”和“评测集”的资源

OpenFrontiers由两部分组成。第一部分是跨学科开放研究问题语料库，记录了12151个问题及其问题陈述、背景、已有进展等信息。第二部分是数学领域的回顾性基准，共200道题，其中110道在数据设定中已经解决，90道仍处于开放状态。每道题都配有Lean 4形式化陈述，并经过自动化探针检查和两名独立评审。

研究者还从中筛选出HQ-50子集，进一步强调问题质量。这样的设计带来一个重要好处：模型面对的不只是“看起来像研究问题”的文本，而是有明确形式化目标、能够被程序验证的任务。

评测重点：证明是否成立，而不是模型是否自信

评测协议在隔离沙箱中运行，并使用两个独立检查器对形式化证明进行验证。实验比较了三种信息条件：

• 闭卷条件：模型不能查询外部资料，主要考察自身推理与知识能力；
• 冻结检索条件：模型只能使用预先限定的信息，减少动态搜索带来的影响；
• 实时联网条件：模型可以访问网络，用于观察检索能力与研究能力之间的差异。

对七个LLM智能体的HQ-50评测显示，在40道已解决问题中，闭卷条件下最多只有7道被重新解决。相较之下，实时联网后的成功往往更多体现为找到已经公开发表的解答，而不一定意味着模型独立重建了证明。

意义与局限

OpenFrontiers的重要贡献，不是宣称模型已经能够解决开放科学问题，而是重新定义了“研究级成功”应如何被测量。它把问题的开放状态、历史解决结果、形式化陈述和可执行验证放到同一评测框架中，使研究者可以更清楚地区分记忆、检索、推理和真正的 rediscovery。

当然，当前基准主要聚焦数学，且正式评测子集规模有限；Lean形式化也可能无法完整表达所有学科中的研究过程。因此，结果不能直接外推到整个科学研究。但作为基础设施，它为未来扩展到更多学科、比较不同智能体策略，以及追踪模型面对仍未解决问题时的进展，提供了较清晰的起点。

Hugging Face Daily Papers