开放世界多智能体数学发现：从模型能力到验证系统设计

近半年我在搭建一套用于数学探索的多智能体实验环境过程中最大的认知转变是不要把“自主数学发现”当成一个模型能力问题而要当成一个系统设计问题。最开始我的做法和大多数人一样——把一道数论题直接丢给一个能力很强的大语言模型让它“自由发挥”。它确实能很快给出看似合理的思路构造样例、归纳模式、提出猜想、写出一段所谓的证明。但只要追问一步“你能把这个猜想形式化并让机器自动验证吗”问题就暴露了证明里藏着未说明的前提归纳跳过了反例同一个数在不同步骤里被悄悄换了定义。更麻烦的是让它自己检查自己它会一遍遍修补漏洞直到把思路修得面目全非却始终没有逼近正确结论。后来我把任务拆给一组智能体去做——有人负责提猜想有人负责翻译成可验证的断言有人专门负责找反例。结果稳定了很多也才真正意识到开放世界多智能体环境中的自主数学发现核心不是让单个智能体变得更聪明而是把“探索—猜想—验证—迭代”变成一条可并行、可复现、可审计的流水线。开放性决定了它能走多远验证层决定了它敢不敢出发。没有验证的开放世界不是探索只是随机游走。1. 先搞清楚“自主数学发现”到底改变了什么1.1 传统研究流程与智能体式探索的区别传统数学研究里开放世界存在于研究者的脑子里。一个人面对一个领域靠直觉、经验和大量试错分辨哪些问题值得深入哪些方向看起来漂亮但其实是死胡同。这个过程的产出不只是定理本身还包括问题筛选、反例构造、方法迁移等一系列判断。恰恰是这些判断很难被当前单一模型稳定复现。过去几年常见的 AI 数学实验大多是“封闭任务集”模式从一个固定题库里取一道题让模型在限定策略空间里搜索证明。评价标准也很简单——证明成功或不成功。这种模式像学生做教材里的习题答案是已知的路径是受限的失败时至少知道自己错在哪一道题上。而开放世界环境完全不同。问题不是预先指定的智能体需要自己决定下一步研究什么是在已有猜想上继续逼近证明还是换一个子问题是去构造更多样例验证模式还是回头怀疑前提本身。这种自选目标的自由度正是“数学发现”区别于“数学解题”的地方。但也正因为如此如果没有外部机制约束自由度会迅速变成失控。1.2 为什么单智能体不够需要分工与制衡我最初觉得一个足够强的模型配上计算工具应该就能完成探索和验证。实际跑下来发现三条硬伤。第一上下文有限。同一个模型既要产生猜想又要验证自己的猜想它的上下文里既有探索过程也有失败记录很快就分不清哪些信息可信。更隐蔽的问题是自我确认偏差模型倾向于说服自己“这个方向是对的”而不是认真否定自己。第二单一视角。同一个模型在同一时刻往往只锁定一种思路。它不会天然地“左手提出一个猜想右手构造一个反例”因为反例会否定自己的产出这在生成逻辑里是反直觉的。第三没有制衡。没有人对假设前提负责没有人追问“这一步为什么成立”。模型给出的每一步看起来都合理但连起来之后整体往往并不成立。多智能体方案的价值就在这里通过角色分离制造“认知温差”。提出猜想的人和验证猜想的人不是同一个减少自我确认偏差验证失败时批判者给出归因探索者修改方向形成真正的闭环。多智能体的意义不是人多力量大而是让不同环节之间保持必要的张力。1.3 这篇文章的主判断先亮明我的判断开放世界多智能体环境中的自主数学发现现阶段真正值得研究的不是“让 AI 独立发表论文”而是把数学探索从“依赖个人灵感的一次性尝试”改造成一个可并行、可复现、可审计的工程流程。这个判断有两层含义。第一层探索本身可以被工程化管理多个智能体并行搜索假设空间每个假设都留有来源记录每次验证都有日志每个结论都能回溯。第二层开放性必须用验证来约束。没有验证的开放产出再多也只是噪音有了验证开放才变成有方向的探索。2. 拆开看一个可落地的多智能体闭环2.1 五个基本角色怎么划分在不同项目里角色设计五花八门但落到数学发现场景通常绕不开五个职能。角色核心职责典型输入典型输出探索者 Explorer生成假设、构造样例、提出子问题当前问题库中的未完成问题候选猜想、实验计划形式化者 Formalizer把自然语言猜想翻译成可验证的形式化断言候选猜想可执行的形式化语句验证者 Verifier运行数值检验、符号计算或形式化证明形式化断言通过 / 不通过 / 反例批判者 Critic对失败和反例分类归因给出修正建议验证失败日志失败原因、修改建议调度者 Orchestrator管理问题队列、记忆库、预算和终止条件各智能体状态下一轮任务分配这里要注意角色是逻辑职责不一定是独立模型。小规模实验里可以让同一个模型扮演不同角色只要在每次调用时明确指示“你现在是批判者只负责找漏洞”并重置上下文即可。等规模变大了再考虑用不同模型或不同温度配置承载不同角色。2.2 多智能体的四种常见交互模式聊多智能体时绕不开“交互模式”这个问题。通常被反复提到的四种是合作式、分工式、竞争式、对抗式。它们不是互斥的更常见的是混用。合作式Cooperative多个智能体共享同一个目标各自负责一部分探索最终把成果合并。适合验证一个猜想的不同分支比如一个负责偶数情况一个负责奇数情况。分工式Collaborative / Role-based按照角色拆成流水线每个智能体只负责一个环节。适合“猜想→形式化→验证→修复”这类顺序明确的流程也是搭建最小闭环时的首选。竞争式Competitive多个探索者独立提出猜想共用同一个验证器拼谁先找到有效结论。适合扩大覆盖面但也容易产生大量重复劳动需要配合去重机制。对抗式Adversarial / Debate一个智能体提出方案另一个专门找漏洞循环攻防。适合打磨证明细节代价是轮次变多、成本上升。实际项目中我建议这样组合探索阶段用竞争式让多个探索者并行覆盖不同思路验证和修复阶段用对抗式让批判者不断对证明过程提出挑战整体串联用分工式保证每个环节的输出格式稳定。2.3 最小闭环流程示意先给一段伪代码展示一个最小可控的主循环。# 伪代码只用于说明流程结构 def main_loop(problem_queue, memory): while not budget.exhausted(): task scheduler.pick(problem_queue) hypothesis explorer.generate(task) statement formalizer.translate(hypothesis) result verifier.check(statement) if not result.passed: reason critic.analyze(result.log) explorer.collect_feedback(reason) memory.save(task, hypothesis, result) scheduler.update_priority(task, result)这段代码的核心思想是每个猜想都必须先翻译成可验证的断言再交给验证器失败后不是直接重试而是先让批判者归因再把归因结果反馈给探索者。没有归因的重试本质上是在同一个坑里反复掉头。如果只是做入门实验不一定要接复杂的定理证明器。可以用一个更轻的验证层对整数猜想随机采样一批数值做反例搜索对代数恒等式用符号化简工具做机械化验证对离散组合命题用枚举或约束求解器做小规模穷举。等这些基础验证都能稳定通过再考虑接入 Lean 这类证明助手做更严谨的形式化证明。3. 为什么验证层才是整个系统的心脏3.1 数学发现的第一原则每个输出都必须可验证在数学发现里“听起来有道理”不是证据。这是整个系统和普通 LLM 应用最本质的区别。普通内容生成场景模型输出一段文字读者自己判断有没有用错误顶多影响理解。数学发现场景不一样一个假猜想如果被当成有效结论写入记忆库就会污染下游所有智能体的推理。更危险的是大模型非常擅长把错误包装得合理它能给一个错误结论配上看似完整的“因为所以”阅读体验越流畅就越容易让人放松警惕。所以验证层不是可选项而是整个系统的信任来源。一个多智能体系统可以没有漂亮的界面可以没有复杂的调度策略但不能没有可靠的验证。哪怕验证方式只是随机数值检验也好过让智能体在对话里自证清白。3.2 验证工具怎么选从轻到重分四档不同的验证工具对应不同置信度选型时要结合问题类型和成本。验证方式适用阶段优点局限随机数值检验探索初期快速筛掉明显错误成本低、速度快只能排除错误不能证明正确符号计算/化简代数恒等式、解析表达式可自动化结果确定适用范围受符号能力限制约束求解/小规模穷举组合、图论、数论反例搜索能发现有效反例规模一大就指数爆炸证明助手形式化验证最终结论的严谨证明推理链可校验形式化成本高对问题表达要求苛刻给一个保守建议先做“三层确认”。第一层随机数值检验目标是排除低级错误第二层符号计算或约束求解目标是发现反例第三层只对通过前两层并且有真实价值的少数候选结论做完整的形式化证明。不要一上来就对所有猜想做形式化证明成本会迅速失控。3.3 验证通过不等于正确必须保留置信度概念即使验证通过了也不能说这就是确定定理。随机数值检验跑一千万个样例通过只能说明“在这些样例里成立”换一个未测试的样例可能立刻失败。符号计算依赖实现库的正确性遇到边界条件可能出现未定义行为。证明助手虽然把推理链拆成了机器可检查的小步骤但前提是自然语言猜想被准确无误地翻译成了形式化语句——这一步恰恰是错误高发区。所以工程上要养成给每个结论标注“验证强度”的习惯只做过数值检验的标记为“候选猜想”通过符号验证的标记为“有效模式”完成形式化证明的标记为“已验证声明”由人工复核过的增加备注。这个标记体系能防止系统在长期运行后把低置信度结论误当成事实使用。我把这一条视为多智能体数学探索系统的数据完整性底线。4. 从单任务到开放世界环境设计的三层约束4.1 “开放世界”不是无限自由而是可变目标空间“开放世界”这个词容易让人误解觉得智能体想干什么都行。实际工程里开放世界指的是问题空间不是预先锁死的智能体可以提出新的子问题可以调整问题边界可以从已有结论中生成新的研究方向。但自由必须被约束。一个完全没有约束的开放环境跑几个小时后会发现各个智能体各自为政有的在重复探索已经被否定的方向有的钻进了无法验证的哲学问题有的产出大量格式混乱的中间结果谁也说服不了谁。自由不配约束成本就是最低效的浪费。4.2 环境分层问题空间、工具空间、评价空间我习惯把环境拆成三个子空间来设计。问题空间决定“什么是合法的问题”。每个候选问题必须满足有明确的研究对象有可判断真伪的断言形式有对应的验证入口。凡是不满足这三条的提议直接回到探索者手里重新表达。工具空间决定“智能体能用什么手段”。包括数值计算器、符号化简库、约束求解器、证明助手工具链等。每次调用工具必须留下入参、出参和执行时间保证可回溯。评价空间决定“什么值得研究”。开放世界里智能体自己提出的问题不一定都有价值。需要用评分机制筛选比如新颖度和记忆库里已有结论的相似度、可验证性是否已经具备验证入口、困难度预期需要多少轮迭代和相关性是否服务于当前研究主线。4.3 探索与利用的平衡防止多个智能体重复劳动开放世界最常见的失控不是智能体不干活而是所有人都在抢同一道题。解决办法是调度者维护一个“问题队列”每个问题记录三个字段当前验证状态、尝试次数、最近一次更新时间。调度者按一个带探索奖励的公式排序而不是简单按问题创建时间排队。一个实用的小方案给每个问题算一个分数等于“已有研究进度 多样性奖励”。多样性奖励和最近 n 轮内研究该问题的智能体数量成反比。某个问题越多人做过下一位探索者去做它的收益权重就越低调度者会更倾向把智能体分配到尚未被充分探索的子问题上。这本质上就是强化学习里 exploration-exploitation 平衡的朴素实现。不一定要用复杂算法简单的计数加权重就能让多智能体系统的覆盖率高出一个量级。5. 落地时最容易踩的六个坑5.1 上下文污染智能体开始相信自己的错误多轮交互之后智能体上下文里可能混入自己之前的失败推理。它会把“我曾经提出过这个思路”误当成“这个思路已经被证明过”然后在新一轮里重复循环。对策是保持任务上下文精简。每轮任务只给当前问题、记忆库中与该问题相关的摘要、以及明确的输出格式要求。不要把所有历史对话都灌进去历史信息放到外部记忆库按需检索。5.2 错误传播一条坏结论污染整棵推理树如果某个验证器因为脚本 bug 返回了错误结果而这个结果被当成“已验证”写进记忆库后续所有智能体都会拿它当依据。对策是给每条结论加上“来源 ID”和“验证强度”。任何新结论必须引用支持它的来源记录。验证器本身也要维护一个健康测试集里面包含若干已知为真和已知为假的命题每次更新验证器后先跑一遍健康测试。5.3 死循环与注意力漂移两个典型故障模式一种是智能体反复提交同一类修改每次只改一个参数然后得到同样的失败另一种是智能体越聊越远从“证明一个数论猜想”漂移到“讨论数学哲学”。对策是两个硬限制。一个是单任务迭代上限比如最多 15 轮超过直接终止并归档。另一个是编辑距离检查如果两次连续的猜想在语义和结构上高度相似说明系统在原地打转强制切换到其他子问题。5.4 成本失控开放世界会把 Token 预算炸穿开放世界 多个智能体 长上下文成本增速是超线性的。很多人跑了一晚上结果烧掉几百美元得到的只是几万条重复日志。对策是给预算做精细控制。每个任务设置 token 预算达到上限自动降级探索阶段用便宜模型只在最终验证和人工复核阶段启用强模型同时定期统计“每验证出一个有效结论的平均成本”把这个指标当成系统健康度的核心观测值。5.5 验证器本身不可靠在数学发现系统里验证器是最后一道防线但它也是一段普通代码可能引入边界错误、类型错误、精度问题。典型例子随机数值检验用浮点数比较遇到大整数时精度溢出把本应成立的等式误判为不成立或者符号化简没有考虑变量定义域在分母为零的边界条件上给出错误结论。对策是给验证器建立“金标准对账集”。挑 20 个已知正确和 10 个已知错误的问题每次验证器改动后跑一遍确保它既能放过正确的也能拦下错误的。验证器可信度是系统可信度的上限。5.6 结果不可复现多智能体系统涉及大量随机采样、模型温度、上下文顺序和工具调用时序任何一个环节不稳定结果就无法复现。数学发现的价值恰恰建立在可复现性上。对策是环境快照。记录模型版本、采样参数、验证器版本、问题队列快照、关键日志。不要嫌麻烦。等真正需要回查一个结论时发现没有版本记录那这个结论就等于没有被验证过。6. 一个可复用的排查链路多智能体系统一旦出问题表象往往五花八门。我建议遵守一套固定的排查顺序不要凭感觉乱调。第一先看现象。是完全没有产出还是产出一堆荒谬结论还是系统陷入循环还是验证结果互相矛盾不同现象指向完全不同的排查方向。第二再看输入。检查问题模板是否清晰工具调用格式是否正确上下文中是否混入了上一轮的噪音记忆库检索返回的字段是否完整。很多“智能体变笨了”的问题其实是输入格式漂移导致模型不知道自己在处理什么。第三再看环境。依赖库版本、证明器版本、API 超时配置、共享目录权限这些都是隐性故障点。尤其要注意并发环境下的共享记忆库写入冲突——两个智能体同时写同一条记录互相覆盖结果就是验证日志和结论对不上。第四再看参数。迭代上限是否设置温度是否过高并发数是否超过承载相似度阈值是否设置合理预算控制是否生效。第五最后才看工具边界。确认当前验证器能不能表达这类命题。如果问题本身就涉及实分析而验证器只支持代数化简那验证失败不是智能体的错是工具选型不匹配。这份排查表可以贴在项目旁边现象优先排查项常见根因多智能体长时间无产出输入模板、工具调用格式工具接口返回异常或问题描述有歧义验证全部失败且原因重复上下文污染、批判者归因逻辑智能体在重复同一条错误路径验证结果互相矛盾验证器健康测试、记忆库并发写并发覆盖导致结论和日志不一致成本远高于预期迭代上限、并发数、模型档位单个任务缺少终止条件或调度器未做去重7. 这个方向真正值得长期关注的原因7.1 它把数学研究变成可控、可追溯的工程流程过去阻碍“AI 参与数学研究”的不只是模型推理能力更是可复现性和可验证性。一个人提出猜想可以通过形式化工具验证但这套流程没有工程化换个环境、换个人、换批数据过程就难以重现。开放世界多智能体系统的真正贡献是让数学探索过程的每一个环节都留痕谁提出了什么猜想依据是什么验证结果如何失败归因是什么最终结论的置信度多高。这些记录合在一起就是一条完整的科研流水线。这件事的长期影响可能比“AI 独立证明定理”更大。它让数学研究从“个人英雄主义”走向“工程化协作”。真正能从这套系统里受益的不只是数学研究者还有所有以推理和验证为核心的知识生产型团队。7.2 适合谁不适合谁适合的人是有数学直觉同时愿意写工程代码的研究者需要大规模探索猜想空间的项目组希望通过大模型做辅助猜想但不打算放弃人工判断的团队。不适合的人是指望完全替代人类数学家的工作流没有可靠的验证机制却想直接生产“新定理”的方案以及预算有限又强行追求全量形式化验证的团队。对最后这一类我的建议很直接先投入资源把验证基建做扎实再谈开放世界。7.3 下一步最该先做什么如果今天你想复现一套这样的环境我的建议是不要一上来就追求“开放”。第一步选一个封闭的、验证手段明确的小问题比如某个恒等式族或某个组合计数模式。第二步先把“探索者→形式化者→验证者→批判者→调度者”的最小闭环跑通跑出至少 100 条有效记录。第三步再做两件事一是把记忆库和日志系统建好确保每条结论都能追溯到源头二是给验证器建立金标准对账集。这两件事做完才真正具备“放开问题空间”的条件。最后想再强调一次开放世界是这套系统的引擎验证层是方向盘。先把方向盘装稳再踩油门。