{"id":"90843c40-2f9f-4b31-bf03-6642ca28001b","arxiv_id":"2508.00514","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"Q-Sylvan parallelizes edge-valued decision diagrams for quantum circuit simulation and equivalence checking, reaching up to 18x speedup on 64 cores on certain circuit classes.","lead":"Quantum circuit simulation and verification are slow, and this paper presents Q-Sylvan, a decision diagram package that parallelizes across CPU cores to reach up to 18x speedup on 64 cores on selected circuit classes. It also passes single-core comparisons against a leading simulator on large benchmarks, making it a practical tool for debugging and validating quantum software.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Approximate floating-point node merging is not correctness-preserving for equivalence checking; the 'x' entries in Tables 3/5 show Q-Sylvan can output wrong answers, so the central claim needs a correctness caveat.","rationale":"The paper has genuine strengths: open-source code, reproducible benchmarks, comparison against several tools, and an honest report of limitations such as the inability to directly compare against prior parallel EVDD implementations. The x18 speedup claim is carefully scoped to 'some sharing' instances at high percentiles, and the single-core comparison is reported with fractions rather than universals. The single most load-bearing concern is correctness under approximate equality. The central claim is not just about speed; it is about an efficient implementation of EVDDs for simulation and equivalence checking. If equivalence checking can silently return wrong answers, the verification use case is unsafe even if the speedups are real. The 'x' entries in Tables 3 and 5 are internal evidence of failure, not external speculation. The paper does not discuss them or offer an explanation, which weakens the claim that the tool is ready for reliable verification. The δ-tolerance and norm-max normalization are hand-set parameters with no error analysis; non-transitivity of δ-closeness and the interaction with canonicalization could easily produce false equivalences. My recommended verdict remains CONDITIONAL: the engineering contribution is plausible and reproducible, but the paper should either fix the incorrect results, disclose them prominently, and add equivalence-checking validation, or restrict the correctness claims accordingly. This matches the reader's identified weakest assumption, so I see no basis to change the reader's verdict.","tokens_in":16498,"tokens_out":3539,"duration_ms":40055,"concrete_test":"Reproduce the VQE 5 and Grover/Q-walk 5-qubit equivalence benchmarks from Tables 3/5 with Q-Sylvan using δ=0 and δ=10^-12/10^-16, and with norm-L2 in place of norm-max, comparing all outputs to MQT QCEC's reference answers. If any 'x' flips to correct at δ=0 or norm-L2, the approximate merging/normalization is the responsible defect; if they remain wrong, the bug is in the equivalence algorithm itself.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing assumption is that δ-close floating-point edge values (δ=10^-14, Algorithm 3) and norm-max normalization preserve the answers of DD operations, including equivalence checking. This is not established: validation in §5.1 only checks l2-norm ≈ 1 and matches DDSIM on state vectors up to 20 qubits; equivalence checking is not validated against ground truth. Tables 3 and 5 contain explicit 'x' (incorrect) results: Q-Sylvan Pauli on Grover (no ancilla) 5, Grover (v-chain) 5, Q-walk (v-chain) 5, and VQE 5; Q-Sylvan alternating on VQE 5. Because δ-equivalence is non-transitive and normalization folds approximation into edge values, distinct circuits can be judged equivalent or a true equivalence missed. These x entries are direct counterexamples to the claim that the tool implements equivalence checking correctly. Although the x18 parallel speedup and DDSIM comparison may survive, a verification tool that silently returns incorrect answers cannot support the unqualified central claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Q-Sylvan, a parallel edge-valued decision diagram (EVDD) package built on top of the Sylvan decision diagram library. The main technical contributions are an EVDD implementation with fine-grained task parallelism via work stealing and lock-free hash tables, including approximate floating-point edge-value merging and four normalization strategies, plus two use cases: quantum circuit simulation and equivalence checking. The empirical evaluation compares Q-Sylvan against MQT DDSIM, Quokka-Sharp, and MQT QCEC on MQT Bench and KetGPT circuits, reporting single-core performance competitive with DDSIM on large instances and parallel speedups up to 7.2x on 8 cores and 18x on 64 cores for a selected 'some sharing' category. The paper also reports equivalence-checking speedups up to 5.8x on 8 cores, but with lower completion rates than QCEC and with several 'x' entries indicating incorrect results.","tokens_in":16713,"tokens_out":4231,"duration_ms":44158,"significance":"If the parallelization approach is sound, the paper addresses a known obstacle: prior EVDD implementations for quantum workloads achieved only limited parallel speedups. The open-source release, reproducible benchmark scripts, and detailed per-instance tables are clear strengths, as is the systematic comparison against state-of-the-art tools. However, the correctness of the approximate floating-point merging is not established for equivalence checking, and the reported incorrect results in Tables 3 and 5 directly affect one of the two headline use cases. The simulation speedup claims are plausible, but the unqualified presentation of the 18x speedup and the 'competitive' single-core claim needs qualification. Overall the paper is a useful systems contribution, but the verification use case requires either a fix, an explicit limitation discussion, or a narrower claim.","major_comments":[{"comment":"The equivalence-checking results contain explicit 'x' entries indicating incorrect results: Q-Sylvan Pauli fails on Grover (no ancilla) 5, Grover (v-chain) 5, and Q-walk (v-chain) 5, and both Q-Sylvan alternating and Pauli fail on VQE 5, among others. The text reports the completion percentages and speedups but never discusses these incorrect answers. Since equivalence checking is one of the two main use cases advertised in the abstract and introduction, the paper must either fix the underlying bug, explain the conditions under which such failures occur, or explicitly restrict the equivalence-checking claims to the instances that were verified correct.","section":"Section 5.2, Tables 3 and 5"},{"comment":"The approximate equality relation |a-b| < δ with δ=10^-14 is not transitive, and the chosen norm-max normalization folds approximation into edge values. The validation in Section 5.1 only checks that simulated state vectors have l2-norm near 1 and matches DDSIM outputs up to 20 qubits; it does not validate equivalence-checking outputs against ground truth. The 'x' entries in Tables 3 and 5 are a direct symptom of this gap. The paper needs a correctness argument or an experimental validation of equivalence checking on small circuits against explicit unitary matrices, or a sensitivity analysis showing that the chosen δ does not change answers on the reported benchmarks.","section":"Section 3, Algorithm 3 and 'Floating-point equality'"},{"comment":"The headline 'parallel speedups of up to x18 on 64 cores' is the P99 of the KetGPT 'some sharing' category, while the same table reports 64-core speedups as low as x0.5-x0.7 for the high-sharing category (i.e., slowdowns). The abstract and introduction present the x18 figure without this context. Please qualify the claim to the specific sharing category and percentile, or explain why the slowdowns on high-sharing diagrams do not affect the stated use cases.","section":"Section 5.1, Figure 4a and abstract"},{"comment":"The claim that Q-Sylvan is 'competitive with MQT DDSIM on large instances' is based on a post-hoc subset: circuits where either tool takes at least 10 seconds. This selection criterion should be stated as the formal definition of 'large instances,' and the number of circuits in that subset should be reported alongside the 61% and 30% win rates. Additionally, all reported runtimes appear to be from single runs with no variance or repeated measurements; for speedup claims, at least median or geomean over several runs is expected.","section":"Section 5.1, Figure 3"}],"minor_comments":[{"comment":"The text 'δ = 10914' before Algorithm 3 appears to be a typo; the intended value is 10^-14 as stated in the algorithm caption and elsewhere.","section":"Section 3"},{"comment":"The definition of norm-L2 is terse: please specify the phase θ and explain why normalizing by α/ν ∈ R+ is always achievable, or cite a reference for this normalization.","section":"Figure 2 caption"},{"comment":"The sentence 'we verified the full state vector output of both tools up to 20 qubits' should report the number of circuits checked and the numerical tolerance used for the comparison.","section":"Section 5.1"},{"comment":"The term 'runtime reduction' is not defined; please state whether it is the ratio of total runtimes on solved instances, a per-instance geometric mean, or some other aggregate.","section":"Table 1"},{"comment":"The open markers for timeouts are defined in the text and captions, but some subfigures lack an explicit legend; adding one would improve readability.","section":"Figures 3 and 4"}],"recommendation":"major_revision","confidential_remarks":"The incorrect equivalence-checking results in Tables 3 and 5 are the main obstacle. If the authors can trace them to a bug or to the δ-approximation and fix or explain them, the paper could be suitable. The simulation speedup claims may survive, but the equivalence-checking use case cannot be presented as correct without addressing these entries. I would not reject outright, because the scope is a systems paper and the parallel EVDD implementation is a genuine contribution, but the correctness caveat is load-bearing."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Q-Sylvan is a genuine engineering contribution: a parallel EVDD package on Sylvan with lock-free hash tables and approximate equality, with public code and reproducible benchmarks. The headline result—up to 18x parallel speedup on 64 cores—is a real advance over prior parallel EVDD attempts (2–3x), and the single-core comparison with DDSIM on large instances is credible.\n\nBefore trusting it, two caveats. First, the 18x number is the 99th percentile of the 'some sharing' category on KetGPT; MQT Bench 64-core P99 is only 4.2x, and some categories show slowdowns. The abstract omits that selection. Second, and more serious, the equivalence checker is demonstrably wrong on several benchmarks: Tables 3 and 5 show 'x' entries (Q-Sylvan Pauli on Grover 5, Q-walk 5, and both algorithms on VQE 5 for a missing gate). The paper never discusses these. The δ-close merging in Algorithm 3 is approximate, and while simulation outputs are checked against DDSIM up to 20 qubits and l2-norm, equivalence checking has no ground-truth validation. The 'x' entries look like the tolerance or normalization (norm-max) can cause wrong equivalence verdicts.\n\nFor simulation, the results are plausible and useful. The lack of repeated runs is minor for a systems paper. The normalization and δ are disclosed but not sensitivity-tested. The Pauli algorithm is new and correctly attributed to existing theory. Citation pattern is fine.\n\nWho gets value: people building quantum circuit simulation and verification tooling. It deserves a serious referee: the artifact is substantial and the simulation speedups warrant evaluation. I would send it to review, but with the expectation that the equivalence checking failures be fixed or disclosed, and the speedup claims qualified. I would not rely on the equivalence checker as it stands.","headline":"Useful parallel simulation package; equivalence checking not yet trustworthy.","tokens_in":17214,"tokens_out":4045,"would_cite":true,"duration_ms":37169,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q12","68W10","68P05"],"pacs":["03.67.-a","03.67.Lx"],"model":"deepseek-v4-flash","headline":"Q-Sylvan shows that edge-valued decision diagrams for quantum circuits can be parallelized, reporting an 18x speedup on 64 cores while staying competitive with a leading simulator on large instances.","keywords":["quantum circuit simulation","equivalence checking","edge-valued decision diagrams","parallel algorithms","work stealing","lock-free hash table","Q-Sylvan"],"falsifier":"Run Q-Sylvan's equivalence checker on two circuits whose unitary matrices differ entrywise by a value below $10^{-14}$; if it reports them equivalent, the delta-merging has produced a false positive. Alternatively, compare Q-Sylvan's simulated state vector to a high-precision (rational or multi-precision) reference on a 30-qubit benchmark and look for amplitude errors exceeding the tool's own acceptance threshold.","tokens_in":16284,"feed_emoji":"⚛️","tokens_out":5690,"duration_ms":50789,"temperature":0.7,"pith_summary":"The paper sets out to show that edge-valued decision diagrams (EVDDs), a compact data structure for quantum state vectors and matrices, can be efficiently parallelized for quantum tasks, something earlier attempts managed only poorly. It introduces Q-Sylvan, which combines fine-grained task parallelism from the Sylvan and Lace libraries with lock-free hash tables for complex edge values, and ships two use cases: circuit simulation and equivalence checking. The core reported result is a speedup of up to 18x on 64 cores on circuits whose diagrams have moderate sharing, together with single-core performance that is competitive with the MQT DDSIM simulator on large instances. If the claim holds, it means quantum circuit verification tools can ride multi-core hardware without giving up the compression that makes decision diagrams useful.","feed_headline":"Quantum circuit tool reports 18x speedup on 64 cores","feed_subtitle":"Parallel edge-valued decision diagrams stay competitive with the leading simulator while scaling across cores.","key_machinery":"The load-bearing object is the edge-valued decision diagram (EVDD), a rooted DAG whose edges carry complex numbers and whose paths multiply to vector entries or matrix elements; Q-Sylvan extends the Sylvan decision-diagram library with complex edge values. Three mechanisms carry the argument: a lock-free hash table that recognizes 'equivalent' complex values by rounding to a tolerance of delta = $10^{-14}$ and comparing components, which lets the DAG stay compact despite floating-point noise; norm-max normalization, which canonicalizes nodes by dividing child edge values by the larger child and multiplying the parent edge accordingly; and Lace-based fine-grained task parallelism, which spawns recursive calls in vector addition and matrix-vector multiplication as work-stealing tasks so many cores cooperate inside a single operation.","core_discovery":"On the paper's own terms, the central claim is that EVDDs with complex edge values are not inherently hard to parallelize for quantum workloads: using work-stealing tasks and a lock-free hash table that stores rounded-then-compared floating-point edge values, Q-Sylvan achieves speedups up to 18x on 64 cores while remaining competitive with MQT DDSIM on a single core for larger circuits. The same machinery is applied to quantum circuit equivalence checking through two algorithms, the 'alternating' method and a Pauli-based method, the latter being the first decision-diagram implementation of that algorithm. The paper reports 8-core speedups of up to 5.8x on equivalence checking benchmarks and solves some instances faster than the portfolio tool MQT QCEC, while not matching its overall single-core throughput.","pith_inferences":["Extending beyond the paper: the delta = 10^-14 merging is the part most likely to bite, since equivalence checking is a yes/no verdict and a false equivalence is silent; the paper's 'x' entries on VQE 5 suggest the risk is real, not hypothetical.","Extending beyond the paper: the speedups should carry over to stabilizer-like circuits, since the Pauli algorithm's polynomial behavior on Clifford gates gives the DD a very flat structure, though the paper does not test that directly.","Extending beyond the paper: the same parallel EVDD core could serve other linear-algebra workloads, such as tensor-network contraction, where the same multiplication and addition primitives appear."],"forward_implications":["On circuits whose decision diagrams have moderate sharing, Q-Sylvan's x18 speedup on 64 cores means quantum simulation and verification can use large multicore machines without abandoning DD compression.","The first DD-based Pauli equivalence-checking algorithm opens a practical route to verifying Clifford-heavy circuits inside a decision-diagram framework.","Because the same lock-free, delta-tolerant edge table serves both simulation and equivalence checking, any fix to numerical soundness would benefit both use cases.","If single-core performance on large instances is indeed competitive with MQT DDSIM, Q-Sylvan becomes a natural baseline for future quantum DD simulators."],"supporting_citations":[{"why":"Supplies the lock-free node table and the Sylvan framework that Q-Sylvan extends with edge values.","marker":"[8]"},{"why":"Provides the Lace work-stealing primitives used for fine-grained intra-operation parallelism.","marker":"[9]"},{"why":"Defines edge-valued decision diagrams with complex edge values, the data structure Q-Sylvan implements.","marker":"[23]"},{"why":"MQT DDSIM, the state-of-the-art EVDD simulator used as the single-core baseline on large instances.","marker":"[39]"},{"why":"Demonstrates that a zero tolerance for edge-value equality prevents node merging, motivating the nonzero delta in Q-Sylvan.","marker":"[24]"},{"why":"Proposes the 'alternating' equivalence-checking algorithm adopted by Q-Sylvan.","marker":"[3]"},{"why":"Gives the Pauli-based equivalence criterion used in Q-Sylvan's novel decision-diagram implementation.","marker":"[33]"},{"why":"Quokka-Sharp, the model-counting equivalence checker used as a comparison baseline.","marker":"[22]"},{"why":"Provides the atomic compare-and-swap shared hash table technique used for concurrent edge-value storage.","marker":"[19]"}],"fun_headline_variants":["Parallel decision diagrams hit 18x speedup for quantum circuits","Quantum circuit tool scales to 18x on 64 cores","Q-Sylvan: 18x speedup via lock-free hash tables","First Pauli-based equivalence checking in decision diagrams"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that treating complex edge values as equal when they differ by less than $10^{-14}$ never changes the answer: the paper relies on this tolerance for both simulation and equivalence checking, yet validates it mainly by checking $\\ell^2$-norm near 1 and matching another simulator's outputs on circuits up to 20 qubits.","fun_headline_variants_meta":{"raw":{"variants":["Parallel decision diagrams hit 18x speedup for quantum circuits","Quantum circuit tool scales to 18x on 64 cores","Q-Sylvan: 18x speedup via lock-free hash tables","First Pauli-based equivalence checking in decision diagrams"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000689,"raw_usage":{"total_tokens":3088,"prompt_tokens":876,"completion_tokens":2212,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":492,"completion_tokens_details":{"reasoning_tokens":2141}},"tokens_in":492,"tokens_out":2212,"duration_ms":16415,"temperature":1.0,"reasoning_tokens":2141,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T10:06:07.598662+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Q-Sylvan's equivalence checker on two circuits whose unitary matrices differ entrywise by a value below $10^{-14}$; if it reports them equivalent, the delta-merging has produced a false positive. Alternatively, compare Q-Sylvan's simulated state vector to a high-precision (rational or multi-precision) reference on a 30-qubit benchmark and look for amplitude errors exceeding the tool's own acceptance threshold.","supporting_citations":[{"cited_title":"STTT 19, 675–696 (2017)","cited_arxiv_id":null,"evidence_quote":"Supplies the lock-free node table and the Sylvan framework that Q-Sylvan extends with edge values."},{"cited_title":"In: Euro-Par 2014: Parallel Processing Workshops: Euro-Par 2014 International Workshops, Porto, Portugal, August 25-26, 2014, Revised Selected Papers, Part II","cited_arxiv_id":null,"evidence_quote":"Provides the Lace work-stealing primitives used for fine-grained intra-operation parallelism."},{"cited_title":"In: International Joint Conference on Automated Reasoning","cited_arxiv_id":null,"evidence_quote":"Defines edge-valued decision diagrams with complex edge values, the data structure Q-Sylvan implements."},{"cited_title":"In: Proceedings of the 59th Design Automation Conference","cited_arxiv_id":null,"evidence_quote":"MQT DDSIM, the state-of-the-art EVDD simulator used as the single-core baseline on large instances."},{"cited_title":"In: 36th International Symposium on Multiple-Valued Logic (ISMVL’06)","cited_arxiv_id":null,"evidence_quote":"Demonstrates that a zero tolerance for edge-value equality prevents node merging, motivating the nonzero delta in Q-Sylvan."},{"cited_title":"IEEE Transactions on TCAD40(9), 1810–1824 (2020)","cited_arxiv_id":null,"evidence_quote":"Proposes the 'alternating' equivalence-checking algorithm adopted by Q-Sylvan."},{"cited_title":"International Journal of Quantum Information 8(05), 807–819 (2010)","cited_arxiv_id":null,"evidence_quote":"Gives the Pauli-based equivalence criterion used in Q-Sylvan's novel decision-diagram implementation."},{"cited_title":"In: Proceedings of the 30th international design automation conference","cited_arxiv_id":null,"evidence_quote":"Quokka-Sharp, the model-counting equivalence checker used as a comparison baseline."},{"cited_title":"In: Formal Methods in Computer Aided Design","cited_arxiv_id":null,"evidence_quote":"Provides the atomic compare-and-swap shared hash table technique used for concurrent edge-value storage."}],"review_version":1}