开放世界多智能体环境中的自主数学发现，简单说就是让多个大模型智能体组成一个科研小组，在一个持续变化、可交互、带工具调用的环境里，自动完成“提出问题、形成猜想、数值验证、符号证明、接受或推翻”的完整数学发现链路。它不是一个单一模型的强化学习任务，也不是一次 prompt 工程能解决的问题，而是环境建模、多智能体协作、形式化验证三者叠加的系统工程。
这个方向适合三类读者：一类是做大模型应用开发，想了解多智能体框架如何落地的工程师；一类是研究数学推理或自动定理证明的研究者，想用符号工具和 LLM 结合做实验；还有一类是做 AI Agent 平台设计的技术负责人，需要判断交互模式、消息协议和验证机制怎么设计才可靠。
本文会带你从概念出发，梳理多智能体处理数学问题的核心矛盾，再对比四种常见交互模式，最后给出一个最小可运行的多智能体数学发现框架，包含代码、配置、验证方式和排错路径。学完之后，你可以把这个框架迁移到自己的开放世界环境，比如棋类推演、算法发现、数据规律挖掘等场景。
1. 为什么数学发现需要多智能体而不是单个大模型
1.1 数学发现和数学证明是两类不同任务
数学发现不是单一能力。一个完整的发现过程至少包含四件事：
- 从数据或现象中观察规律，提出一个可检验的猜想。
- 用数值、符号或模拟手段做实验，验证猜想在小规模样本上是否成立。
- 构造证明思路，把非形式化论证转换成可检查的推理步骤。
- 对证明进行审查，找出漏洞、补全缺失条件，或者给出反例推翻猜想。
这四种能力对同一个模型来说，目标函数是互相冲突的。提出猜想要求发散和联想，构造证明要求严谨和线性推理，审查证明要求怀疑和挑剔。如果让一个智能体同时承担这些角色，即使模型能力很强，也会因为“既当运动员又当裁判”而降低结论可信度。实际运行中更容易出现的情况是：模型提出了一个很有启发的猜想，然后在证明环节开始编造理由，把不成立的中间步骤写得像真的一样。
1.2 开放世界环境提供了反馈来源
传统问答式数学任务只给模型一个题目，模型输出一个答案，没有中间反馈。开放世界环境的特点是：智能体可以通过工具调用改变环境状态，并从环境中获得结果。这里的“开放世界”可以是一个带有状态和规则的计算沙箱，可以是一个符号计算环境，也可以是模拟真实物理规律的网格世界。
环境反馈对数学发现至关重要。以“n 的三次方减 n 是否能被 6 整除”为例，智能体先做数值实验，对 n 从 1 到 100 逐项计算，得到全部被 6 整除的结果。这个反馈本身不是证明，但它能快速纠正模型的直觉，避免模型在错误方向上写长篇推导。环境在这里扮演的是“实验台”角色，它提供的数据是后续验证和证明的原材料。
在实现层面，开放世界环境通常暴露出统一的工具接口，比如run_python(code)、run_sympy(expression)、query(dataset)。智能体不直接操作底层系统，而是通过工具函数进行交互，这样既能保证安全，也方便记录每步操作，便于事后审计。
1.3 单智能体的三个明显缺陷
单智能体做数学发现，通常会遇到三个问题：
- 幻觉无法被及时纠正。模型产出一段看似严密的证明，但它没有外部渠道验证中间步骤，错误会被不断放大。
- 上下文污染。提议、实验、证明混在同一个上下文里，前面的错误结论会引导后续输出，形成自我强化。
- 缺乏分工导致的效率下降。让一个模型从零开始做完整证明，不仅 token 消耗大，而且一旦失败无法定位失败角色。
多智能体设计把上面每个职责拆成独立 Agent，每个 Agent 只负责一个环节，通过消息协议协作。这样每个环节的输入输出都清晰，出现问题时也能定位到具体智能体和具体消息，而不是在一大段自由文本里找问题。
2. 多智能体的四种交互模式如何选型
在实现多智能体数学发现系统之前，先要确定智能体之间“怎么说话”。业内常见的多智能体交互模式可以归纳为四种：流水线模式、层级编排模式、协作讨论模式、对抗批判模式。它们不是互斥的，实际系统往往混用。
2.1 流水线模式：按顺序传递中间结果
流水线模式是最简单的一种。智能体按固定顺序执行任务，前一个的输出是后一个的输入。在数学发现场景下，典型链路是：数据观察者 -> 猜想提议者 -> 数值实验者 -> 证明构造者 -> 结果汇总者。
这种模式的优势是流程清晰、易于实现、每个阶段都可以单独记录日志。缺点是前序智能体一旦输出低质量内容，后序智能体只能在坏输入上工作，整个链路质量受制于最弱环节。适合任务边界明确、顺序依赖强、对实时性要求不高的场景。
2.2 层级编排模式：一个主控 Agent 分派子任务
层级编排模式引入一个 orchestrator（编排者），它负责理解总目标，把任务拆解成子任务，分派给不同的 worker Agent，再汇总结果。worker 之间不直接通信，所有信息经编排者中转。
在数学发现系统里，编排者负责维护“当前猜想状态机”：是已经验证，还是被推翻，还是证据不足需要更多实验。它根据状态决定下一步派发哪个 worker。这种模式的优点是全局状态可控，适合任务动态变化的环境；缺点是一次请求往返较多，编排者容易成为性能瓶颈。
2.3 协作讨论模式：多角色围绕同一问题迭代
协作讨论模式让多个智能体共享同一讨论上下文，轮流发表观点。每个智能体能看到其他人的发言，然后补充、修改或附议。这模拟了论文组会的场景。
数学发现中，协作讨论常用于猜想细化阶段。比如提议者提出一个边界条件模糊的猜想，验证者指出“n 的取值范围没有说清楚”，实验者补充“n 为偶数时结果不成立”，最终大家一起修正。这个模式的优势是能利用集体智慧逐步逼近正确表述；劣势是上下文会迅速膨胀，讨论也可能跑题，需要控制轮次和引入主持人。
2.4 对抗批判模式：用攻击性反馈提高结论可靠性
对抗批判模式的核心是“建设性对抗”。提议者提出猜想和证明，批判者负责找反例、找证明漏洞、指出条件缺失。两方交替发言，直到批判者无法再提出有效疑问，或者提议者承认失败。
这是数学发现中最重要的模式之一，因为数学结论的价值在于可证伪性。一个没有被批判过的猜想，即使数值实验全部通过，也不具备可信度。对抗模式需要特别注意的是：批判者必须基于符号计算、反例搜索或逻辑规则给出具体反对理由，而不能只是说“我觉得不够严谨”。
2.5 四种模式对比与选型建议
| 模式 | 数据流向 | 优点 | 缺点 | 数学发现中的典型用途 |
|---|---|---|---|---|
| 流水线模式 | 前序输出 -> 后序输入 | 实现简单，流程清晰，易监控 | 前序错误会传导，缺少反馈 | 固定流程的数值实验 |
| 层级编排模式 | 编排者分派，worker 回传 | 全局状态可控，适合动态任务 | 编排者瓶颈，往返延迟高 | 猜想状态机管理 |
| 协作讨论模式 | 所有成员共享上下文轮流发言 | 能逐步修正错误表述 | 上下文膨胀，容易跑题 | 猜想细化和条件完善 |
| 对抗批判模式 | 提议者与批判者交替攻击 | 能显著提高结论可信度 | 需要控制轮次，成本较高 | 证明审查和反例搜索 |
选型建议是：不要一上来就用最高级的模式。先跑通流水线，让每个 Agent 单独输出可检查的结果；再加入验证者，形成“提议 -> 实验 -> 验证”最小闭环；最后按需要加入批判者，形成对抗讨论。等系统稳定后，再考虑用层级编排管理多个并行子任务。这个顺序能最大程度降低调试难度。
3. 环境准备与依赖配置
3.1 技术栈选型
多智能体数学发现系统可以由几个成熟组件拼装而成，不需要从零训练模型。核心依赖如下：
| 组件 | 作用 | 常见选型 |
|---|---|---|
| 大模型接入层 | 提供对话和推理能力 | OpenAI 兼容接口，支持任意文本模型 |
| 数学工具层 | 执行符号计算和数值实验 | SymPy、NumPy、SciPy |
| 执行沙箱 | 安全运行 Python 代码 | 本地 subprocess 或容器隔离 |
| 消息协议 | 定义智能体间通信格式 | JSON 消息，包含 sender、receiver、type |
| 编排层 | 控制多轮对话和状态流转 | Python 编写的会话循环 |
如果原始代码对模型的接口协议没有明确要求，建议使用 OpenAI 兼容的 chat completions 接口，这样后续可以替换为本地部署的模型服务。落地前要确认你使用的 SDK 版本和服务端接口是否兼容。
3.2 Python 依赖安装
项目建议使用 Python 3.10 以上版本，并创建独立的虚拟环境。下面是一组最小依赖：
python -m venv .venv source .venv/bin/activate pip install openai sympy numpy pandas python-dotenv如果你需要把执行代码放进隔离环境，可以额外安装pytest用于验证，或使用 Docker SDK 远程执行。学习阶段不建议先搭建容器集群，本地 subprocess 已经足够跑通最小闭环。
生产环境还需要考虑：模型密钥管理、执行超时、沙箱资源限制、日志持久化、结果数据库。这些放在第 7 节讨论。
3.3 大模型接入配置
通过环境变量保存模型访问信息，不要硬编码在代码里。创建一个.env文件：
LLM_BASE_URL=https://api.openai.com/v1 LLM_API_KEY=sk-xxxx LLM_MODEL=gpt-4o-mini LLM_TEMPERATURE=0.7如果本地有兼容 OpenAI 协议的模型服务，把LLM_BASE_URL指向本地服务地址即可。需要注意：不同模型对 JSON 输出、工具调用、上下文长度的支持不同，建议在项目 README 中记录实际测试通过的模型名称。
3.4 用 SymPy 做符号验证的可行性检查
数学发现系统里，SymPy 承担的是“可计算验证层”。安装完后，可以用下面这段代码确认环境可用：
import sympy as sp n = sp.Symbol("n", integer=True, positive=True) expr = n**3 - n print("factor:", sp.factor(expr)) print("simplify:", sp.simplify(expr))预期输出类似：
factor: n*(n-1)*(n+1) simplify: n**3 - n如果能看到 factor 输出，说明 SymPy 本身可用，后续可以让验证者 Agent 调用sp.factor、sp.limit、sp.simplify等函数对表达式做自动检查。
4. 一个最小可运行的多智能体数学发现框架
4.1 总体架构
这个最小框架包含四个角色：
- 提议者 Proposer：根据观测数据提出猜想。
- 执行者 Executor：调用 Python 运行数值实验。
- 验证者 Verifier：调用 SymPy 检查符号表达，并给出验证意见。
- 批判者 Critic：对验证结果提出反例或漏洞，决定结论是否成立。
编排循环的核心逻辑是：提议者给出猜想 -> 执行者做数值实验 -> 验证者做符号检查 -> 批判者审查，若批判者无法推翻则记录结论，否则将批判意见反馈给提议者，进入下一轮。
4.2 定义统一消息格式
多智能体之间不能直接用自然语言字符串传来传去，必须定义结构化消息。这里用 dataclass 表示一条 Agent 消息：
# message.py from dataclasses import dataclass, field from typing import Optional @dataclass class AgentMessage: sender: str receiver: str msg_type: str # proposal, experiment, verification, critique, result content: str metadata: Optional[dict] = field(default_factory=dict) def to_dict(self): return { "sender": self.sender, "receiver": self.receiver, "msg_type": self.msg_type, "content": self.content, "metadata": self.metadata, }消息字段含义如下：
| 字段 | 含义 | 说明 |
|---|---|---|
| sender | 发送者名称 | 使用固定角色名，如 proposer |
| receiver | 接收者名称 | 便于路由到对应 Agent |
| msg_type | 消息类型 | 决定内容如何被处理 |
| content | 消息正文 | 通常是 Markdown 或 JSON 文本 |
| metadata | 附加信息 | 用来传参、传实验结果、传错误代码 |
4.3 实现一个通用的 LLM Agent 基类
所有角色都复用同一个调用大模型的基类，只通过 system prompt 区分职责：
# agent_base.py from openai import OpenAI class LLMAgent: def __init__(self, name: str, system_prompt: str, base_url: str, api_key: str, model: str, temperature: float = 0.7): self.name = name self.system_prompt = system_prompt self.client = OpenAI(base_url=base_url, api_key=api_key) self.model = model self.temperature = temperature def run(self, messages): response = self.client.chat.completions.create( model=self.model, messages=[{"role": "system", "content": self.system_prompt}] + messages, temperature=self.temperature, ) return response.choices[0].message.content这里的关键点是：职责只通过 system prompt 区分，而不是写多个不同的请求函数。这样新增一个角色只需要增加字符串常量，代码维护成本低。
4.4 实现提议者、执行者与验证者
提议者的 prompt 决定它输出的格式，要求它把自然语言猜想和符号表达式都写出来，方便后续解析：
# agents.py PROPOSER_PROMPT = """ 你是一个数学发现助手。你会收到环境观测数据和其他智能体的反馈。 请输出一个数学猜想，并遵循以下格式： 猜想: <自然语言描述> 符号: <sympy 可解析的表达式，如 f(n)=n**3-n> 依据: <一句话直觉> """.strip() VERIFIER_PROMPT = """ 你是一个数学验证助手。你会收到一个猜想和数值实验结果。 请使用提供的符号检查结果判断猜想是否可能成立。 如果发现条件不完整，请指出缺失条件。 不要编造证明，只基于给出的工具结果给出判断。 """.strip() CRITIC_PROMPT = """ 你是一个数学批判者。你的任务是为别人提出的猜想寻找反例或证明漏洞。 请只给出具体、可检验的反对理由。 如果找不到反例，请明确说：未发现反例。 """.strip()执行者不调用大模型，它是一个纯工具 Agent，负责运行 Python 代码，并返回标准输出、错误和返回码：
# executor.py import os import subprocess import tempfile def run_python_code(code: str, timeout: int = 10) -> dict: with tempfile.NamedTemporaryFile( mode="w", suffix=".py", delete=False, encoding="utf-8" ) as f: f.write(code) path = f.name try: result = subprocess.run( ["python", path], capture_output=True, text=True, timeout=timeout, ) return { "stdout": result.stdout, "stderr": result.stderr, "returncode": result.returncode, } except subprocess.TimeoutExpired: return {"stdout": "", "stderr": "timeout", "returncode": -1} finally: os.unlink(path)学习环境下，这个执行函数已经够用。如果用于生产，必须把subprocess换成容器或沙箱方案，避免任意代码直接运行在宿主机器上。
4.5 编排循环：把四个角色串起来
编排层负责组装消息历史，并在每轮结束后判断是否达到终止条件：
# orchestrator.py from message import AgentMessage from agent_base import LLMAgent from executor import run_python_code from agents import PROPOSER_PROMPT, VERIFIER_PROMPT, CRITIC_PROMPT import sympy as sp import json class DiscoveryOrchestrator: def __init__(self, config): self.proposer = LLMAgent( "proposer", PROPOSER_PROMPT, config["base_url"], config["api_key"], config["model"] ) self.verifier = LLMAgent( "verifier", VERIFIER_PROMPT, config["base_url"], config["api_key"], config["model"] ) self.critic = LLMAgent( "critic", CRITIC_PROMPT, config["base_url"], config["api_key"], config["model"] ) self.max_rounds = config.get("max_rounds", 3) def start(self, observations: str): history = [] final_result = [] for round_index in range(self.max_rounds): proposal = self.proposer.run([ {"role": "user", "content": f"第 {round_index + 1} 轮。观测数据：\n{observations}"} ] + history) history.append({"role": "assistant", "content": proposal}) # 提取数值验证代码，这里简化处理：让执行者从 proposal 中提取表达式做实验 experiment_code = self._build_experiment_code(proposal) exp_result = run_python_code(experiment_code) verification = self.verifier.run([ {"role": "user", "content": f"猜想：\n{proposal}\n数值实验结果：\n{exp_result}"} ]) history.append({"role": "assistant", "content": verification}) critique = self.critic.run([ {"role": "user", "content": f"请审查以下猜想和验证结论：\n{proposal}\n{verification}"} ]) history.append({"role": "assistant", "content": critique}) final_result.append({ "round": round_index + 1, "proposal": proposal, "experiment": exp_result, "verification": verification, "critique": critique, }) if "未发现反例" in critique: break return final_result def _build_experiment_code(self, proposal: str) -> str: # 简化实现：从文本中提取符号表达式做数值抽样 # 这里实际项目应使用正则表达式解析，示例只演示结构 expr_str = "n**3 - n" return f''' for n in range(1, 101): value = {expr_str} if value % 6 != 0: print("counterexample:", n, value) break else: print("all ok: n^3 - n is divisible by 6 for n in 1..100") '''这个编排器最大的简化点是_build_experiment_code没有真正解析提案中的符号表达式。实际项目中应该用ast或正则解析出符号:后面的表达式，再动态构造实验代码。学习阶段可以先用固定表达式，验证流程本身。
5. 运行验证与结果分析
5.1 用简单的整除猜想验证闭环
启动脚本如下：
# main.py import os from dotenv import load_dotenv from orchestrator import DiscoveryOrchestrator load_dotenv() config = { "base_url": os.environ["LLM_BASE_URL"], "api_key": os.environ["LLM_API_KEY"], "model": os.environ["LLM_MODEL"], "max_rounds": 3, } orchestrator = DiscoveryOrchestrator(config) results = orchestrator.start("给定一个整数 n，考虑函数 f(n)=n^3-n。") print(json.dumps(results, ensure_ascii=False, indent=2))运行后，正常流程会出现三类结果：
- 提议者输出了一个形式良好的猜想，比如“对所有正整数 n，n^3-n 都能被 6 整除”。
- 执行者运行
n=1..100的数值实验，输出all ok。 - 验证者调用 SymPy 做符号分解，发现
n**3 - n = n(n-1)(n+1)，指出这是三个连续整数之积，必然同时被 2 和 3 整除，因此可被 6 整除。 - 批判者本轮找不到反例，给出“未发现反例”，循环提前终止。
5.2 从日志中判断每个 Agent 是否合格
多智能体系统的调试不能只看最终结果，要看每一环的输出质量。建议按以下检查点逐项核对：
| 检查点 | 合格标准 | 不合格表现 |
|---|---|---|
| 猜想表达 | 有明确条件和结论 | 含糊其辞，缺变量范围 |
| 实验代码 | 能覆盖代表性样本 | 只测了 n=1，样本太少 |
| 验证理由 | 引用符号工具的分解结果 | 直接说“显然成立” |
| 批判意见 | 给出反例或明确表示未找到 | 输出“我觉得可能不太行”这种空话 |
如果某轮输出不合格，不要急着换模型，先检查对应角色的 system prompt 是否足够具体。比如验证者的 prompt 里没有提到“必须引用符号工具结果”，它就可能依赖模型记忆作答，而不是基于工具输出。
5.3 把这个闭环扩展到其他开放世界场景
这个最小框架的扩展点在于两点：环境观测接口和工具集合。
环境观测接口负责把“开放世界”的状态转换成文本或结构化数据。例如：
def collect_observations(state) -> str: # 从环境状态中采样，生成观测文本 return f"当前状态: {state}"工具集合负责把环境能力暴露给 Agent。比如在序列规律发现场景中加入query_next_value(sequence)，在几何推理场景中加入angle_sum(polygon)。每次新增工具，都要在验证者的 prompt 里说明工具的返回值格式和可信范围，否则 Agent 不会主动使用。
6. 常见问题与排查路径
6.1 问题现象、原因与处理对照表
多智能体数学发现项目最容易踩的坑，集中在模型调用、代码执行、消息解析和上下文控制四个方面。
| 问题现象 | 常见原因 | 检查方式 | 处理建议 |
|---|---|---|---|
| Agent 输出无法解析 | prompt 没有限定输出格式，或模型没遵循格式 | 打印原始回复，检查是否有猜想:等标记 | 在 prompt 中给出严格格式模板，并用程序校验 |
| 数值实验一直没有反例输出 | 实验代码只测了少量样本，或表达式写错 | 打印实验代码，手动运行一次 | 统一从提案中解析表达式，增加样本量和随机性 |
| 验证者不看符号工具结果 | verifier prompt 没有要求引用工具输出 | 查看 verifier 收到的消息内容 | 在 prompt 中明确要求“必须基于符号检查结果” |
| 多轮之后上下文超长 | 每轮把完整历史都传给模型 | 查看 API 请求的 token 消耗 | 只保留最近两轮和最终结论摘要 |
| 执行环境执行了危险操作 | subprocess 直接运行模型生成的代码 | 检查执行日志和资源消耗 | 生产环境改用容器隔离，限制网络和文件权限 |
| 批判者说找不到反例但结论其实是错的 | 批判者被前序结论带偏 | 单独用反例搜索工具复核 | 给批判者独立的数值反例搜索能力 |
6.2 从日志反向定位问题 Agent
多智能体系统里最忌讳“结果错了但不知道哪一步错的”。关键是给每个 Agent 的输出加上独立编号并落盘。
import logging logging.basicConfig(level=logging.INFO, format="%(asctime)s %(levelname)s %(message)s") def log_agent_output(agent_name, round_index, output): logging.info("[ROUND %s][%s] output saved", round_index, agent_name) # 实际项目应写入数据库或文件排查顺序按这个优先级来：
- 检查输入观测是否包含足够信息。
- 检查消息格式是否被正确解析和路由。
- 检查实验代码是否真实运行，以及 stdout 是否被完整保留。
- 检查验证者是否基于工具结果而不是模型记忆。
- 检查批判者的反例搜索范围是否足够。
- 最后才考虑更换模型或调整 temperature。
如果实验输出显示returncode非 0，说明执行者生成的代码有语法错误，优先修复_build_experiment_code的解析逻辑，而不是去调 prompt。
6.3 防止“多智能体共谋式幻觉”
多个 Agent 可能互相引用错误结论，形成集体幻觉。典型表现是：提议者说“经验证成立”，验证者说“同意”，批判者说“无异议”，但实际没有任何一个 Agent 真正运行过工具。
应对方法只有一条：程序层强制工具调用，而不是把工具结果作为可选附件。也就是说，验证者收到的消息里必须包含 executor 的真实返回结构，如果 executor 返回returncode != 0，验证流程应直接中断，不允许模型“脑补”实验结果。
另一个方法是给每个 Agent 设置不同的 temperature。提议者用较高温度强化发散，验证者和批判者用较低温度强化稳定输出。这个细节对结论质量影响很大。
7. 生产化建议与可复用清单
7.1 从学习环境到生产环境要补齐的能力
学习环境只要能跑通最小闭环，生产环境则要面对并发、权限、审计和失败恢复四类问题。
| 维度 | 学习环境 | 生产环境 |
|---|---|---|
| 代码执行 | 本地 subprocess | 容器或沙箱，限制 CPU、内存、网络、文件系统 |
| 密钥管理 | .env 文件 | 密钥管理服务，禁止写入代码库 |
| 日志 | print / logging | 结构化日志，按 trace_id 串联整轮对话 |
| 结果存储 | JSON 文件 | 数据库，记录猜想、实验、验证、批判完整链路 |
| 失败恢复 | 直接重跑 | 断点续跑，某一步失败后从中断轮次恢复 |
| 成本控制 | 手动控制 | 每轮 token 预算，超限自动熔断 |
7.2 发布或运行前检查清单
以下清单可以在每次运行多智能体数学发现任务之前逐项确认：
- [ ] 大模型接口地址、密钥、模型名称是否已通过环境变量注入。
- [ ] SymPy 和 NumPy 是否已安装，并能执行最小符号计算。
- [ ] 执行器是否有超时限制，超时后是否有统一错误返回。
- [ ] 每个 Agent 的 system prompt 是否限定了输出格式。
- [ ] 消息记录是否包含 sender、receiver、msg_type 三个字段。
- [ ] 验证者是否强制要求引用符号工具结果。
- [ ] 批判者是否有独立的数值反例搜索机制。
- [ ] 每轮输出是否被独立落盘。
- [ ] 上下文是否做了截断或摘要，避免 token 超限。
- [ ] 生产环境是否使用容器隔离执行代码。
7.3 扩展方向
如果最小框架已经稳定运行，下一步可以在三个方向扩展：
- 引入自动定理证明器，比如 Lean 或 Coq，把验证者的自然语言判断升级为形式化证明检查。这个方向工程量较大，建议先从命题级语句开始，而不是直接做整篇证明。
- 引入记忆和长期存储，让智能体跨任务复用已经被验证过的引理，避免每轮从零发现。
- 引入并行搜索，由编排者同时派发多个提议者，让它们在不同子空间做探索，再汇总候选结果。这个方向要特别注意成本控制和结果去重。
把提议、执行、验证、批判四个角色拆开，并让每个角色都基于工具结果工作，这是整个系统可靠性最关键的工程决策。先跑通最小闭环，再逐步增加形式化验证和并行能力，是学习这个方向最稳妥的路径。
