开放世界多智能体自主数学发现系统设计与实践 开放世界多智能体环境中的自主数学发现简单说就是让多个 AI 智能体在一个可持续交互的虚拟环境里自己探索、提出数学猜想、互相反驳最后沉淀出可验证的数学结论。它不像传统刷题系统那样有标准答案也不像强化学习那样只追固定奖励而是把“发现过程”本身当成目标。适合对多智能体系统、AI4Math、自动定理发现感兴趣的人读。下面会拆清楚环境怎么设计、智能体角色怎么分工、正反博弈加裁判的机制怎么落地也会列出在实际搭建这种系统时容易踩的坑和排查顺序。最值得关注的是这套思路可以复用到很多非数学场景比如代码生成、配方搜索、策略挖掘核心都是同一个“提出-反驳-验证”循环。1. 先定义清楚它到底是在做什么不是做什么1.1 从“发现”而不是“解题”出发“自主数学发现”和常见的数学解题 AI 有很大区别。解题 AI 面对的是已经整理好的题目输入、输出、评分标准都明确模型只需要在有限步骤内找到答案。自主数学发现的目标不是做一道题而是让智能体在环境里主动找到隐藏的规律比如“任意两个素数的平方差有什么特征”“某种网格路径上是否永远存在至少一条不经过障碍的走法”。这类问题没有现成题库甚至没有预先定义的正确答案。这意味着系统设计要反过来。普通任务先给目标再让模型推理自主发现系统先给环境再让智能体自己决定下一步探索哪里。判断系统好坏的标准也变了不是单次回答正确率而是能否持续产生有意义的新命题、能否通过反驳去除错误结论、能否把零散发现整理成可用的引理库。所以搭建这类系统时不要一上来就堆大模型。先想明白你要的是“发现能力”还是“解题能力”。如果只是希望模型能做一些数学证明题那不需要开放世界也不一定需要多智能体。真正需要开放世界的场景是当数学规律藏在大量可交互对象和状态变换里单靠文本推理抓不住的时候。1.2 开放世界带来的情报不完整和交互自由开放世界环境有三个特征状态空间大、信息不完整、行动会影响后续观测。这和传统机器学习里的固定数据集差别很大。固定数据集把样本提前切好模型只能被动读取开放世界则允许智能体主动移动、组合对象、施加操作然后观察结果。比如一个二维网格世界里面散布着不同颜色的数字块智能体可以移动、合并、相邻比较从而发现“某些颜色块之间差的奇偶性有规律”。正是这种交互自由才让数学发现有了“自主”的味道。智能体不需要靠记忆硬凑关系而是可以自己制造新样本。一个智能体提出“红色块和蓝色块的数量差总是偶数”另一个智能体可以主动构造一个红块和蓝块数量差为奇数的环境状态来反驳它。如果没有行动自由反驳者也造不出有效反例整个发现过程就会退化成纯文本猜测。但开放世界也带来麻烦。环境状态一旦太大智能体容易迷失。比如网格是 100x100每个格子有多种属性那观测空间可能达到几万个 token。这时候需要设计信息摘要和采样策略让智能体每次只关注一小块有代表性的局部区域而不是让它一次性看完整张地图。1.3 这条路线适合谁想动手做这个方向的人需要具备三块基础一是熟悉至少一种大模型调用方式因为提出者和反驳者通常由 LLM 充当二是能写一点环境交互代码至少会封装“观察-行动-反馈”的循环三是对数学证明有基础直觉能分辨什么算有效反例、什么算无关约束。如果完全没有编程经验建议先别碰多智能体把单 Agent 在数学环境里做一轮探索跑通再扩展。如果只是对“多智能体合作”感兴趣但不想碰数学也可以把下面的机制迁移到其他开放世界任务里。重点不是数学符号而是提出、反驳、验证这条通用链路。2. 环境怎么搭把数学关系放进可探索的沙盒2.1 为什么不能用固定题目集代替开放环境很多人会问既然目标是发现数学规律为什么不直接给模型一堆数值对让它回归因为固定题目集只能验证已知模式很难发现未知结构。当你知道要输入哪些数据、输出哪些指标时其实已经预设了问题形式。开放环境的意义在于让智能体连“该看什么特征”都能自己决定。举个例子你想让智能体发现“正整数的约数和”的变化规律。如果直接给一个表格列出一堆 n 和 σ(n) 的值模型很容易去做函数拟合但很难想到“这个规律可能和质因数分解有关”。放在开放环境里可以让智能体把整数拆成质因数块组合两个整数并观察约数和的变化它会自然生成更多候选关系奇偶性、整除性、倍数关系、互质条件。这些候选很多是错的但正是试错过程让发现有了深度。所以环境设计的核心不是“模拟真实世界”而是“把数学对象的操作过程具象化”。你可以构建一个小宇宙里面的对象是数、图形、集合行动是组合、拆分、比较、映射反馈是布尔判断或者数值变化。环境越抽象越容易聚焦数学规律。2.2 三种数学任务的沙盒化映射常见数学任务可以分成三类适合用不同沙盒来承载任务类型典型问题沙盒示例智能体主要操作数论质数、整除、同余、数列规律正整数长廊数字可拆分质因数取相邻数做差、求最大公约数、合并倍数离散几何格点路径、凸包、覆盖率二维网格放置障碍物和目标点画线、移动点、包围格点、统计交点代数/组合括号匹配、排列逆序数、递推关系符号串环境支持替换和重排生成新串、交换位置、计算逆序对我建议第一次实验先选数论因为验证成本最低。一个命题是否正确往往可以通过遍历有限范围快速判断。离散几何更直观但反例构造需要比较精确的坐标计算调试起来麻烦。符号串任务则要小心语法错误智能体很容易生成无意义的表达式浪费大量轮次。2.3 观测空间与行动空间的设计原则观测空间决定智能体“看到什么”行动空间决定它“能做什么”。设计观测空间时一定要给智能体提供结构化摘要而不是原始状态全量输出。比如网格世界中可以输出“当前区域的颜色分布图”“最近 20 次合并操作的结果”“当前候选命题已验证样本数”等这样 LLM 才能在不超长上下文的情况下做决策。行动空间要小但够用。不要一次性开放 50 种操作智能体根本记不住。我更建议按阶段开放探索阶段只开放移动、观察、采样。生成阶段开放组合、比较、记录候选命题。验证阶段开放构造反例、运行检查器、标记已证结论。这个阶段划分能让智能体不要过早陷进局部搜索。行动数量控制在 5 到 10 个之间比较合适。动作不是越多越好而是越明确越好。用自然语言描述动作时也要统一句式比如“sample_objects(n)”“merge(a,b)”“check_parity(x)”避免模型因为表达歧义而乱调用。3. 智能体角色提出者、反驳者、裁判缺谁都不行3.1 正反博弈裁判为什么比单个 Agent 更稳单个 LLM Agent 做数学发现时经常会自我确认。它提出一个猜想自己抽样验证几次发现没问题就把它当成结论写进输出。问题在于大模型生成验证代码时很容易用同一种思路选择样本导致反例被系统性地漏掉。两个 Agent 分开后情况会好很多提出者负责构建可能的规律反驳者专门负责破坏这个规律。因为反驳者的目标是找反例它会主动构造极端情况、边界条件、特殊输入而不是像提出者那样倾向于验证成立样本。但只有对抗会带来两个问题。一是反驳者可能为了“赢”而伪造假证据比如用不完整的数值枚举冒充反例二是提出者可能因为连续被反驳而变得保守不敢提出有难度的猜想。这时候需要第三个角色裁判。裁判的职责是裁决反例是否合法、候选命题是否被充分验证、有没有资格进入知识库。裁判不参与对抗它只做规则执行和证据审查。所以“正反博弈裁判”的结构本质是一边生产假设一边生产挑战制造者对所有结论做最终把关。这个结构不只在数学发现里有用在代码生成、策略搜索里同样有效。与其说它是多智能体协作范式不如说它是一套可控的假设检验流程。3.2 三个角色的职责和提示词示例以数论沙盒为例三个角色的提示词可以这样设计。提出者你是数学探索者。你可以观察环境中的数字对象提出一个可能成立的数学命题。 要求命题必须可验证尽量具体不能只写“存在某种规律”。输出格式 命题... 依据你观察到的样本 建议验证范围正整数 1 到 500反驳者你是反例猎手。你会收到一个数学命题你的目标是构造一个让命题不成立的环境状态或数值组合。 要求必须调用环境检查器不能伪造结果。输出格式 攻击点... 构造方式... 验证结果...裁判你是数学裁判。你负责审查提出者的命题和反驳者的反例。 判断标准 1. 命题是否表达清晰 2. 反例是否真正覆盖命题的适用条件 3. 如果反例有效命题应被拒绝 4. 如果反例无效需要说明原因。 输出accept / reject / insufficient实际使用时不一定要把提示词写这么长但职责边界要清楚。尤其是裁判绝不能让它直接相信反驳者的文字结论一定要让它看到原始验证日志。3.3 核心代码骨架一个带裁判的发现循环下面给出一段可以在本地跑通的简化骨架省略了具体环境实现但完整展示了三个角色的交互关系。# discover_with_referee.py 核心循环简化版 from dataclasses import dataclass, field from typing import List dataclass class Candidate: statement: str proposer: str evidence: List[str] field(default_factorylist) class MathWorld: 开放世界沙盒维护对象、可执行操作和检查器 def sample_objects(self, n10): # 返回 n 个数学对象例如整数、点坐标、方程组 pass def check(self, statement: str, sample_space) - bool: # 在指定样本空间内验证命题返回是否成立 pass def construct_counterexample(self, statement: str, hint: str): # 根据提示构造可能的反例 pass class ProposingAgent: def observe(self, world) - str: # 返回环境摘要 pass def propose(self, observation: str) - Candidate: # 调用 LLM返回 Candidate pass class RefutingAgent: def attack(self, candidate: Candidate, world) - dict: # 调用 LLM尝试构造反例 # 返回 {counterexample: ..., log: ..., success: bool} pass class JudgeAgent: def verify(self, candidate: Candidate, attack: dict, world) - str: # 调用 LLM结合攻击日志和 world.check 结果做裁决 # 返回 accept / reject / needs_more_examples pass def discover(max_rounds100, target_pool10): world MathWorld() proposer ProposingAgent() refuter RefutingAgent() judge JudgeAgent() accepted [] for round_id in range(max_rounds): observation world.sample_objects(20) candidate proposer.propose(observation) attack refuter.attack(candidate, world) verdict judge.verify(candidate, attack, world) if verdict accept: accepted.append(candidate) world.note_lemma(candidate.statement) if len(accepted) target_pool: break return accepted这段代码不是成品环境而是一个可扩展框架。实际落地时你需要把 MathWorld 实现成具体环境并在三个 Agent 内部调用大模型接口。建议先跑通这个骨架再逐步加入候选池去重、结果缓存、失败日志等机制。3.4 角色数量不是越多越好可能有人会想既然三个角色效果不错那再加一个“评论者”“监督者”“总结者”会不会更好。实际表现往往相反。角色越多上下文越长任务延迟越高角色之间互相干扰的概率也越大。一个角色漏看信息后面所有环节都会受到污染。我更建议先保证三个角色的质量而不是拼数量。如果一定要扩展可以考虑给反驳者增加多个“攻击风格”比如“边界值攻击”“极端组合攻击”“随机搜索攻击”这是在一个角色内部做并行而不是新增独立 Agent。这样既保证了多样性又不会让职责边界变得混乱。4. 从环境观察到结论沉淀自主发现的标准动作4.1 探索采样先让环境先生成足够多样的事实自主发现的第一步不是让智能体直接写猜想而是采样。采样的目的是让环境状态覆盖更多情况。常见做法是先用随机策略跑一段探索让智能体生成一批包含不同数字范围、不同几何构型、不同符号组合的样本。采样阶段不需要太多智能体参与一个探索者就够。关键是多样性指标。比如数论环境里样本必须同时包含奇数、偶数、质数、合数、大数、小数网格环境里样本必须包含空旷区域、障碍密集区域、边界点、临近重叠的图形。如果样本分布偏了后面提出的猜想一定会偏。我一般会在采样后加一个去重步骤。用一个哈希函数记录已见过的样本特征重复样本直接丢弃。这样可以避免反驳者反复拿同一类反例攻击导致裁判误以为命题已经很稳。4.2 候选生成把观察转成可测试的命题当环境积累了一定样本提出者开始生成候选。生成命题时要同时带上“依据样本”和“建议验证范围”。这两个字段非常重要。没有依据样本裁判无法判断提出者是不是在空想没有验证范围反驳者不知道应该去哪里找反例。例如一条候选命题命题任意两个不同的奇质数 p 和 qp^2 - q^2 一定能被 8 整除。 依据样本3 和 5差为 167 和 11差为 7213 和 17差为 120。 建议验证范围100 以内的奇质数对。这条命题的表述就足够干净。后续反驳者可以直接构造 p3, q7发现 9-49-40也能被 8 整除说明目前没问题。它也可以构造 p3, q2 但 2 不是奇质数因此不适用。这种边界测试能帮助精炼命题。如果提出者输出了过于模糊的命题比如“质数之间有很多有趣关系”裁判应该直接拒绝并要求提出者重写。这相当于设了一个质量门槛避免后面几轮浪费算力。4.3 反驳攻击反向样本比正向例子更重要反驳者要做的不是随便测几个数而是有策略地寻找反例。常用的攻击策略包括小值边界p2q3几乎所有命题都可能在边界出错。缺失条件直接输入不符合假设前提的样本看命题是否错误泛化。构造偏移把数值放大到超大范围测试是否出现溢出或规则失效。重复组合同一个对象重复使用例如要求两个不同质数但让 q 等于 p。每一条攻击尝试都必须生成可复现日志记录输入对象、调用操作、输出结果。裁判需要看这些日志而不是只看反驳者的总结。很多系统出错就是因为反驳者口头说“找到一个反例”但代码里根本没有这条日志。如果反驳者连续多轮攻击失败说明候选命题可能比较可靠。但也不要立刻接受可以让裁判再发起一轮“压力测试”扩大验证范围。这个压力测试可以由裁判调用一个穷举脚本在小范围内检查所有可能组合。你会发现这一步能拦住大量“看起来对但只是没撞到反例”的伪猜想。4.4 裁判验证和知识入库当一条命题通过反驳者的攻击并扩大验证后裁判会决定接受它。接受后不能直接扔进最终列表要有一个知识入库动作。入库内容包括完整命题文本、提出者记录、反例攻击记录、验证范围、验证时间、抽样方法。这份记录既是为了追溯也是为了让后续智能体能基于已接受的引理继续探索。知识库最好用结构化文件保存例如 JSON 或 SQLite。每次入库前检查是否和已有结论冲突。如果新结论和旧结论矛盾需要触发一次裁判回溯重新评估旧结论。这个过程很麻烦但避免了知识库内部不一致。4.5 一轮典型成功的输出长什么样跑完一轮实验后你应该看到一个类似下面的结果[ { statement: 任意两个不同的奇质数 p 和 q 的平方差能被 8 整除, status: accepted, evidence_count: 120, counterexamples_tried: 45, proof_or_validation: p^2-q^2(p-q)(pq)因为 p,q 为奇数p-q 和 pq 都是偶数且其中一个能被 4 整除所以乘积能被 8 整除, creator: proposer_v1, created_at: 2025-01-01T12:00:00Z } ]这里的 proof 字段不一定是形式化证明可以是对数学结构的解释。如果只是通过有限验证状态不能用 accepted应该用 “verified_in_range”。这个细节很关键它决定了知识库的可信度。很多自主发现系统最后被质疑就是因为把有限验证写成了全部证明。5. 实测最容易踩的五个坑5.1 智能体在环境里空转半天提不出新命题如果跑了 50 轮提出者还在生成“数字之间有关系”“质数很特殊”这种废话问题通常出在观测信息太稀薄。它看到的只是 20 个随机数字没有提示数字之间可以发生什么操作。解决方法是把环境摘要写得更结构化比如直接给出“这组样本中奇数和偶数的比例是 3:7质数共有 2 个相邻数字差的最小值是 1最大值是 15”。这样提出者就能沿这几个特征去生成命题。另一个原因是温度设置过低。探索阶段可以把采样温度调到 0.8 左右让提出者放开一点。一旦它提出一个初步命题后续规范化成候选时再调低温度。5.2 反驳者用“伪反例”骗过裁判这是最隐蔽的坑。反驳者声称找到了反例但它实际上是在符号表达式里做了手脚比如把两个变量当成同一个变量或者偷偷改了前提条件。裁判如果不仔细看日志很容易被蒙混过去。针对这个问题我建议在裁判提示词里加入强制规则必须检查反例对应的所有输入参数是否符合命题前提。同时在代码层面每次调用反例验证时把命题语句和反例对象传给一个独立检查函数只有检查函数返回 False才允许裁决为 reject。也就是说裁判只能基于第三方检查结果做最终判断而不是基于反驳者的叙述。5.3 环境任务和自然语言描述不一致有时候提出者输出的是“两个相邻质数的差的绝对值是偶数”但环境理解里“相邻”指的是数字相邻而不是质数序列中的相邻。这种不一致会浪费大量轮次。解决办法是在环境里维护一份“术语表”把每个自然语言词条绑定到唯一操作。比如“相邻”分别定义为consecutive_numbers和consecutive_primes两种操作让提出者在命题里明确指定操作名称。这一步虽然增加了一点输入长度但能显著减少歧义。5.4 候选池膨胀递归引用把自己绕晕当知识库越来越大提出者可能会说“由引理 A 和引理 B可以得到命题 C”但引理 A 本身还未被验证或者引理 B 已被新反例推翻。这种递归依赖会让系统进入混乱。我建议引入状态标签每条知识只能处于hypothesis、verified_in_range、proved、rejected四种状态之一。提出者引用知识时只能引用proved或至少verified_in_range的条目。裁判最终接受一条新结论时必须把依赖链也写进元信息。一旦某个依赖被推翻所有下游结论立刻标记为suspended重新审查。5.5 排查顺序先环境、再角色、再参数遇到问题不要乱猜。我一般按固定顺序排查先看环境检查器是否有 bug。用十条人工标注的命题跑一遍看 check 函数是否返回正确。再看日志完整性。确认每个角色的输入输出是否有记录是否有多处没有写到日志的隐藏调用。再看提示词边界。检查提出者是否经常越权反驳者是否引用外部知识。最后调参数温度、候选池大小、最大轮数、采样空间范围。顺序不能反。很多团队一上来就调大模型参数结果发现是环境里的整除函数写错了白白浪费大量时间和 token。6. 边界、算力和后续扩展6.1 低配机器能跑到什么程度如果只是做一个小型实验目标是验证“两个数之间的某种整除规律”那么单张普通显卡甚至只有 CPU 也能跑。因为每个提案只是调一次大模型接口环境检查器负责真正的数学计算计算量不大。限制主要来自采样空间和验证范围。如果验证范围到达几百万检查器会变成瓶颈。低配环境建议这样做样本空间控制在 500 以内候选池不超过 30 条最多跑 50 轮探索。先把流程跑通再逐步扩大。不要一上来就追求发现复杂定理那是大型集群和长时间任务该做的事。6.2 发现成功不代表证明成立这是最容易给人误导的地方。自主发现系统能发现“某个范围内成立”的规律不代表它已经完成了数学证明。比如在 1 到 1000 范围内验证了某个命题它依然可能在 1001 处失效。因此系统输出结论时必须区分“猜测”和“定理”。如果没有给出一段形式化证明我只能把它称为“强启发式猜想”。想让系统输出正式证明需要叠加一步证明搜索模块。这个模块可以是基于规则的自动证明器也可以继续用多智能体做证明尝试。但要注意证明搜索的难度比发现高很多。设计系统时最好把发现服务和证明服务拆成两个独立管道避免一个环节卡住拖垮整个流程。6.3 把数学发现框架迁移到代码和策略生成我在前面提到过这套“提出-反驳-裁判”框架不局限于数学。你完全可以在代码生成任务中使用生成者写出一段函数测试者构造边界输入和极端输入裁判根据单元测试和代码覆盖率决定是否接受。这里的“开放世界”就是函数运行环境和测试用例空间。迁移时注意不要照搬数学环境里的验证函数。代码环境需要处理运行超时、异常、资源消耗等额外问题。数学环境的检查器快速且确定代码环境的执行则可能产生副作用。所以要在环境层加入沙箱机制控制输入大小和运行时间。6.4 长期维护该盯住哪些东西如果要把这个系统当长期工具用日志和知识库就是核心资产。每一轮探索的输入、输出、攻击日志、裁判结论都要落盘。不要只保存最终发现列表因为后续你可能会回溯某个结论为什么被接受涉及哪些依赖。另外定期清理无效候选也很重要。候选池里堆满被拒绝的命题后会干扰提出者的探索方向。你可以每周跑一次聚合分析统计被拒绝率最高的命题类型和反驳者最常用的攻击模式这些数据能直接指导环境设计。如果让我重新做一次这样的系统我会先把环境缩小到单个规律比如“奇质数平方差整除性”用三个角色跑通 20 轮确认所有日志完整再开放更大的探索空间。先把整个链路跑稳再去追求“发现新定理”的惊喜感。开放世界多智能体数学发现这件事真正难的不是让智能体多想一步而是让整个系统在成千上万次探索里保持可信、可追溯、不崩溃。能做到这一点就已经比大多数 demo 往前走了很远。