EULER：通过证据检验返回探索未充分利用链接的多智能体数学发现系统

# 探索未充分利用的桥梁：基于验证回溯的多智能体数学发现
来源：https://arxiv.org/html/2609.00032
###### 摘要
数学社群围绕不同的对象、不变量和工具开展研究，因此将问题在不同社群间转换代价高昂，且常被忽略。本文提出EULER系统——一个多智能体架构，它将此类转换（即"桥梁"）作为搜索单元。围绕一个固定猜想，EULER竞争性地运行直接路径、邻域桥梁和远域桥梁；只有当桥梁提供了源表示无法执行的操作，且其目标侧证据能沿已验证的蕴含关系返回到原始命题时，该桥梁才能保留其计算预算。在昂贵的搜索开始前，六个有序压力测试会排除无效桥梁。我们在120个近期猜想上评估了EULER。这些猜想在搜索前被冻结并经污染筛查筛选，均来自近期在组合数学顶级期刊《组合论杂志A辑》上发表论文的作者公开的文献。EULER产生了10个证明和3个反例，以及45个范围有限的局部结果。消融实验验证了两个机制：桥梁特定压力测试将错误结论从9个降至3个；桥梁材料与目标原生操作的结合产生了+4.2个已解决任务的积极交互效应，而这两个因素单独均无法达到此效果。领域距离并不能可靠预测成功；可执行操作的增益和有效回溯才是关键。## 1 引言
数学通过许多专业社群得以推进。组合数学家、代数学家、优化研究者和形式化专家可能面临相似的存在性问题，但使用不同的对象、不变量和证据标准。在社群内部，稳定的表示、熟悉的反例和成熟的工具使搜索高效。跨社群的连接则需要更多工作。研究者必须学习另一种语言，确定对象如何对应，揭示导入定理中隐藏的假设，并将结论带回到原始问题。这些转换之所以未被充分利用，是因为构建和验证代价高昂，而非其缺乏价值。此处的"未充分利用"是一个评估范围内的术语：在搜索前，冻结的直接和邻域操作库中缺乏等效的目标原生操作。这并非声称该连接在全球数学文献中完全不存在。
EULER将部分转换工作分配给一个协调的多智能体系统，该系统包含生成、检索、工具使用、批评和验证角色，并得到确定性程序和Lean的支持。围绕一个固定的源问题，它开发三种距离上的竞争路径：源领域的直接方法、到邻近社群的邻域桥梁，以及到不同对象或工具家族的远域桥梁。桥梁仅靠类比无法获得持续预算。系统首先搜索廉价的失败见证，检查目标领域是否增加了可执行操作，然后要求目标证据沿已注册的蕴含关系返回源命题。
一个近期结果提供了一个简明的例子。Zhoe猜想涉及有限阿贝尔群上的序列。自然语言搜索难以同时追踪重复元素的位置、子序列长度和零和约束。EULER为每个出现分配索引，将子序列编码为位掩码，并用确定性程序进行穷举检查。第一个编码合并了等值出现，未能通过往返测试。修正后的编码产生了一个具体的反例。第二个实现枚举了所有相关子集，之后人类审阅者将见证逐一代入原始命题的各个条件。该猜想被对象本身反驳，而非通过找到它的程序的成功终止。这个例子揭示了跨域搜索中两个常见的失败点。首先，目标工具必须改变可用操作。用另一种词汇重写群序列问题不会产生穷举证明；精确枚举则会。其次，目标表示中的成功并非终点。程序使用的对象、范围和谓词必须与源命题一致，且见证必须以正确的逻辑方向返回。一条不满足任一要求的路径可能看似有说服力，却未能证明原始问题的任何东西。
长期存在的著名猜想是自主数学发现的不良主要测试。诸如哥德巴赫猜想和Hadwiger猜想等问题积累了数十年的教科书、论文、论坛和网络讨论，在网络规模的训练语料库中存在先验暴露的可能性。当训练数据无法完全检查时，在此类任务上的成功尝试无法清晰区分新搜索与先前所见论证的回忆或重组。在已建立的和新委托的数学基准之间进行的对照比较发现，对于某些模型家族，性能差距与污染一致（Zhang等人，2024）。因此，我们优先考虑带有时间戳的近期源问题，并在执行前对任务和路径进行答案线索筛选。
本文研究EULER如何构建跨社群路径，这些路径如何在近期猜想上产生可检查的进展，以及系统的哪些部分解释了观察到的结果。我们全文使用以下术语：
- **桥梁**记录源对象、目标对象、映射、目标操作和返回义务。
- **邻域桥梁**链接共享主要对象或不变量的相邻社群。**远域桥梁**改变对象类、主控不变量或工具社群。
- **压力测试**是一种可检查的任务，旨在在路径获得大量预算前暴露方向、假设、边界情况、往返、工具增益或返回方面的错误。
- **已验证的解决**要求目标证据返回到固定的源命题，并涵盖证明或反例所需的每项义务。
图1：邻域和远域桥梁将源问题连接到目标原生操作。压力测试和源侧返回决定了目标证据是否改变源侧结果。
EULER将直接路径、邻域桥梁和远域桥梁置于一个长期运行的搜索过程中。路径竞争资源，共享引理或反例，并记录已失败的映射。六个桥梁特定压力测试决定何时停止和何时深入一条路径，其主要目标是源问题的已验证解决，而非目标侧验证。评估涵盖120个近期猜想、三个独立可检查的研究轨迹，以及对可执行操作集、返回安全性、模型多样性和成本的对照比较。远域检索解决了8个任务，而完整系统解决了13个。任务级别的配对差异为4.2个百分点，95%置信区间为[-0.1, 8.4]。桥梁特定压力测试将错误返回从9个减少到3个。在2x2实验中，桥梁材料和目标原生操作的交互效应为4.2个已解决任务，即3.5个百分点。每次已验证解决的中位数归一化成本比为1.12，其上限1.36超过了1.15的非劣效界。因此实验识别出返回安全效应和可执行操作集中的交互效应；在此样本量下，总体解决差异仍不确定。
第2节描述系统及一次运行的数据流。第3节按执行顺序介绍桥梁搜索和压力测试。第4节解释数学状态和验证。第5节介绍数据集构建和三个研究轨迹，第6节报告对照评估。最后两节讨论局限性和下一步工作。## 2 系统概述
EULER接收一个固定的源问题，返回路径谱系、数学结果和分项成本。中间对象跨天持续存在，当其证据改变时可在本地撤回。系统有四层：控制、执行、验证和数学状态。图2展示了它们如何交互。
控制层：路径选择、测试后预算重新分配、暂停与重启。
执行层：生成智能体、检索智能体、工具智能体、Lean智能体、确定性程序。
验证层：目标检查器、桥梁检查器、独立重放器、源侧审查器。
数学状态层：任务图、声明图、制品与记录、依赖与版本。
图2：一个EULER研究循环。中间行遵循数学工作流，控制层分配资源，状态层存储任务、依赖和验证记录。
### 2.1 四层架构
控制层维护路径池和预算。它根据源问题的结构为直接、邻域和远域路径分配配额，接收压力测试结果，并决定哪些桥梁停止，哪些进入更昂贵的目标搜索。其状态包括已知最便宜的拒绝测试、已通过检查、新可检查对象、估计返回成本和剩余预算。预算更新需要记录的测试结果或独立可检查的证据，而非仅叙述性评估。
执行层执行开放式工作。生成智能体提出证明草图和桥梁机会。检索智能体定位目标机制和定理。工具智能体调用枚举、计算机代数、SAT/SMT或领域特定检查器。Lean智能体翻译命题、检索前提并构建候选证明。确定性程序生成有限见证或覆盖证明。运行采用Claude 4.8、GPT-5.6和DeepSeek的异构组合。单次模型调用是一个执行事件，而非单独智能体；角色由其权限、输入和所需输出定义。
验证层处理那些陈述已精确的对象。目标检查器确定目标侧命题在目标表示中是否成立。桥梁检查器审计方向、假设差异、保持的结构和往返。独立重放器在隔离环境中重新运行Lean文件或程序证书。源侧审查器将目标结果代入固定的返回模板，并决定源命题是否已解决。路径提议者不能证明其自己的输出。
数学状态层存储两个图。任务图记录操作、预算、失败和恢复点。声明图记录精确陈述、证据、数学依赖和版本。数学制品和验证记录连接两者。完成目标搜索任务不必创建一个可能依赖于后续推理的声明。反之，一个局部声明可能为真而不解决根本问题。第4节指定了更新规则。
层间接口被刻意设计得狭窄。控制仅调度已注册的路径；执行提交候选和证据制品；验证发布范围有限的记录；数学状态从这些记录更新节点。表1列出了每个角色的输入、所需输出和状态权限。
表1：核心角色的输入、所需输出和状态权限
每个证据制品都由(q_v, r, b_v, c_v)键控：问题版本、路径、桥梁版本和声明版本。修改桥梁会创建新的b_v，因此为早期版本生成的证据不会自动支持修订版。模型可以在不改变数学依赖结构的情况下被替换。
### 2.2 系统组件与相关工作
EULER整合了四种能力：显式桥梁表示、持久数学状态、并行搜索和形式化验证。所有运行共享相同的问题版本、桥梁记录、运行标识符和成本定义。历史案例研究和工程测试不进入120任务评估。该设计补充了近期的数学智能体系统。Aletheia和RMA展示了长期自然语言研究和迭代角色分配。QED将系统组件与特定失败模式联系起来。Rethlas/Archon将非形式化探索与Lean验证连接起来。Albilich和Danus分别提供持久的证明状态和事实图编排。AI Co-Mathematician将相关能力置于异步研究工作空间中。EULER以数学社群间的桥梁作为其搜索单元，并在一个实验设计内评估目标操作和返回到源命题的证据。表示的改变也已被直接研究。Raggi等人寻找在离散数学中简化证明的表示，而基于对应和元搜索的方法对备选问题表示进行排序。翻译验证检查目标计算是否对应其源实例；反例引导的细化使用失败检查来改进抽象。近期关于可扩展数学发现的工作同样将问题选择和表示视为系统级瓶颈。EULER将表示选择与显式源返回测试相结合，并在同一任务级评估中度量两者。
### 2.3 单次运行的数据流
一次运行始于 S = (Γ_s, φ_s, v)，其中 Γ_s 包含假设，φ_s 是待证明或证伪的命题，v 是问题版本。系统固定允许的证据、边界对象、预算和停止规则，然后生成一个路径池。每个路径产生一条"桥梁机会"记录。通过压力测试的桥梁进入目标搜索。验证层重放提交的制品，并将其记录写入声明图。