FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models
该论文介绍了 FormalTCS，这是一个利用 2025–2026 年前沿理论计算机科学（TCS）研究并经过专家验证的基准测试，旨在揭示当前的大型语言模型在端到端自动化研究方面存在显著困难，这主要是由于其在自动形式化以及生成新颖、高质量数学断言方面的严重局限性所致。
原始论文根据 CC0 1.0（http://creativecommons.org/publicdomain/zero/1.0/）发布到公有领域。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
理论计算机科学是研究信息如何被处理以及计算能力的根本极限的学科。它是现代技术的基石，提供了决定哪些问题可以由机器解决以及如何高效解决这些问题的数学规则。几十年来，这一领域一直依赖人类数学家来构建精确的定义、构建逻辑论证，并证明其结论是不可动摇的。最近，一种新型工具出现了：大语言模型。这些是经过海量文本训练的人工智能系统，它们能够阅读、写作并对复杂话题进行推理。随着这些系统变得越来越强大，研究人员开始询问，它们是否能做得更多，而不仅仅是回答问题或总结文本。它们真的能独立进行科学研究，发现关于计算的新真理，并以与人类专家相同的严谨性来证明它们吗？
来自哈尔滨工业大学的一个研究小组致力于回答这个问题，他们构建了一个名为 FORMALTCS 的新测试场。他们希望超越简单的测验或教科书练习，看看这些人工智能是否能够应对前沿研究中那些混乱且困难的现实。为此，他们从该领域最顶尖的会议中收集了 175 个真实的科研问题，涵盖了算法、复杂度以及机器学习理论等主题。这些并非虚构的问题；它们是 2025 年和 2026 年被接收论文中的实际核心发现。随后，研究人员与人类专家合作，将这些发现转化为计算机可以验证的形式，从而建立了一个衡量人工智能的严格标准。
这项实验的结果揭示了这些模型在“理解能力”与“实际执行能力”之间存在的显著鸿沟。当研究人员要求模型阅读一段研究发现的高层摘要，并用通俗易懂的语言解释其背后的逻辑时，模型的表现相当出色。它们能够把握大局，并能较为准确地描述证明策略。然而，一旦任务转向将这些想法转化为计算机可以检查的正式数学语言，模型便撞上了南墙。这个过程被称为“自动形式化”（autoformalization），即人类研究者将一个模糊的想法转化为一组精确的规则和定义的步骤。在这个关键阶段，最优秀的人工智能模型仅在约 11.5% 的情况下取得了成功。相比之下，当研究人员为模型提供精确的数学定义进行操作时，模型能够完成最终证明的成功率约为 28.6%。
这一差距表明，人工智能在该领域面临的主要障碍不在于一旦路径铺设好之后遵循逻辑路径的能力，而在于构建路径本身的能力。模型难以将一个自然语言描述的问题转化为计算机验证解法所需的特定、无歧义的定义。这就像是模型可以阅读地图并理解目的地，但它们却无法绘制地图本身。此外，当研究人员构建了一个允许模型从零开始生成自身新研究想法的系统时，结果更加发人深省。在系统生成的 64 个新主张中，只有 6 个被人类专家认为具有足够的新颖性和价值，值得去研究。其余的主张要么与现有工作过于相似，要么缺乏真正的意义，或者根本无法被证明。
研究结论指出，尽管这些人工智能系统在理解和讨论理论计算机科学方面正变得越来越好，但它们距离独立进行研究仍有很大差距。它们缺乏识别哪些新想法真正值得探索所需的“品味”或直觉，并且在将想法转化为严谨数学语言方面存在困难。通往该领域完全自主科学发现的道路需要解决两个截然不同的问题：提高将想法转化为严谨数学语言的能力，以及培养对研究想法价值感的深刻认知。在这些障碍被克服之前，人工智能在该领域中的角色仍将是强大的助手，而非独立的科研人员。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。