多智能体是最近一年讨论度最高的 AI 方向之一但大多数讨论都停留在“多个大模型角色扮演、轮流发言、最后生成报告”的层面。这种用法并非没有价值却没有触及多智能体最独特的能力让多个拥有不同目标的智能体互相竞争通过可验证的反馈逼近正确结论。数学发现恰好是这一能力最好的试金石因为数学结论不依赖“谁说得更有道理”只依赖严谨的证明或反例。我的判断是自主多智能体数学发现的真正突破口不是模型数量变多而是“生成—反驳—仲裁”的认知分工。其中“正反博弈 裁判”是最值得关注的一种实现形态。该系统由一方负责提出数学猜想另一方负责寻找反例裁判负责验证反例是否真实有效。它并不一定马上推翻哪条已知定理但会系统性地挑战一种更深层的共识AI 只能模仿人类数学不能在数学发现中扮演主动角色。这篇文章会从开发者的视角讲清这套机制并用一个可运行的最小 Python 框架演示完整流程。你会看到多智能体如何从局部数据中提出公式如何在更大范围搜索反例以及为什么“裁判必须用可计算、可验证的规则仲裁而不是让模型投票”是工程上最重要的一条原则。1. 这篇文章真正要解决的问题很多开发者在尝试多智能体项目时会遇到一个尴尬的情况智能体之间讨论得热火朝天但最终结论的质量并没有明显提高。原因在于多数框架只解决了“多角色对话”的问题没有解决“结论如何被验证”的问题。对话可以掩盖不确定性数学却不能。数学发现天然具备三个特征结论可验证、反例可构造、证明过程可审计。正因如此它是检验多智能体系统是否真正“自主”的理想场景。与写营销文案、生成代码片段不同数学结论无法用“模型置信度”或“投票多数”来证明。一个猜想只要存在一个反例无论多少智能体赞同它结论都是错的。这逼迫设计者把验证环节做成系统的一等公民而不是最后加一个“总结器”。这篇文章要解决的核心问题是当多个智能体协作进行数学探索时如何设计它们的角色关系才能让最终结果可信、可复现、可控制文章给出的答案是“正反博弈 裁判”架构提议者负责生成猜想批评者负责攻击猜想裁判负责验证攻击是否成立。这套架构看似简单内部却包含责任分离、验证权威和终止条件等工程细节。无论你是想构建一个数学猜想辅助系统还是想把多智能体方法引入科研自动化这篇文章都能提供一套可直接运行的基线实现并指出真实落地中容易踩的坑。2. 基础概念与核心原理开始写代码之前需要先把几个容易被混淆的概念说清楚。智能体Agent在本文语境下指能够感知输入、做出决策并执行动作的独立计算单元。它不一定是大模型也可以是一个符号计算函数、一个搜索程序或一个规则引擎。智能体的核心特征是“自主”在给定目标后它可以自行决定下一步动作。多智能体系统Multi-Agent System是由多个智能体共同组成的系统。这些智能体之间可能存在协作、竞争、分工或博弈关系。多智能体系统之所以有价值不是因为“人多力量大”而是因为不同智能体可以持有不同视角彼此纠错。单智能体在数学推理中的主要问题是单向思维它沿着一条推理路径前进遇到反例时缺少主动对抗的机制。多智能体解决方案则把“提出观点”和“挑战观点”分成两个角色迫使系统从两个方向逼近问题。正反博弈在这里指一类机制一方智能体尽量提出有说服力的数学命题另一方智能体尽量找出该命题的漏洞或反例。这种对抗能让系统暴露局部假设的脆弱性。它的思想与生成对抗网络有相似之处但验证目标完全不同。GAN 的判别器学习真伪样本的统计差异数学发现中的反方则需要构造出严格的、可以被独立验证的反例。裁判Judge / Verifier是整个架构中最关键的角色。裁判不负责提出猜想也不负责寻找反例只负责判定反方给出的反例是否真正推翻了正方的命题。在理想情况下裁判不依赖大模型的“感觉”而是依赖符号计算、定理证明器或确定性的数值验证。只有裁判足够严格整个系统才不会变成一场“诡辩大赛”。数学发现的概念也需要界定。本文讨论的数学发现不是指“证明一个教科书定理”而是指一个更开放的过程从观察数据或已有结论中生成候选模式验证模式是否成立如果成立则给出解释如果不成立则构造反例。这个过程中“反例”本身就是重要成果。数学史上不少共识正是被反例推翻的。例如表面上看某个公式连续生成很多素数容易让人误以为它永远生成素数但扩大验证范围后就能发现反例。这就是“局部共识”的脆弱性。3. 为什么“正反博弈 裁判”是多智能体数学发现的关键模式一个常见的误区是只要把多个大模型 Agent 串在一起让它们轮流发言就能自动获得更好的数学推理能力。实际上松散对话产生的多智能体系统只是一个“多角色语境窗口”并不会自然形成纠错能力。要让系统真正可靠必须引入对抗性反馈和确定性仲裁。数学家的工作方式本质上就是正反博弈。一个人通过归纳或类比提出猜想另一个人通过构造反例尝试推翻它如果反例有效猜想被修正或被放弃如果找不到反例数学家会尝试证明。这个过程是长期的、动态的。多智能体系统把这一过程显式建模为三个角色正方Proposer负责从已知数据中提炼候选模式生成可检验的公式或命题。反方Critic负责在更广泛的空间中搜索反例挑战正方命题的普适性。裁判Judge负责验证反例是否成立并维护实验过程的完整记录。为什么需要至少三个角色而不是两个因为“提出观点”和“验证观点”如果由同一方完成系统会陷入自我验证的偏见。裁判一旦也是反方就会为了“找出问题”而过度解读裁判一旦也是正方就会为了“维护成果”而降低标准。独立的裁判角色保证了最终裁决具备更强的客观性。“正反博弈 裁判”另一个优势是可插拔性。正方和反方可以使用大模型裁判则可以使用符号计算引擎或定理证明器。这意味着系统的验证能力不依赖于模型的“口才”而是建立在可计算的规则上。对于数学发现这种高风险场景这是必要的架构选择。从生成对抗网络到 RLHF 中的奖励模型对抗与仲裁的思想已经在机器学习中反复出现。数学发现场景的特殊之处在于裁判有机会做到完全精确一个整数反例一个公理体系内的证明都可以被独立程序验证。这正是多智能体系统最接近“可证明正确”的场景。4. 一个最小可运行的多智能体数学发现框架为了把上面的概念落地我设计了一个最小沙盘项目。它不会真的去挑战黎曼猜想但完整展示了“正反博弈 裁判”的流程。4.1 环境准备与前置条件本文示例基于 Python重点依赖sympy做符号计算与素数判定。环境准备如下Python 3.9 或更高版本。pip包管理器。操作系统不限Linux、macOS、Windows 均可。建议使用虚拟环境隔离依赖。依赖文件requirements.txtsympy1.11安装命令pip install -r requirements.txt版本号请以实际安装为准。这里选择sympy而不是完全自己实现符号运算是为了让代码更短、更可靠同时保证裁判具备独立的数学计算能力。4.2 场景设计我们使用一个经典数学现象作为演示多项式f(n)n^2n41在n0到39范围内都生成素数因此很容易让人误以为它对所有非负整数都生成素数。但事实上当n40时f(40)168141^2已经不再是素数。沙盘系统的目标是模拟一个“受局部观察引导”的发现过程系统观察到n0..9时f(n)的值都是素数这是一个局部的朴素共识。正方智能体根据观测点拟合出候选公式其中一个候选就是n^2n41。反方智能体从n10开始扩大范围搜索反例最终在n40处找到反例。裁判验证并记录结果判定这个局部共识被挑战。需要说明的是这里不存在神秘的“神谕”。系统在初始观测中只知道“这些值是素数”并不知道背后的完整公式。候选公式是通过符号插值生成的反例则通过独立计算素数性来发现。4.3 完整代码实现下面是一个完整的 Python 文件可以直接保存为math_agents_sandbox.py。代码包含三个智能体角色并在主流程中运行一轮完整博弈。 math_agents_sandbox.py 最小多智能体数学发现沙盘 使用“正反博弈 裁判”架构自动验证一个局部的素数公式猜想。 from itertools import combinations from typing import Dict, List, Optional, Tuple import sympy as sp x sp.Symbol(x, integerTrue) def collect_observations(start: int 0, end: int 10) - List[Tuple[int, int, bool]]: 模拟科学观察收集 nstart..end-1 时 n^2n41 的值及其是否为素数。 真实场景中这一步由实验数据或已有计算结果提供。 observations [] for n in range(start, end): value n * n n 41 observations.append((n, value, sp.isprime(value))) return observations class ProposerAgent: 正方智能体根据局部观测数据提出候选数学公式。 这里的启发式策略是在观测点中选取不同的三元组用二次插值生成多项式。 二次插值会产生很多过拟合公式所以最后通过观测点残差排序保留误差最小的三个。 def __init__(self, observations: List[Tuple[int, int, bool]]): self.observations observations def propose(self) - List[sp.Expr]: points [(n, value) for n, value, _ in self.observations] candidates [] # 在观测点中枚举三元组生成二次插值多项式 limit_points points[: min(len(points), 8)] for subset in combinations(limit_points, 3): poly sp.expand(sp.interpolate(list(subset), x)) candidates.append(poly) if len(candidates) 12: break # 去重 unique_candidates [] seen set() for expr in candidates: key sp.srepr(expr) if key in seen: continue seen.add(key) unique_candidates.append(expr) # 计算每个候选公式在所有观测点上的总误差误差越小越可信 scored [] for expr in unique_candidates: error 0 for n, value, _ in self.observations: error abs(int(sp.simplify(expr.subs(x, n))) - value) scored.append((error, expr)) scored.sort(keylambda item: item[0]) return [expr for _, expr in scored[:3]] class CriticAgent: 反方智能体在更大的范围内搜索反例。 这里检验的性质是“由公式生成的值是否仍然是素数”。 只要在搜索范围内找到一个非素数值就返回一个可验证的反例。 def __init__(self, search_start: int, search_end: int): self.search_start search_start self.search_end search_end def find_counterexample(self, expr: sp.Expr) - Optional[Dict[str, object]]: for n in range(self.search_start, self.search_end 1): value int(sp.simplify(expr.subs(x, n))) if not sp.isprime(value): return { n: n, value: value, factorization: sp.factorint(value), } return None class JudgeAgent: 裁判智能体验证反方找到的反例是否有效并维护判定记录。 裁判不提出猜想也不主动找反例只做确定性仲裁。 def __init__(self): self.records: List[Dict[str, object]] [] def judge(self, expr: sp.Expr, counterexample: Optional[Dict[str, object]]) - str: if counterexample is None: verdict not_refuted else: # 裁判独立验证反例中的 value 不是素数 value int(counterexample[value]) if not sp.isprime(value): verdict refuted_by_counterexample else: verdict invalid_counterexample self.records.append( { expr: str(expr), counterexample: counterexample, verdict: verdict, } ) return verdict def main() - None: # 第 1 步收集局部观测 observations collect_observations(0, 10) print(局部观测n0..9 时f(n)n*nn41 均为素数。) print(观测点, [(n, v) for n, v, _ in observations]) print() # 第 2 步正方提出候选公式 proposer ProposerAgent(observations) candidates proposer.propose() print(正方 Proposer 提出的候选公式) for idx, expr in enumerate(candidates, start1): print(f 候选 {idx}: {expr}) print() # 第 3 步反方搜索反例 critic CriticAgent(search_start10, search_end200) judge JudgeAgent() for idx, expr in enumerate(candidates, start1): counterexample critic.find_counterexample(expr) verdict judge.judge(expr, counterexample) if verdict refuted_by_counterexample: print( f反方 Critic 找到反例候选 {idx} ({expr}) 在 n{counterexample[n]} f时取值为 {counterexample[value]} f因数分解为 {counterexample[factorization]}。 ) print(f裁判 Judge 判定{verdict}局部共识被挑战。) elif verdict not_refuted: print(f候选 {idx} ({expr}) 在搜索范围内未找到反例。) print(裁判 Judge 判定当前搜索范围内暂时成立。) else: print(f候选 {idx} 的反例无效。) print() # 第 4 步输出裁判结论 print( 裁判结论 ) print(系统从有限观察中提出了‘该公式持续生成素数’的候选共识。) print(但通过扩大搜索范围反方在 n40 处构造了反例1681 41 * 41。) print(这说明有限归纳只能提供启发式线索不能替代全局验证。) print(在本沙盘中多智能体协作成功挑战了一个基于局部数据的朴素共识。) print() print(最终判定记录) for record in judge.records: print(f - {record[expr]}: {record[verdict]} | {record[counterexample]}) if __name__ __main__: main()4.4 关键逻辑说明ProposerAgent是系统中的“创造者”。它不知道真实函数只知道观测点上的数值。通过枚举不同三元组做二次插值它生成多个可能的多项式再用观测点残差进行排序。这样系统既保留了一定随机性又能自动选出拟合效果最好的公式。插值公式中存在大量过拟合这是符合现实的任何有限数据都支持无穷多个假设关键在于后续的验证环节。CriticAgent是系统中的“怀疑者”。它在更大的范围内逐一计算候选公式的值并判断这些值是否为素数。只要找到一个非素数值就返回反例。这个阶段刻意选择独立判定而不是让模型“判断是否像一个反例”。JudgeAgent是系统的“仲裁人”。它不负责创造也不负责搜索只负责最终验证。如果反方返回了一个反例裁判会独立计算数值并检查素数性。如果反方没有找到反例裁判只给出“当前搜索范围内未推翻”的保守结论绝不将其推广为“永远成立”。主流程将三者串起来形成完整闭环观察数据 → 提出猜想 → 攻击猜想 → 仲裁结论。这个闭环看起来简单却是很多多智能体项目缺失的部分。5. 运行结果与效果验证运行沙盘程序python math_agents_sandbox.py如果依赖已经安装输出会接近下面的内容局部观测n0..9 时f(n)n*nn41 均为素数。 观测点 [(0, 41), (1, 43), (2, 47), (3, 53), (4, 61), (5, 71), (6, 83), (7, 97), (8, 113), (9, 131)] 正方 Proposer 提出的候选公式 候选 1: x**2 x 41 候选 2: 3*x**2 - 9*x 41 ... 反方 Critic 找到反例候选 1 (x**2 x 41) 在 n40 时取值为 1681因数分解为 {41: 2}。 裁判 Judge 判定refuted_by_counterexample局部共识被挑战。 ...判断运行成功的关键标志是反方能够在n40处找到非素数值1681裁判判定反例有效。这说明正反博弈的反馈回路是通的验证不是走形式。1681不是素数因为168141^2。表面上前十个观测值全部是素数这很容易形成“该公式永远生成素数”的直觉。但多智能体系统通过主动扩大搜索范围快速找到了反例。这正是数学发现中最朴素也最重要的动作不要轻信局部模式。需要特别强调的是这个沙盘中的“反例搜索”只是数值验证并不能证明某个候选公式对所有更大的 n 都成立。如果反方在给定范围内没有找到反例只能说明“还没发现反例”不能说明“没有反例”。真实数学发现需要把裁判从isprime升级为定理证明器或者要求给出严格证明。6. 如何把框架扩展到真实的数学发现系统沙盘的意义在于展示机制而不是解决端到端问题。要把“正反博弈 裁判”延伸到更真实的数学发现场景需要在三个方向上升级。6.1 用大模型增强提议者和批评者当前沙盘中的ProposerAgent只会在多项式空间插值表达能力有限。真实系统中可以让大模型承担“启发式猜想生成”的职责。大模型能够把自然语言推理、数学直觉和符号工具结合起来生成更复杂的候选结构比如递归定义、不等关系、涉及素数分布的命题等。但大模型生成的内容是软性的很容易出现幻觉。因此建议保留CriticAgent作为硬性检查器让大模型负责“提出思路”让确定性的搜索程序负责“验证思路”。可以提供一个抽象接口把大模型封装为新的Agentclass MathAgent: 多智能体系统通用接口。 实际项目中可以接大模型也可以接符号计算器。 def __init__(self, name: str, description: str, backendNone): self.name name self.description description self.backend backend def run(self, task: str): if self.backend is None: raise NotImplementedError(backend 未配置。可接入大模型 API 或本地模型。) # 例如self.backend.chat(你是数学提议者请提出候选公式) return self.backend.chat(task)如果接入大模型 API不要把密钥硬编码在代码中应该从环境变量读取并使用最小权限原则。同时必须在调用外层设置超时、重试、内容过滤与日志审计。6.2 用符号系统和证明器作为裁判沙盘中的裁判只能判断“是否为素数”真实数学问题远比这复杂。裁判需要升级为独立的验证后端可能的选项包括sympy适合多项式化简、求值、因数分解等可计算代数问题。SageMath覆盖更广的数学计算场景。Lean/Coq/Isabelle适合形式化证明验证。自研验证器针对特定问题实现确定性检查逻辑比如一致哈希、状态机、协议正确性。数学发现最重要的原则是裁判的验证能力决定了整个系统的可信度上限。如果裁判只会统计模型投票系统产出的结果就不具备数学意义上的可靠性。6.3 引入记忆和并行搜索真实数学发现需要持续积累前一轮失败的候选公式、已知的反例模式、已经证明过的引理都可以作为下一轮搜索的上下文。建议为系统引入一个结构化记忆组件保存历史记录候选公式、提出时间、依据的观测范围。反例的具体数值、判定结果、验证日志。最终结论已推翻、未推翻、已证明。反例搜索本身非常适合并行化。CriticAgent可以把[10, 200]的范围拆成多个子区间用进程池或消息队列并发搜索。对于需要大量计算的真值测试这会显著提升效率。真实系统中还需要设置明确的中止条件。正反博弈如果无限制运行可能陷入无限循环正方不断提出新公式反方不断找到反例。建议设置最大轮数、总搜索范围上限、单次运行超时等参数。7. 常见问题与排查思路多智能体数学发现系统在运行时问题通常集中在依赖、反例搜索和角色逻辑三个方面。下面列出最容易遇到的几种情况。问题现象可能原因排查方式解决方案安装sympy失败或版本冲突全局环境中已存在其他版本依赖查看 pip 错误日志执行pip show sympy使用虚拟环境锁定sympy1.11运行时不输出反例搜索范围太小或候选公式在范围内都成立检查CriticAgent的search_start/search_end打印每个候选的检查进度扩大搜索范围或简化候选公式集ProposerAgent生成大量重复公式不同观测点组合插值得到同一多项式代码中已用sp.srepr去重但仍可能出现化简前不同先展开再比较使用sp.simplify后统一格式候选公式在观测点有较大误差插值组合点不够代表性打印观测点检查是否存在异常值或重复点增加观测点数量或改用最小二乘拟合裁判判定结果不生效裁判只是返回文本没有真正执行数学验证检查JudgeAgent是否独立调用 sp.is