AutoGraphForge: Towards Automated Graph Theory Discovery

Ján Pastorek

Source-linked AI summary

AutoGraphForge: Towards Automated Graph Theory Discovery

Ján Pastorek

arXiv:2609.03478v1Sep 3, 2026cs.AIcs.LOmath.CO

TL;DR

AutoGraphForge targets the missing integration of automated graph-theoretic conjecturing, refutation, formalization, and proving. It combines counterexample-guided generation, novelty filtering, refutation, deterministic Lean export, and kernel-checked neural proving. The generate–refute run produced 6,522 surviving conjectures, while the proving stage has only passed initial sanity checks and has not yet been run over those candidates.

Problem
No existing system integrates automated graph-theory conjecturing, refuting, formalizing, and proving in a closed loop.
Method
AutoGraphForge generates and filters conjectures, refutes them across rounds, deterministically translates survivors to Lean, and checks candidate proofs with an independent kernel.
Results
6,522 conjectures survived the merged multi-round generate–refute run after duplicate removal.
Takeaways & Limitations
The implemented pipeline demonstrates large-scale generate–refute operation and supplies a formal verification path for surviving conjectures.
Takeaways & Limitations
The formalization-and-proving stage has not yet been run over the surviving conjectures, so the loop is not closed.

Abstract

from arXiv · show

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.

1. Introduction

AutoGraphForge addresses the lack of a closed-loop graph-theory system integrating conjecturing, refutation, formalization, and proving. It combines counterexample-guided generation, novelty filtering, large-scale search, and formal verification, while its proving stage remains unevaluated over surviving conjectures.

Computer-assisted mathematical discovery increasingly combines machine learning, counterexample search, and formal proof assistants.
Graph-theory conjecturing systems generate invariant inequalities from finite graph datasets but face risks of false, known, trivial, or overfit conjectures.
Adversarial counterexample search, novelty filtering, and selection heuristics mitigate these failure modes, though triviality is not eliminated.
AutoGraphForge combines generate–refute rounds with Lean translation and automated theorem proving in one computational pipeline.
The system runs its first three stages end-to-end at scale, while the proving stage is implemented and sanity-checked but not yet properly evaluated.

2. Preliminaries

The paper works with finite simple graphs and computes a broad invariant vocabulary, including classical parameters and less-standard quantities relevant to later formalization and proving.

All graphs are finite and simple, with order n=|V(G)| and size m=|E(G)|.
The pipeline computes 59 graph invariants, while the paper defines only those used in its arguments.
The invariant set includes degree, independence, matching, covering, coloring, domination, connectivity, metric, spectral, and triangle-count parameters.
On regular graphs, the common degree, minimum and maximum degree, average degree, and spectral radius satisfy Δ = δ = 2m/n = ρ.
Zero-forcing and total zero-forcing numbers are less-standard invariants whose definitions matter for the proving stage.
The paper also uses cographs, split graphs, and well-covered graphs as specialized graph classes.

3. The AutoGraphForge Architecture

AutoGraphForge couples conjecture generation, ranking, refutation, and formalization/proving around an evolving invariant table. Its invariant computations were cross-validated without mismatches on sampled House of Graphs data.

AutoGraphForge uses a knowledge base of graphs and computed invariants plus known theorems, with counterexamples added to the evolving snapshot table T.
Candidate conjectures are generated from T, filtered and ranked, aggressively refuted, and advanced only after surviving multiple rounds.
GraphCalc computes stored invariant values exactly or leaves them empty after timeout, while networkx provides an independent cross-check.
0 mismatches were found across shared invariants when GraphCalc was compared with independently computed House of Graphs values on 2,500 graphs.

3.2. Conjecture generation as theory selection

AutoGraphForge treats conjecture generation as selecting informative theory statements from an evolving geometric snapshot. Graffiti3 produces numeric and boolean candidates, which are filtered and tested before refutation.

AutoGraphForge builds on TxGraffiti2 and Graffiti3, whose native conjecture objects are consumed by the novelty filter, selection heuristics, and refutation engine.
The generator represents invariant inequalities as halfspaces that must hold over every graph in the current snapshot T.
Only facet inequalities tight on an extremal snapshot object are information-bearing among the infinitely many inequalities valid on T.
Graffiti3 generates ratio, product, square-root, logarithmic, and boolean conjectures using graph predicates and the Sophie heuristic.
Conjectures begin from expressive graphs and a 59-invariant snapshot that grows only when counterexamples are found.

3.3. Sorting candidates and novelty filtering

AutoGraphForge reduces candidate overload and filters out conjectures that are trivial, redundant, or already implied by known graph-theoretic relations. Its novelty test uses sound class-restricted linear implications and an LP feasibility certificate.

Candidate sorting: Without aggressive filtering, conjecture systems can generate thousands of trivial or redundant statements, motivating tight-bound selection and novelty checks.Graffiti3 applies Dalmatian, Morgan, and Touch sorting heuristics to candidate bounds.
Novelty filtering: The novelty filter tests whether a linear candidate bound is implied by known bounds that hold over its entire hypothesis class or a superclass.This restriction preserves soundness when aggregating known theorems and lower bounds.
Novelty filtering: A candidate is redundant when a convex combination of known theorems is at least as tight as the candidate.The same implication framework handles equalities, reverse inequalities, and selected necessary or sufficient conditions.
Novelty filtering: LP feasibility certifies redundancy by matching invariant coefficients using non-negative theorem weights, slacks, and free class-identity multipliers.The resulting identity expresses the candidate-minus-aggregate difference as terms known to be non-negative.
Novelty filtering: 559 classical, folklore, and trivial relations populate the novelty knowledge base after closing simple inequalities under transitivity.Examples include Whitney’s connectivity chain, König’s equality for bipartite graphs, and Gallai’s identity.

3.4. Counterexample search and refutation

AutoGraphForge treats survival on a finite graph table as insufficient evidence and progressively attacks candidates with larger datasets, graph families, random models, and specialized counterexample searches. A shared violation margin lets different search backends optimize for decisive refutations.

Refutation workflow: A conjecture that survives the current snapshot is not thereby generalized to all finite graphs, so the system actively searches for counterexamples.The pipeline combines dataset testing, parametric and random families, and specialized search algorithms.
Refutation workflow: 348,207 graphs form the static first-line refutation dataset before candidates proceed to parametric families, random models, and active search.The dataset combines House of Graphs data with additional graph sources and computed invariant columns.
Refutation dataset: The dataset contains 59 invariant columns: 45 numeric targets for generated inequalities and 14 boolean graph-class predicates.Two derived order thresholds are also added for the battery’s graph-class conditions.
Counterexample-search algorithms: The margin measures a graph’s violation of a candidate, with positive values identifying refutations and larger values indicating more decisive counterexamples.Every backend shares this interface and seeks graphs maximizing the margin.
Counterexample-search algorithms: Search backends include SMT encoding, linear cross-entropy distribution search, and variable-neighbourhood search with stochastic edge modifications.Backends may start randomly or be seeded from another graph.

3.5. Formalization and proving

The formalization stage deterministically converts surviving conjectures into Lean 4 goals, while neural provers attempt proofs that are independently checked by the Lean kernel. The stage is integrated and sanity-checked but has not yet undergone full evaluation.

Stage status: The proving layer has not yet been fully run over surviving conjectures and has so far received only initial sanity checks on trivial cases.This distinguishes implementation readiness from evidence about proving performance.
Formalization: Each supported conjecture is mechanically translated from invariant and graph-class names into a Lean 4 theorem skeleton.The exported skeleton elaborates to a type-correct goal with a sorry placeholder rather than a certified proof.
Proving: DeepSeek-Prover-V2-671B and OProver-32B generate candidate proofs, while mathlib4 and the GraphInvariants preamble provide the checked formal environment.Passing proofs are persisted as self-contained Lean files and re-verified by a standalone kernel pass.
Initial checks: Initial checks showed faithful, type-correct export and successful end-to-end proofs for δ≤Δ and ω≤n.These deliberately trivial results validate integration of export, prover interfacing, and independent verification, not broad proving capability.
Scope and difficulty: Many surviving conjectures may be difficult because invariants such as zero-forcing are defined in the custom preamble and absent from prover training data.The paper identifies this training-distribution mismatch as a likely reason proving will be the hardest stage.

4. Discovery in graph theory

AutoGraphForge runs a counterexample-guided generate–refute loop at cluster scale, producing thousands of survivors while revealing both rediscoveries and meaningful provable relations. The discovery results include 6,522 merged survivors, but auditing shows that many inspected candidates remain trivial or definitional artefacts.

Iterative run dynamics: 1,249 of 3,959 baseline candidates were refuted, mostly by extremal-family, random-model, and House of Graphs datasets before counterexample search.The baseline used an intermediate snapshot of 1,554 graphs and supports testing fast parametrised datasets before expensive search.
Iterative run dynamics: The five-partition run started from 2,860 graphs, added witnesses until fixed points, and produced 8,281 raw survivors before merging.Partition 1 terminated at round 9, while the other four terminated at round 5; first-round growth was approximately 500–790 witnesses per partition.
Survivor set: 6,522 survivors remained after merging, comprising 2,677 class-conditioned inequalities and 3,845 Sophie conditions.The merge removed 1,413 candidates refuted by witnesses from other partitions and 346 cross-partition duplicates.
Survivor set: The pipeline recovered 33 classical results, providing a soundness check rather than evidence of discovery capability.Recovered examples include Gallai’s identity, the König–Egerváry theorem, and standard matching, covering, and domination inequalities.
Audit and examples: Among 100 highest-touch survivors, 49 were recognised rediscoveries, 2 were implied by stronger survivors, 1 was decorative, and 48 were neither known trivial nor false to the authors.All 100 had survived refutation against the full 348,207-graph dataset, so the authors did not classify any as probably false.
Audit and examples: Two complementary class-conditioned relations between annihilation number and edge-cover number were nontrivial, true, and provable by short arguments.The bipartite relation follows from Gallai, König, and Pepper’s bound; the regular relation uses a(G)=floor(n/2), matching bounds, and Gallai’s identity.

5. Discussion and future work

The authors identify further analysis and proof-search integration as future work, while proposing additional filters and language-model roles for expanding the pipeline.

Future work: 6,522 surviving conjectures await further analysis, and the authors want more known results in the novelty filter to make this set more manageable.The stated goal is to reduce the number of conjectures requiring downstream analysis.
Closing the loop: The formalization-and-proving stage is implemented but has not yet been run on the surviving conjectures.Running Lean proof search over the translated conjectures is identified as the immediate next step.
Closing the loop: A preamble-specific lemma library is expected to be the main obstacle because the neural provers were not trained on the custom invariants.The proposed lemma library would ground proof search in the paper’s invariant definitions.
Additional filters: The proposed Devil’s Advocate filter would assume surviving conjectures are true and explore their consequences, but it has not yet been implemented.The authors describe this as an extension of the generate–refute and proving loops.
Language-model extensions: The authors also propose using large language models as conjecture critics and potentially as generators and provers across the pipeline.The critic would assess plausibility and provide feedback to help prioritize candidates.

Declaration on Generative AI

The author used a large language model as a coding and experimentation assistant while retaining responsibility for reviewing, editing, and verifying the work.

Generative AI use: A large language model assisted with implementing the pipeline, running experiments, and drafting the manuscript.The declaration describes the model’s role as assistance during preparation of the work.
Author responsibility: The author reviewed and edited all content and takes full responsibility for the publication’s content.Computational results were verified against authoritative data sources, including House of Graphs and exact GraphCalc recomputation.

A. Computational setup

The computational setup combines large-memory HPC nodes, deterministic invariant partitioning, and an extensive precomputation workload whose expensive NP-hard components motivate alternative solver encodings.

Cluster hardware and execution: HPC workloads ran on HPE Cray XD2000 nodes with 256 cores, 1,536 GB RAM, and 200 Gb/s InfiniBand.The generate–refute experiment used five independent full-node SLURM partitions.
Computational bottleneck: Precomputation dominates runtime, with NP-hard invariants as the main contributors to cost.The authors identify replacing ILP formulations with SAT or CP-SAT as the most promising engineering change.
Target-invariant partitioning: 45 numeric target invariants were split into five alphabetical blocks of nine for deterministic load balancing, not semantic grouping.Related invariant families were deliberately scattered across partitions.
Target-invariant partitioning: The partitions cover graph invariants including connectivity, annihilation, domination, edge-cover, matching, spectral, and forcing measures.The listed blocks include annihilation number, edge-cover number, matching number, spectral radius, and several domination and zero-forcing variants.

B. Counterexample-search backend settings

Counterexample-search backends used fixed standard settings and bounded per-candidate runtime, while the HPC sweep extended search across graph orders from 10 to 100.

Backend settings: Active-search hyperparameters were not optimized and remained unchanged across all conjectures.All backends were seeded from the structured base library and run under a per-candidate wall-clock cap.
Backend settings: Table 3 reports standard backend hyperparameters rather than settings tuned separately for each conjecture.The caption characterizes the values as standard defaults.
Order sweep: The HPC search covered graph orders n=10 to n=100, scaling trials down at larger orders while preserving a meaningful minimum.A per-candidate wall-clock budget bounded round time as exact invariant computation became more expensive.