AutoGraphForge：走向自动化图论发现

# AutoGraphForge：面向自动化图论发现  
**来源**：https://arxiv.org/html/2609.03478  

###### 摘要  
我们报告正在进行中的项目——开发一条计算流水线 *AutoGraphForge*，旨在构建自动化的图论猜想生成、反驳、形式化与证明系统。猜想生成采用反例引导机制并分轮进行：Graffiti3生成器在一个小型、不断演化的快照表 \(T\) 上提出猜想（该表初始包含数百个图及其计算不变量），并且仅因自身猜想的反例而逐步扩展。一个包含559个经典与常见关系的*新颖性过滤器*（在传递组合与线性恒等替换下封闭）通过线性规划判定候选猜想是否已被已知结果蕴含。随后，该猜想会在包含约348,000个图的数据集上进行检验，该数据集合并了完整的“House of Graphs”不变量导出、所有9阶及以下连通图的穷举枚举以及多种极图族（强正则图、极小拉姆齐图、凯莱图、笼图、哑铃图、棒棒糖图、蜘蛛图等），并辅以随机模型生成的图（随机正则图、\(G(n,p)\)、随机树与随机二分图）。接着，*反例搜索算法*尝试为仍存活的猜想寻找反例。该循环在高性能计算集群上运行多轮后，最终得到6,522个存活猜想——它们在反例数据集中无反例、未被新颖性过滤器标记为已知，且未被主动搜索过程排除。其中包含我们能手工证明的、关于二分图与正则图的湮灭数与边覆盖数之间的非平凡关系。后续的*形式化与证明*阶段将每个存活猜想确定性地转换为Lean 4语句框架；每个候选证明都经过内核验证，使用固定的mathlib4库和我们自定义的不变量前置定义。该阶段集成了两个前沿神经证明器——DeepSeek-Prover-V2-671B（通过vLLM提供服务）与Lean专用的OProver-32B——并在此独立内核检查之后运行。该阶段已实现端到端执行并通过初步健全性检查：确定性导出生成类型正确的Lean语句，证明器独立完成内核验证（针对平凡不等式），目前完整流水线正在集群上运行。  

###### 关键词  
自动化猜想生成，自动化定理证明，计算机辅助图论，反例搜索，人工智能，高性能计算  

††版权年份：2026††版权：本文版权归作者所有。允许在知识共享署名4.0国际协议（CC BY 4.0）下使用。  
††会议：ITAT 2026：信息技术——应用与理论，2026年9月25–29日，斯洛伐克弗尔沙茨  
††邮箱：[email protected]  
††单位：斯洛伐克布拉迪斯拉发，科米尼乌斯大学应用信息学系  

## 1 引言  
计算机辅助的数学结果与猜想发现拥有悠久历史，相关文献记载可见 Larson 与 Cleemput (2017)（https://arxiv.org/html/2609.03478#bib.bib1）；DeLaViña (2005)（https://arxiv.org/html/2609.03478#bib.bib2）。随着人工智能与高性能计算的发展，计算机在数学发现中的作用预计将进一步增强。事实上，陶哲轩 (Tao, 2025)（https://arxiv.org/html/2609.03478#bib.bib3）指出，计算机辅助数学研究的新方法已包括利用机器学习发现新关系、搜索反例以及使用形式化证明助手验证证明。此外，如该作者所言，ChatGPT 等大型语言模型可用于协助数学研究，例如检索已知文献或提出证明策略。该领域的一个全面入门资源是 2023 年 6 月美国国家科学院举办的“AI辅助数学推理”研讨会论文集 Koretsky (2023)（https://arxiv.org/html/2609.03478#bib.bib4）；作为成果之一，Talia Ringer 主持编制了 AI 数学应用的社区资源列表，该列表可在 https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 获取并持续更新。  
本文基于计算机辅助的数学研究阶段，将其划分为四类：(i) 基于知识库进行*猜想生成*新命题，(ii) 通过搜索反例或矛盾进行*反驳*，(iii) 将其*形式化*为严格语言，以及最终在形式系统中进行*证明*。图论中的自动化猜想生成已有四十年历史，从 Fajtlowicz 的 Graffiti Fajtlowicz (1988)（https://arxiv.org/html/2609.03478#bib.bib5）；Wikipedia contributors (2026)（https://arxiv.org/html/2609.03478#bib.bib6）；Larson (2002)（https://arxiv.org/html/2609.03478#bib.bib7）与 DeLaViña 的 Graffiti.pc DeLaViña (2002)（https://arxiv.org/html/2609.03478#bib.bib8）；DeLaViña (2005)（https://arxiv.org/html/2609.03478#bib.bib2），到 Aouchiche、Caporossi、Hansen 与 Mélot 的 AutoGraphiX/GraPHedron 项目 Aouchiche et al. (2009)（https://arxiv.org/html/2609.03478#bib.bib9）；Caporossi and Hansen (2004)（https://arxiv.org/html/2609.03478#bib.bib10）；Mélot (2008)（https://arxiv.org/html/2609.03478#bib.bib11），以及近期的 Davila 的 TxGraffiti Davila (2024)（https://arxiv.org/html/2609.03478#bib.bib12）；Caro et al. (2022)（https://arxiv.org/html/2609.03478#bib.bib13）与 The Optimist Davila (2024)（https://arxiv.org/html/2609.03478#bib.bib14），Larson 基于 Dalmatian 的 Conjecturing Larson and Cleemput (2016)（https://arxiv.org/html/2609.03478#bib.bib15）；Larson and Cleemput (2017)（https://arxiv.org/html/2609.03478#bib.bib1）与 Graffiti3 Davila (2026)（https://arxiv.org/html/2609.03478#bib.bib16），以及多面体 PHOEG 系统 Bonte et al. (2026)（https://arxiv.org/html/2609.03478#bib.bib17）。  
这些系统通过将候选界限拟合到有限图数据集，并仅保留通过一组过滤器与启发式方法的猜想，提出图不变量之间的不等式（如 \(\alpha(G) \leq \nu(G)\)、\(\chi(G) \leq \Delta(G)+1\) 等）。搜索图论不等式空间已形成三种不同范式：*代数表达式树*（用于 Graffiti 与 Conjecturing）将候选猜想构建为以一元和二元运算（和、积、平方根）组合不变量的有根树，并通过穷举或启发式树搜索枚举候选；*线性与混合整数规划*（用于 TxGraffiti Davila (2024)、Caro et al. (2022)，The Optimist Davila (2024)，以及 Graffiti3 Davila (2026)）则在预计算的表状数据集上求解优化模型，通过最小化目标不变量与其他不变量线性组合之间的距离，在无需枚举的情况下找到最紧可能界限；*多面体/几何*方法（用于 GraPHedron Mélot (2008)、Caporossi and Hansen (2004)，PHOEG Bonte et al. (2026)、Christophe et al. (2008) 以及近期的 Graffiti3 Davila (2026)）将每个图嵌入不变量空间作为点，并读取结果凸包的面作为猜想，从而为这些不变量产生最优线性不等式的完整集，并使最优性成为几何证书。  
许多生成的猜想已成为定理；部分已被手工或机器搜索反驳，例如 Brewster et al. (1995)（https://arxiv.org/html/2609.03478#bib.bib19）；Larson and Cleemput (2017)（https://arxiv.org/html/2609.03478#bib.bib1）；Jooken (2025)（https://arxiv.org/html/2609.03478#bib.bib20）。任何使用此类系统的人都可能遇到五种潜在故障模式：第一，候选不等式在有限数据集中成立，但*整体为假*——数据集缺乏破坏它的结构；第二，系统产生*真但已知*的候选，已在文献中记录；第三，系统产生*真但平凡*的候选，导致“平凡性雪崩”；第四是*巨型猜想* Davila (2026)——单个猜想通过积累多项与常数过度拟合表格，产生不必要的复杂界限（如 \(\alpha \leq 0.31\,\Delta + 0.42\,\nu - 0.07\,m + 1.8\)）；第五，系统可能“发现”一个完善猜想的反例，这几乎总是表明不变量程序中的错误。  
第一与最后一种故障模式涉及信任：生成的“成立”不等式与验证的“反例”均仅依赖其背后的数据与不变量计算。第二与第三种故障模式涉及新颖性：真但已知或真但平凡的候选在数学上无趣，对实践者价值有限。所有这些故障模式在我们的流水线中均通过对抗性反例搜索、新颖性过滤器与选择启发式方法得到缓解——尽管如 §4.2（https://arxiv.org/html/2609.03478#S4.SS2）所示，平凡性问题尚未完全消除。为应对第一与第四种故障模式——虚假界限与过拟合——需要健壮的反驳引擎。Jorik Jooken 的综述文章最近总结了用于搜索图（反）例的计算方法 Jooken (2025)（https://arxiv.org/html/2609.03478#bib.bib20），其中包括带分支定界穷举搜索、随机搜索与启发式搜索。近期，深度强化学习已被用于反驳多个猜想 Wagner (2021)（https://arxiv.org/html/2609.03478#bib.bib21）。  
关于后两个阶段，*证明助手*（如 Lean 4 de Moura et al. (2015)（https://arxiv.org/html/2609.03478#bib.bib22））是一种编程语言，数学命题及其证明以形式对象编写；一个小型可信*内核*机械检查每个证明，因此命题仅在其证明正确直至公理时才被接受——没有含糊步骤的空间。Lean 与 mathlib4 van Doorn et al. (2020)（https://arxiv.org/html/2609.03478#bib.bib23）配对，这是一个大型社区库，包含已形式化的数学内容（定义、引理与标准图论词汇），人们可在此基础上构建而非从头推导。将非正式自然语言命题转换为这种形式化 Lean 语句称为*自动形式化* Wu et al. (2022)（https://arxiv.org/html/2609.03478#bib.bib24）；寻找其证明则是*自动化定理证明器*的任务。近期的*神经*证明器是大型语言模型，在形式化证明上训练，旨在输出候选 Lean 证明——要么一次性生成（*全证明*），要么通过迭代编译器错误消息（*代理*循环）——然后交给内核进行独立检查，因此模型仅提议，内核裁决。  
近期关于自动形式化与自动化定理证明（尤其在 Lean 中）的工作日益增多，包括图论领域，例如 Wu et al. (2022)；Mavani and Pflueger (2026)（https://arxiv.org/html/2609.03478#bib.bib25）；Nader et al. (2026)（https://arxiv.org/html/2609.03478#bib.bib26）；Kalfus and Lidický (2026)（https://arxiv.org/html/2609.03478#bib.bib27）；Zhang et al. (2026)（https://arxiv.org/html/2609.03478#bib.bib28）；DeepSeek-AI (2025)（https://arxiv.org/html/2609.03478#bib.bib29）。尽管我们在 Davila (2026)（https://arxiv.org/html/2609.03478#bib.bib16）中发现了某些相关实验，但据我们所知，目前尚无系统在图论发现的闭环中集成自动化猜想生成、反驳、形式化与证明。  
本文描述并报告了此类计算系统 AutoGraphForge 的开发，旨在将 (i)-(iv) 整合为一条流水线。前两个阶段组合为*生成-反驳*循环，其中猜想被生成，然后在包含已知定理与（极）图（附带计算不变量）的数据库上检验。针对候选猜想的反例被添加到数据集中，用于后续轮次中猜想的精炼。存活此过程的猜想被转换为形式化语言 Lean，并尝试使用自动化定理证明器进行证明。  
我们当前的贡献包括：  
1. 我们构建了计算流水线 AutoGraphForge 的第一个版本，并在高性能计算集群上大规模运行其生成-反驳循环：一个分轮进行的反例引导循环，分为五个全节点 SLURM 作业，随后进行合并。形式化与证明阶段已实现并集成到软件包中（确定性 Lean 导出加两个前沿神经证明器——通过 vLLM 提供的 DeepSeek-Prover-V2-671B 与 Lean 专用的 OProver-32B，以及基于 mathlib4 的独立内核验证）；它通过了初步健全性检查——确定性 Lean 导出产生类型正确的目标，证明器独立完成平凡不等式的内核验证——但尚未在存活猜想上进行受控评估（§3.5）。  
2. 我们创建了包含 559 个经典、常见与平凡关系的新颖性过滤器（§3.3）——涵盖色数、连通性、匹配/覆盖、控制与零强迫族——在 \(\leq\) 关系的传递组合与线性恒等替换下封闭。该过滤器还包括一个线性规划新颖性测试，用于判定候选不等式是否被已知关系蕴含。  
3. 我们构建了包含 348,207 个图（携带最多 59 个精确计算的不变量）的反驳数据集，合并了完整的 House of Graphs (HoG) Coolsaet et al. (2023)（https://arxiv.org/html/2609.03478#bib.bib30）导出与许多其他极图族，包括强正则图、极小拉姆齐图、凯莱图、笼图、补可约图、极小刚性图、哑铃图、棒棒糖图、蜘蛛图等，以及从随机模型（正则图、Erdős–Rényi、二分图与树图）生成的图。  
4. 我们实现了反例搜索算法（§3.4.2），其中包括近期前沿方法，如使用交叉熵法与蒙特卡洛方法的概率搜索。需注意，我们的系统并非从零构建，而是建立于猜想生成、反驳、形式化与证明这三个领域现有前沿文献中的包、框架与方法之上。特别地，猜想生成基于 TxGraffiti2 Davila (2024) 与 Graffiti3 Davila (2026)；反例搜索算法基于近期前沿方法构建。