Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

该论文提出了一种名为"Agent Hunt"的基于赏金机制的协作式自动形式化框架，通过让多个大语言模型代理在交互式定理证明环境中动态发布、竞标并完成代数拓扑领域的证明任务，从而探索去中心化的协作证明搜索与理论构建方法。

要点

这篇论文讲述了一个非常有趣的实验：如何让一群人工智能（AI）像“自由职业者”一样，通过“悬赏竞标”的方式，共同完成一项极其复杂的数学证明任务。

想象一下，你有一本厚厚的、全是数学公式的“天书”（代数拓扑学），需要把它翻译成计算机能读懂的“代码语言”（形式化证明）。以前，这通常需要一个超级天才（或者一个超级 AI）从头写到尾，既慢又容易卡壳。

但这次，作者们想出了一个新招：“悬赏猎人”（Agent Hunt）模式。

1. 核心概念：数学界的“赏金猎人”游戏

想象有一个巨大的数学工地，上面堆满了还没完成的证明任务（定理）。

• 悬赏（Bounty）： 工头（人类专家）给每个任务贴上一个价格标签（比如 100 个虚拟金币）。
• 猎人（Agents）： 四个 AI 助手（Alice, Bob, Charlie, Dave）就是这里的“猎人”。
• 规则：
  • 抢单： 猎人看到任务，可以付一点定金（锁定任务），然后开始干活。
  • 竞争： 如果两个猎人都想干同一个活，谁先做完谁拿钱。
  • 合作： 如果任务太难，猎人可以把它拆成小任务，再悬赏给其他人（或者自己接别人的小任务）。
  • 结算： 只有当计算机（证明助手）严格检查并确认证明完全正确时，猎人才能拿到钱。如果证明错了，钱就没了。

2. 他们做了什么？

• 目标： 他们要翻译一本著名的数学教材《Munkres 拓扑学》的后半部分（代数拓扑），大约 200 页的内容。
• 工具： 他们用了四个不同版本的 AI 模型（像是有不同性格的工人），在一个叫"Megalodon"的数学检查器里工作。
• 过程：
  • 一开始，人类专家先给所有定理贴好了价格标签，并设定了规则。
  • 四个 AI 猎人开始疯狂工作。它们互相竞争，看谁证明得快；同时也互相帮忙，比如 Alice 证明了一个基础定理，Bob 就可以基于这个定理去证明更难的定理。
  • 它们还会自己写代码、检查错误、甚至重新定义一些概念，就像工人在工地上自己发明新工具一样。

3. 成果如何？（惊人的速度）

• 速度爆发： 在短短 2 天半 的时间里，这四个 AI 联手写出了 12 万行 代码（证明）。
• 对比： 以前只有一个 AI 在干类似的“普通拓扑学”项目，干了 60 天才写了 40 万行（平均每天 7000 行）。而这次四个 AI 合作，平均每天能产出 3.9 万行！
• 效率： 这就像是一个人的小作坊，突然变成了四个熟练工组成的流水线，效率翻了 5 倍以上。

4. 有趣的故事和插曲

• 抢单大战： 有一次，Bob 正在艰难地证明一个定理，快要完成了，但他没来得及“锁定”这个任务。结果 Alice 冲进来，把 Bob 那 3000 多行的半成品证明，直接替换成了一个完美的完整证明，然后拿走了奖金。Bob 只能看着奖金飞走。
• 分工明确： 虽然大家在一起干活，但自然形成了分工。比如 Bob 擅长“基础结构”，Charlie 擅长“几何形状”，Alice 擅长“基础逻辑”。大家各展所长。
• 踩坑经历： 有时候 AI 会“走火入魔”。比如它们试图证明一个关于“圆”的定理，但因为数学定义里把“正弦”和“余弦”定义得太模糊（就像定义“苹果”时，既可以是红色的也可以是绿色的，甚至可以是石头），导致 AI 怎么证明都证明不通。最后人类专家发现是定义错了，必须重写定义。

5. 这个实验意味着什么？

这就好比以前我们试图用一个超级大脑去解决所有数学难题，现在变成了建立一个去中心化的数学市场。

• 优点： 不需要人类事无巨细地指挥谁做什么（因为数学证明太复杂，人类很难提前规划好每一步）。AI 们自己根据“价格”和“能力”动态分配工作，更灵活，速度更快。
• 未来： 这种方法可能让 AI 在数学、科学发现领域发挥更大的作用。它们不再是单打独斗的程序员，而是像一群在集市上自由交易、互相协作的“数学工匠”。

总结一句话：
这篇论文展示了如何通过**“悬赏机制”，让一群 AI 像自由职业者一样，在数学工地上既竞争又合作**，从而以前所未有的速度完成了复杂的数学证明任务。这不仅是 AI 的胜利，更是**“市场机制”在科学探索中的一次成功实验**。

技术摘要

Agent Hunt：基于赏金机制的 LLM 代理协同自动形式化论文技术总结

1. 研究背景与问题 (Problem)

大型语言模型（LLM）代理在数学教材的自动形式化（Autoformalization）方面已展现出潜力，但在处理超大规模项目时仍面临挑战。

• 现有局限：之前的“一般拓扑学（General Topology）”项目（基于 Munkres 教材第一部分）虽然进展显著（超过 35 万行代码），但仅由单个代理完成，耗时极长（截至 2026 年 2 月仍在进行中），效率低下。
• 核心挑战：如何有效地让多个 LLM 代理协作，并行处理大规模形式化任务？传统的集中式、预先规划的任务分配方式在面对数学证明中不可预测的缺口、前向引用（forward references）和复杂的依赖关系时显得僵化且难以扩展。
• 目标：探索一种去中心化的、基于市场机制的协作模式，以加速代数拓扑（Munkres 教材第二部分，约 200 页）在交互式定理证明器（ITP）环境中的自动形式化进程。

2. 方法论 (Methodology)

该研究提出并实施了一个名为"Agent Hunt"的基于赏金（Bounty-based）的协作自动形式化框架。

2.1 核心机制：赏金市场

• 去中心化协作：不再依赖人工预先规划任务，而是构建一个模拟的赏金市场。
• 代理角色：四个 LLM 代理（Alice, Bob, Charlie, Dave）作为独立参与者。
• 工作流程：
  1. 悬赏发布：代理可以提出新的引理（形式化陈述）并附加赏金（模拟货币）。
  2. 竞争与协作：代理竞争证明这些定理以获取赏金，同时也通过协作（如解决他人的子任务）来加速整体进度并获得奖金。
  3. 锁定机制：代理可以支付赏金的 10% 来“锁定”一个定理（最多 10 个，有效期 24 小时），获得独家证明权。若他人证明，赏金仍归锁定者；若超时未证明，锁定失效。
  4. 动态调整：代理可以引入新的形式化定义和中间引理来构建证明结构。

2.2 技术栈与环境

• 目标领域：代数拓扑（Munkres 教材第 9-14 章，第 51-85 节）。
• 形式化系统：Megalodon（高阶集合论证明检查器）。
• LLM 模型：使用了 4 个代理，分别基于 ChatGPT Pro Codex 5.3 和 Claude Code (Opus 4.6, Sonnet 4.6)。
• 初始设置：
  • 由单个 LLM 预先将 200 页 LaTeX 内容形式化为定义和定理（无证明），并估算难度和赏金（基于教科书证明行数、难度评分 1-10 及$100/小时的成本估算）。
  • 严格的质量控制：禁止修改已有定义，禁止重复，必须通过编译检查。

2.3 规则与治理 (Guard Scripts)

• 严格纪律：禁止修改他人的锁定、部分证明或沙箱；禁止修改现有定义/定理陈述。
• Guard Scripts（守卫脚本）：
  • 本地运行的脚本，在提交（Commit）前检查不变量（如余额非负、赏金为正、锁定数量限制、过期时间等）。
  • 从基于行的解析升级为基于 Token 的流式处理，确保定义和定理陈述的不可变性，精确追踪 Qed（完成）与 Admitted（承认/未证）状态，防止关键词滥用。
• Megalodon 改进：
  • 优化了检查管道，替换了低效的线性查找。
  • 收紧信任模型：仅当依赖项被递归检查通过后，才允许使用 Qed 命令。
  • 改进错误信息：将哈希值转换为可读符号，帮助 LLM 理解错误。

3. 主要贡献 (Key Contributions)

1. 去中心化市场机制在 ITP 中的应用：首次将“赏金市场”概念引入交互式定理证明的自动形式化，展示了其比集中式规划在应对大规模、不可预测数学任务时的灵活性和扩展性。
2. 多代理协同与竞争策略：验证了多个 LLM 代理在竞争（争夺赏金）与协作（解决子问题、共享成果）之间的动态平衡，能够有效并行化工作流。
3. 大规模自动形式化实验：在短短 2 天 15 小时内，完成了约 3.9 万行/天的形式化代码生成，远超单代理项目的平均速度（约 7k 行/天）。
4. 系统架构优化：
   • 设计了针对 LLM 代理的专用守卫脚本和状态管理机制。
   • 对 Megalodon 证明器进行了针对性修改，以适应 LLM 生成的长文件和非人类风格的证明。
5. 成本效益分析：实验总成本约为 150 美元（基于订阅费），平均每 1000 行归一化代码成本约 1 美元，展示了极高的性价比。

4. 实验结果 (Results)

• 形式化规模增长：
  • 实验开始于 2 月 16 日晚，初始库约 1.9 万行。
  • 2 月 19 日上午，代码量增长至 12.1 万行。
  • 速度：四个代理联合产出约 39,000 行/天，是单代理项目（General Topology）平均速度的 5-6 倍。
• 经济激励有效性：
  • 代理们累计放置了 709 个赏金。
  • 完成模式：279 个由创建者自己完成，114 个由其他代理完成（跨代理协作），312 个在实验结束时仍活跃/未解决。
  • 代理通过锁定机制和策略性选择（合作 vs 竞争）最大化收益。
• 分工情况：
  • 形成了自然的主题分工：Bob 专注于同伦和覆盖空间；Charlie 专注于几何拓扑（圆/盘、射影空间）；Alice 专注于基础路径连接和群律；Dave 专注于抽象群论支持。
  • 尽管有重叠，但每个区域主要由特定代理主导，避免了全员的混乱冲突。
• 重大定理证明：
  • 证明了多个长证明定理（如 cyclic_infinite_order_iff_Z 1999 行，thm60_1_pi1_product 1474 行）。
  • 布劳威尔不动点定理（Brouwer Fixed Point Theorem）：代理成功构建了该定理的证明链（包括非零向量场、包含映射非零伦等），但最终未能证明“圆的基本群同构于整数”这一关键引理。
• 遇到的障碍：
  • 定义缺陷：实验发现 Munkres 中关于 sin 和 cos 的定义（基于 epsilon 选择算子）存在歧义（不唯一），导致代理无法提取性质。这暴露了自动形式化中源文本定义质量的重要性。
  • 练习题误导：初始阶段对教科书练习题的赏金估算过低（因为通常无答案），导致代理投入大量精力却获得微薄回报。后续规则已调整，优先处理主定理。

5. 意义与展望 (Significance)

• 可扩展性验证：证明了基于市场机制的分布式代理系统在处理超大规模数学形式化任务时，比单一大模型或集中式规划更具可扩展性和鲁棒性。
• 人机协作新范式：展示了人类专家（作为管理员和初始定义者）与 LLM 代理（作为执行者和竞争者）结合的新工作流。人类负责设定框架和初始质量，代理负责执行和迭代。
• 未来方向：
  • 需要更智能的初始定义生成，避免源文本中的定义歧义。
  • 进一步优化代理间的协作策略，减少重复劳动。
  • 将此类框架推广到更广泛的数学领域和更复杂的证明系统中。

总结：Agent Hunt 项目通过引入“赏金市场”机制，成功实现了多 LLM 代理在代数拓扑领域的高效、并行自动形式化。它不仅大幅提升了形式化速度，还揭示了去中心化协作在解决复杂数学问题中的巨大潜力，为未来大规模 AI 辅助数学研究提供了重要的技术路径和实证依据。