自动发现图论新猜想，通过智能筛选与验证，已生成6522条未被证伪的猜想。
AutoGraphForge: Towards Automated Graph Theory Discovery
- 基于反例引导的迭代机制，逐步扩展图数据库并生成新猜想。
- 在34.8万张图上验证后，筛选出6522个未被证伪的新关系，包括非平凡图论命题。
- 集成神经证明器与形式化系统，实现从猜想到可验证定理的自动化流程。
我们报告了正在开发的自动化图论发现系统AutoGraphForge，该系统旨在实现猜想生成、反驳、形式化与证明的全流程自动化。猜想生成采用反例引导机制，以不断演化的图快照表T（初始包含数百张图及其不变量）为基础，仅通过自身猜想的反例来扩充数据。一个包含559个经典与俗成关系的新颖性过滤器，通过线性规划判断候选猜想是否已被已有结果蕴含。通过筛选的候选猜想在约34.8万张图的数据集上进行测试，该数据集整合了完整的图之家不变量导出、所有连通图至九顶点的穷举普查、多个极值族（强正则图、最小拉姆齐图、凯莱图、围图、吊坠图、棒棒糖图、蜘蛛图）以及随机模型。剩余候选由反例搜索算法进一步攻击。在超算集群上运行多轮后，共获得6522条经反例数据集、新颖性过滤和主动搜索均未被证伪的猜想，其中包括关于二分图与正则图中湮灭数与边覆盖数之间非平凡关系的命题，已人工证明。后续形式化阶段将每个幸存猜想确定性地转化为Lean 4语句框架；每项候选证明均经内核校验，基于固定版本的mathlib4及自定义不变量前置库。该阶段集成了两个神经证明器——DeepSeek-Prover-V2-671B（通过vLLM服务）与专用于Lean的OProver-32B——并置于独立内核检查之下。系统端到端实现并通过初步合理性检验，当前全管道已在集群上运行。
原文摘要 · Abstract (English)
We report on our ongoing project to develop a computational pipeline, AutoGraphForge, for an automated graph-theoretic conjecturing-refuting-formalizing-proving system. Conjecture generation is counterexample-guided and runs in rounds: a Graffiti3 generator proposes conjectures over a small, evolving snapshot table $T$ (initially a few hundred graphs with their computed invariants) that grows only by counterexamples to its own conjectures. A novelty filter of $559$ classical and folklore relations, closed under transitive composition and linear identity substitution, decides via a linear program whether a candidate is already implied by known results. Surviving candidates are tested against a dataset of about $348,000$ graphs, unioning the complete House of Graphs invariant export, the exhaustive census of all connected graphs on at most nine vertices, several extremal families (strongly regular, minimal Ramsey, Cayley, cages, barbells, lollipops, spiders), and random models. Counterexample-search algorithms then attack the remainder. Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset, the novelty filter and every active-search run -- among them nontrivial relations between the annihilation number and the edge-cover number for bipartite and regular graphs, which we prove by hand. A subsequent formalization and proving stage deterministically translates each surviving conjecture into a Lean 4 statement skeleton; every candidate proof is kernel-verified against a pinned mathlib4 and our custom invariant preamble. This stage integrates two neural provers -- DeepSeek-Prover-V2-671B (served with vLLM) and the Lean-specialised OProver-32B -- behind the independent kernel check. It is implemented end-to-end and passes initial sanity checks, with the full pipeline currently running on the cluster.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。