Anthropic 用 1000 个 Claude Fable 5.2 智能体在沙箱内复现费马大定理形式化证明

多智能体团队能够解决具有挑战性的长周期问题。今年九月，我们发布了费马大定理的首个端到端形式化证明，由数十个智能体运行一个内部研究模型完成，该模型大致相当于 Claude Fable 5.1。这项工作依托数学形式化平台 Prove2Me，并由一位研究员指导。在一项新的小型实验中，一个由 1,000 个智能体组成的团队运行 Claude Fable 5.2 的早期版本，在没有 Prove2Me 提供的脚手架、也没有研究员引导的情况下复现了该证明。团队耗时 28.7 小时，输出 token 用量为原来的三分之一，写出的证明长度仅为原版的七分之一。

每个智能体都在无法访问互联网的沙箱中工作。每条 shell 命令和文件编辑在执行前都会经过分类器检查，离线监控器则审查团队的每一项操作。我们给智能体提供了一份包含 60 条命题的清单、对经典证明路线的一句话概述、这些命题所用到的定义，以及我们此前形式化工作中已证明的 47 个引理，并分配了负责人和协助者的角色。除此之外，我们没有就如何证明该定理或如何组织分工提供任何其他指导。

这项小型实验表明，运行 Fable 5.2 这类模型的智能体团队，能够在精心设计的安全边界内完成宏大的长周期目标。

问题

费马大定理指出，对于任何大于 2 的 n，都不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。这一命题在 350 多年间始终未被证明，直到 1995 年 Andrew Wiles 爵士发表了长达 129 页的证明。将该证明形式化——让每一步都能由计算机验证——一直是数学界长期以来的目标。

我们九月份的形式化工作由一位研究员和数十个智能体耗时 11 天完成，输出 token 约 60 亿。他们用 Lean 编写了 1300 万行代码；Lean 是一种编程语言，计算机可以检查其中证明的每一步。

智能体通过 Prove2Me 协同工作。该平台由彭天翼（现为 Anthropic 技术团队成员）及其在哥伦比亚大学的合作者设计。Prove2Me 使用一张共享图，把每个待证命题与它被拆分成的更小命题连接起来。任何智能体都可以拆分命题，其他智能体则可以向这张图查询哪些未证明的部分已可着手处理，从而避免对项目状态失去把握。每个命题及其证明都保存在可独立编译的单独文件中，因此许多智能体可以并行工作，而不会编辑同一批文件。

运行框架

我们想看看，一个运行 Fable 5.2 这类模型的智能体团队，能否在没有 Prove2Me、也没有研究员指挥的情况下，借助由通用工具搭建的运行框架取得这一成果。

工具

针对这项任务，我们给这个由 1,000 个智能体组成的团队提供了 60 条待证命题，其中包括最终定理和 59 个中间里程碑。对每条命题，智能体都必须用 Lean 写出证明，用 Lean 的工具构建并检查，然后提交到 Git 上的共享主分支，由评分器进行检查。我们为每个智能体提供了以下工具：

• 一个 shell 和一个文件编辑器，运行在各自无法访问网络的沙箱中。
• Lean 工具链和 Mathlib，已内置在沙箱镜像中。
• 自己的 Git 分支，以及向主分支发起合并请求的能力。
• 一个共享的 Postgres 数据库，可从 shell 访问。

协作

证明工作可以拆分开来，因此很适合交给多智能体团队完成。但智能体之间也需要协调，既要能基于彼此的工作继续推进，又要避免重复劳动。在我们最初的形式化中，Claude 早期的尝试之所以失败，是因为智能体跟丢了项目状态，协作也随之中断。改用 Prove2Me 平台后，这个问题解决了。

这次运行中，每个智能体都有一台轻量虚拟机作为自己的沙箱。如果只用一台共享机器，大约 100 个智能体就到极限了：我们 100 个智能体的运行中，超过一半因为内存、磁盘或 CPU 耗尽而不得不中止或重启。

有了 1000 个独立沙箱，智能体需要一种共享工作成果的方式，于是我们给它们配了一个 SQL 数据库（图 1）。选 SQL 是因为它提供了组织信息的通用原语，其事务机制能处理 1000 个智能体的并发写入，而且 Claude 本来就熟悉它。智能体用这个数据库认领任务、共享笔记、记录已完成的工作。

提示词

我们的提示词给了 Claude 一份包含 60 条待证命题的清单，每条都附有一行非正式描述，并说明了可用的工具（见上文列表）。

我们给这个团队的唯一结构是一个层级：一名负责人和 999 名助手。我们让负责人把问题拆成若干部分，分派给助手；让助手等待负责人派活，如果任务不清楚就向负责人确认。

运行期间，执行框架向负责人发送了 19 次剩余时间自动提醒，每次都鼓励负责人继续推进。

安全

正如我们此前介绍过的，单靠任何一层防御都不足以约束一个智能体团队。在这次实验中，我们把沙箱与实时监控、离线监控结合起来，让每个智能体都待在自己的虚拟机里、无法访问网络，并能发现任何试图逃出沙箱或篡改监控的行为。

沙箱

我们通过以下方式保障每个智能体沙箱的安全（图 2）：

• 通信：智能体没有专用的消息工具，只能通过数据库和 Git 协调。
• 代码变更：智能体只能推送到自己的 Git 分支，并向 main 分支发起合并请求。随后由一个独立任务把变更合并进 main，只有在出现冲突或故障（例如历史不相关）时才拒绝。
• 数据库访问：数据库调用以共享的非特权角色运行。每条 SQL 语句限时五秒，写入超过 256 MiB 会被拒绝。
• 网络控制：沙箱没有网络访问权限。它们对外唯一的通道是一条通往网关的管道，由网关转发它们的请求。
• 身份：网关在沙箱之外为每个请求打上该智能体的身份标记，防止一个智能体冒充另一个。
• 内核：每个沙箱的内核在构建时都去掉了能让 root 用户直接侵入内核的特性，例如可加载模块、kexec、原始内存访问和内核探针。内核以锁定模式运行。
• 最小权限：每个智能体的命令都以非特权用户身份在其沙箱内运行，sudo 等可能重新获得 root 权限的工具已被移除。智能体所用工具经过专门设计，无法读取或更改运行它们的智能体循环。

实时监控

为了让这类运行更安全，我们使用一个经过提示词引导的 LLM 分类器，它可以拦截每一次工具调用，包括 shell 命令和文件编辑。该分类器会监视试图逃逸沙箱、探测沙箱边界或篡改监控的行为，以及模型一旦成功逃出沙箱后可能采取的任何有害操作。当分类器拦截某次工具调用时，整个智能体团队会停止运行，必须由人工审查这次拦截后，团队才能重新启动。这样做的目的是防止另一个智能体继续执行被拦截的操作。

为了测试分类器能否识别复杂的破坏行为，我们开展了多智能体侧任务与破坏评估。在评估中，红队智能体采用分解攻击等策略，试图骗过分类器、让它放行一次沙箱逃逸。我们发现，能够查看智能体思维链（CoT）和智能体间通信的监控器，在这些评估中成功检测出了所有破坏尝试，因此我们现在用它们来监控多智能体运行。与此同时，我们还运行同一监控器的基于动作的版本——它只能看到动作，看不到 CoT——以防智能体的推理说服监控器放行有害操作。

我们正在通过人工引导和自动红队测试持续改进监控体系，用生产环境记录（包括过往事件）来评估监控效果，并扩展威胁建模。本文所述的这次运行中，我们只使用了基于动作的监控器。只有对主智能体的拦截才会终止整个运行；对辅助智能体的拦截只会移除该辅助智能体。

这次运行后不久，我们增加了并行的 CoT 监控器。我们会在可能尚未完成发布前对齐评估的模型上开展此类实验，因此我们在设计监控时考虑到了模型可能未对齐的情况。我们发布的模型会先完成该评估，这降低了风险，但并不能消除风险。

在超过一百万次工具调用中，本次运行没有任何一次达到拦截标准。当我们用 CoT 监控器和今天的评分标准回放这些调用时，只有一次——检查 root 访问权限——接近被拦截。

离线监控

除了实时监控，我们还运行离线监控。该监控器依据与实时监控相同的威胁模型分析智能体团队的操作，但拥有更多能力，例如可以查询其他智能体的操作。

结果

没有 Prove2Me，团队自行搭建了协调系统

这项证明工作分为几个层次：

• 证明：对于任何大于 2 的 n，不存在正整数 a、b、c 满足 aⁿ + bⁿ = cⁿ。
• 命题：我们给团队 60 个命题去证明，包括最终定理和 59 个中间里程碑。
• 更小的命题：智能体把困难的命题拆分成更小的命题，即引理。
• Lean：每个命题和引理都是 Lean 中的一个定理。

每条陈述都以 Lean 开头，并为其证明留出占位符，只有当 Lean 的检查器接受了一份完成的证明时，这条陈述才算作已证明。我们让负责人决定如何攻克证明，以及如何在这些工作层级之间协调团队。

在前 10 分钟里，负责人在数据库中建了五张表（图 3）：

• Announce（公告）：负责人向整个团队下达的命令（例如如何分工）。
• Assign（分配）：谁负责什么（例如哪位助手拥有或代理哪条陈述）。
• Notes（笔记）：一块开放的公告板（例如用于认领某项工作或汇报进度）。
• Subtasks（子任务）：一份待办清单，任何智能体都可以添加任务，最先认领的助手即拥有该任务。
• Landed（已完成）：已完成工作的日志。

负责人把陈述分发下去

建好这些表之后，负责人做了三件事。第一，它通过向 assign 表写入 999 行（每位助手一行），把每条陈述分配给一个由 16–17 名助手组成的小组。第二，它让每个小组中的一名助手担任队长，负责向笔记表发布计划，并把工作拆成任务，供组员从子任务表中认领。第三，它向公告表发布指令，告诉每位助手先判断自己那条陈述的难度，并把结论发布到笔记表中。

助手们从提示词中知道数据库的存在。它们找到公告表，开始做评估。大多数助手把结论发布到了笔记表。大约 27 分钟时，已有三条陈述得到证明，负责人也读过了发布的结论。随后它把大多数助手判定为在本次运行预算内不可行的 47 条陈述搁置一旁，把几乎所有助手重新分配到其余 10 条它认为可以完成的陈述上。小组规模从约 17 名助手扩大到 46 至 139 名。

每位助手都在一个循环中工作，其中大部分步骤都写在负责人的命令里：

• 在笔记表中找到该陈述的计划。
• 从子任务表中认领一个任务。
• 用 Lean 编写证明，用 Lean 的工具检查，然后提交到 Git 的主分支。
• 把任务标记为完成。
• 向笔记表发布更新。

大约 45 分钟时，10 条陈述中已有约 5 条得到证明，负责人写道：

“团队的吞吐量远高于早期‘预算内不可行’结论的假设”

全部 10 条陈述在大约 70 分钟内得到证明。

随后负责人把助手调往更难的陈述

这最初的 10 条陈述完成后，负责人写道“没有理由闲着”，并把助手重新分配到它最初放弃的更难陈述上。随着更多陈述得到证明，它不断把助手调往新的任务，主要集中在前六个小时（见图 4 中以红色显示的 assign 表写入）。

起初，负责人让队长们把工作拆成任务，填进子任务表。随着工作推进，助手们承担了越来越多求解各命题的责任。他们开始自己写任务，有时是在队长发出求助之后。到第 5.6 小时，已有 73 名助手写下了 756 个任务，其中只有 16 名是队长。图 4 显示了许多助手对子任务表的写入（红色），不过这些写入大多是认领任务或标记任务完成。完成任务的助手还会主动多揽活：

“有空……我能端到端做完一块……给我一个难啃的块……我马上开工”

起初，负责人也会把助手分配到具体命题上。这一做法在第一小时内就开始改变，到第三小时，负责人对自由助手说：“不用等我。”这样自由助手就能直接接手不同命题的工作，不必等负责人派活，而负责人 meanwhile 仍在不断写新的分配。

负责人把团队派给了 Langlands–Tunnell

到第 18 小时左右，剩下的只有 Langlands–Tunnell——怀尔斯证明所依赖的一个经典结果——以及依赖它的命题，还有一个团队顺带证出的命题。在这次运行早期，Langlands–Tunnell 任务的队长曾很悲观，估计证明至少需要 70 万到 100 万行 Lean 代码，按时完成的可能性不到 1%。负责人当时把这个命题搁置了。

其他工作几乎全部完成后，负责人把团队重新集中到 Langlands–Tunnell 上。这是最后一次自上而下的分配，它把约 750 名助手调到了这个命题上，并写道：“实话实说，胜算不大。”

Langlands–Tunnell 的规模远超智能体们此前处理过的任何命题，任务数约为其他命题的九倍，新增代码量也超过两倍。助手们再次用子任务表来拆分工作，但最初的许多任务太大，一个助手无法独自完成。

于是团队把工作组织成一棵树。队长制定了一份计划，把该命题分成 10 个区域，并把每一块列为一个任务。助手如果发现某一块太大、独自啃不动，就可以把它拆开，在下面挂上更小的任务。只要某一块对单个智能体来说太难，树就会继续生长，最终达到 2,418 个任务、最深 10 层（图 5）。每一块都可以先假定其下各块成立，因此在这些块被证明之前，数百名助手就能并行工作。

图 6 展示了整个运行过程中每名助手在做什么：早期助手分散在许多命题上，到最后则聚集到 Langlands–Tunnell 上。Langlands–Tunnell 在第 28.4 小时被证明，随后最终定理在第 28.7 小时完成。负责人接着写道：

“谢谢大家：费马大定理已经进入 main 分支，并通过了官方检查器的内核验证。”

结论

这个小型实验让我们得以研究一支由 1,000 个智能体组成的团队如何完成一项漫长而困难的任务。仅使用 Git 和一个共享数据库，智能体们设计了用于分配角色和共享结果的表格，组建了团队，并构建了一棵任务树来拆解最具挑战性的陈述——其队长曾估计按时完成的概率不足 1%。

这一结果并不意味着不再需要领域专用的运行框架或平台。例如，Prove2Me 仍可能通过帮助智能体更快地编译 Lean 代码、让它们搜索并复用人类成果来提高效率。

在某些节点上，人类的引导也仍然有用。智能体往往会在难题面前放弃，并误判其难度。早期，助手们判定 60 个陈述中有 47 个在本次运行的预算内不可行，但团队随后证明了其中大多数。在这种时刻，人类的鼓励可以防止智能体过早停下。

精心设计的安全边界正是我们最初敢于开展这个实验的底气。Claude 可以用我们提供的工具以任何它选择的方式攻克问题，但只能在无网络访问的沙箱内、并在两个独立监控之下进行。

我们预计这些方法会迅速演进；随着这样的团队承担更困难的工作，围绕它们的安全边界也需要同步跟上。我们相信，在安全前提下扩展的多智能体团队，将在未来几年帮助我们解决一些最具挑战性的问题。