{"id":"8d88d88f-727e-4dce-ab0c-9745600c189d","arxiv_id":"2608.08118","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"A frozen LLM agent paired with SageMath discovered verified algebraic constructions for all 100 benchmark two-orbit graphs and for a new 16-vertex counterexample to the Bernhart-Kainen dispersability conjecture.","lead":"An AI agent that can talk to a math software package was able to read a bare description of 100 symmetric graphs and, one by one, find short algebraic formulas that build each graph exactly. The same method found a 16-vertex graph that contradicts a 46-year-old conjecture about book embeddings, the smallest such counterexample known.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 100/100 core result depends on a fallback audit that the paper does not describe: only the exact Graph(g6(G)) pattern is rejected, so disguised embeddings of the target's raw data would pass the isomorphism check and inflate the algebraic-construction count.","rationale":"The reader's weakest assumption targets Sage's is_isomorphic as a trust base; a bug there would indeed collapse the claim, but is_isomorphic on at most 25 vertices is heavily exercised code where a failure is unlikely, and both nauty/Traces and Sage have extensive empirical validation. The hidden-fallback issue is more immediate because it concerns the semantics of the claim itself: 'algebraic construction' must exclude raw data in any form, not just one exact syntax. Section 2 defines the fallback narrowly as Graph(g6(G)), and Section 3 says it is recognized by syntax; no audit of other raw-data embeddings is described in the manuscript. This is a concrete and checkable gap, not a disagreement with community consensus. The released transcripts make the proposed test cheap and decisive. If the audit finds no raw-data literals, the 100/100 claim is genuinely supported, and the remaining reader conditions (dispersability verification and benchmark timeline) are then the only blockers. If the audit finds hidden raw-data use, the headline success count and the 'no fallback' statement would need to be revised. I therefore keep the reader's conditional verdict rather than strengthening or weakening it, while noting that the specific condition I would attach is a transcript-level fallback audit rather than a question about Sage's isomorphism implementation.","tokens_in":9695,"tokens_out":6107,"duration_ms":60762,"concrete_test":"Write a script that parses all 100 released accepted constructions and flags any occurrence of (i) the target graph6 string or a faithful substring, (ii) the target adjacency matrix or edge list as a literal, or (iii) Graph(g6(G)) nested inside further graph operations. For each flagged construction, check whether deleting the raw-data component changes the isomorphism result. If none of the 100 constructions embeds raw data, the core claim stands; if any do, recompute the 100/100 success count and the 'no fallback' statement using only constructions free of raw-data literals.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Section 4.2) is that the agent returned a verified non-fallback algebraic construction for all 100 benchmark graphs. The verification pipeline checks only isomorphism via Sage's is_isomorphic and rejects the fallback Graph(g6(G)) by syntax (Sections 2-3). But the open language L also accepts expressions that carry the same raw data in a different syntactic form: e.g., Graph('...') with the target graph6 string, Graph(matrix(...)) from the target's adjacency matrix, an edge-list constructor, or operations applied to a Graph(g6(G)) object. All of these are certified by Sage as isomorphic to the target, yet they do not reveal algebraic structure in the intended sense. The paper reports no scan of the 100 accepted transcripts for the target graph6 string, adjacency data, or derived constants, and only one full construction is shown in the text. Since the transcripts are released, the 100/100 claim is checkable, but as written it is not fully supported: 'not using the fallback' is established only for one exact syntactic pattern.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a neurosymbolic pipeline in which a frozen general-purpose LLM, acting through a Model Context Protocol (MCP) server, proposes SageMath constructions for a target graph given only its graph6 string, and SageMath's exact isomorphism test certifies each accepted construction. The main experiment reports that the agent found verified non-fallback algebraic constructions for all 100 highly symmetric two-orbit graphs on up to 25 vertices, while a strong template-enumeration baseline covers only 21 and catalog lookup none. Additional experiments examine LLM backbone dependence, the degradation of construction quality on less symmetric random regular graphs, and recall on graphs with planted constructions. The paper concludes with a case study giving an algebraic construction for a claimed 16-vertex counterexample to the Bernhart–Kainen dispersability conjecture, smaller than the previously known 20-vertex Folkman graph.","tokens_in":9912,"tokens_out":4017,"duration_ms":40706,"significance":"If the central claim holds, this is a valuable demonstration that a general-purpose frozen LLM, paired with an exact symbolic verifier, can turn raw enumeration data into short algebraic descriptions for a nontrivial class of graphs. The paper is unusually transparent: it releases the MCP server, the agent harness, the system prompts, run transcripts, and per-experiment data, and it reports detailed cost and token statistics. The baselines (template enumeration and database lookup) provide a meaningful comparison, and the symmetry-tracking and planted-recall experiments help calibrate when the method succeeds. The Bernhart–Kainen application, if verified, is a concrete and significant byproduct. The main technical risk is whether the 'no fallback' claim truly excludes raw-data encodings beyond the one exact syntactic pattern that is audited.","major_comments":[{"comment":"The paper states that 'the Graph(g6(G)) fallback is recognized by its syntax' and then reports in Section 4.2 that the agent used no fallback on the 100-graph benchmark. However, the construction language L also admits expressions such as Graph('...') containing the target graph6 string, Graph(matrix(...)) built from the target adjacency matrix, an edge-list constructor, or operations applied to a Graph(g6(G)) object; all of these would pass the sole is_isomorphic check. Since the input feature record includes the graph6 string, a raw-data construction in these disguised forms would be certified as a valid construction without exposing algebraic structure. The released transcripts make this checkable, but as written the 'not using the fallback' claim is established for only one exact syntactic pattern. Please report a systematic scan of the 100 accepted transcripts for the target graph6 string, adjacency-matrix entries, or edge lists, and either restrict L or broaden the fallback detector accordingly.","section":"Section 3, fallback recognition"},{"comment":"The paper claims that a 16-vertex graph is the smallest known counterexample to the Bernhart–Kainen dispersability conjecture, but it does not show the dispersability computation. The algebraic construction C10 ⊕ 2K3 is verified only up to isomorphism; it does not by itself establish that every book embedding interleaves two edges of some color. The sentence 'Dispersability can therefore be checked by inspecting the construction rather than by exhaustive search over vertex orderings and page assignments' is an assertion, not a certificate. Please provide the exhaustive verification (e.g., the search code and its output) or a rigorous argument from the construction that proves non-dispersability.","section":"Section 4.4, Bernhart–Kainen counterexample"}],"minor_comments":[{"comment":"The text says the benchmark was 'fixed in advance,' but also that the n=24 order was added after the original 90-graph benchmark once its enumeration became feasible; please clarify the timeline so a reader can see exactly which targets were fixed before any agent runs.","section":"Section 4.1, benchmark fixity"},{"comment":"The informal notation O1 ⊕ O2 for orbit-pair constructions is used repeatedly in the four family descriptions; a short formal definition or a representative Sage expression for one member of each family would make the taxonomy easier to verify.","section":"Section 4.2, family descriptions"},{"comment":"The phrase 'The judge is systematically 0.32 grades stricter' could be more precise, since strictness may vary by grade; the mean absolute error of 0.48 and the 24/25 agreement within one grade are the more informative statistics and could be reported together with the direction of the bias.","section":"Section 4.2.1, LLM judge calibration"},{"comment":"The sentence 'The three fallbacks appeared in the two bins of lowest symmetry' is slightly ambiguous because the paper earlier says fallback was used for three graphs total; please state explicitly whether the three fallbacks are distinct graphs and which bins they belong to.","section":"Section 4.3.2, symmetry-tracking statement"}],"recommendation":"major_revision","confidential_remarks":"The main results are reproducible in principle because transcripts and data are released. The two major comments are both local and fixable with additional reporting or a small additional experiment: scanning transcripts for raw-data patterns, and providing a dispersability certificate. Neither issue appears to invalidate the core method, so major revision rather than rejection seems appropriate. The paper fits the conference's neurosymbolic scope well."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing to know: this is a solid, useful paper, but the headline claims need one round of verification before I'd trust them without checking transcripts myself.\n\nWhat's genuinely new: pairing a frozen, off-the-shelf LLM with an exact CAS verifier through an MCP server, applied to turning raw graph6 strings into algebraic constructions. The MCP-Sage bridge is a real reusable artifact. On 100 two-orbit graphs, the agent reports finding verified constructions for all, with a mean canonicity grade of 4.4, while template enumeration gets ~20% and catalog lookup 0%. The 16-vertex counterexample to the Bernhart-Kainen conjecture, beating the 20-vertex Folkman graph, is a nice concrete win. They release transcripts and data, which is exactly what you want.\n\nThe soft spots are about verification, not the method. First, the fallback is defined syntactically as Graph(g6(G)) and the acceptance check only rejects that exact pattern. An agent could smuggle the raw data in as a matrix or edge-list expression, pass the isomorphism test, and be counted as a non-fallback construction. The paper never reports scanning the 100 transcripts for raw-data encodings. The transcripts are public, so this is checkable, but as written the 100/100 claim is not fully supported. Second, the dispersability counterexample is asserted but not verified: the paper just says 'we checked all two-orbit graphs' and claims dispersability can be checked by inspecting the construction, but gives no code, no exhaustive-search description, no reference. That's a load-bearing gap for the application claim. Third, the benchmark wasn't entirely fixed in advance — n=24 was added later. The paper discloses this, but the abstract's 'fixed in advance' is a bit strong. Minor.\n\nNone of this sinks the paper. The core design — model proposes, exact symbolic verifier decides — is sound, and the authors are honest about quality being subjective. This is for people working on LLM-based discovery and computational graph theory; a reading group would get a good discussion out of it. The work deserves peer review; a referee should ask for the transcript audit and the dispersability check. I'd be comfortable citing the MCP server and the benchmark after those are in.\n\nRecommendation: engage it, but conditionally.","headline":"Solid neurosymbolic pipeline with exact verification, but the 100/100 claim needs a transcript audit and the dispersability counterexample needs its check shown.","tokens_in":10419,"tokens_out":8100,"would_cite":true,"duration_ms":69020,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A frozen language model, with an exact computer algebra verifier, recovered algebraic constructions for all 100 symmetric test graphs.","keywords":["algebraic graph constructions","neurosymbolic agent","large language model","isomorphism testing","SageMath","two-orbit graphs","Bernhart–Kainen dispersability conjecture"],"falsifier":"Re-run the hundred benchmark graphs through an independent exact isomorphism checker, for instance a second computer algebra system or a standalone canonical-labeling tool, and compare its verdicts with the paper's accepted constructions; any mismatch breaks the certification chain. Separately, exhaustively test the claimed 16-vertex graph for a dispersable book embedding and enumerate all two-orbit graphs on 15 vertices to confirm that no smaller counterexample exists.","tokens_in":9502,"feed_emoji":"🧩","tokens_out":8675,"duration_ms":72811,"temperature":0.7,"pith_summary":"The paper asks whether raw graph data alone — a graph6 string or adjacency matrix — can be turned into a short algebraic description such as a Cayley graph or a lexicographic product. It proposes an agentic loop in which a frozen, general-purpose language model proposes constructions and tests them in SageMath, with a single exact isomorphism test deciding acceptance. On a benchmark of 100 highly symmetric two-orbit regular non-joins on up to 25 vertices, the agent produced verified non-fallback constructions for all 100, while a strong template-enumeration baseline reached only about 20% and catalog lookup identified none. The authors further report that the same approach found an explicit algebraic construction of the smallest known counterexample to the Bernhart–Kainen dispersability conjecture, a 16-vertex two-orbit graph that improves on the 20-vertex Folkman graph.","feed_headline":"Agent recovers algebraic form for all 100 symmetric test graphs","feed_subtitle":"A frozen LLM, with a computer algebra system as exact judge, beat a 20% template baseline.","key_machinery":"The mechanism is the ReAct-style agent loop: the LLM interleaves reasoning with calls to SageMath through an MCP server, proposing candidate Sage expressions and revising them after exact feedback. The load-bearing piece is SageMath's is_isomorphic test, which the paper treats as an unconditional trust base; because every accepted construction is certified by this single exact test, erroneous proposals are rejected rather than trusted. The testbed is a catalog of two-orbit graphs, whose symmetry roughly tracks the existence of algebraic structure.","core_discovery":"The paper's central claim is that a neurosymbolic pairing — an untrained general-purpose LLM proposing over an open construction language, and a computer algebra system deciding correctness by exact isomorphism testing — can discover algebraic graph constructions that no fixed grammar or catalog finds. On the paper's evidence, all one hundred benchmark graphs were solved without the raw-encoding fallback, and the returned constructions cluster into identifiable families such as orbit partitions with parity cross-edge rules and wreath-product constructions. The same pipeline gave the 16-vertex counterexample an explicit construction as $C_{10} \\oplus 2K_3$, exposing the parity coupling between a 10-cycle and two independent triples so that dispersability can be checked by inspecting the construction rather than by exhaustive search.","pith_inferences":["The 100/100 success rate is a property of the deliberately favorable regime — the most symmetric two-orbit regular non-joins — and should not be read as evidence that the approach generalizes to arbitrary graphs; the paper's own low-symmetry results (grades down to 2.3, with three fallbacks) bound that reading.","Because the entire certificate chain rests on one isomorphism test, swapping in an independent exact verifier would test the robustness of both the benchmark results and the counterexample's construction.","The construction families the agent rediscovered — parity cross-edge rules, wreath products, weighted blow-ups — could be compiled into a grammar that lifts the template-enumeration baseline, suggesting a hybrid between the agent and systematic search."],"forward_implications":["Verified algebraic constructions can replace raw graph6 data as the output of graph search, exposing automorphism groups, degrees, and structural invariants.","The released MCP server is a general-purpose bridge, so the same agentic construction-discovery pattern can be applied to any discrete object SageMath can express.","The 16-vertex graph displaces the Folkman graph as the smallest known Bernhart–Kainen counterexample, and its explicit construction makes the dispersability check a matter of inspection.","The monotone decline in construction quality with decreasing symmetry indicates that falling back to raw data is a structural signal, not a search failure."],"supporting_citations":[{"why":"Supplies the partition-refinement canonical labeling technique that SageMath's isomorphism test is based on, making it the trust base for accepting or rejecting constructions.","marker":"[McKay and Piperno, 2014]"},{"why":"Catalog of over seven million two-orbit graphs, from which the 100-graph benchmark and the 16-vertex counterexample are drawn.","marker":"[Seka and Szeider, 2026]"},{"why":"Formulates the dispersability conjecture whose smallest known counterexample the paper constructs.","marker":"[Bernhart and Kainen, 1979]"},{"why":"Reports the previously smallest known counterexample, the 20-vertex Folkman graph that the new 16-vertex graph improves upon.","marker":"[Alam et al., 2021]"},{"why":"Defines the ReAct pattern of interleaved reasoning and action that the agent follows.","marker":"[Yao et al., 2023]"},{"why":"Provides the House of Graphs database used in the literature-lookup baseline, which could not identify any benchmark graph.","marker":"[Brinkmann et al., 2013]"}],"fun_headline_variants":["Neurosymbolic agent finds algebraic form for every graph in 100-graph benchmark","LLM + SageMath discovers algebraic constructions for 100 symmetric graphs","Explicit construction found for 16-vertex dispersability counterexample","Untrained LLM + exact CAS judge: 100% on graph construction benchmark","SageMath-backed LLM finds algebraic forms for all 100 two-orbit graphs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that SageMath's is_isomorphic is an unconditional, error-free trust base on every instance; if that test ever misclassifies an isomorphism, or the agent's expression is evaluated against the wrong target, the claimed 100/100 result and the counterexample's certification lose their guarantee.","fun_headline_variants_meta":{"raw":{"variants":["Neurosymbolic agent finds algebraic form for every graph in 100-graph benchmark","LLM + SageMath discovers algebraic constructions for 100 symmetric graphs","Explicit construction found for 16-vertex dispersability counterexample","Untrained LLM + exact CAS judge: 100% on graph construction benchmark","SageMath-backed LLM finds algebraic forms for all 100 two-orbit graphs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001463,"raw_usage":{"total_tokens":5934,"prompt_tokens":1043,"completion_tokens":4891,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":659,"completion_tokens_details":{"reasoning_tokens":4789}},"tokens_in":659,"tokens_out":4891,"duration_ms":34046,"temperature":1.0,"reasoning_tokens":4789,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T00:23:17.858539+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Re-run the hundred benchmark graphs through an independent exact isomorphism checker, for instance a second computer algebra system or a standalone canonical-labeling tool, and compare its verdicts with the paper's accepted constructions; any mismatch breaks the certification chain. Separately, exhaustively test the claimed 16-vertex graph for a dispersable book embedding and enumerate all two-orbit graphs on 15 vertices to confirm that no smaller counterexample exists.","supporting_citations":[{"cited_title":"Enumerating two-orbit graphs","cited_arxiv_id":null,"evidence_quote":"Catalog of over seven million two-orbit graphs, from which the 100-graph benchmark and the 16-vertex counterexample are drawn."},{"cited_title":"Bekos, Vida Dujmovic, Martin Gronemann, Michael Kaufmann, and Sergey Pupyrev","cited_arxiv_id":null,"evidence_quote":"Reports the previously smallest known counterexample, the 20-vertex Folkman graph that the new 16-vertex graph improves upon."}],"review_version":1}