LLM
Interpret and propose
Recover formulation semantics, connect matrix patterns to algorithms, propose reductions and invariants, design falsification tests, and coordinate certificate construction.
Benchmark conclusion
What the benchmark establishes
The LLM did not independently certify feasibility, compute valid global dual bounds, or validate its own reductions. MILP solvers, SAT engines, exact dynamic programs, exhaustive searches, rational arithmetic, and deterministic original-model audits performed the computational search and verification tasks.
This is an empirical finding, not an impossibility theorem. The observed workflow did not replace solvers; the result does not establish that future systems cannot replace a particular computational component.
What “solve” meant
Roles in the computational workflow
Backend
Search and bound
Find feasible points, optimize reduced models, enumerate finite state spaces, refute cutoffs, and compute numerical lower bounds or exact lower-bound certificates.
Checker
Accept or reject
Replay proof traces, verify rational certificates, audit every original row, test mapping directions, and prevent claims from exceeding their verified scope.
Acceptance rule: no benchmark result is accepted solely from an LLM output. A hypothesis is reported as a result only after computational testing and independent validation appropriate to the claim.
20-instance comparison
Primal and dual bounds favor different workflows
Choose a metric. “Skill-guided” means use of one structure-research workflow; it does not mean LLM-only.
The structure-guided arm produced the better primal bound on 11 of 20 instances, four strict primal-bound improvements over its frozen public baseline, and certified global optimality for two instances. The comparison arm produced the stronger dual bound on 12 of 20 and the smaller relative gap on 11. Improving primal bounds does not replace global dual bounding; strong branch-and-bound performance does not by itself yield a portable optimality certificate.
Six skill-arm primal bounds were tolerance-indexed. The two comparison-study certified global optima—ns1456591 and neos-3682128-sandon—are included once in the complete 217-instance catalogue; this 20-instance experiment remains a separate comparison.
Benchmark-wide validation results
52 resolved instances across the complete study
The 217-instance study reports 49 optimal, 2 infeasible and 1 unbounded result, together with 59 primal-bound and 136 dual-bound improvements. Exact certificates, numerical solver results, tolerance-accepted closures and source-model qualifications are documented individually.
Inspect all results and verification summaries →Paired benchmark results
Instance-level bound comparison
Swipe sideways to see every column.
| Instance | Batch | Better primal bound | Better dual bound | Smaller relative gap | Skill bounds | Comparison bounds | Skill method |
|---|
Requirements for a controlled benchmark
Design of a controlled solver-replacement study
A causal test should freeze identical MPS hashes, machines, solver versions, threads, seeds, starts, external information, tolerances, and wall-clock budgets. It should also reserve separate budgets for structural analysis, primal construction, dual search, proof production, and independent verification—then score unsupported claims and verification failures, not only final objective values.
Practical recommendation
Use the LLM to enlarge the hypothesis space and compress human research overhead. Use the best available computational backend for search and proof. Keep acceptance outside both.
Read the underlying study
The full skill package, comparison dataset, CSV, audit JSON, and methods report are available on the comparison page.
Open skill comparison