Theory-Scale Auto-Formalization of Logics for Computer Science
本文介绍了 LCS-Bench，这是一个通过一种新颖的半自动化智能体流水线，从 327 个教科书条目中提取出超过 4,000 个 Lean 声明而构建的综合性理论规模基准测试，研究表明当前的先进模型在连贯的大规模自动形式化方面表现挣扎，成功率仅为 20.1%。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你拥有一本极其庞大且复杂的机器组装说明书。这本手册是用人类语言编写的，充满了图表、交叉引用，以及人类专家能够直觉理解的微妙假设。现在，想象你想让一个机器人将整本手册翻译成一种严格的、计算机可读的编程语言，其中每一个步骤在机器运行之前都必须经过数学证明。
这本质上就是这篇论文——《计算机科学逻辑的理论规模自动形式化》（Theory-Scale Auto-Formalization of Logics for Computer Science）——所探讨的内容。研究人员正试图教会人工智能将一整本逻辑学教科书翻译成一种名为 Lean 的正式编程语言，而且不仅仅是逐句翻译，而是将其作为一个完整的、相互关联的系统进行翻译。
以下是使用简单类比对他们工作的解读：
1. 问题所在：“孤岛”与“大陆”
以往教授人工智能这项技能的尝试，就像是要求它翻译一个个孤立的“孤岛”。它们会取一个数学定理，将其翻译，然后检查是否正确。但真正的数学是一个**“大陆”**。定义依赖于引理，而引理又依赖于其他定义。如果你在其中一个小环节出错，整个结构就会崩塌。
作者认为现有的 AI 基准测试规模太小了。它们就像是在模拟器中测试飞行员能否完成一次单次的转弯，而不是要求飞行员驾驶飞机从纽约飞往伦敦，同时还要应对风暴和燃油限制。这个新项目 LCS-Bench 就是那场“从纽约到伦敦的飞行”。它选取了一本完整的教科书（《计算机科学逻辑》），并试图实现整个内容的正式化——包含 327 个条目、超过 4,000 个代码声明和 85,000 行代码。
2. 解决方案：“建筑师与建筑工”流水线
为了完成这项大规模的翻译工作，团队并没有只是简单地要求 AI “去做”。他们构建了一个半自动化的流水线，就像一个施工队：
- 建筑师（规划）： 首先，AI 分析教科书并绘制一张“概念图”。它理清了每个想法是如何连接到下一个想法的（例如：“在理解‘证明树’之前，你必须先理解‘公式’”）。
- 建筑工（实现）： 另一个 AI 根据这张地图尝试编写实际的代码。
- 安全检查员（人类专家）： 这至关重要。人类介入以修复“隐藏陷阱”。例如，教科书可能会说：“假设 X 在本章余下部分成立”，但并未明确写出这一点。AI 可能会忽略这一点，从而建立起一个不稳固的基础。人类负责捕捉这些缺失的假设。
- 反例猎人： 如果 AI 陷入困境，系统会尝试证明它试图证明内容的“反面”。如果成功了，系统就知道 AI 的定义错了（就像通过尝试用重型卡车驶过桥梁来寻找桥梁的裂缝一样）。
3. 基准测试：“障碍赛跑”
在构建完这个庞大的库之后，他们将其转化为了一个测试（基准测试），用于测试其他 AI。他们创建了五个不同的“赛道”或障碍赛：
- 条目级（Item-Level）： 翻译一个特定的定义或定理。
- 子章节级（Subsection-Level）： 一次性翻译一整个章节。
- “干扰项”测试（The "Distractor" Test）： 给定 AI 正确答案，但将其隐藏在一堆无关紧要、令人困惑的代码中，以观察它是否能从噪声中找到信号。
- 定理证明（Theorem Proving）： 给定 AI 代码，但留下“证明”部分为空白（用一个叫做
sorry的占位符标记），看它能否填补逻辑空白。
为了给答案评分，他们发明了一个 DefEq 检查器。你可以把它想象成一把超级精确的尺子。它不仅检查代码是否能编译通过，还会检查 AI 的翻译是否与原始教科书的含义完全一致，即使 AI 使用了不同的词汇或变量名。
4. 结果：“现实检验”
他们将 14 个目前最顶尖的 AI 模型（包括来自 OpenAI、Anthropic 等公司的顶级模型）放在这个赛场上进行了测试。结果令人警醒：
- 得分： 即便是最优秀的 AI，也只有大约 20% 的条目是正确的。
- 难度： 模型在处理需要深度抽象推理或处理“绑定替换”（binder substitution，一种技术性说法，意为“追踪哪个变量属于哪条规则”）的任务时表现最差。
- “过度思考”陷阱： 有趣的是，当模型失败时，它们消耗的计算时间和算力往往比成功时还要多。它们会“过度思考”，在原地打转，而不是快速找到解决方案。
- 干扰效应： 当 AI 被给予额外的、无关的信息（干扰项）时，其表现显著下降。这表明目前的 AI 在处理大型上下文时难以过滤掉噪声，而这对于处理理论规模的工作至关重要。
5. 结论
论文得出结论：虽然 AI 在数学方面正在进步，但理论规模的自动形式化（即翻译整个连贯的知识体系）仍然是一个巨大的挑战。目前的模型就像是那些能解出单个代数题，但在被要求编写一整章相互依赖的教科书内容时就会迷失方向的学生。
作者希望这个基准测试（LCS-Bench）能作为一个“训练场”，帮助未来的 AI 模型学习如何处理处理计算机科学逻辑所需的复杂性、一致性和忠实度。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。