--- layout: post.njk source: https://yage.ai/share/chao-xu-ai-math-dual-loop-20260721.html speaker: yage.ai title: |- 从数学家如何用 AI 来看 Harness 如何兼顾开放性与严谨性 date: '2026-07-21' summary: 文章探讨了数学研究中‘开放探索’与‘严谨判定’之间的矛盾，并提出了一个双循环工作流来解决这一冲突。该方案将路线探索和结论推导拆分为两个互相反馈的循环：一个用于预算分配和路径探索，另一个用于候选证明的敌意审计和盲重构验证，从而在保持研究创造性的同时确保知识的可信状态流转。 area: knowledge-meta category: workflow-tools tags: - exploration-vs-verification - agentic-workflow - proof-validation - knowledge-management people: [] companies_orgs: [] products_models: [] media_books: [] draft: true status: evergreen --- 2026 年 7 月 18 日，电子科技大学（UESTC）计算机学院副教授 Chao Xu 发布了《AI Agents for the Working Mathematician》。他分享了自己如何组织数百个 subagents，长时间寻找开放数学问题的证明、反例和中间引理。 这套协议最显眼的地方是严苛的质检：候选证明必须通过专项找错、从头重构和跨模型审查。不过，如果只把它看成更严厉的审稿机制，就漏掉了它更核心的设计。这套协议同样在管理结论形成前的路线探索。 这两件事的目标方向相反。寻找路线需要容忍大量不成熟的想法，否则无法发现新路径；后续推导却必须隔离这些不成熟的想法，防止隐藏的逻辑漏洞变成整个项目的前提。Chao Xu 的方案是将它们拆成两个互相反馈的循环：一个决定下一份预算用来探索什么，另一个决定哪项结果可以进入共享前提。这正是它对 AI 知识工作最有意思的启发。 ## 数学把探索和判定放在了同一道题里 假设我们正在证明一个固定的数学命题。在动笔之前，谁也无法预先列出完整的证明路线。寻找证明的过程是高度开放的，可能先寻找反例，再转向某个中间引理，或者换一种数学构造。目标虽然固定，通往目标的道路却有无限可能。 但当一份候选证明写完、进入判定阶段后，要求就变得极度严格。哪怕整篇推导极具启发性，只要量词用错、边界条件遗漏，或者关键一步依赖了未证的前提，证明就无法成立。在已冻结的命题下，逻辑缺口没有妥协空间。 严格的判定并不意味着检查很容易。如果候选证明是用形式语言写成的，我们可以交给证明助手核验；如果是具体反例，可以直接计算代入。然而，尚未形式化的自然语言证明目前缺少廉价的通用检查器。AI co-mathematician 论文提到，AI 几分钟就能生成数十页的证明草稿，人类专家却可能需要几天来核验。这就带来了极度不对称的验证成本。 数学研究正好落在这两重矛盾的交集里。一方面，它需要像其他知识工作那样，在未知的路径中进行开放探索；另一方面，它又要求像软件测试那样，接受毫无协商余地的逻辑判定。 数学研究位于开放探索与明确验证的交集 但这并不意味着职业之间存在互斥的界限。事实上，任务会随着阶段而移动，比如软件项目也会从需求探索进入规格冻结后的实现。下面的任务地图展示了这种动态分布：同一个任务在完成形式化或写入测试后，其校验难度和所处的位置也会随之改变。 任务在探索开放度与判定要求上的概念位置 这种冲突也普遍存在于安全漏洞分析、新算法设计和复杂的科学发现中。数学之所以是高对比度的案例，是因为它把这种张力推到了极致：路线无法预先编写，判定不能靠偏好妥协，自然语言的证明又缺乏便宜的自动测试。要解决这个冲突，就必须将探索和判定剥离，运行两套不同的循环。 ## 第一套循环决定下一步还要探索什么 探索一个开放命题时，长周期运行并不等于让单个模型在线写上几十个小时。相反，协调者需要在证明推导、寻找反例和构建中间引理等动作之间频繁切换，并在多条解题路线中分配计算预算。 系统必须把整个探索过程的状态持久记录下来。首先，协调者把目标命题写入 STATEMENT.md，以此固定研究终点。 在具体的路径搜索中，智能体把每一次尝试都记录在 REGISTRY.md 里。这本路线日志不仅登记了“试过什么”，还包括每条路线卡在什么地方、遇到了哪些逻辑阻碍，以及下一项决定生死的关键测试。新启动的智能体接手任务时，只要先阅读这本日志，就能避免因为采样的随机性而重复尝试已经证实走不通的思路。 如果在寻找证明时，某条路线卡在一个与原命题同样困难的未知引理上，系统不会把这条路线标记为“接近成功”。协调者会把它判定为阻塞状态，记录进 FAILED.md，并立即停掉这一方向的计算预算。只有当其他探索分支产生了新的数学机制、构造或证据时，这条卡住的路线才可能重新激活。 经过不断的尝试与回退，探索循环最终可能会产出一份看似完整的证明。此时，系统会给它贴上 candidate 标签。就算生成该证明的智能体进行了自我核对，标签也仅能升级为 self-audited。对后续的智能体而言，这两个标签没有任何区别，都不能当作已经成立的定理来引用。 ## 第二套循环决定什么可以成为前提 当候选证明从探索中产生、需要成为下一步推导的凭证时，晋升循环便会启动，用多道防线对其进行交叉核验。 首先，证明需要接受敌意审计（hostile audit）。担任对手的智能体只负责挑错，尝试构造具体反例，检查逻辑跳跃、隐藏前提和遗漏的边界条件。 如果候选证明通过了这一关，系统再安排一个 fresh agent 进行盲重构。这个新智能体完全看不到原本的推导文字，只拿到目标命题和记录在案的关键思路，在隔离环境里从头推导。这一步能验证核心思路是否脱离了原推导的叙述。它与敌意审计的侧重点不同，但两个阶段的模型如果来自同一个家族，在面对共同的训练集偏见时，仍可能共享相同的盲区。 只有通过这两道关卡，候选证明才能升级为 verifier-backed。当系统将它写入 PROVED.md 后，它的状态正式晋升为 promoted，后续的路径搜索才允许引用这个前提。若要获得 independently audited 标签，就必须引入不同的模型家族或人类专家。单纯启动同一个模型家族的新实例不算跨家族独立审查，因为它们极易犯同一种错误。 Chao Xu 证明晋升与状态流转流水线 两个循环正是通过这种方式相互反馈。如果敌意审计发现了缺口，证明就会失去晋升资格，相关路线带着最新的漏洞信息退回 REGISTRY.md，甚至写入 FAILED.md 并冻结；如果证明成功写入 PROVED.md，它就会变成下一轮探索可以依赖的合法前提。系统不需要在每次搜寻时都做全局核验，也不会让一段刚生成的文字悄悄混进推导链条。 我们需要强调，晋升协议管理的是可信状态的流转，并不直接生产数学真理。跨模型的共识依然有可能共同出错。Chao Xu 在报告中提到，他动用数百个 subagents 尝试了十个开放数学问题，其中成功解决三项，每题运行至少十小时（提前解决的除外）。这只是作者自报的经验数据，其题目、运行轨迹均未公开，也缺少同预算基线的受控对照或独立数学判定，因此不能当作通用的 benchmark。 此外，协议中的设计机制多有前人踪迹。OpenAI 的 CDC prompt 已有路线登记和阻塞预算控制的思路；Danus 明确划分了生成与验证的权限；Chao Xu 先前开发的 coverify 也是一套基于多个审查者的验证架子。Chao Xu 的贡献，在于把这些分散的校验动作组织成了一份可持续运行、支持随时恢复的长周期数学合同。 ## 知识工作可以从中拿走什么 在数学研究的演进中，终极的检查手段是形式化。证明助手 Lean 就像逻辑编译器，能直接验证用形式语言写出的命题和推导。不过，它只检查机器读到的形式化代码，无法判定人类是否忠实地把自然语言命题翻译成了代码。其生态库 mathlib 保存了大量可复用的定义和引理。如果在研究中要使用库里没有的概念，我们就得自己定义、补齐引理并接受审查。OpenAI 的 cdc-lean 则展示了自然语言草稿与 Lean 形式化证明文件的结合。形式化需要巨大的前期投入，但一旦进入 mathlib 库，校验成本就会降得极低。Chao Xu 的协议管理的正是形式化覆盖之外的空白区域。 这种“探索时放开、引用前严卡”的思路，能够直接启发其他非数学的知识工作。 许多决策、分析和战略规划任务缺少像数学那样单一的判定器。一份报告可能在几种取舍下都言之成理。但哪怕标准是多元的，关键的中间前提依然有对错：引用的事实可能失实，数据可能算错。当后续任务需要依赖这些推论时，我们应当把“新产生的草稿”与“团队可直接复用的共享前提”区分开，登记失败路线，并隔离未经核验的前提。 在此，我们不能简单地把整份决策晋升为唯一正确的答案。更合适的晋升单位是建议中的事实、因果判断和限制条件。我们只把证据确凿的客观事实升为共享前提；对于依赖价值取舍的建议，则应保留它成立的边界和反方证据。通过这种隔离，探索循环能继续允许问题和方向发生变化，晋升循环也只阻止没有检验过的假说伪装成团队共识。 软件工程所处的位置也会随着阶段而移动。在需求发现和架构设计阶段，团队同样需要高度的探索，规格往往在实现中逐步明确。而当规格冻结后，我们就应当优先使用编译器、自动测试、schema 校验和干跑等可执行检查。对于这些成本更低的校验手段，应当先扩大自动测试的覆盖范围，绝不能用几个智能体讨论出的“共识”代替实际测试。只有像 SDK 兼容性判断、无法自动测试的安全假设等尚未得到自动测试覆盖、又会影响下游实现的前提，才适合采用候选隔离与 fresh agent 盲重构。 这套双循环工作流并没有消灭研究的创造性，它保留了探索最重要的自由：确定目标后，路线可以随时重构。与此同时，它建立了一道显式的限制：一个想法可以自由出现，但在它改变其他人的推导之前，必须先亮出自己通过了什么检查。