Benchmark results and research summaries, in the words of the posters and papers themselves. Each result states its own scope and conditions, including where we did not win. Full posters and papers are available on request by email.
Garmo Solvers benchmark results
Head-to-head results against established solvers, with every answer re-checked against the original input. Win, tie and loss counts are reported as measured.
GARMO SOLVERS · S01
Proof-Carrying Max-Cut on a GH200: 67 Biq Mac Optima Proved vs HiGHS's 49
Rigorous SDP and Odd-Cycle LP Bounds in a GPU Branch-and-Bound, Every Proof Re-Checked by an Independent Verifier.
67 vs 49Biq Mac instances proved optimal, CertCut vs HiGHS (148)
58/83/7wins / ties / losses vs HiGHS
71/71Gset upper bounds re-verified by the CPU verifier
L = 92-D ±J torus: every seed proved up to n = 81
Biq Mac proved optimal per family (families where anyone proves) No method proves g05_100, pm1d, w05/w09 or the Ising sets with n ≥ 200 within 300 s.
Time to proof where both prove Above the line CertCut is faster.Every lever vs the basic control Only the density-routed odd-cycle LP bound pays (+32 proofs).
Full Biq Mac: 67 vs 49 proved; W/T/L 58/83/7; 0 bound mismatches
Sparse families (pre-declared 48): 44 vs 40 proved, 33/6/9
Gset 71/71 rigorous bounds verified VALID; median certified gap 10.05 %
Weighted MaxSAT on a GH200: From 14/33/50 to 33/38/26 Against NuWLS-c-IBR
GPU Local Search, a SAT-Based Improver and a Native Local Search Racing Together. 97 MaxSAT-Evaluation Instances at 60 s; Held-Out 59: 22/34/3.
33/38/26wins / ties / losses vs NuWLS-c-IBR, 97 instances
22/34/3on the 59 held-out instances
−36 → +7net wins minus losses, first build to 1.0.2
35/59/3SAT-based LNS vs the previous default
The road from a loss to a win None
Every lever vs its control (paired, same code) Three adopted; the others stay opt-in.LNS on the six worst losses Engine off, 60 s; NuWLS from the 1.0.2 run.
1.0.2 vs NuWLS-c-IBR: 33/38/26 on 97; held-out 59 22/34/3; 93 vs 93 feasible
SAT-based LNS vs the previous default: 35/59/3 (held-out 10/47/2)
Large-Instance TSP on 16 Arm Cores: 0.692 % → 0.165 % Mean Gap, Still Behind LKH-3
Sequential 5-Opt Basis Moves, Pi-Alpha Candidates and a Wider Kick Window, Each Confirmed on 8 Held-Out National Instances.
0.165 %mean gap, 8 held-out national TSPs (was 0.692 %)
2/0/6vs LKH-3 best config, held-out, 30 s
7/7dev instances improved by 5-opt + pi-alpha
0.020 %d18512 with the LKH-style search (LKH-3: 0.049 %)
Development path on the 7 dev instances, with LKH-3 None
Kick-window sweep (dev 7) NoneWhy LKH-3 leads: one LKH-3 descent, ablated Given our local optimum, LKH-3's chains take it from 1.02 % to 0.36 %: the gap is the chained 5-opt search.
Held-out 8: mean gap 0.692 → 0.224 → 0.165 %
vs LKH-3 still 2/0/6 held-out (wins on ho14473 and ch71009)
LKH-style variants beat LKH-3 on brd14051, d15112, d18512 (opt-in)
A Native QCDCL Solver vs DepQBF: From 0 vs 4 to a 15–15 Tie, Then 15 vs 18 on Fresh Instances
Dependency Learning, Solution-Flip Search and Universal Expansion, Measured on QBFEVAL'22 With Zero Disagreements.
15 vs 18solved, fresh 100 instances, ours vs DepQBF
0verdict disagreements in every run
26/36dev set after tuning (restart base 50, was 20)
3Organic-Synthesis instances only we solve
Every head-to-head run vs DepQBF (0 disagreements in all) None
Who solves what (three 100-instance sets) NoneTuning sweeps on the dev set (top 10 configurations) Restart base 50 lifts 20 → 26; DepQBF-inspired heuristics hurt.
100-instance set: 15 vs 15 (3 unique each)
Held-out: 12 vs 16; fresh 100: 15 vs 18: LOSS
Every DepQBF-only solve is a Hex game: the TRUE side needs short learned cubes
Vehicle Routing vs PyVRP: a C++ Iterated Local Search Wins 37/26/21 at Equal Budget
CVRPLIB X, Solomon and Gehring–Homberger, One Thread Each, Every Route Set Re-Checked by an Independent Checker.
37/26/21vs PyVRP, 84 instance-runs, equal budget
25/6/9on CVRPLIB X
25/66/21full Solomon set, paired
4.36 → 0.29 %X mean gap, GPU HGS → ILS
C++ ILS vs PyVRP on the 42 pre-declared instances None
First benchmark (GPU HGS) vs PyVRP, OR-Tools, cuOpt The GPU HGS lost to PyVRP everywhere; replaced by the C++ ILS.Certified LP lower bounds (sample of 10) Proof gap of the best-known value vs our answer's distance from the bound.
Subsets: 37/26/21 (X 25/6/9, Homberger 12/3/5)
Full Solomon 56, both at once: 25/66/21 narrow win
The 12-instance Solomon subset alone remains a loss (1/16/7)
UNISOLVE 0.16.1: One Solver Platform, 13 Problem Domains, Every Answer Checked
106 CUDA Gauntlet Cases Passed on One GH200; 8 Real Application Models Answered and Checked; One Airline Optimum Proved Exactly.
106/106CUDA gauntlet cases passed (one GH200)
14,207tests passed on Brev (13 skipped)
8/8real application models answered and checked
gap 0flugpl airline optimum 1,201,500 proved exactly
CUDA gauntlet: fitted size exponents per graph family Finite-range fits; launch latency and contention can change them.
Real application models: evidence per answer Seven optima remain unproved; tours use a local route.Release gates on Brev Full suite plus five targeted gates, run in sequence.
Ground-State Geometry of Large Random Sparse Max-Cut: σ=ln2 Universality, a Certified Degree Law to d=1024, a T=0 Droplet Link-Overlap Signature, and the Finite-T Spin-Glass Transition at the Bethe Value
We characterize the ground-state geometry of random sparse max-cut (Ising spin glasses on random-degree graphs) at scales to 1.65 × 10¹⁰ variables with a GPU parallel-tempering solver and independent certification. Four results: (1) σ = ln2 universality, independent ground states are mutually orthogonal (per-spin configurational entropy = ln 2, the maximum) across uniform, bimodal ±J, and gaussian couplings and degree d = 3 → 256, demonstrated at the extreme by the first ground-state overlap matrix ever measured at a billion spins (off-diagonal ⟨q⟩ = 7.5 × 10⁻⁵, folded Hamming 0.49996); (2) a certified degree law c(d) = ½ + a/√d − b/d with the leading constant a = 0.7646 ≈ the Sherrington–Kirkpatrick/Parisi mean-field constant 0.7632 at finite d (b = 0.136); the apparent ≈ln 2 (0.68) value at small d is the −b/d subleading term (α_eff(3) = 0.686 ≈ ln 2 is a coincidence): recount-verified (MATCH=True, relative error ≤ 3.6 × 10⁻⁶) to d = 256 across three generator seeds, cross-checked independently, and extended to d = 1024; (3) a link-overlap droplet signature at T = 0, link overlap pinned at its trivial factorized value with variance shrinking ∝ 1/N toward a delta; (4) a corrected finite-T result: a non-equilibrium cooling-quench decorrelates (⟨q²⟩ ∝ 1/N), but the equilibrated measurement (companion P12) finds the spin-glass transition at the analytically-known T_c = 2.08 for d = 6 ±J ((d−1)tanh²β_c = 1; Binder crossings 2.05/2.13 bracket it); the quench simply fails to equilibrate below T_c, and the T = 0 link-overlap droplet signature (§3.3) and this finite-T transition are different observables, not in tension. We report honest negatives, including the retraction of an earlier finite-T "RSB-like" result that was a within-chain autocorrelation artifact.
Classical GPU Parallel Tempering Outscales Quantum Annealing on D-Wave's Own Pegasus Time-to-Solution Benchmark
We test the central empirical claim behind quantum-annealing advantage: favorable time-to-solution (TTS) scaling on hard spin-glass instances, using a classical GPU parallel-tempering solver (SpinForge) run on D-Wave's own Pegasus topology and own TTS metric. Across 60,080 runs on a Pegasus-QAC instance ladder (graph sizes N = 210 → 3432), SpinForge exhibits a TTS scaling exponent of α = 0.087 (bootstrap 95% CI [0.035, 0.117]), versus the published D-Wave quantum-annealing- correction (QAC) exponent of 1.69 and the classical population-annealing PT-ICM baseline of 1.93 on the same family. A lower exponent is strictly better: it means time-to-solution grows far more slowly with problem size. On 3D Edwards–Anderson spin glasses, the same solver also beats tuned simulated annealing, Toshiba's Simulated Bifurcation Machine (SBM), and Gurobi. We frame the result honestly: the α figure is a point estimate with a wide confidence interval, a strong-but-bounded refutation, not a closed proof, and we detail every place a baseline was under- or over-favorable.
Certified Maximum-Cut at 16.5 Billion Variables: GPU Parallel Tempering, Independent-Recount Certification, and N-Invariant Solution Quality
We report the solution of maximum-cut (equivalently, ground-state search for an Ising spin glass) at 2.0 × 10¹¹ variables (200 billion), to our knowledge the largest max-cut instance ever solved, reaching a recount-verified near-optimal cut of 0.77419 (degree-6, GPU simulated annealing, ~11.4 h wall), with a graph-analysis proof bundle. At the smaller, fully certified-to-the-Parisi-band scale of 1.65 × 10¹⁰ variables, the largest instance (degree-3, cut 89.4392%) is independently re-counted on CPU (22,136,207,143 cut edges, relative difference 3.2 × 10⁻⁷, MATCH) with the problem and result cryptographically hashed, to our knowledge the largest combinatorial-optimization instance certified at converged optimal-band quality. (The 200 B run is recount-verified, the reported cut is independently recomputed and matches, but it is near-optimal, sitting below the d6 Parisi ceiling 0.796 and above the quench fixed point 0.734, not a converged-band certification.) We establish three systems results: (1) solution quality is N-invariant, the degree-6 family cuts 79.595% from 1 billion to 10.3 billion variables, every record independently recounted; (2) the optimal cooling factor 0.9435 is N-universal (peak at N = 10⁶, 10⁷, and 5×10⁷; a faster 0.950 cool collapses to 76.9% at every size); and (3) bit-packed spins give a 1.41× speedup at bit-identical cut, confirming a prediction that the kernel is memory-latency bound. We document an instructive bug: a quality "dip" at 5 billion variables that was a multi-GPU sharding artifact (a non-annealing temperature ladder), traced by code-diff and fixed. We do not claim 20 billion (it ran out of memory).
An Algorithmic Phase Transition Between Annealing and Quench in Large-Scale Parallel Tempering
We identify a sharp algorithmic phase transition in GPU parallel tempering on large random max-cut, controlled by the cooling schedule and sweep budget, with a binary order parameter: the final cut either reaches the equilibrated band (0.7960) or freezes at a quench fixed point (0.7694), with almost nothing in between. On a degree-6, N = 10⁹ instance, varying only the cooling factor gives 0.9435 → 79.5958%, 0.945 → 79.5721%, then a cliff at cool_c ≈ 0.947 dropping −2.63 points to a flat quench plateau (0.950 → 76.9377%, 0.952 → 76.9380%, 0.965 → 76.9382%: identical to four digits). The plateau value 0.7694 is a single physical object, the typical greedy / zero-temperature-descent fixed point, and it is the same number behind four previously-separate observations: hardware- invariance (every GPU froze into it), the cooling collapse, a retracted multi-GPU "attractor," and the CERT-009 8-billion-variable placement solve (76.9463%). The transition unifies the campaign's entire errata: every retraction (two-band, "sharded 6× faster," the 5B dip) was a run that quenched instead of annealed, and the data forces a finer picture, a ladder of partial-anneal attractors (the 5B dip froze at 79.4632%, the full quench at 76.94%) set by how early the schedule quenches. We define the annealing gap, 0.7960 − 0.7694 = 0.0266 points, as the measurable worth of equilibrate-to-band over greedy descent. Honest caveat: the much-cited "escape at ~100 sweeps" is the schedule's floor-reach time (k = ln 0.01 / ln cool), not an emergent constant, what survives is that an N-independent sweep budget suffices to reach the band.
Where Is the Hardness? An Empirical Account of Typical-Case vs. Worst-Case Combinatorial Optimization
We give a precise, falsifiable, empirical account of where in instance-space the hardness of NP-hard combinatorial optimization actually lives, backed by solver experiments to 1.65 × 10¹⁰ certified variables. The claim has three parts, each measured. (1) Random large sparse max-cut is maximally degenerate (σ = ln 2, confirmed N = 10⁹–10¹⁰ across uniform/bimodal/gaussian and degree 3 → 256), and an N-independent sweep budget suffices to reach its optimal band, random instances are not where worst-case hardness bites. (The σ=ln2 / orthogonal-random premise was stress-tested 2026-06-18: an apparent refutation showing a clustered near-optimal manifold was a global-Z2-flip gauge artifact; gauge-fixed against exhaustive ground truth the random near-optimal set decays toward orthogonal, so the "random sits outside the hard regime" premise holds: see P0 §3.6.) (2) Real structured problems (portfolio, NN-quantization, chip-placement, planted) are not σ = ln 2, the Structure Atlas scores all four as structured (basins < K, finite overlap): i.e. they carry exploitable structure and are also outside the adversarial hard regime. (3) Worst-case NP-hardness is therefore carried by a narrow, adversarially-constructed regime that neither random-typical nor real-structured instances occupy, and the Structure Atlas (companion P6) is an instrument that locates any instance relative to it. We state plainly what this is not: not P = NP, not a claim that worst-case instances are easy, not a claim that every real problem is trivial. The disciplined version is both correct and more useful than the aspirational one.
A Dynamical Second Law for Optimization on Sparse Ising: the Entropy–Energy Envelope
the formal object behind "Second Law": Φ = s_eq(e)−s_exp ≥ 0; fixed-T H-theorem dΦ/dt≤0 (proven, demonstrated Φ 0.735→0.001); deficit monotone in cooling rate (measured N≤22, ✓; = P7's 0.0266 gap at scale); Clausius form Y ≥ T·X; P10 is its time-reversed special case
A Statistical Mechanics of Search: State Variables, an Arrow of Time, a Carnot Bound, and the Geometry of Discoverability
We assemble a statistical mechanics for computational search on the σ=ln2 Ising/Max-Cut family and test how far it extends to other domains. The framework has a closed set of macroscopic state variables (the effective dimension of the search state is ~5), a free energy the dynamics minimizes, a proven + measured arrow of time (cooling↔heating hysteresis 2.5–4.1× a reversible control across four landscapes), a proven + measured Carnot-type efficiency bound (no search beats the quasi-static limit; the price of speed is the measured dissipation Φ(τ)), a closed equation of statec*(d,N,W) composed from four independently-measured fragments, a measured effective temperature (fluctuation–dissipation, validated to ~30%), and a measured phase diagram (fluid → critical T_c≈0.596 → glassy → frozen, with the explore→commit transition present in spin glasses and in diffusion/language/vision/RL training). From it we give a measurable answer to why finite computation finds structure in nominally-infinite spaces: in the typical case hardness is set by the geometry of the near-optimal manifold, not the size of the space, the manifold is extensively dense (σ=ln2) and reachable in constant work per degree of freedom. We report two clean negatives: there is no conserved Noether invariant of search, and search across domains is not one universality class (exponents split: spin γ=0.64, EDA γ=1.68; cross-modal curves do not collapse, 21×). Results summary figure: P12_search_mechanics_summary, (A) density of states s(e)→ln2 (why discovery is possible); (B) equation of state c(d)=½+α/√d; (C) arrow of time (hysteresis vs reversible control); (D) REFUTED single universality class (split exponents); (E) gauge-invariant overlap per domain; (F) the seven-law status board.
MATHGEN: Experimental Mathematics via Billion-Scale Ising / Spin-Glass Search
Most extremal combinatorial objects, low-correlation sequences, orthogonal ±1 matrices, extremal graph colorings, optimal rulers, are defined as the solution of an optimization or constraint-satisfaction problem, which is exactly what the SpinForge energy-minimization engine solves at billion-variable scale. MATHGEN turns that engine into an instrument for experimental mathematics: a GPU generator/searcher for mathematical objects, validated against established mathematics before any push to scale. We enforce a three-guarantee discipline (incremental-ΔE self-check = from-scratch recompute; validation against known results; only then scale) and report only what is verified. Verified headline results, all independently re-checked in this draft from the stored result objects: the LABS searcher hits the exhaustive optimum exactly for N = 11, 13, 15, 18 (recomputed energies E = 5, 6, 15, 25; merit factors F = 12.10, 14.083 = the Barker-13 value, 7.50, 6.48), with every incremental-ΔE self-check returning exactly 0.0; a constructive Hadamard generator (Sylvester + Paley I + Kronecker) produces 27/27 matrices validated H Hᵀ = nI exactly (max off-diagonal error 0.0), orders up to n = 8192, including the orders 24, 32, 44 at which naive local search stalled; the Ramsey searcher matches the Goodman monochromatic-triangle minimum for all 12 orders n = 5…16 (verified against OEIS A014557 and confirmed by independent exhaustive brute force for n = 5, 6, 7) and constructs a zero-monochromatic-K₄ coloring of K₁₇, reproducing the bound R(4,4) > 17; the Golomb searcher reproduces optimal rulers for orders 4–12 (nine orders, all rulers independently re-verified to have distinct pairwise differences at the published OGR length). We are explicit about scope: the search-based large-N LABS, OGR ≥ 13, and R(5,5) fronts are honest search results, not records, beating live world records requires the documented specialist algorithms, which we scope precisely. MATHGEN is a working experimental-mathematics engine that reproduces real mathematics across sequences, designs, graphs, and rulers, and is correct by construction in every searcher.
A Spin-Glass Theory of Innovation: Invention as Frustrated Combinatorial Search on a Rugged Value Landscape
We propose that invention has the mathematical structure of a spin glass: an invention is a subset of reusable building blocks, its value is a mixed-sign frustrated quadratic form over those blocks, and a breakthrough is an escape to a deeper basin of that disordered energy landscape. From this single mapping we derive seven falsifiable laws of innovation: glassiness, bursty (avalanche) breakthroughs, heavy-tailed impact, a recombination degree law, a thermodynamics of search, an emergence (drive × self-modification) condition, and constant-work reachability, each of which inherits a result already proven for the disordered-spin model by the SpinForge program (σ=ln2 near-optimal geometry, the Parisi degree law, the dynamical Second Law, the Emergence Equation). We demonstrate the laws in silico on a recombination landscape run on the SpinForge GPU engine and we test the theory empirically on real bibliometric data: 12,000 OpenAlex articles (4 fields, 2010–2016), with citation impact as the observable. The result is deliberately reported on a four-rung honesty ladder, formal-mapping / proven-for-model / in-silico-measured / empirically-tested, and we preserve the key honest negative: the original conjecture that the heavy tail of impact is the static extreme-value statistics of landscape basin depths is refuted, the static recombination landscape produces Gaussian design values (kurtosis ≈ 3.0). The refuted law forces a sharp refinement: the landscape decides which designs can win; the dynamics (cumulative advantage on that substrate) decides how unequal the winnings are. On real data the refined heavy-tail law is confirmed, impact is power-law in all four fields with exponent α = 2.48 (CS), 2.52 (mathematics), 2.97 (medicine), 2.97 (physics), and a recombination-breadth interior optimum is supported in 3 of 4 fields. We do not assert this as established social science. The contribution is the falsifiable structure: innovation has the form of a spin glass, that form makes specific quantitative predictions, and the predictions are testable today.
Ghost Collider: A Model-Independent Physics-Discovery Engine on Real CMS Open Data
The frontier in collider physics is increasingly one of inference rather than collision energy: petabytes of public open data already encode physics that has never been exhaustively re-analyzed. We present Ghost Collider, a GPU-ready, model-independent discovery engine that reanalyzes real CMS Open Data and binds every claim to a tamper-evident reproducibility certificate. On 100,000 real 2010 CMS di-muon events (record 545, DOI 10.7483/OPENDATA.CMS.CB8H.MFFA) the engine, with no resonance model supplied, blindly rediscovers three Standard-Model resonances: J/ψ at 3.093 GeV (0.13% from PDG, 135σ local), Υ(1S) at 9.445 GeV (0.16%, 42σ), and Z at 90.76 GeV (0.47%, 92σ). From the eight raw four-momentum components alone, no physics prior, a sparse symbolic regressor recovers the relativistic invariant-mass law with the Minkowski signature (+,−,−,−) at held-out R² = 1.000000. A model-independent anomaly stack (dense autoencoder + RealNVP normalizing flow) concentrates its flagged events in the rare high-mass Drell–Yan tail (flagged-median 32.8 GeV vs 12.4 GeV bulk) and is calibrated by labelled signal injection (0 injected → no false peak; 1000 injected → 28.7σ, yield recovered to ~1%). A selected dimuon trigger compiles to both a CUDA kernel and synthesizable Verilog RTL, and the RTL is verified bit-exact against the float selection through real iverilog simulation (0 mismatches). All four pillars are reproduced here from the repository's certificates and re-runs. We are explicit about scope: the resonances and the law are real-data results; no new physics is claimed in this dataset, the correct, honest null, and the injection is the only synthetic input, always labelled as a calibration.
SAT-Based Combinational Equivalence Checking for a Native EDA Flow: a From-Scratch CDCL Solver with AIG and Tseitin Encoding
A logic-synthesis or timing-restructuring transform is only safe if the transformed circuit computes the same Boolean function as the original. We present the combinational equivalence checker (CEC) used inside the SpinForge EDA flow: a from-scratch CDCL SAT solver, an And-Inverter-Graph (AIG) circuit representation with O(1) structural hashing, and a Tseitin CNF encoding that builds a miter between two circuits. The miter is satisfiable if and only if some input distinguishes the two circuits; proving the miter UNSAT is a sound, complete proof of equivalence. The implementation is pure CPU Rust, we are explicit that the CDCL search is not GPU-accelerated, in contrast to the placement, routing, static-timing-analysis, and placement-DRC stages of the surrounding flow, which run on CUDA. The checker is wired into the flow as a gate on depth-reducing restructuring: a candidate netlist is accepted only if it is both shallower and proven equivalent by the SAT checker, otherwise the baseline is kept, so no transform can introduce a logic regression. We also document a corrected XOR-construction bug (the gate was computing XNOR, which inverts the miter polarity and would have silently passed non-equivalent circuits / failed equivalent ones); the corrected construction is exercised by the test suite. The forge-formal crate passes 31/31 unit tests (14 SAT/CEC-specific, run on CPU in well under one second), including UNSAT proofs of the pigeonhole principle PHP(3,2), SAT model extraction, AND-commutativity, De Morgan's law, and associativity (balanced-vs-linear AND-tree) equivalence.
A Sharp Recovery Threshold for Planted Partitions in Sparse Max-Cut
The SpinForge geometry program (P0) and structure atlas (P6) characterize random sparse Max-Cut, whose near-optimal solutions are orthogonal (σ=ln2) and carry no recoverable structure. Here we ask the complementary question: when a graph contains a planted partition of signal strength f (a fraction f of edges placed to respect a hidden ground-truth assignment σ*, the remaining 1−f uniformly random), at what f does the optimizer recover σ*? We find a sharp recovery threshold that sharpens with system size. Solving for the maximum cut and measuring the gauge-fixed overlap with the planted assignment, the overlap stays at the no-signal null (|⟨s·σ*⟩|/N ≈ 0.01–0.14) for f ≤ 0.5 and jumps to near-perfect recovery (≈0.95–1.00) by f = 0.75; the structure-ratio of the solution against the max-entropy null rises from ≈1.0 to 8.1× at N=2000 and 15.8× at N=8000 across that step: i.e. the transition is N-sharpening, consistent with a sharp threshold f_c in the large-N limit. A finer GPU sweep (N up to 128,000) localizes f_c ≈ 0.49, essentially N-independent, while below f_c the overlap decays toward zero with N and above it the recovery curves collapse, the recovery boundary steepens into a step as N→∞. This is the structured counterpart to P0's random-glass result and a concrete recovery boundary the structure atlas (P6) can be calibrated against.
