Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust

在计算领域，人们正日益雄心勃勃地试图构建能够解决远超当今超级计算机能力的难题的机器。这些被称为量子计算机的设备，利用亚原子世界的奇特规则来处理信息，其方式似乎是经典机器无法实现的。它们承诺破解那些需要现有计算机花费数千年才能破解的代码，或者模拟可能导致新药研发的化学反应。然而，为了让这些机器发挥作用，科学家必须首先编写指令，即算法，来告诉它们该做什么。挑战在于，量子力学极其难以精准掌握。逻辑中哪怕是一个微小的错误都可能导致整个计算失败，而且由于数学极其复杂，即使是人类专家也难以确定自己的指令是否完美无瑕。

这种不确定性促使研究人员转向寻求人工智能的帮助。AI 智能体在编写代码甚至证明数学定理方面正变得异常出色。但一个新的问题出现了：仅仅因为一个 AI 能写出一个在电脑屏幕上看起来正确的证明，并不意味着这个证明真的解决了人类想要解决的问题。计算机可能正在检查问题的另一个版本，或者它在统计运行程序所需的资源时，忽略了隐藏的成本。如果一个 AI 声称找到了破解特定加密代码的方法，但其证明依赖于对计算机如何统计步骤的误解，那么结果将毫无用处。科学界需要一种方法，以确保当 AI 声称它解决了一个问题时，它确实解决了那个特定的问题，并考虑到了所有的成本和条件。

一组研究人员现在引入了一个名为 Lean-QuantumAlg 的新系统来解决这一困境。他们构建了一个数字框架，作为人类用户与人工智能之间的严格契约。在这个系统中，人类定义问题和游戏规则，而 AI 则负责构建算法并证明其有效性。其核心创新在于，该框架强制要求 AI 将正确性的证明直接与资源使用的证明挂钩。简单来说，该系统确保如果 AI 实际使用的能量或时间超过了所承认的量，它就不能声称解决方案是高效的；并且如果它在计算完成后未能将计算机恢复到原始状态，它就不能声称解决方案是正确的。

研究人员通过让 AI 智能体形式化九种不同的量子算法来展示这一方法的威力，这些算法涵盖了从基础搜索方法到针对现代加密标准（如 RSA-2048）的复杂攻击。在过去，验证这类算法需要人类阅读数千行代码以检查每一个细节。有了这个新框架，一旦系统的核心规则经过人类审计并获得信任，AI 就可以承担繁重的工作。研究人员发现，对于这九种算法中的每一种，只有不到 1% 的代码需要人工审查。其余的工作由框架处理，它会自动检查 AI 的证明是否有效，以及算法是否满足契约中的每一项要求。

该系统通过将验证过程分解为若干个不可更改的部分来运作。首先，人类指定问题，明确算法必须实现的目标以及允许使用的资源。这一规范与解决方案本身是分离的。接下来，AI 构建算法，这本质上是一套给量子计算机的指令。随后，框架会对该算法进行模拟运行，以观察其发生的情况。它会检查三个关键点：算法是否以要求的概率产生正确答案、是否将“借用”的量子系统部分精确地恢复原状，以及是否保持在人类设定的时间和内存限制之内。如果 AI 试图省略一个昂贵的步骤或错误统计资源，框架将拒绝该证明。

该方法处理“借用”资源的方式是其最重要的发现之一。在量子计算中，算法通常需要使用一些它并不拥有的额外内存，前提是它在结束后必须将这些内存恢复到原始状态。如果 AI 虽然将内存恢复到了正确的状态，却以一种未被允许的方式使其与其他部分发生纠缠，那么该算法就是有缺陷的。Lean-QuantumAlg 框架以极高的精度检查这种联合状态，确保借用的内存确实得到了恢复。这种细致程度此前难以实现自动化，但新系统将其作为验证过程的标准组成部分。

研究人员还展示了这种方法具有良好的扩展性。通过对系统的共享基础进行一次性审计，他们可以将此复用于许多不同的算法。对于测试的九种算法（其中包括针对用于安全通信的 P-256 加密标准的攻击），人类需要阅读的代码量大幅下降。在最复杂的情况下，人类审查仅限于总代码量的极小部分，而框架处理了剩余部分。这表明，在未来，只要有一个可信的系统来验证结果，AI 就可以被用来发现并认证新的量子算法，其速度和规模将是人类专家单打独斗永远无法企及的。

这项工作并不声称 AI 已经解决了所有量子问题，也不代表这些算法已经准备好立即在物理硬件上运行。相反，它提供了一种严谨的方法，用以确保 AI 生成的数学证明是值得信赖的。它将任务进行了分离：人类负责定义什么是重要的，而机器负责检查逻辑。通过这样做，它为量子算法的可扩展发现开辟了一条路径，确保当 AI 声称找到了一个解决方案时，该解决方案是真实的、高效的，并且完全符合最初的要求。其结果是，在自动化科学发现时代建立了一个新的信任标准——由机器完成工作，但人类始终是判断价值的最终裁决者。