在人工智能研究中数学推理一直被视为衡量机器智能的重要试验场。传统自动定理证明和数学软件更多依赖人工定义规则、搜索策略或预置题库系统本身并没有“提出问题”的能力。而“开放世界多智能体环境中的自主数学发现”这个方向尝试让多个智能体在一个可持续探索的数学环境中自己生成猜想、验证猜想、寻找反例并在多轮博弈中不断修正结论。它不是让你给模型背答案而是让模型学会像研究者一样发现问题再用严谨工具确认问题。本文将围绕一条可落地的技术主线展开如何使用 Python 构建一个“提议-验证-攻击-裁决”的多智能体数学发现环境。在这个环境里提议者负责生成数学猜想验证者使用符号计算或数值采样检查猜想攻击者主动寻找反例裁判负责终结无意义的争论。整个过程是开放式的智能体可以不断引入新的数字域、新的运算规则和新的关系约束从而形成一个可持续扩展的自主发现闭环。这个方向适合以下读者正在做多智能体协作框架选型的算法工程师希望把大模型接入数学验证工具链的研究者以及想在强化学习或群体智能项目里加入“共同推理”机制的开发者。读完本文后你会得到一个最小可运行的 Python 工程骨架理解每个智能体扮演的角色知道如何让系统真正运行起来也了解它距离自动化数学研究还有哪些工程差距。1. 先想清楚为什么自主数学发现需要多智能体环境1.1 单智能体做数学发现的三个瓶颈单个智能体直接做数学发现时最容易出现的问题是“自说自话”。它可能生成一个结构看起来很漂亮的结论但由于缺少外部检验常常把偶然的数值巧合当作一般规律。例如一个模型在 1 到 100 的整数范围内验证了某个不等式成立就认为它是全局定理实际上第 101 个数就是反例。这种问题不能单纯靠更大规模的模型解决。数学发现包含两个不同性质的任务生成候选结论和验证候选结论。生成是发散性的验证是收敛性的。单个模型很难同时扮演这两种角色让生成者去验证它会倾向于维护自己写出的结论让验证者去生成它会变得保守失去探索能力。把两个角色拆开让不同智能体负责不同目标函数是工程上的自然选择。第二个瓶颈是局部搜索。一个智能体如果只在一个固定数字域里探索很容易陷入自己熟悉的模式反复提出类似猜想。开放世界环境则需要智能体有能力跳出现有边界去改变数字域、改变运算规则、改变关系约束。这种“跳出舒适区”的动作只有在环境中存在竞争或激励差异时才会稳定发生。第三个瓶颈是可信度。数学发现的最终产物应该是可验证的命题而不是自然语言表述的“感觉”。单智能体输出一段文字说这个猜想成立没有结构化表达也没有工具参与校验后续人类无法复查。多智能体环境中加入验证者和裁判角色后每个结论都带上了验证记录可信度会明显提高。1.2 把“开放世界”理解成可扩展的状态空间这里的“开放世界”并不是指一个图形化的 3D 场景而是指数学生成环境的状态空间可以动态扩展。环境内部维护一组数学对象比如整数、有理数、模数、图、函数以及一组操作符比如加法、乘法、取模、连接。智能体可以建立新的对象并把新对象加入环境供后续回合使用。从工程实现上看开放世界环境至少需要三层抽象对象层保存当前环境中的数学实体每个实体有类型和值。规则层保存可用的运算规则规则定义了输入类型、输出类型和求值函数。关系层保存智能体关心的关系例如“相等”“整除”“同余”“小于”以及已经被验证或证伪的命题记录。与传统封闭题库不同环境本身不预先知道哪些结论是正确的。它的职责是提供计算工具和存储记录让智能体在探索过程中逐步积累知识。这也是“自主数学发现”区别于“自动求解已知问题”的核心差异。1.3 多智能体在这里不是聊天群而是角色分工模型很多项目把多个大模型实例放在一起让它们互相聊天美其名曰多智能体系统。这种做法在开放世界数学发现里效率很低因为每个智能体没有明确的生存目标消息很快会漂移成泛泛而谈。真正有效的多智能体环境每个角色必须有独立的效用函数和决策边界。在本文的框架中环境内部至少存在四类角色角色核心目标典型行为失败表现提议者生成新猜想数量优先于质量构造表达式、关系、边界条件重复陈旧猜想验证者对给定猜想执行确定性检查或高精度检查符号化简、数值采样、定理调用误判为真攻击者寻找反例验证猜想边界随机搜索、边界扫描、遗传搜索只做随机数生成裁判判断论战是否收敛决定记录或终止汇总验证记录和反例证据偏袒某个角色这种结构类似工业界的“红队对抗”提议者提出一个假设攻击者负责打掉它验证者负责给出专业结论裁判负责维护交流协议。它并不是为了热闹而是为了让每个智能体的失败都能被其他角色发现并纠正。2. 设计一套可运行的“提议-验证-攻击-裁决”框架2.1 消息不是自然语言而是结构化 Hypothesis 对象多智能体系统最容易踩的坑是让智能体之间传递自然语言。数学表达对精确性要求极高一句话里含糊一点整个推导链条就全错了。因此在工程实现中智能体之间的所有通信都应当使用结构化对象本文统一称为Hypothesis。一个 Hypothesis 至少包含四个字段id假设的唯一编号用于追溯。expression数学表达式使用 Python 可求值的字符串或 AST。domain这个假设适用的集合例如整数集、正整数集、模 7 整数集。relation关心哪种关系例如“对一切 xexpression(x) 为真”还是“存在某个 x 使 expression(x) 成立”。用 Python 表示如下from dataclasses import dataclass, field from typing import List, Any dataclass class Hypothesis: id: str expression: str domain: str relation: str # forall 或 exists variables: List[str] constraints: dict field(default_factorydict) status: str pending # pending / verified / refuted / disputed这个对象在提议者生成后立即广播给验证者和攻击者。验证者在同一个对象上执行检查攻击者在这个对象上生成反例搜索。裁判最后根据两者返回的记录更新 status。2.2 环境黑板让智能体共享历史而不是各自记忆每个智能体如果只在本地维护自己的历史知识的复用就会很弱。提议者提出的猜想被验证为真后攻击者下一次搜索应该避开已被验证的区域同样的被证伪的表达式模式也应该被记录下来。为了实现这一点环境内部设计一个共享黑板保存所有历史命题和验证记录。黑板的数据结构可以设计成以 Hypothesis id 为主键的字典值为验证记录集合class Blackboard: def __init__(self): self.records {} def add_hypothesis(self, hypothesis: Hypothesis): self.records[hypothesis.id] { hypothesis: hypothesis, evidence: [] } def add_evidence(self, hypothesis_id: str, evidence: dict): self.records[hypothesis_id][evidence].append(evidence) def get_verified(self): return [ r[hypothesis] for r in self.records.values() if r[hypothesis].status verified ] def get_refuted(self): return [ r[hypothesis] for r in self.records.values() if r[hypothesis].status refuted ]有了黑板之后新的提议者可以查询已经证伪的模式避免重复提出完全相同的猜想。验证者也可以参考历史证据如果某个表达式曾经在高精度数值采样中失败它可以选择更快地返回 refuted。2.3 回合制调度一轮发现中每个智能体只做一件事为了防止智能体之间互相阻塞或无限争论调度器采用回合制。每个回合包含四个阶段每个阶段由对应角色执行一次动作Round N: 1. Proposer proposes 1 new hypothesis. 2. Verifier checks numeric/symbolic status. 3. Attacker searches for counterexamples. 4. Judge aggregates evidence and sets status.这种设计借鉴了游戏开发中的固定时间步长调度。每个角色在一个回合内只做有限计算系统整体保持确定性和可控性。否则一旦攻击者陷入大规模搜索整个环境的推进就会被卡住。class DiscoverySession: def __init__(self, proposer, verifier, attacker, judge, blackboard): self.proposer proposer self.verifier verifier self.attacker attacker self.judge judge self.blackboard blackboard def run_round(self, round_id: int): hyp self.proposer.propose(self.blackboard.get_refuted()) self.blackboard.add_hypothesis(hyp) verify_result self.verifier.check(hyp) self.blackboard.add_evidence(hyp.id, verify_result) attack_result self.attacker.attack(hyp) self.blackboard.add_evidence(hyp.id, attack_result) final_status self.judge.decide(hyp, verify_result, attack_result) self.blackboard.update_status(hyp.id, final_status) return final_status这个 minimal 调度器已经能让系统跑起来。后续所有扩展例如并行提议、多攻击者协同、验证缓存等都可以在保持回合结构不变的前提下加入。3. Python 环境准备与工程骨架搭建3.1 依赖选择符号计算、数值计算、基础工具库实现这个框架不需要重型深度学习框架。核心依赖是 Python 3.9 以上版本搭配 sympy 做符号验证和表达式化简numpy 做向量化数值采样pydantic 或 dataclass 做结构化通信对象。推荐环境清单如下依赖用途安装命令sympy符号化简、模式匹配、安全表达式求值pip install sympynumpy大规模候选点采样、数组计算pip install numpypydantic假设对象校验与序列化pip install pydanticpytest验证器和裁决逻辑测试pip install pytest学习环境可以直接在 Jupyter Notebook 中运行。生产环境建议使用 Python 3.11 或 3.12安装依赖前先锁定版本文件避免 sympy 和 numpy 版本不兼容导致表达式解析行为变化。3.2 项目目录结构为了让这个工程具备扩展性建议按角色拆分模块而不是把所有逻辑写在一个文件里math_discovery_env/ ├── core/ │ ├── __init__.py │ ├── hypothesis.py # 假设对象定义 │ ├── blackboard.py # 共享黑板 │ └── session.py # 回合调度器 ├── agents/ │ ├── __init__.py │ ├── proposer.py # 提议者 │ ├── verifier.py # 验证者 │ ├── attacker.py # 攻击者 │ └── judge.py # 裁判 ├── domains/ │ ├── __init__.py │ ├── integer_domain.py # 整数域 │ ├── modular_domain.py # 模数域 │ └── poly_domain.py # 多项式域 ├── experiments/ │ └── run_discovery.py # 运行入口 └── tests/ ├── test_verifier.py └── test_session.py3.3 早期协议先用“通用规则”跑通最小系统不要一开始就接入大模型。这个阶段的目标是让多智能体框架在简单数学域中工作即使智能体逻辑非常幼稚。可以先实现一个固定规则提议者它根据预设模版生成猜想例如“对任意正整数 nn 是奇数则 n^2 是奇数”class RuleProposer: def __init__(self): self.counter 0 def propose(self, refuted_hypotheses): self.counter 1 expression x ** 2 1 return Hypothesis( idfhyp_{self.counter}, expressionexpression, domainpositive_integers, relationforall, variables[x] )这里提议者虽然傻但它已经能进入完整的验证循环。等系统跑通后可以逐步替换成基于大模型的提议者让它生成更有探索性的表达式。早期协议的重要性在于排除“框架问题”和“模型能力问题”的混淆如果你一开始就接入大模型出现 bug 时很难判断是框架错了还是模型错了。4. 核心代码实现四个角色的职责与参数设计4.1 提议者从模板生成到开放式探索提议者的核心功能是把“灵光一现”变成一个结构化的 Hypothesis。模板式提议者虽然简单但它能保证生成内容的安全性和可验证性。在数字域内常用的数学表达式模板包括多项式恒等式例如 x^2 y^2 与 (x y)^2 的关系。整除性关系例如 n^2 - 1 是否能被 8 整除。同余关系例如 x^2 mod p 的取值集合。不等关系例如 x^2 1 2x 是否对全体整数成立。实现时提议者内部维护一个候选运算符池和变量池随机组合成一个表达式再选择一个关系类型生成 Hypothesis。为了防止生成无意义的纯随机字符串应该限制表达式深度并确保所有变量在使用前出现在变量列表中。class RandomProposer: def __init__(self, operators, domainintegers, max_depth3): self.operators operators self.domain domain self.max_depth max_depth self.counter 0 def propose(self, refuted_hypothesesNone): self.counter 1 expr self._random_expression(x, depth2) hyp Hypothesis( idfhyp_{self.counter}, expressionexpr, domainself.domain, relationforall, variables[x] ) return hyp注意refuted_hypotheses 参数在这个简单实现里暂时没被使用但在完整系统中应该传入给模型避免重复提出相同类型的问题。4.2 验证者用 sympy 做符号校验用 numpy 做边界采样验证者负责对 Hypothesis 做“确定性检查”和“高置信度检查”。确定性检查适合多项式恒等关系可以通过 sympy 展开表达式差值看化简结果是否为 0。例如要验证“x^2 1 2x 是否恒成立”可以化简表达式x**2 1 - 2*x结果应该为(x - 1)**2。import sympy as sp class SympyVerifier: def check(self, hypothesis: Hypothesis): x sp.Symbol(x) try: expr sp.sympify(hypothesis.expression) if hypothesis.relation forall: simplified sp.simplify(expr) return {result: unknown, simplified: str(simplified)} except Exception as e: return {result: error, message: str(e)}对于不确定的情况验证者需要调用数值采样。采样点不是均匀取 1000 个随机数而是要在边界处密集取值因为数学反例最常出现在“接近边界”的位置。例如如果 domain 是正整数采样应该是 1 到 1000 的数。如果 domain 是实数则需要对负数、零、小数、大数分别采样。数值采样永远无法证明“恒成立”但能暴露反例。因此验证者的返回值必须包含check_type字段区分是symbolic还是numeric。裁判在决定结论时对 symbolic 验证结果给予更高权重。4.3 攻击者给反例搜索加一点策略而不是纯随机攻击者是最容易出现“看起来在干活实际上没效果”的角色。如果攻击者只是生成 uniform 随机数它很难发现边界反例。更有效的做法是结合遗传算法或领域启发式规则。攻击策略可以拆成三部分边界扫描在 domain 的边界附近集中采样。候选变异从已验证为真的点出发加入小的扰动检查扰动后性质是否仍然成立。模式生成根据验证者返回的疑似问题点反向构造新的测试点。在 Python 中攻击者可以维护一个候选点队列class Attacker: def __init__(self, rngNone): self.rng rng or np.random.default_rng() def attack(self, hypothesis: Hypothesis): expr hypothesis.expression counterexamples self._search_counterexamples(expr, hypothesis.domain) if counterexamples: return {result: refuted, counterexamples: counterexamples[:5]} return {result: not_found, counterexamples: []} def _search_counterexamples(self, expr, domain): examples [] # 边界和中心采样策略 candidates list(range(1, 100)) [10**6, 10**9] for val in candidates: x val if not self._check_expression(expr, x): examples.append(x) return examples实际运行中攻击者的搜索时间应该被限制。每个 Hypothesis 最多允许 1000 次采样或 0.5 秒计算时间避免整个会话被卡住。4.4 裁判用加权证据决定命题状态裁判是最终裁决者。它读取验证者的符号结果、数值采样结果和攻击者给出的反例列表然后决定该 Hypothesis 的状态。设计一个简单但严谨的裁决逻辑如果存在反例直接判定为refuted。如果 sympy 给出确定性的符号化简结果且证明等式恒成立判定为verified。如果只有数值采样没有反例且采样数量超过阈值判定为disputed表示有初步支持但还没得到证明。如果验证者和攻击者都没有结果判定为disputed。class Judge: def decide(self, hypothesis, verify_result, attack_result): if attack_result[result] refuted: return refuted if verify_result.get(result) verified: return verified if verify_result.get(result) unknown and attack_result[result] not_found: return disputed return pending裁判的价值在于把“数值上没找到反例”和“数学上证明了正确性”区分开。很多初级实现把两者混为一谈最后输出的所谓定理其实只是“在采样范围内没被发现错误”。这会让整个系统的可靠性下降。4.5 把四个角色接入调度器最后把四个角色组合成完整的发现会话def main(): blackboard Blackboard() proposer RandomProposer(operators[, *, **], domainpositive_integers) verifier SympyVerifier() attacker Attacker() judge Judge() session DiscoverySession(proposer, verifier, attacker, judge, blackboard) for round_id in range(10): status session.run_round(round_id) print(fRound {round_id}: {status})运行后你会在终端看到每个回合的命题状态变化。这个最小系统已经能让“规则提议者”提出猜想由验证者和攻击者检查并由裁判归档结论从而形成自主发现的完整循环。5. 运行验证跑通一轮并检查结果质量5.1 最小验证用一个已知结论验证框架判断能力为了确认框架没有逻辑错误建议先准备一个已知为真的数学事实。例如“对任意整数 nn^2 不等于 2 mod 4”。这个结论很容易用符号方法验证攻击者也找不到反例。将这个结论以 Hypothesis 形式手动放入黑板运行验证者和攻击者确认裁判状态输出为verified。known_true Hypothesis( idknown_true_1, expression(x**2 - 2) % 4, domainintegers, relationforall, variables[x] ) # 期望 verify_result 为 symbolic verified # 期望 status 为 verified这个测试能快速发现基础错误比如表达式解析失败、模运算域未定义、裁判状态转换逻辑写反等。5.2 再测一个已知为假的猜想看看反例会不会被抓住另一个关键测试是传入一个错误命题例如“对任意正整数 nn^2 n 41 总是素数”。这个命题在 n 较小时成立但当 n 40 时结果是 1681 41 * 41这是经典反例边界。攻击者的边界扫描策略应该能在候选点中覆盖这个位置。如果攻击者没有返回反例问题通常出在采样范围过小或没有覆盖边界值。解决方法是把采样策略从“均匀随机”调整为“等比数列 特殊值列表”并将诸如 40、41、42 这类常见反例点加入候选集。5.3 验证指标不要只统计通过率要看探索覆盖率衡量一个自主发现系统不能只记录“验证通过了多少个猜想”。更有价值的指标包括指标含义计算方式新假设率提议者生成与历史假设不重复的比例重复假设数 / 总假设数反例攻击命中率攻击者返回反例的假设比例被证伪数 / 参与攻击数验证置信度已验证假设中符号验证占比符号验证数 / 已验证数探索覆盖率新变量、新操作符、新域出现频率环境变化计数器这些指标缺一不可。只有通过率高说明提议者太保守只有新假设率高说明提议者太发散。要在探索性和可靠性之间取得平衡最好的办法是让攻击者样本数和验证者采样数成为可调参数并观察系统输出随参数变化的情况。6. 常见问题排查从现象定位到根因6.1 假设对象校验失败表达式中存在未知符号现象运行验证者时抛出sympy.SympifyError或NameError提示y未定义。可能原因提议者在变量列表中没有声明所有变量而验证者直接把字符串传给 sympy 求值。处理方式在Hypothesis创建时对变量列表做严格校验验证者在解释表达式前先用 sympy 的symbols()显式初始化变量再从作用域中查询表达式里的自由符号确保所有自由符号都在变量列表中。def _validate_variables(expr: str, variables: List[str]): free_symbols {str(s) for s in sp.sympify(expr).free_symbols} declared set(variables) if not free_symbols.issubset(declared): raise ValueError(fFree symbols {free_symbols - declared} not declared)6.2 数值采样没有找到反例但状态被判为 verified现象攻击者跑了 10000 次随机采样没有反例裁判直接判定为 verified。原因验证者的返回值里包含了result: verified字段但它的逻辑只做了数值采样没有做符号化简。裁判无法区分“已证明”和“未发现反例”。处理方式在验证者中增加check_type字段。数值采样阶段不能返回verified只能返回maybe或not_found。只有 sympy 化简或定理证明接口返回确定性结果时才允许返回verified。裁判端再做一次最终校验。6.3 探索过程发散提议者不断提出无意义的复杂表达式现象10 轮后黑板里全是x**7 y**3 - x*y**2 1这类混乱表达式验证者和攻击者只能勉强执行但系统没有积攒任何有价值的结论。原因提议者的表达式深度和复杂度没有限制导致生成的 Hypothesis 超出了现有验证器能力范围。处理方式在提议者中设置复杂度评分表达式深度超过阈值时直接重新生成。同时提供一个“温度参数”控制表达式中的操作符数量。对纯模板生成的表达式建议先使用限定操作符集合、*、**、%并限制指数不超过 3。这样能够保证每个假设至少是“可分析”的。6.4 裁判只依赖攻击者结果导致命题状态反复横跳现象同一个假设攻击者偶发采样到反例时状态为 refuted下一轮攻击者随机采样没找到反例状态又变回 disputed。原因裁判没有保存历史裁决结果每一轮都根据当前攻击结果重新决定。处理方式裁决逻辑应该是单调的——一旦某个假设被 refuted就不能再变回 verified 或 disputed。实现时在 Judge 的 decide 方法中加入状态机判断并且建议把攻击结果缓存到黑板上避免重复计算。问题现象常见原因检查方式处理建议表达式校验失败变量列表与表达式自由符号不一致打印 free_symbols 与 variables校验变量声明没有反例却被判为真验证者把数值采样当成证明检查 check_type 字段数值采样只能返回未发现系统生成过于复杂提议者没有复杂度控制统计表达式节点数设置深度和操作符上限状态反复横跳裁判没有历史记忆查看同一 id 的多条记录状态机单调更新7. 最佳实践从最小原型走向可信赖的数学发现环境7.1 先让环境“可信”再让模型“聪明”许多团队拿到 “自主数学发现” 这个题目后第一反应就是接入一个大型语言模型让模型直接输出数学猜想。这种做法的风险在于模型输出带有随机性而验证环境如果本身不可信最终结论就完全无法依赖。工程上正确的顺序是先让环境具备可信验证能力再逐步替换智能体内部逻辑。早期使用规则模板生成假设用 sympy 做确定性检查用人工已知反例测试验证器和攻击者确保基础设施没错之后才让模型承担提议和攻击中的策略部分。这样即使模型输出质量不高环境也能兜底不会把错误结论当作定理保存下来。7.2 使用黑板缓存验证结果避免重复计算数学探索过程中大量假设在结构上是相似的。例如x^2 1和(x1)^2 - 2x在化简后可能等价。如果每次都对这类假设重新做符号化简和数值采样计算成本会线性膨胀。黑板系统可以缓存表达式规范化后的摘要键已经验证失败的表达式模式可以直接被拒绝。def _normalize_expr(expr: str): x sp.Symbol(x) return sp.srepr(sp.sympify(expr))使用srepr获取表达式的规范表示形式比使用字符串拼接更可靠因为x1和1x会在规范化后变成同一个键。7.3 限制每个智能体的单轮预算保证系统可控多智能体环境里的智能体如果不受资源限制任何一个角色的死循环都可能拖垮整个会话。实际工程建议为每个角色设置独立的预算包括时间预算、采样点预算和调用次数预算。例如攻击者每轮最多采样 2000 点验证者每轮最多执行 2 秒符号计算提议者每轮最多生成 3 个候选假设。这样做除了防止失控还让系统时间可预期便于调试和压测。注意限制预算不只是为了性能更是为了语义清晰。当命题状态是 disputed 时如果没有预算限制你无法区分“搜索得不够久”和“确实没有反例”的区别。有了预算每一轮验证结果都附带了搜索强度信息便于后续分析。7.4 生产环境还需要补上日志、监控和回滚如果这个系统要长期运行那么建议输出结构化日志把每个假设的ID、表达式、验证结果、攻击结果和裁决状态记录为 JSON 行。这样后续可以重放某一段探索过程分析提议者策略的变化是否有效。{event: hypothesis_verified, id: hyp_001, expr: x**2 % 4, check_type: symbolic} {event: counterexample_found, id: hyp_002, value: 40}7.5 三个可以直接落到自己项目里的做法如果你的项目只是想利用这个框架的一部分能力建议从下面三个做法开始把“提议者”和“验证者”拆成独立服务通过消息队列通信。这样可以方便地把数学发现能力嵌入流水线而不是在一个进程里强行耦合。把验证者从 sympy 扩展到更专业的定理证明工具。先定义统一验证接口再为不同工具写适配器避免把环境绑定到某个具体库。给攻击者加入强化学习策略。攻击者在不断寻找反例的过程中实际上是在做奖励稀疏的搜索。把它训练成一个能优先在“可疑区域”采样的策略网络是目前这个方向比较自然的大模型接入点。8. 扩展方向从数字游戏走向自动化数学研究目前这套最小系统只能处理简单的数字域和表达式关系。真正要让多智能体环境做出更有价值的数学发现还需要三个层面的扩展。第一层是领域扩展。除了整数和多项式新的领域可以包括密码学里的有限域、代数中的群论、拓扑中的图结构以及组合数学中的格路径。环境每增加一个新的领域就必须同时提供对应的规则、验证工具和攻击策略工作量不小但每个领域都能带来新的研究问题。第二层是证明生成。当前框架只能判断一个命题是否被反例推翻或者是否能用符号化简验证。真正的数学发现要求系统在 verified 状态下能够生成证明轨迹而不仅仅是返回一个布尔值。这意味着验证者需要记录完整推导步骤并把步骤结构化存储。这是向自动定理证明延伸的关键路径。第三层是智能体之间的长期协作。当智能体数量增多后提议者可以依赖其他角色的历史结果继续做更复杂的抽象。例如在某个子问题被证明后提议者可以把该命题作为“引理”组合进更大的假设中。这种层次化推理能力是开放世界环境相比封闭题库的最大优势。如果读者想从最小工程开始练习建议顺序是先把本文的框架在本地跑通再用 sympy 替换验证器增加两个数字域然后接入一个开源大模型作为提议者最后加入日志和可视化。每一层扩展都能独立验证而不是推到重来。这个方向真正困难的不是让智能体说出一个结论而是让它学会在一个拥有验证、反例、争论和证据的开放世界里不断修正自己的判断。多智能体机制的价值就在这里每个角色都有不同的功利目标它们的博弈让系统的结论更加接近数学研究“可证明、可复现、可承认”的标准。
