AutoGraphForge自动发现6522个图论猜想，还挖出非平凡关系并亲手证明！
AutoGraphForge: Towards Automated Graph Theory Discovery
📖 AI 总结
AutoGraphForge是一个旨在自动化图论发现的计算管道系统，其核心流程涵盖猜想生成、反驳、形式化与证明四个阶段。系统采用反例引导的迭代机制，由Graffiti3生成器基于小型演化快照表提出猜想，并通过包含559条经典关系的线性规划新颖性过滤器排除已知结论。候选猜想需在约34.8万个图的数据库上接受验证，涵盖House of Graphs导出数据、九顶点以内连通图全集及多种极值图族。在HPC集群上运行多轮后，系统产生6,522条通过所有筛选的猜想，其中部分关于二部图和正则图的湮灭数与边覆盖数关系已被人工证明。最终阶段将幸存猜想自动转化为Lean 4语句骨架，并集成DeepSeek-Prover-V2-671B和OProver-32B两个神经证明器，通过内核验证确保正确性。该工作展示了AI驱动数学发现与机器验证结合的技术路径。
🔑 关键词速览
| AutoGraphForge | 一个自动化的图论猜想生成与证明流水线系统。 |
| Graffiti3 | 一个基于反例引导的猜想生成器，用于提出图论猜想。 |
| novelty filter | 新颖性过滤器，用于判断候选猜想是否已被已知结果蕴含。 |
| Lean 4 | 一个交互式定理证明器，用于形式化数学证明。 |
| kernel check | 内核检查，指对证明进行独立验证以确保其正确性。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅