发表机构
Comenius University in Bratislava（布拉迪斯拉发考门斯基大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本项目开发AutoGraphForge自动化图论发现流水线，整合Graffiti3生成器、新颖性过滤器、大规模图数据集及神经证明器，可生成并验证图论猜想，已通过初始测试。
AI 中文摘要
我们报告了正在进行的项目AutoGraphForge，旨在开发一个计算流水线，用于构建自动化的图论猜想-反驳-形式化-证明系统。猜想生成以反例为引导，分轮进行：Graffiti3生成器在小型、不断演化的快照表T（初始为数百个带有计算不变量的图）上提出猜想，该表仅通过对其自身猜想的反例进行扩展。一个包含559种经典和民间关系的新颖性过滤器（在传递复合和线性恒等替换下闭合），通过线性规划判断候选是否已被已知结果隐含。存活的候选将在约348000个图的数据集上接受测试，该数据集整合了完整的House of Graphs不变量导出、所有最多9个顶点的连通图的详尽普查、若干极值族（强正则图、最小拉姆齐图、凯莱图、笼图、杠铃图、棒棒糖图、蜘蛛图）以及随机模型。随后反例搜索算法对剩余候选展开攻击。在HPC集群上运行多轮后，该循环产生了6522个在反驳数据集、新颖性过滤器和所有主动搜索运行中存活的猜想——其中包括二分图和正则图的湮灭数与边覆盖数之间的非平凡关系，我们通过手动证明了这些关系。后续的形式化与证明阶段会将每个存活猜想确定性地转换为Lean 4的语句框架；每个候选证明都会针对固定的mathlib4和我们自定义的不变量序言进行内核验证。该阶段集成了两个神经证明器——DeepSeek-Prover-V2-671B（通过vLLM提供服务）和Lean专用的OProver-32B——置于独立的内核检查之后。该流水线已实现端到端运行，并通过了初始健全性检查，目前完整流水线正在集群上运行。
英文摘要
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.
Comments17 pages, 1 figure, 3 tables. Submitted to ITAT 2026 (Information Technologies -- Applications and Theory), CEUR Workshop Proceedings. Code: https://github.com/JanPastorek/AutoGraphForge
