{"id":"d2aacbf1-f31b-4dbb-a1ce-0f0afd47cf74","arxiv_id":"2506.07635","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"A sampling-plus-LP pipeline synthesizes barrier certificates for quantum circuits and SMT-verifies them over continuous state spaces, for finite or infinite horizons with uncertainty.","lead":"The authors propose a sampling-based method to construct barrier certificates, which are mathematical proofs that a quantum circuit never reaches forbidden states. The method handles finite and infinite time horizons and uncertainties in initial states and gate dynamics, with case studies on gates such as Z, X, and Grover's algorithm.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Grover certificates are SMT-checked in a 2D angle abstraction whose mapping to the original n-qubit circuit and its Z0/Zu is unproved; the reported gamma, lambda, delta also fail Definition 5.","rationale":"The core LP-plus-SMT pipeline is sound when the certificate is defined and verified on the actual state space of the circuit, and the direct case studies such as the Z gate and alternating CX/CZ are plausible demonstrations. The Grover case is the only place where the paper claims to handle uncertainty in initial states and dynamics, and it is also the place where the verification is shifted to a reduced 2D angle model. The paper asserts that Grover's evolution is confined to a 2D subspace, but that fact alone does not justify replacing the original initial and unsafe sets with angle intervals: the original Z0 contains states outside the 2D manifold, the original Zu (high probability on a single non-solution basis state) is not represented by the chosen angle interval, and the effect of uncertain M and noise mu on states outside the manifold is not analyzed. Without a formal abstraction proof, the Grover certificates do not establish safety of the original n-qubit circuit. The separate numerical inconsistency in the reported gamma, lambda, and delta values is an independent correctness defect: the listed certificate does not satisfy Definition 5 as written, so the example is not reproducible from the reported parameters. These issues do not necessarily invalidate the whole methodology, but they undermine the paper's central uncertainty-handling claim and require correction or a clearly stated weaker claim. The reader's weakest-assumption analysis identified the same load-bearing concern, so the recommended conditional verdict is unchanged.","tokens_in":15830,"tokens_out":11953,"duration_ms":155163,"concrete_test":"Implement the n=5, K=32, M=8, err=0.5, eta=0.3 Grover instance in its full 32-dimensional form in an SMT solver, with the Section VI-C definitions of Z0 and Zu and with the noisy rotation angle theta+mu as the only uncertainty. Take the reported certificate B(z)=21.22065*phi, extended to the full state space by B(z)=+infinity for z not in the 2D manifold. Check the three Definition 5 conditions; the initial-set constraint (5a) is refuted by any z0 in Z0 with a nonzero imaginary component outside span{|alpha>,|beta>}. Additionally, verify whether the image of the original unsafe set |z_p|^2 >= 0.9 intersects the manifold {z(phi)}; since it is empty for the stated K and M, the abstract Zu cannot be the image of the original unsafe set. Either check settles whether the 2D certificate applies to the original circuit.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The paper's central claim is that a synthesized and SMT-checked certificate proves safety of the original quantum circuit. That conclusion is only as sound as the abstraction used in each case study. The uncertain-Grover experiments (Sec. VI-B3, Table III) use B(c,z(phi))=c*phi on the 2D manifold z(phi)=cos(phi)|alpha>+sin(phi)|beta>, and the SMT check is performed only over phi in [0,2*pi]. No theorem or argument shows that the original n-qubit system with initial set Z0={z: 1/2^n - err <= |z_j|^2 <= 1/2^n + err, |Im z_j| <= sqrt(err)} and unsafe set Zu={z: |z_p|^2 >= 0.9} (Sec. VI-C) is exactly or conservatively represented by this manifold. Z0 contains states with small imaginary components that are not in span{|alpha>,|beta>}; the dynamics with uncertain M and rotation noise mu is never proved to keep such states in the manifold; and the chosen abstract Zu=[3*pi/2, 11*pi/6] is not derived from |z_p|^2 >= 0.9. In fact a state in the 2D subspace has single non-solution probability cos^2(phi)/(K-M), which cannot reach 0.9 for K=32, M=8, so the abstract unsafe set corresponds to a different property. Thus the Grover* certificates verify a purely rotational 2D system, not the specified quantum circuit. Separately, the reported certificate for n=5 (gamma=11.49015, lambda=28.58842, delta=100, T=2) violates Definition 5 because gamma+delta*T=11.49+200 is not less than 28.59. Until the abstraction is proved sound and the numbers corrected, the Grover experiments do not support the uncertainty-handling claims.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a scenario-based synthesis method for barrier certificates for discrete-time quantum circuit models. Given a parametrized certificate template, the method samples states from the initial, unsafe, and full state sets, solves a linear program to fit the template parameters, and then uses an SMT solver to verify the candidate against the universally quantified barrier-certificate conditions. The framework covers invariant, k-inductive, time-varying k-inductive, and finite-horizon certificates. Experiments are reported for several small circuits (Z, CNOT, T, CZ, Hadamard, X, SWAP, alternating CX/CZ), and for Grover's algorithm using a two-dimensional angle abstraction with uncertainty in the number of solutions and in the rotation angle.","tokens_in":16247,"tokens_out":10730,"duration_ms":135412,"significance":"If the method works as claimed, it provides a practical, machine-checkable route to safety verification of small quantum circuits under initial-state and dynamics uncertainty, combining sampling-based optimization with SMT validation. The non-Grover case studies are supported by the final SMT checks over the original state space, and the implementation is publicly available, which aids reproducibility. However, the Grover case studies currently do not support the paper's central claim: the abstraction from the n-qubit circuit to the two-dimensional rotation model is unproved, and the reported finite-horizon parameters violate Definition 5. The central methodology is sound in principle, but these issues are load-bearing for a major advertised application.","major_comments":[{"comment":"The Grover* certificates in Table III are synthesized and SMT-checked only over the two-dimensional manifold z(φ)=cosφ|α⟩+sinφ|β⟩ with φ∈[0,2π], while the specification in Section VI-C is stated for the full n-qubit state space. The paper never establishes that this manifold is a sound or conservative abstraction of the original uncertain dynamics and of the sets Z0={z: 2^{-n}-err≤|z_j|²≤2^{-n}+err, |Im z_j|≤√err} and Zu={z: |z_p|²≥0.9}. This matters because Z0 contains states outside span{|α⟩,|β⟩}, and Zu cannot be represented on the manifold: for K=32 and M=8, any state on the manifold has probability cos²φ/(K-M)≤1/24≈0.042 for a fixed non-solution state p, which never reaches 0.9. The abstract unsafe set [3π/2,11π/6] therefore corresponds to a different property. An SMT check over φ does not imply safety of the original circuit; a sound abstraction relation or direct verification over the original state space is required.","section":"Section VI-B3 and Section VI-C"},{"comment":"The reported finite-horizon certificate for n=5, M=8 with γ=11.49015, λ=28.58842, δ=100, T=2 does not satisfy the defining inequality γ+δ·T<λ, since 11.49015+200=211.49015 is not less than 28.58842. The certificate is therefore not a valid barrier certificate according to Definition 5, and the safety conclusion for that case does not follow from Theorem 1. The numbers also appear internally inconsistent: for B(c,z(φ))=21.22065φ, the maximum one-step increase on Z0 is c·(θ+η)≈28.59, so δ should be at most ≈28.59, while the minimum of B on Zu is ≈100.0, so λ should be at least ≈100.0 for the condition γ+δ·T<λ to hold. The authors should correct the reported parameters and re-run the SMT verification.","section":"Section VI-B3, Definition 5"}],"minor_comments":[{"comment":"The displayed certificate B(z)=-9.99934 z0 z0 + 12.99994 should use |z0|² (or ̅z0 z0); as printed, z0z0 is ambiguous. With the reported γ=4, evaluating the displayed expression at |z0|²=0.9 gives about 4.0005, which exceeds γ; the rounded coefficients should be reconciled with the SMT-verified values.","section":"Section VI-B1"},{"comment":"The Sobol-sequence sampling description is inconsistent: it first decomposes z_j=x_j+iy_j into real variables, then describes constructing a probability vector and assigning independent phases θ_j∈[0,2π). Please clarify the exact dimension and algorithm used to map Sobol points to normalized quantum states.","section":"Section V-C"},{"comment":"The constraint derivation contains typographical errors: 'B(c, G(z(ϕ)) − B(c, z(ϕ)) = c·(ϕ+eθ) − c·ϕ' has a missing parenthesis and an undefined symbol eθ; it should state the one-step increment as c·(θ+μ), where μ is the rotation noise. The worst-case condition c·(θ+η)≤δ should be written explicitly as the constraint used in the linear program.","section":"Section VI-B3"}],"recommendation":"major_revision","confidential_remarks":"The Grover case is the only part of the paper where the verified model differs from the original circuit. If the authors can either prove a sound abstraction from the n-qubit system to the two-dimensional rotation model or replace the Grover* rows with certificates verified over the original state space, the paper would be close to publishable. The numerical inconsistency in Table III should be caught and fixed during revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the core pipeline is sound and some case studies are real, but the Grover section does not establish what it claims. Read it as an engineering contribution with a load-bearing gap in the headline experiment.\n\nWhat's actually new: the paper adapts the scenario approach (sample, solve LP, SMT-check) to quantum circuits with uncertainty in initial states and gates, covers finite and infinite horizons, and releases code. The final SMT check against universally quantified constraints is the right thing: the certificate is not trusted because it fits samples, it is trusted because the solver says no counterexample exists. Several case studies (Z gate, alternating CX/CZ, T, SWAP) look correct and are reported with reproducible numbers. The discussion of template choice and unsolved cases is honest.\n\nThe soft spots are real, and they concentrate in Section VI-B3. The Grover reduction to the 2D span of |α> and |β> is never proved conservative for the original n-qubit circuit. The paper's own Z0 (amplitudes near uniform, with imaginary components) and Zu (|z_p|^2 >= 0.9) are replaced by angle intervals with no argument that one containing the other. In fact, for the n=5 case (K=32, M=8), a state on that manifold has a single non-solution probability at most 1/(K-M)=1/24, so the abstract unsafe set {φ in [3π/2, 11π/6]} is not the set of states with |z_p|^2 >= 0.9. The verified certificate proves safety of a different, purely rotational system. On top of that, the printed certificate parameters for that row (γ=11.49, δ=100, T=2, λ=28.59) violate the paper's own Definition 5: γ+δT=211.49 is not less than λ. That is not a rounding artifact. The Z gate certificate in Section VI-B1 also has a small inconsistency: with the printed coefficient, B at |z0|^2=0.9 is about 4.0005, slightly above the reported γ=4. Minor, but it makes you wonder about the exactness of the tables.\n\nNet: the method is plausible and worth a serious referee, but the Grover case needs a correct justification of the abstraction (or a statement that the certificate applies to the reduced model only), and the tables need fixing. I'd send it out, but with the expectation of major revision. Right now I would not cite the uncertainty results.","headline":"Solid sampling+SMT pipeline for small circuits, but the Grover case study overclaims: the 2D abstraction is unproved and the reported parameters violate the definition.","tokens_in":16768,"tokens_out":4086,"would_cite":false,"duration_ms":46136,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes that sampling-based linear programming can synthesize formally verified barrier certificates for quantum circuits, covering uncertain initial states and gate noise over finite or infinite horizons.","keywords":["quantum circuit verification","barrier certificates","scenario-based optimization","SMT verification","formal verification","Grover's algorithm","uncertain quantum dynamics","k-inductive certificates"],"falsifier":"Run the exact n-qubit Grover circuit for the certified parameter choices (for example, 5 qubits, M=8, err=0.5, and η=0.3 with horizon T=2), sampling many initial states and noise values from the certified ranges, and check by state-vector simulation whether any exact trajectory reaches the unsafe angle interval within the horizon. A single such counterexample would show either that the two-dimensional reduction is not exact or that the SMT check was unsound.","tokens_in":15639,"feed_emoji":"⚛️","tokens_out":9215,"duration_ms":100792,"temperature":0.7,"pith_summary":"The paper claims that a formal safety proof for a quantum circuit can be produced by sampling a finite number of states, solving a linear program for the coefficients of a barrier-certificate template, and then checking the resulting candidate against the full state space with an SMT solver. If the check passes, the circuit is certified never to move from any of the specified initial states into any undesired state, even when the initial states and gate rotations are uncertain and the time horizon is unbounded. The authors demonstrate the approach on several small circuits and on Grover's search with an uncertain number of solutions and rotation noise, for both finite and infinite horizons. The payoff for a user is a machine-checkable certificate that covers infinitely many states without exhaustive simulation.","feed_headline":"Sampling builds machine-checkable safety proofs for quantum circuits","feed_subtitle":"Certificates verified over all states, not just samples, cover uncertain initial states and gate noise.","key_machinery":"The load-bearing object is the barrier-certificate template $B(\\alpha,z)$: a parameterized real-valued function, usually a polynomial of bounded degree in the complex amplitudes, whose defining conditions become a linear program once states are sampled from the initial, unsafe, and full state regions. The second component is the verification step: the candidate returned by the linear program is checked with an SMT solver against the original universally quantified constraints, so the final certificate is not just a statistical statement about samples. For Grover's algorithm the machinery is a geometric reduction: the $n$-qubit search dynamics is confined to the two-dimensional subspace spanned by the uniform non-solution state $|\\alpha\\rangle$ and the solution state $|\\beta\\rangle$, the Grover operator becomes a rotation by angle $\\theta$, and the certificate template is simply $B(c,\\varphi)=c\\cdot\\varphi$ with $\\varphi$ the polar angle of the state.","core_discovery":"The central discovery is that barrier certificates for quantum circuits do not have to be constructed by hand or by solving a hard robust-optimization problem: a candidate can be synthesized from finitely many sampled complex states as the solution of a linear program, then promoted to a genuine proof by an SMT check of the universal constraints. The certificate is a real-valued function $B$ on the complex state space satisfying $B \\leq 0$ on the initial set, $B > 0$ on the unsafe set, and a decrement condition along the circuit dynamics, with relaxed $k$-inductive and finite-horizon variants for harder cases. For complex polynomial templates the imaginary part is discarded, turning the sampled constraints into real linear inequalities. The case studies include verified certificates for the Z, T, CX, CZ, SWAP and Hadamard circuits, and for Grover's search under uncertainty in the number of solutions and the rotation angle after reducing the dynamics to a two-dimensional rotation.","pith_inferences":["Inference: if the sampling-and-LP pipeline is the bottleneck, then exploiting low-dimensional invariant subspaces of the sort used for Grover may be the main route to scaling, and other algorithms with known symmetry reductions are natural next targets.","Inference: the paper leaves open whether every safe quantum circuit admits a barrier certificate; if that necessity question is answered affirmatively, the two-phase synthesize-then-check scheme would become a complete verification method rather than a sufficient one.","Inference: a direct experimental check of the Grover reduction would be to run the exact state-vector circuit for the certified parameters and compare reachable angles with the angle-interval certificate; disagreement would localize the failure to the reduction rather than to the certificate search.","Inference: the same sampling, linear-programming, and SMT-check recipe could be applied to time-dependent classical systems and to hybrid quantum-classical circuits, provided the dynamics are given as computable unitary or superoperator maps."],"forward_implications":["A verified barrier certificate is a formal proof of non-reachability; no simulation or testing of individual runs is needed to trust the safety claim for the specified initial and unsafe sets.","Uncertain initial states and uncertain gate parameters can be folded into the sampled constraints, so certificates can cover whole families of circuits rather than a single nominal circuit.","Finite-horizon certificates can certify algorithms like Grover with a bounded number of iterations, where an invariant barrier that must hold forever would be too strict.","If no certificate is found, the method only reports that the chosen template failed on the samples; it does not imply the circuit is unsafe, so a user must change the template or sampler rather than declare failure.","The approach currently scales exponentially with qubit count because sampling density and SMT verification cost grow with the dimension of the state space, so the demonstrated cases are small circuits."],"supporting_citations":[{"why":"Supplies the original barrier-certificate conditions (initial, unsafe, decrement) that define the safety argument.","marker":"[9]"},{"why":"Introduces the scenario-based sampling synthesis for k-inductive barrier certificates that this paper extends to quantum circuits.","marker":"[11]"},{"why":"Introduces discrete-time barrier certificates for quantum circuits and the time-dependent hybrid variant used for alternating gates.","marker":"[20]"},{"why":"Defines k-inductive barrier certificates, whose relaxed decrement condition the paper uses for infinite-horizon cases.","marker":"[24]"},{"why":"Defines finite-horizon barrier certificates, which the paper uses for bounded-time circuits and Grover's algorithm.","marker":"[25]"},{"why":"Provides the low-discrepancy sequence used to sample quantum states across the initial, unsafe, and full state regions.","marker":"[30]"},{"why":"Is the interior-point linear programming solver used to solve the sampled constraint problem.","marker":"[31]"},{"why":"Is the SMT solver used to verify the candidate certificate against the universal constraints.","marker":"[32]"},{"why":"Gives the two-dimensional subspace reduction of Grover's algorithm that the paper's angle-based certificate relies on.","marker":"[33]"}],"fun_headline_variants":["Finite samples, infinite proof: quantum circuit safety verified","Scenario-based certificates verify quantum circuits exactly","LP and SMT hand quantum circuits machine-checkable safety","Barrier certificates from samples, verified for all states"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the circuit model used in the constraints—for Grover, the two-angle rotation—matches the true circuit exactly for every allowed uncertainty, so that a certificate for the model is a certificate for the real circuit.","fun_headline_variants_meta":{"raw":{"variants":["Finite samples, infinite proof: quantum circuit safety verified","Scenario-based certificates verify quantum circuits exactly","LP and SMT hand quantum circuits machine-checkable safety","Barrier certificates from samples, verified for all states"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000259,"raw_usage":{"total_tokens":1535,"prompt_tokens":846,"completion_tokens":689,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":462,"completion_tokens_details":{"reasoning_tokens":627}},"tokens_in":462,"tokens_out":689,"duration_ms":8059,"temperature":1.0,"reasoning_tokens":627,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:30:02.593131+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the exact n-qubit Grover circuit for the certified parameter choices (for example, 5 qubits, M=8, err=0.5, and η=0.3 with horizon T=2), sampling many initial states and noise values from the certified ranges, and check by state-vector simulation whether any exact trajectory reaches the unsafe angle interval within the horizon. A single such counterexample would show either that the two-dimensional reduction is not exact or that the SMT check was unsound.","supporting_citations":[{"cited_title":"Safety verification of hybrid systems using barrier certificates,","cited_arxiv_id":null,"evidence_quote":"Supplies the original barrier-certificate conditions (initial, unsafe, decrement) that define the safety argument."},{"cited_title":"A scenario approach for syn- thesizing k-inductive barrier certificates,","cited_arxiv_id":null,"evidence_quote":"Introduces the scenario-based sampling synthesis for k-inductive barrier certificates that this paper extends to quantum circuits."},{"cited_title":"Verification of Quantum Circuits through Discrete-Time Barrier Certificates","cited_arxiv_id":"2408.07591","evidence_quote":"Introduces discrete-time barrier certificates for quantum circuits and the time-dependent hybrid variant used for alternating gates."},{"cited_title":"Safety verification of dynamical systems via k-inductive barrier certificates,","cited_arxiv_id":null,"evidence_quote":"Defines k-inductive barrier certificates, whose relaxed decrement condition the paper uses for infinite-horizon cases."},{"cited_title":"Formal verification of unknown discrete- and continuous-time systems: A data- driven approach,","cited_arxiv_id":null,"evidence_quote":"Defines finite-horizon barrier certificates, which the paper uses for bounded-time circuits and Grover's algorithm."},{"cited_title":"Distribution of points in a cube and approximate evalu- ation of integrals,","cited_arxiv_id":null,"evidence_quote":"Provides the low-discrepancy sequence used to sample quantum states across the initial, unsafe, and full state regions."},{"cited_title":"Parallelizing the dual revised simplex method,","cited_arxiv_id":null,"evidence_quote":"Is the interior-point linear programming solver used to solve the sampled constraint problem."},{"cited_title":"Z3: An Efficient SMT Solver,","cited_arxiv_id":null,"evidence_quote":"Is the SMT solver used to verify the candidate certificate against the universal constraints."},{"cited_title":"Quantum computation,","cited_arxiv_id":null,"evidence_quote":"Gives the two-dimensional subspace reduction of Grover's algorithm that the paper's angle-based certificate relies on."}],"review_version":1}