Graph Invariant Search Lab

A Python-first research workbench for searching for counterexamples to inequalities between graph invariants, minimizing discovered witnesses, and producing reproducible verification artifacts.

This repository contains two things:

1. a runnable Stage-0/Stage-1 baseline (gilab) for exact and approximate invariant evaluation, random search, hill climbing, simulated annealing, parallel portfolios, result storage, minimization, and benchmarking;
2. a detailed implementation plan for Codex CLI to turn the baseline into a research-grade system.

The baseline is deliberately conservative. It can certify a violating evaluation only when every required quantity is exact or rigorously enclosed, the comparison is decisive, and the configuration does not request an independent backend that has not yet been run. Floating-point spectral values are discovery signals, not certificates.

Research objective

For a graph class (\mathcal C) and a conjectured inequality

[ L(G) \le R(G) \qquad \text{for every }G\in\mathcal C, ]

the search score is

[ s(G)=L(G)-R(G). ]

A graph with (s(G)>0) is a counterexample, provided that:

• the graph satisfies every domain hypothesis;
• the invariant definitions match the source exactly;
• the values are exact or accompanied by a rigorous certificate;
• an independent verifier reproduces the result.

The software must never promote a numerical near-violation to a theorem-level claim.

Supported baseline

The included implementation supports:

• undirected simple graphs;
• a compact integer-bitset graph representation;
• exact basic, distance, matching, clique, and independence invariants;
• approximate spectral invariants for discovery only;
• first-class exact integer, rational, rigorous interval, approximate, and unknown values;
• resource-bounded safe arithmetic expressions in YAML conjecture files;
• domain predicates such as connected, tree, bipartite, regular, planar, triangle-free, and degree bounds;
• random search, hill climbing, simulated annealing, and a multi-process portfolio;
• versioned SQLite run records with explicit candidate/verified/certified states, graph6 witnesses, JSON reports, and greedy minimization;
• invariant microbenchmarks and a preliminary capacity report.

The full roadmap adds nauty/Traces canonical labeling, exhaustive non-isomorphic generation, stronger exact solvers, incremental invariant updates, VNS/tabu/genetic/MCTS/AMCS search, independent certificates, and experiment scheduling.

Quick start on Ubuntu/Linux

1. Install system prerequisites

sudo apt update
sudo apt install -y \
  build-essential git python3 python3-dev python3-venv \
  pkg-config libgmp-dev graphviz sqlite3 jq time \
  numactl sysstat htop parallel zstd

Optional tools are described in docs/05_LINUX_TOOLCHAIN.md.

2. Create the Python environment

python3 -m venv .venv
source .venv/bin/activate
python -m pip install --upgrade pip wheel
python -m pip install -e '.[dev]'

Optional performance and solver dependencies:

python -m pip install -e '.[dev,fast,solvers]'

3. Validate the installation

make check
make doctor
make smoke

The smoke test uses an intentionally false demonstration inequality. It should find a certified counterexample quickly.

Milestone 1's negative controls are under configs/conjectures/traps/: one rejects an attractive graph outside the connected domain, and one ensures a floating-point spectral boundary result remains only a candidate.

4. Run a benchmark before any long experiment

make benchmark
cat benchmarks/smoke/REPORT.md

For the target 16-core / 192 GB machine:

python -m gilab.cli benchmark \
  --experiment configs/experiments/server_16c_192g.yaml \
  --output benchmarks/server-baseline

Do not assume that all 16 cores should be used. The correct worker count depends on the selected invariants, BLAS behavior, peak resident memory, and solver tail latency.

Use with Codex CLI

Codex reads AGENTS.md automatically from the repository. The complete implementation task is in CODEX_START_PROMPT.md.

Interactive workflow:

cd invariant-forge
codex

Then ask Codex to read CODEX_START_PROMPT.md, create a plan, and implement one milestone at a time.

Non-interactive first pass:

codex exec --sandbox workspace-write --ask-for-approval on-request \
  "Read AGENTS.md and CODEX_START_PROMPT.md. Inspect the repository, run the baseline tests, and produce a milestone-by-milestone implementation plan. Do not modify code until the plan identifies risks and acceptance tests."

Do not use a sandbox-bypass flag for this project. Search code executes generated configurations and external mathematical tools; keep the agent and experimental workloads bounded.

Core commands

# Show available invariant names and exactness metadata
gilab list-invariants

# Evaluate one graph6 witness
gilab evaluate \
  --conjecture configs/conjectures/demo_false_triangle_bound.yaml \
  --graph6 'C~'

# Search
gilab search \
  --conjecture configs/conjectures/demo_false_triangle_bound.yaml \
  --experiment configs/experiments/smoke.yaml

# Re-evaluate and graph6 round-trip a candidate
gilab verify \
  --conjecture configs/conjectures/demo_false_triangle_bound.yaml \
  --graph6-file runs/<run-id>/best.graph6

# Greedily minimize a certified witness
gilab minimize \
  --conjecture configs/conjectures/demo_false_triangle_bound.yaml \
  --graph6-file runs/<run-id>/best.graph6

Repository map

AGENTS.md                    Durable instructions for Codex
CODEX_START_PROMPT.md        Full implementation assignment
configs/                     Conjectures and experiment profiles
docs/                        Research and engineering specifications
scripts/                     Setup, resource-limited run, and reproducibility helpers
templates/                   Intake, campaign, review, and LLM accounting forms
src/gilab/                   Runnable baseline
tests/                       Unit and end-to-end smoke tests
runs/                        Generated experiment artifacts, ignored by Git
benchmarks/                  Generated performance measurements, ignored by Git

To create clean source archives after development:

make package

The packaging script excludes virtual environments, caches, generated runs, and generated benchmarks, and emits ZIP/tar.gz files plus SHA-256 checksums under dist/.

Non-goals

The initial system does not:

• prove a conjecture by failing to find a counterexample;
• certify floating-point spectral inequalities;
• treat a solver timeout as UNSAT;
• guarantee exact isomorphism deduplication without nauty/Traces;
• search all graphs beyond small orders;
• protect against every hostile third-party binary; run experiments in a cgroup or container;
• replace mathematical source review or independent peer verification.

Required reading

Start with:

1. docs/00_EXECUTIVE_SPEC.md
2. docs/01_MATHEMATICAL_MODEL.md
3. docs/02_SYSTEM_ARCHITECTURE.md
4. docs/06_RESOURCE_SAFETY.md
5. docs/07_BENCHMARKING_AND_CAPACITY.md
6. docs/08_EXPERIMENT_PROTOCOL.md
7. docs/11_IMPLEMENTATION_ROADMAP.md
8. docs/17_COST_AND_THROUGHPUT_MODEL.md

For a bounded one-hour pilot on the reference server, review the resource values and run:

scripts/run_pilot_1h.sh configs/conjectures/<reviewed-target>.yaml

Do not use the pilot profile on an open conjecture until the source interpretation, controls, benchmark report, and cgroup limits have been reviewed.

License

CC0-1.0 for the repository code. Third-party mathematical tools retain their own licenses and citation requirements.