{"id":"99db645d-672c-471c-94d7-67f27bbb7b76","arxiv_id":"2502.08839","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"QUBIKOS is the first benchmark set with provably optimal non-zero SWAP counts, showing current quantum layout synthesis tools are far from optimal.","lead":"This paper introduces QUBIKOS, a set of quantum circuits whose minimum required number of SWAP gates is provably known. Using it, the authors measure that leading quantum layout synthesis tools use 63 to 330 times more SWAP gates than optimal on their benchmark.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 1's proof is invalid as written: the asserted inequality |S1| > |S2| is reversed; the construction actually yields |S2| = |S1| + 1, so the non-isomorphism argument needs the opposite degree-count comparison.","rationale":"The reader correctly identified Lemma 1 as the weakest load-bearing premise, but the precise problem is stronger than 'unproved': the stated inequality is reversed. My analysis of the construction shows that the intended pigeonhole direction, |S2| > |S1|, in fact holds under the algorithm's design, so the lemma itself may be true despite the erroneous proof. Therefore the central claim is not refuted, but the proof as written is incomplete and needs correction. Additionally, Theorem 4's reliance on an undefined 'claim 2' and the informal treatment of redundant-gate insertion in Section III-D leave further gaps; however, these are fixable and do not decisively invalidate the benchmark methodology. Since the reader's verdict of CONDITIONAL already captures the need for proof repairs, my stress-test read does not change that verdict.","tokens_in":11808,"tokens_out":14758,"duration_ms":138782,"concrete_test":"Re-derive Lemma 1 from Algorithm 1: instantiate the construction on a coupling graph with a degree-2 node (e.g., a corner of a 2D grid) and compute S1 and S2 for the special-gate endpoint q. If |S2| = |S1| + 1 in that example, the paper's asserted |S1| > |S2| is false. Then run a graph-isomorphism check (e.g., NetworkX VF2) of the generated interaction graph against all subgraphs of GC for several architectures (grid, heavy-hex, star); if any embedding exists, Lemma 1 fails. This separates a fixable proof typo from a genuine construction failure.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 1 (Section III-D) asserts that the interaction graph from Algorithm 1 is not isomorphic to any subgraph of GC. Its proof states: 'We know ∃q ∈ {g[0], g[1]} such that |S1| > |S2|', with S1 = {p ∈ P : deg(p) ≥ deg(q)} and S2 = {q′ ∈ Q : deg(q′) ≥ deg(q)}. This inequality is backwards: if |S1| > |S2|, there are more high-degree physical nodes than high-degree program qubits, so a degree-preserving mapping is still possible; the pigeonhole obstruction requires |S2| > |S1|. Moreover, in the construction, let q be the special-gate endpoint mapped to physical node p of degree d. Then q has degree d+1 in the interaction graph (all current neighbors plus the special gate), while every program qubit mapped to a physical node of degree > d has all its incident edges included (Algorithm 1 lines 7-8). Hence |S2| = 1 + |{physical nodes with deg > d}| = |S1| + 1, so |S1| > |S2| never holds. The proof of Theorem 4 also refers to an undefined 'claim 2' when asserting C0 ⊆ C′_0. These gaps mean the central lower-bound proof is not valid as written, even if the underlying lemma may be repairable with the corrected inequality.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces QUBIKOS, a family of benchmark quantum circuits for which the optimal number of SWAP gates required by quantum layout synthesis (QLS) is claimed to be known by construction. The construction generates n circuit sections, each designed to require exactly one SWAP by building an interaction graph that is not isomorphic to any subgraph of the device coupling graph, and orders the sections serially via a gate dependency graph. A proof of optimality is given in Section III-D, and experiments with the exact tool OLSQ2 on small circuits confirm the claimed SWAP counts for the tested instances. The benchmarks are then used to evaluate LightSABRE, ML-QLS, QMAP, and t|ket> on four architectures; reported average optimality gaps range from 1x to several hundred times, with LightSABRE performing best among the tested tools. A case study attributes one LightSABRE failure to the equal weighting of lookahead costs.","tokens_in":12063,"tokens_out":7874,"duration_ms":78809,"significance":"If the optimality claim is correct, QUBIKOS fills a real gap: existing benchmarks either have zero SWAPs (QUEKO) or no provable optimum (QUEKNO). The benchmark is not fitted to tool outputs, so the reported optimality gaps are externally anchored rather than circular. The large gaps and the LightSABRE lookahead analysis are concrete and actionable findings, and the small-circuit verification with OLSQ2 is a useful sanity check. However, the benchmark's central value rests on the general proof that each constructed section forces exactly one SWAP, so the proof gaps described below are what currently prevent acceptance. The contribution would be valuable after a rigorous repair of Lemma 1 and Theorem 4.","major_comments":[{"comment":"The proof of Lemma 1 does not establish the stated non-isomorphism. With S1 and S2 as defined, the pigeonhole obstruction to a degree-preserving injection requires |S2| > |S1| (more program qubits of degree at least d than physical nodes of degree at least d); the inequality asserted in the proof, |S1| > |S2|, says the opposite and, if anything, makes a mapping easier to find. No argument is given for why |S1| > |S2| should hold for every graph produced by Algorithm 1; in the construction the special-gate endpoint q has degree one larger than its currently mapped physical node, which can yield |S2| = |S1| + 1 rather than |S1| > |S2|. Since Theorem 4 uses Lemma 1 to rule out SWAP-free execution of each section, the central lower-bound proof is incomplete as written. The authors should replace this proof with a correct degree-count or structural argument, or state the precise construction-dependent condition and prove it from Algorithm 1.","section":"Section III-D, Lemma 1"},{"comment":"The proof of the base case invokes an undefined 'claim 2' to conclude that every gate of C0 lies in C′0. No such claim is stated anywhere in the paper, and this step is exactly what forces the whole first section to be executed before the first SWAP; without it the contradiction from Lemma 1 does not follow. The induction step has a related gap: from Ci+1 ∪ {gsi+1} ⊆ C′i+1 it is not shown that the interaction graph of this subset is the same object to which Lemma 1 applies, because C′i+1 may contain additional gates and may not coincide with the section Ci+1. The proof should be rewritten with a precise notation for sections, SWAP boundaries, and the special-gate dependency argument.","section":"Section III-D, Theorem 4"},{"comment":"The final paragraph asserts that inserting 'redundant' gates into the backbone cannot increase the optimal SWAP count and that the non-isomorphism and dependency properties are preserved. The non-isomorphism part is correct, but the dependency part is only argued informally ('can only make the dependency chain either longer or remain the same'), and Algorithm 3 does not specify the conditions under which a gate may be inserted into Cans while keeping the n-SWAP solution valid. Since the benchmark circuits used in Section IV-B have hundreds to thousands of gates and are not verified exactly, this step is load-bearing for the claimed optimal counts of the actual test instances. Please provide either a formal insertion invariant or a precise insertion rule with proof.","section":"Section III-D, final paragraph"}],"minor_comments":[{"comment":"The caption lists '(b)' twice; the last panel should be labeled '(e)'.","section":"Figure 1"},{"comment":"The variable p′ is overwritten in line 2 before being used in line 3, and the selection conditions in lines 1-3 are not stated with enough precision to guarantee that such vertices exist for all coupling graphs used in the paper.","section":"Algorithm 1"},{"comment":"The running text, the figure captions, and Algorithm 1 use different qubit labels (for example, the text describes a special gate g(q1,q7) while the figure caption says the graph enforces SWAP(q0,q4)); aligning these names would greatly improve readability.","section":"Section III-A and Figure 2"},{"comment":"The symbol C0 is overloaded: it denotes both the first section of the backbone circuit and the first partial gate sequence in the transpiled circuit C′. Using different symbols for these objects would remove a source of confusion in the proof.","section":"Section III-D, Theorem 4"},{"comment":"There are small textual errors, e.g., 'experimment' and 'we uses'; also, the relationship between the average gap values quoted in the text and the per-architecture results in Figure 4 should be stated explicitly.","section":"Section IV-B"},{"comment":"For a benchmark paper, an explicit code and data availability statement, with a repository containing the circuit generator and the exact verification scripts, would substantially increase the usability and reproducibility of the results.","section":"General"}],"recommendation":"major_revision","confidential_remarks":"The main uncertainty is whether the proof gap in Lemma 1 is a simple typo or a genuine flaw in the construction. The small-circuit verification and the overall approach suggest the construction is likely repairable, so I would not recommend reject at this stage. If the authors can supply a corrected inequality and proof for Lemma 1, repair the undefined 'claim 2' in Theorem 4, and make the redundant-gate insertion argument rigorous, the paper could be suitable for publication. I would also ask the editor to request a code/data availability statement, since the benchmark's value depends on the community being able to generate and verify new instances."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"QUBIKOS is worth a serious referee. It is the first benchmark set with provably optimal non-zero SWAP counts, and the reported optimality gaps (LightSABRE 63x, ML-QLS 117x, etc.) are a genuinely useful signal that current QLS tools are far from optimal. The construction idea—concatenating serial sections, each forced to consume one SWAP by a non-isomorphic interaction graph—is sound, and the small-circuit verification via OLSQ2 (400 circuits per architecture, no deviations) is real evidence.\n\nWhere the paper is soft: Lemma 1's proof states the wrong inequality. It says |S1| > |S2|, but the pigeonhole obstruction needs |S2| > |S1|. In the construction, the special gate gives the chosen endpoint degree d+1, and all program qubits mapped to physical nodes of degree > d get full degree, so |S2| = |S1|+1. Thus the lemma is true with the inequality reversed; the text has a sign error. That is fixable, but it is a real gap in the written proof. Theorem 4 also refers to an undefined 'claim 2' when asserting C0 ⊆ C′_0, and the redundant-gate insertion argument is sketched rather than proved. These are all repairable, but as submitted the proof is not self-contained.\n\nTwo other issues: the abstract's headline gaps (63x, 117x, 250x, 330x) do not match the body numbers (LightSABRE 1.95x/12.17x/233.97x on three architectures, ML-QLS optimal on Aspen-4 and Rochester). There is an unlabeled aggregation somewhere, and it should be stated. And the benchmarks/code are not released, which undercuts reproducibility; a benchmark paper should ship artifacts.\n\nWho this is for: anyone working on quantum layout synthesis or benchmarking compilers. It is an incremental extension of the QUEKO line, but the zero-SWAP gap was a real limitation and this closes it. With the proof fixed and artifacts released, I would cite it. As is, it deserves peer review with a request for revision.","headline":"QUBIKOS is a genuinely useful first benchmark with provably optimal non-zero SWAP counts, but the proof as written has a sign error in Lemma 1 and an undefined reference in Theorem 4; both are repairable, and the paper deserves peer review.","tokens_in":12631,"tokens_out":3657,"would_cite":true,"duration_ms":29975,"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":"This paper introduces QUBIKOS, a benchmark family whose circuits require a provably minimal number of SWAP gates, and uses it to show that leading layout synthesis tools use 63 to 330 times more SWAPs than necessary.","keywords":["quantum layout synthesis","qubit mapping and routing","SWAP minimization","benchmark circuits","known-optimal cost","optimality gap","NISQ compilation"],"falsifier":"Run Algorithm 1 on a coupling graph where the degree-count inequality of Lemma 1 is not guaranteed (for example, a regular graph where all physical and program qubits have equal degree), generate the backbone circuit, and check with an exact QLS solver whether the optimal SWAP count is ever less than the number of sections; any such case would disprove the claimed optimality.","tokens_in":11525,"feed_emoji":"⚛️","tokens_out":7423,"duration_ms":60283,"temperature":0.7,"pith_summary":"This paper introduces QUBIKOS, a benchmark family of quantum circuits whose minimum required number of SWAP gates is provably known: exactly one per constructed section of the circuit. This is the first benchmark with known-optimal non-zero SWAP counts, so for the first time heuristic quantum layout synthesis (QLS) tools can be scored against an absolute optimum rather than against each other. Using QUBIKOS, the paper measures optimality gaps on four architectures and finds that even the best tool, LightSABRE, uses on average 63 times more SWAPs than optimal, with ML-QLS at 117x, QMAP at 250x, and t|ket> at 330x. The benchmark is also shown to help diagnose why a tool makes a suboptimal routing decision, via a case study of LightSABRE.","feed_headline":"Benchmark proves optimal SWAP counts: compilers miss by up to 330x","feed_subtitle":"For the first time, heuristic quantum compilers can be measured against a provable optimum; the gaps are 63x to 330x.","key_machinery":"The construction's engine is the non-isomorphic interaction graph: a set of two-qubit gates, generated by Algorithm 1, whose interaction graph cannot be embedded into the device coupling graph, so any layout must insert a SWAP. A distinguished 'special gate' is placed last in its section so that only that SWAP makes it executable, and the remaining gates are ordered by breadth-first search so that every gate in a later section depends on the previous special gate and precedes the next one. This serial dependence chain is what makes the per-section SWAP requirements add up, turning the section count into a provable lower bound that the explicit solution attains.","core_discovery":"The paper's central claim is that QUBIKOS circuits have a provable optimal SWAP count equal to the number of sections n. Each section is built so that its interaction graph is not isomorphic to any subgraph of the device's coupling graph, forcing at least one SWAP, and a special gate scheduled after all other gates in the section makes that SWAP unavoidable under any mapping. Gate dependencies (enforced by breadth-first searches) serialize the sections, so the SWAP requirements add; the construction explicitly provides a transpiled circuit with n SWAPs, proving optimality. The paper verifies the claim on small circuits with an exact solver and then applies the benchmark to measure optimality gaps of four leading heuristic QLS tools.","pith_inferences":["If the gap magnitudes hold beyond the tested circuit sizes, heuristic QLS may still be far from practical optimality on large devices, making exact or hybrid methods worth revisiting for moderate qubit counts.","The section-and-special-gate construction is a general template: it could be extended to produce benchmarks with simultaneously known-optimal SWAP count and depth, or to target other routing objectives such as gate-error-weighted cost.","A direct testable extension is to generate QUBIKOS circuits on regular or highly symmetric coupling graphs where Lemma 1's degree-count inequality is strained, to check whether the proof's unstated condition ever fails.","The lookahead-decay fix suggested by the case study could be implemented in LightSABRE; if it reduces the QUBIKOS gap, that would validate the cost-function diagnosis."],"forward_implications":["QLS tools can now be compared against an absolute optimum; the measured average gaps are 63x (LightSABRE), 117x (ML-QLS), 250x (QMAP), and 330x (t|ket>) on the tested architectures.","Optimality gaps grow with device size and with sparse connectivity: on the 127-qubit Eagle the best tool reaches a 233.97x gap, while on the 16-qubit Aspen-4 ML-QLS finds optimal solutions in all cases.","Sparse, heavy-hex topologies such as Rochester are harder for current tools than dense grid topologies such as Sycamore, even at similar qubit counts.","QUBIKOS can evaluate standalone routers by supplying the optimal initial mapping, so that non-optimal results are attributable to the router itself.","A case study of LightSABRE traces one suboptimal choice to the lookahead cost and suggests adding a decay factor to the lookahead term could improve routing."],"supporting_citations":[{"why":"Establishes that QLS is NP-hard, motivating the need for benchmarks that can measure heuristic suboptimality.","marker":"[1]"},{"why":"OLSQ2 exact QLS solver used to independently verify the claimed optimal SWAP counts of QUBIKOS circuits.","marker":"[10]"},{"why":"ML-QLS, one of the four heuristic QLS tools whose optimality gap is measured.","marker":"[27]"},{"why":"Introduces SWAP-free benchmarks with known-optimal depth, the baseline QUBIKOS extends by adding known-optimal non-zero SWAP counts.","marker":"[28]"},{"why":"Proposes circuits requiring SWAPs but without known optimal counts, the limitation QUBIKOS addresses.","marker":"[29]"},{"why":"LightSABRE, the best-performing tool tested, with its gap measured and its suboptimal case analyzed.","marker":"[31]"},{"why":"t|ket>, one of the tools whose gap is measured.","marker":"[32]"},{"why":"QMAP, one of the tools whose gap is measured.","marker":"[33]"}],"fun_headline_variants":["First optimal-SWAP benchmarks reveal 330x compiler gap","QUBIKOS: provable SWAP optima expose 63x-330x compiler gaps","Quantum layout tools found 330x off from optimal SWAP counts","Benchmark proves SWAP optimality: tools lag by 63x to 330x","Heuristic quantum compilers miss optimal SWAPs by up to 330x"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is Lemma 1, which asserts that for every interaction graph the construction generates, some endpoint of the special gate has more physical qubits of degree at least its degree than program qubits, so the graph cannot fit into the coupling graph; this inequality is stated without proof, and if it fails on some topology the claimed optimal SWAP count could be wrong.","fun_headline_variants_meta":{"raw":{"variants":["First optimal-SWAP benchmarks reveal 330x compiler gap","QUBIKOS: provable SWAP optima expose 63x-330x compiler gaps","Quantum layout tools found 330x off from optimal SWAP counts","Benchmark proves SWAP optimality: tools lag by 63x to 330x","Heuristic quantum compilers miss optimal SWAPs by up to 330x"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000286,"raw_usage":{"total_tokens":1686,"prompt_tokens":953,"completion_tokens":733,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":569,"completion_tokens_details":{"reasoning_tokens":628}},"tokens_in":569,"tokens_out":733,"duration_ms":6545,"temperature":1.0,"reasoning_tokens":628,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T23:31:11.773848+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Algorithm 1 on a coupling graph where the degree-count inequality of Lemma 1 is not guaranteed (for example, a regular graph where all physical and program qubits have equal degree), generate the backbone circuit, and check with an exact QLS solver whether the optimal SWAP count is ever less than the number of sections; any such case would disprove the claimed optimality.","supporting_citations":[{"cited_title":"Benchmarking Quantum Circuit Transformation with QKNOB Circuits","cited_arxiv_id":"2301.08932","evidence_quote":"Proposes circuits requiring SWAPs but without known optimal counts, the limitation QUBIKOS addresses."}],"review_version":1}