AutoGraphForge: Towards Automated Graph Theory Discovery

• URL: http://arxiv.org/abs/2609.03478v1
• Date: Thu, 03 Sep 2026 07:35:29 GMT
• Title: AutoGraphForge: Towards Automated Graph Theory Discovery
• Abstract summary: AutoGraphForge is an automated graph-theoretic conjecturing-refuting-formalizing-trivial system.<n>A novelty filter decides via a linear program whether a candidate is already implied by known results.<n>Run for several rounds on an HPC cluster, the loop yields $6,522$ conjectures that survived the refutation dataset.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• GRAND-HC: Graph-Refined Author Name Disambiguation [58.02589236670033]
  From-Scratch Name Disambiguation (SND) groups papers sharing an ambiguous name into clusters of distinct real-world authors.<n>We propose textbfGRAND-HC, a complete end-to-end SND framework.
  arXiv  Detail & Related papers  (2026-08-24T08:21:28Z)
• Neurosymbolic Discovery of Algebraic Graph Constructions [22.962110170304594]
  We ask whether one can automatically discover a short algebraic description if only this raw data is provided.<n>We propose an agent that runs on a general-purpose large language model with no fine-tuning or per-target training.<n>We test the approach on a benchmark of 100 highly symmetric graphs.
  arXiv  Detail & Related papers  (2026-08-08T13:07:51Z)
• Machine-Checked Certificates for the Geometric Half of the Minimum Kochen-Specker Bound [0.0]
  The best known lower bound for the minimum Kochen-Specker vector system in $mathbbR3$ rests on a computational proof whose half emits DRAT but whose geometric half does not.<n>We introduce exact rational case-tree certificates of real nonembeddability, whose splits are factorizations and rational sum-of-squares decompositions.<n>All certificates, checkers, and proofs are available and replayable from a single build.
  arXiv  Detail & Related papers  (2026-07-29T02:53:00Z)
• Formalizing Flag Algebras in Lean [8.924529562496874]
  Razborov's flag algebra method is a powerful tool for proving inequalities in extremal graph theory.<n>We present a machine-checked formalization of the method, together with a certificate-to-proof compiler.<n>Case studies yield formal proofs of seven Turn-type upper bounds.
  arXiv  Detail & Related papers  (2026-07-26T07:07:29Z)
• Quantum Algorithm for Identifying Hidden Graphs: Spectral Theory and Numerical Evidence [0.0]
  We give a quantum algorithm for identifying a hidden $d$-regular base graph $G$ on $n$ vertices from access to an obfuscated version of it.<n>Our algorithm is conceptually simple: a continuous-time walk on $G_rm spire$, followed by a single Hadamard test at a classically pret*$.
  arXiv  Detail & Related papers  (2026-05-11T20:44:32Z)
• Accelerated Evolving Set Processes for Local PageRank Computation [75.54334100808022]
  This work proposes a novel framework based on nested evolving set processes to accelerate Personalized PageRank computation.<n>We show that the time complexity of such localized methods is upper bounded by $mintildemathcalO(R2/epsilon2), tildemathcalO(m)$ to obtain an $epsilon$-approximation of the PPR vector.
  arXiv  Detail & Related papers  (2025-10-09T09:47:40Z)
• Graph Random Features for Scalable Gaussian Processes [52.89901965157282]
  We study the application of graph random features (GRFs) to scalable Gaussian processes on discrete input spaces.<n>We prove that (under mild assumptions) Bayesian inference with GRFs enjoys $O(N3/2)$ time complexity with respect to the number of nodes $N$, compared to $O(N3)$ for exact kernels.
  arXiv  Detail & Related papers  (2025-09-03T20:13:23Z)
• On the Unlikelihood of D-Separation [69.62839677485087]
  We provide analytic evidence that on large graphs, d-separation is a rare phenomenon, even when guaranteed to exist. For the PC Algorithm, while it is known that its worst-case guarantees fail on non-sparse graphs, we show that the same is true for the average case. For UniformSGS, while it is known that the running time is exponential for existing edges, we show that in the average case, that is the expected running time for most non-existing edges as well.
  arXiv  Detail & Related papers  (2023-03-10T00:11:18Z)
• Graph Signal Sampling for Inductive One-Bit Matrix Completion: a Closed-form Solution [112.3443939502313]
  We propose a unified graph signal sampling framework which enjoys the benefits of graph signal analysis and processing. The key idea is to transform each user's ratings on the items to a function (signal) on the vertices of an item-item graph. For the online setting, we develop a Bayesian extension, i.e., BGS-IMC which considers continuous random Gaussian noise in the graph Fourier domain.
  arXiv  Detail & Related papers  (2023-02-08T08:17:43Z)
• AnchorGAE: General Data Clustering via $O(n)$ Bipartite Graph Convolution [79.44066256794187]
  We show how to convert a non-graph dataset into a graph by introducing the generative graph model, which is used to build graph convolution networks (GCNs) A bipartite graph constructed by anchors is updated dynamically to exploit the high-level information behind data. We theoretically prove that the simple update will lead to degeneration and a specific strategy is accordingly designed.
  arXiv  Detail & Related papers  (2021-11-12T07:08:13Z)
• Inferring Hidden Structures in Random Graphs [13.031167737538881]
  We study the two inference problems of detecting and recovering an isolated community of emphgeneral structure planted in a random graph. We derive lower bounds for detecting/recovering the structure $Gamma_k$ in terms of the parameters $(n,k,q)$, as well as certain properties of $Gamma_k$, and exhibit computationally optimal algorithms that achieve these lower bounds.
  arXiv  Detail & Related papers  (2021-10-05T09:39:51Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.