Pith. sign in

REVIEW 4 major objections 7 minor 76 references

Formal Verification of Variational Quantum Circuits

T0 review · 4 major / 7 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read A formal framework certifies robustness of variational quantum circuits against input perturbations.

desk verdict Solid abstract-interpretation core for VQC robustness, but the NP-hardness proof does not connect to the formal definition and the abstract classifier has an inversion bug; both are fixable but load-bearing as printed. read the letter →

arxiv 2507.10635 v1 pith:PEKH3MOH submitted 2025-07-14 quant-ph cs.LGcs.PL

Nicola Assolini , Luca Marzari , Isabella Mastroeni , Alessandra di Pierro This is my paper
classification quant-phcs.LGcs.PL MSC 68Q6081P68
keywords variationalquantumcircuitsformalverificationabstractinterpretationintervalarithmeticrobustnesscertificationmachinelearningNP-hardnessreachabilityanalysis
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Variational quantum circuits, the quantum analogue of trained neural networks, are known to misclassify when their inputs are slightly perturbed, but until now no framework gave provable robustness guarantees. This paper claims the first formal verification framework for VQCs: it abstracts circuit execution by representing quantum states and inputs as intervals of complex and real values, and it proves the resulting abstract semantics is sound, meaning every concrete behaviour is covered by the abstract one. It also proves that the robustness verification problem, called RVVQC, is NP-hard, and it identifies where the interval abstraction loses precision because of state normalization. To make the approach practical, it introduces precision-recovery techniques and reports a tool that certifies, on standard benchmarks, the largest input perturbation a trained VQC can tolerate. If correct, the work replaces purely empirical robustness checks with certificates and explains why exact verification is inherently hard.

What carries the argument

The mechanism that carries the argument is the abstract semantics built on complex intervals, defined as pairs of real intervals over basis states, combined with abstract environments that map inputs to real intervals. Representing states as mappings from basis vectors to complex amplitudes lets every rotation gate become a matrix of functions or constants whose entries are evaluated by interval arithmetic; the unit-norm constraint on concrete states is exactly the dependency that the interval hull forgets, and the paper traces its incompleteness results to this loss. Precision is recovered partially by composing parametric gates into a single symbolic operator before abstracting, by clipping amplitudes to $[-1,1]$ and probabilities to $[0,1]$, and by splitting input intervals, and these techniques are what make the tool's certificates possible.

What would settle it

Build the paper's VQC from a satisfiable 3-SAT formula and run its verifier on a small but nonzero perturbation ball around a satisfying assignment; if the abstract output no longer certifies the expected class, or a concrete simulation changes the classification under perturbation, the equivalence between satisfiability and RVVQC robustness used in the NP-hardness proof fails.

Watch

Extended reading notes

Core claim

The central claim is that variational quantum circuit verification can be carried out through an interval-based abstract interpretation of a purpose-built language, LVQC, whose states are functions from basis vectors to complex amplitudes. The paper defines a concrete semantics for encoding gates, parametric gates, measurement, and classification, then an abstract semantics in which inputs are real intervals, amplitudes are complex intervals, and every gate is evaluated by interval arithmetic. Theorem 5.6 states that this abstract semantics is sound. The paper also shows it is incomplete in general, because normalization couples amplitudes that the non-relational interval domain treats independently, and it gives completeness conditions for generalized-permutation unitaries, for encoding from basis states, and for measurement on states with only real or only imaginary parts. On top of this, the paper formalizes robustness as RVVQC, proves the problem NP-hard by a reduction from 3-SAT, and reports the first tool that provably certifies the maximum epsilon perturbation tolerable by a given VQC.

Load-bearing premise

The NP-hardness result assumes that a 3-SAT formula can be converted into a VQC whose robustness to input perturbations, not just whose output on each single assignment, is equivalent to the formula's satisfiability.

Editorial extensions

If this is right

  • Robustness of trained VQCs can be certified with formal guarantees rather than estimated by sampling adversarial examples.
  • For any classifier fitting the LVQC language, the maximum input perturbation can be bounded by combining interval verification with exponential and binary search, as demonstrated on standard benchmarks.
  • Exact robustness verification for VQCs is NP-hard, so no polynomial-time complete verifier should be expected in general; abstraction-based certificates are the realistic target.
  • The incompleteness analysis tells circuit designers which operations preserve precision, such as generalized permutations and basis-state encodings, and which lose it, guiding more robust ansatz design.
  • Sound abstract classification returns a set of possible classes, and an unambiguous class with strictly higher interval lower bound is guaranteed to be the concrete class.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same abstract semantics could verify properties other than robustness, such as safety bounds on measurement distributions or stability over prescribed input regions, by swapping only the post-processing predicate.
  • Because the incompleteness is traced to the unit-norm constraint, a natural next step is an abstract domain that keeps amplitudes on the unit sphere, such as intervals intersected with the circle, which would reduce false alarms while preserving soundness.
  • The certification procedure runs after training on fixed parameters, so it could be embedded in the training loop as a robustness check on each candidate model, making robustness part of the optimization objective.
  • If the interval precision results scale beyond the reported low-dimensional inputs, the same pipeline could be applied to larger quantum feature maps, where empirical adversarial testing is currently the only option.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 7 minor

Summary. The paper introduces LVQC, a small imperative language for variational quantum circuits, together with a concrete semantics based on a functional representation of quantum states and an abstract interval semantics over real and complex intervals. The main theoretical claims are: soundness of the interval abstraction (Theorem 5.6), an incompleteness analysis with sufficient conditions for local completeness (Section 6), the definition of the robustness verification problem RVVQC (Definition 7.2), an NP-hardness result for RVVQC (Theorem 7.4), and a set of precision-recovery techniques (Section 8). The paper also reports a prototype verification pipeline and evaluates it on trained VQC classifiers for Iris and MNIST subsets, claiming that it is the first tool able to certify the maximum tolerable input perturbation for a VQC.

Significance. The interval-based abstract semantics for VQCs is a natural and potentially useful contribution to quantum machine learning verification. The soundness theorem (Theorem 5.6) follows from standard interval arithmetic and is plausible as stated, and the local completeness analysis in Section 6 - generalized permutations, single-active-basis encodings, and degenerate measurement conditions - is a genuine attempt to understand when interval propagation loses precision. The paper also gives concrete precision-recovery techniques and a working implementation, which is valuable for the community. However, the formal definition of the abstract classifier xi^sharp in Section 7.2 appears inconsistent with the surrounding prose, and the NP-hardness proof in Section 7.3 does not connect the 3-SAT reduction to the definition of RVVQC. Because the complexity result is one of the headline contributions, this is a load-bearing gap that must be repaired before the claims as stated can be accepted.

major comments (4)
  1. [§7.3, Theorem 7.4] The proof of NP-hardness of RVVQC does not establish the required reduction to Definition 7.2. Definition 7.2 requires that for every environment sigma, the set of classifications over the perturbation ball Sigma_{sigma,epsilon} is the singleton containing the clean classification. Lemma 7.6, however, only shows that for the single environment sigma_a induced by a Boolean assignment a, the exact, unperturbed circuit outputs class 1 if and only if a satisfies Phi. The proof never fixes epsilon, never quantifies over Sigma_{sigma,epsilon}, and never analyzes whether perturbing sigma_a changes the output. Moreover, formula satisfiability is an existential property, while RVVQC is a universal property over all centers sigma. Consequently Theorem 7.4 is unsupported as written, and Proposition 7.8, which inherits the result, is unsupported as well. The final sentence 'The proof is complete' at the end of Lemma 7.6 closes a proof about a different predicate.
  2. [§7.2, definition of xi^sharp] The formal definition of xi^sharp appears to invert the intended comparison. The set comprehension selects classes b for which the aggregated interval of b is strictly below the aggregated interval of every b', including b itself, so no b can satisfy the strict inequality as stated. This contradicts the prose, which says that xi^sharp selects 'the intervals with a lower bound greater than any other interval distribution', and it contradicts the example, which returns {00, 11} as the high-probability set. Since xi^sharp is used in Proposition 7.1 and in the abstract verification predicate, this definition must be corrected and the soundness proof rechecked.
  3. [§7.3, Lemma 7.6] The reduction relies on an undefined property: 'Pi is satisfiable on c' with Pi = {1} is never defined, and Lemma 7.5 only states that the encoding gadget maps assignments to computational basis states, not that the circuit is robust in the sense of Definition 7.2. The proof is also carried out on one concrete formula with three variables and two clauses, with no argument that the construction generalizes to arbitrary 3-SAT instances. The authors should either provide a complete reduction that quantifies over perturbation balls or explicitly revise the claimed complexity theorem.
  4. [§9, verification results] The claim that the pipeline is 'the first tool able to provably certify the maximum epsilon input perturbation' is stronger than what the evaluation supports: the reported maximum epsilon is a mean over 10 randomly selected inputs, no comparison with existing verifiers is provided, and the Verify procedure is described algorithmically without a formal termination or completeness guarantee for the search over epsilon. This claim should be qualified or substantiated.
minor comments (7)
  1. [§7.2] In the example for xi^sharp, the line '010 -> [0.1, 0.03]' has a lower bound larger than the upper bound; this is likely a typo for [0.03, 0.1].
  2. [§8.1, Proposition 8.1 proof] The proof contains the ill-formed inequality '-1 <= Re(psi(e)) >= 1'; it should be '-1 <= Re(psi(e)) <= 1', and similarly for the imaginary part.
  3. [§9] The sentence 'we have q0 equal to 1 with a probability in [0.461, 1.04], 1' contains a stray digit '1' at the end.
  4. [§2.1] The text says 'All quantum circuits can be constructed by using only gates in {Rx, Rx, Rx, CX}'; this should presumably read {Rx, Ry, Rz, CX}.
  5. [§7.3, Definition 7.2] The notation uses 'q in CV^n_c' for the list of output observed qubits, but the set of qubits is denoted QV_c elsewhere; the notation should be made consistent.
  6. [§6.2, Theorem 6.7] The condition 'Re(Psi_c(e)) = 0 or Im(Psi_c(e)) = 0' is written for the set Psi_c; it should be stated pointwise for every state psi in Psi and every basis element e.
  7. [§5.4] The sentence 'the probability of measuring 1 ranges between [0.407, 1, 221]' contains a comma in place of a decimal point; it should read [0.407, 1.221].

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: soundness (Thm 5.6), completeness results (Thms 6.4–6.7), and abstract classification soundness (Prop 7.1) are derived from interval arithmetic and the paper's own definitions; the NP-hardness gap in Thm 7.4 is a separate correctness issue, not a circular reduction.

full rationale

The paper's central formal results are self-contained. Theorem 5.6 is proven by composing sound interval-arithmetic operations; the incompleteness and local-completeness results (Lemma 6.1, Theorems 6.4, 6.6, 6.7) are established from the definitions of the abstract domain and the structure of the operators. Proposition 7.1 follows directly from the soundness of the abstract semantics and the definition of the abstract classification function. The verification pipeline in Section 9 computes maximum tolerated perturbations via interval propagation and refinement; it does not fit parameters to the quantities it reports as certified, so no fitted-input-called-prediction pattern occurs. Self-citations such as [31,44,46] are used only to cite pre-existing concepts of local completeness and abstract robustness for neural networks; they do not carry the derivation of any theorem in this paper. One issue flagged by the skeptical reading is real but not circular: the NP-hardness proof of Theorem 7.4 reduces 3-SAT to the property that the unperturbed circuit outputs class 1 (Lemma 7.6), never connecting to the universal perturbation-ball condition in Definition 7.2. That is a correctness/completeness gap in the hardness argument, not a reduction of a claimed prediction to its own inputs by construction. Therefore the circularity score is 0.

Assumptions & free parameters 1 free parameters · 6 assumptions · 0 invented entities

The ledger is clean on the theory side: no ad hoc parameters are fit to make theorems hold, and no physical entities are postulated. The only fitted quantities are the trained circuit weights, which are inputs to the empirical certification rather than parts of the derivation. The main axioms are standard quantum mechanics, standard interval arithmetic, universality of the gate set, and a cited circuit construction for 3-SAT.

free parameters (1)
  • Trained VQC weights for QCL, CCQC, and PV models = not reported
    The certified max-epsilon results in Section 9 depend on the specific trained parameter values, which are optimized on each dataset but never listed in the paper; the theoretical framework treats these as fixed constants after training.
assumptions (6)
  • domain assumption Quantum states are unit vectors and evolution is unitary (postulates of quantum mechanics)
    Section 2.1, used to define state normalization and unitary operators throughout, including the incompleteness argument in Lemma 6.1.
  • standard math Interval arithmetic operations are sound over-approximations of real arithmetic
    Used in Theorem 5.6 and in the definition of abstract semantics in Section 5.3; sourced from Moore et al. [51].
  • standard math The gate set {Rx, Ry, Rz, CX} is universal for quantum computation
    Invoked in Section 4.1 to justify that LVQC can express any quantum circuit.
  • standard math A Boolean formula can be compiled into a quantum circuit U_3SAT in polynomial size (Kitaev et al.)
    Used in the NP-hardness reduction in Theorem 7.4, Section 7.3.
  • domain assumption Classification is defined by the argmax of aggregated measurement probabilities
    Section 7.1, used for both concrete classifier xi and abstract classifier xi sharp.
  • domain assumption Input environments are restricted to computable reals with fixed precision
    Section 7.3, introduced to make the verification problem decidable.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Formal Verification of Variational Quantum Circuits." pith.science (2026). https://pith.science/paper/PEKH3MOH

@misc{pith2026250710635,
  author       = {Pith},
  title        = {Pith review of: Formal Verification of Variational Quantum Circuits},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/PEKH3MOH}},
  note         = {Machine review of arXiv:2507.10635}
}
read the original abstract

Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms, offering a hybrid quantum-classical framework that, under certain aspects, can be considered similar to classical deep neural networks. A shared aspect is, for instance, their vulnerability to adversarial inputs, small perturbations that can lead to incorrect predictions. While formal verification techniques have been extensively developed for classical models, no comparable framework exists for certifying the robustness of VQCs. Here, we present the first in-depth theoretical and practical study of the formal verification problem for VQCs. Inspired by abstract interpretation methods used in deep learning, we analyze the applicability and limitations of interval-based reachability techniques in the quantum setting. We show that quantum-specific aspects, such as state normalization, introduce inter-variable dependencies that challenge existing approaches. We investigate these issues by introducing a novel semantic framework based on abstract interpretation, where the verification problem for VQCs can be formally defined, and its complexity analyzed. Finally, we demonstrate our approach on standard verification benchmarks.

Figures

Figures reproduced from arXiv: 2507.10635 by the authors.

Figure 1
Figure 1. A simple quantum circuit implementing the unitary operator [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. A Variational Quantum Circuit. The input [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. We represent a complex number as a point with real and imaginary parts on the [PITH_FULL_IMAGE:figures/full_fig_p013_3.png] view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Encoding Gadget E In detail, the input of E corresponds to |𝑋 | qubits initialized to |0⟩. Then for a given an assignment 𝑎 for {𝑥1 → {0, 1}, . . . , 𝑥𝑛 → {0, 1}}, we define a static environment 𝜎𝑎 as: 𝜎𝑎 (𝑥𝑖) ← ( 𝜋 if 𝑎(𝑥𝑖) = 1 0 if 𝑎(𝑥𝑖) = 0 (12) For the output of E,…
Figure 5
Figure 5. Figure 5: Complete reduction of a formula Φ(𝑥1, 𝑥2, 𝑥3) = (𝑥1 ∨ 𝑥2 ∨ 𝑥3) ∧ (¬𝑥1 ∨ 𝑥2 ∨ ¬𝑥3) into a VQC c. Lemma 7.6. Any 3-SAT formula Φ can be reduced into a VQC c and a property Π = {1}, such that Π is satisfiable on c if and only if Φ is satisfiable. Proof. Without loss of ge…
Figure 6
Figure 6. Figure 6: An example of the clipping function (a), and of the refinement based on splitting intervals (b) [PITH_FULL_IMAGE:figures/full_fig_p021_6.png]
Figure 7
Figure 7. Figure 7: The QCL model, used to classify a 4-feature input data. [PITH_FULL_IMAGE:figures/full_fig_p024_7.png]
Figure 9
Figure 9. Figure 9: The PV model, used to classify a 16-feature input data. [PITH_FULL_IMAGE:figures/full_fig_p024_9.png]
Figure 10
Figure 10. Figure 10: Left: Training algorithm for a Variational Quantum Classifier using SGD. Right: Empirical decision [PITH_FULL_IMAGE:figures/full_fig_p025_10.png]
Figure 11
Figure 11. Figure 11: Left: the verification pipeline. Right: robustness verification results. The mean of the maximum [PITH_FULL_IMAGE:figures/full_fig_p025_11.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

76 extracted references · 42 canonical work pages

  1. [1]

    Matthew Amy. 2018. Towards Large-Scale Functional Verification of Universal Quantum Circuits. InProceedings of the 15th International Conference on Quantum Physics and Logic (QPL 2018) (EPTCS, Vol. 287) . https://doi.org/10.4204/ EPTCS.287.1

    work page 2018

  2. [2]

    Matthew Amy. 2019. Formal Methods in Quantum Circuit Design . Ph. D. Dissertation

    work page 2019

  3. [3]

    Matthew Amy and Joseph Lunderville. 2025. Linear and Non-linear Relational Analyses for Quantum Program Optimization. Proceedings of the ACM on Programming Languages 9, POPL (Jan. 2025), 1072–1103. https://doi.org/10. 28 Nicola Assolini, Luca Marzari, Isabella Mastroeni, and Alessandra Di Pierro 1145/3704873

    work page 2025

  4. [4]

    Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni. 2024. Abstracting Entanglement. In Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains, NSAD 2024, Pasadena, CA, USA, 22 October 2024, Vincenzo Arceri and Michele Pasqua (Eds.). ACM, 34–41. https://doi.org/10.1145/3689609.3689998

    arXiv 2024

  5. [5]

    Nicola Assolini, Alessandra Di Pierro, and Isabella Mastroeni. 2025. A Static Analysis of Entanglement. In Verification, Model Checking, and Abstract Interpretation - 26th International Conference, VMCAI 2025, Denver, CO, USA, January 20-21, 2025, Proceedings, Part II (Lecture Notes in Computer Science, Vol. 15530) , Shankaranarayanan Krishna, Sriram Sank...

    work page doi:10.1007/978-3-031-82703-7_3 2025

  6. [6]

    Bennett, Richard Cleve, David P

    Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. 1995. Elementary gates for quantum computation. Phys. Rev. A 52 (Nov 1995), 3457–3467. Issue 5. https://doi.org/10.1103/PhysRevA.52.3457

    doi:10.1103/physreva.52.3457 1995

  7. [7]

    Izaac, Maria Schuld, Christian Gogolin, and Nathan Killoran

    Ville Bergholm, Josh A. Izaac, Maria Schuld, Christian Gogolin, and Nathan Killoran. 2018. PennyLane: Automatic differentiation of hybrid quantum-classical computations. CoRR abs/1811.04968 (2018). arXiv:1811.04968 http: //arxiv.org/abs/1811.04968

    arXiv 2018

  8. [8]

    Jacob Biamonte, Peter Wittek, Nicola Pancotti, Patrick Rebentrost, Nathan Wiebe, and Seth Lloyd. 2017. Quantum machine learning. Nature 549, 7671 (2017), 195–202

    2017

Show all 76 references
  1. [9]

    Benjamin Bichsel, Anouk Paradis, Maximilian Baader, and Martin T. Vechev. 2023. Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation. Quantum 7 (2023), 1185. https://doi.org/10.22331/Q-2023-11-20-1185

    2023 doi

  2. [10]

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. Proceedings - Symposium on Logic in Computer Science 2021-June (2021). https://doi.org/10.1109/ LICS52264.2021.9470608

    2021

  3. [11]

    Roberto Bruni, Roberto Giacobazzi, Roberta Gori, and Francesco Ranzato. 2023. A Correctness and Incorrectness Program Logic. J. ACM 70, 2, Article 15 (March 2023), 45 pages. https://doi.org/10.1145/3582267

    2023 doi

  4. [12]

    Rudy Bunel, Jingyue Lu, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. 2020. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research 21, 42 (2020), 1–39

    2020

  5. [13]

    Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. 2018. A unified view of piecewise linear neural network verification. Advances in Neural Information Processing Systems 31 (2018)

    2018

  6. [14]

    Marco Cerezo, Andrew Arrasmith, Ryan Babbush, Simon C Benjamin, Suguru Endo, Keisuke Fujii, Jarrod R McClean, Kosuke Mitarai, Xiao Yuan, Lukasz Cincio, et al. 2021. Variational quantum algorithms. Nature Reviews Physics 3, 9 (2021), 625–644

    2021

  7. [15]

    Clément Chareton, Sébastien Bardin, François Bobot, Vincent Perrelle, and Benoît Valiron. 2021. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. In Programming Languages and Systems. ESOP 2021 (Lecture Notes in Computer Science, Vol. 12648) ...

    2021 doi

  8. [16]

    Yanbin Chen and Yannick Stade. 2023. Quantum Constant Propagation. InStatic Analysis - 30th International Symposium, SAS 2023, Cascais, Portugal, October 22-24, 2023, Proceedings (Lecture Notes in Computer Science, Vol. 14284) , Manuel V. Hermenegildo and José F. Morales (Eds....

    2023 doi

  9. [17]

    Bob Coecke and Ross Duncan. 2009. Interacting Quantum Observables: Categorical Algebra and Diagrammatics. CoRR abs/0906.4725 (2009). arXiv:0906.4725 http://arxiv.org/abs/0906.4725

    2009 arXiv

  10. [18]

    Patrick Cousot. 2021. Dynamic interval analysis by abstract interpretation. Formal Methods in Outer Space 13065 (2021), 61–86. https://doi.org/10.1007/978-3-030-87348-6_4 Series Title: Lecture Notes in Computer Science

    2021 doi

  11. [19]

    Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Los Angeles, Ca...

    1977

  12. [20]

    Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (San Antonio, Texas) (POPL ’79). Association for Computing Machinery, New York, NY, USA, 269–...

    1979

  13. [21]

    Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival

  14. [22]

    Evandro Chagas Ribeiro Da Rosa and Rafael De Santiago. 2021. Ket Quantum Programming.J. Emerg. Technol. Comput. Syst. 18, 1, Article 12 (Oct. 2021), 25 pages. https://doi.org/10.1145/3474224

    2021 doi

  15. [23]

    Pierre-Luc Dallaire-Demers and Nathan Killoran. 2018. Quantum generative adversarial networks. Phys. Rev. A 98 (Jul 2018), 012324. Issue 1. https://doi.org/10.1103/PhysRevA.98.012324 Formal Verification of Variational Quantum Circuits 29

    2018 doi

  16. [24]

    Sumanth Dathathri, Sicun Gao, and Richard M Murray. 2019. Inverse abstraction of neural networks using symbolic interpolation. In Proceedings of the AAAI Conference on Artificial Intelligence , Vol. 33. 3437–3444

    2019

  17. [25]

    Suguru Endo, Zhenyu Cai, Simon C Benjamin, and Xiao Yuan. 2021. Hybrid quantum-classical algorithms and quantum error mitigation. Journal of the Physical Society of Japan 90, 3 (2021), 032001

    2021

  18. [26]

    Yuan Feng and Sanjiang Li. 2023. Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. Information and Computation 294 (2023), 105077. https://doi.org/10.1016/j.ic.2023.105077

    2023

  19. [27]

    Jérôme Feret. 2004. Static Analysis of Digital Filters. InProgramming Languages and Systems, 13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, ...

    2004 doi

  20. [28]

    Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. 2022. Complete verification via multi-neuron relaxation guided branch-and-bound. ICRL (2022)

    2022

  21. [29]

    Irene Gargantini and Peter Henrici. 1971. Circular arithmetic and the determination of polynomial zeros. Numer. Math. 18 (1971), 305–320

    1971

  22. [30]

    Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. 2018. AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 ...

    2018

  23. [31]

    Roberto Giacobazzi, Isabella Mastroeni, and Elia Perantoni. 2024. Adversities in Abstract Interpretation - Ac- commodating Robustness by Abstract Interpretation. ACM Trans. Program. Lang. Syst. 46, 2 (2024), 5. https: //doi.org/10.1145/3649309

    2024 doi

  24. [32]

    Roberto Giacobazzi, Francesco Ranzato, and Francesca Scozzari. 2000. Making abstract interpretations complete. J. ACM 47, 2 (2000), 361–416. https://doi.org/10.1145/333979.333989

    2000

  25. [33]

    Edward Grant, Leonard Wossnig, Mateusz Ostaszewski, and Marcello Benedetti. 2019. An initialization strategy for addressing barren plateaus in parametrized quantum circuits. Quantum 3 (Dec. 2019), 214. https://doi.org/10.22331/q- 2019-12-09-214

    2019 doi

  26. [34]

    Córcoles, Kristan Temme, Aram W

    Vojtech Havlicek, Antonio D. Córcoles, Kristan Temme, Aram W. Harrow, Abhinav Kandala, Jerry M. Chow, and Jay M. Gambetta. 2019. Supervised learning with quantum enhanced feature spaces. Nature 567, 7747 (March 2019), 209–212. https://doi.org/10.1038/s41586-019-0980-2 arXiv:18...

    2019 arXiv

  27. [35]

    Kentaro Honda. 2015. Analysis of quantum entanglement in quantum programs using stabilizer formalism. arXiv preprint arXiv:1511.01572 (2015)

    2015 arXiv

  28. [36]

    Po-Wei Huang and Patrick Rebentrost. 2024. Post-variational quantum neural networks. arXiv:2307.10560 [quant-ph] https://arxiv.org/abs/2307.10560

    2024 arXiv

  29. [37]

    A. Yu. Kitaev, A. H. Shen, and M. N. Vyalyi. 2002. Classical and Quantum Computation . American Mathematical Society

    2002

  30. [38]

    Suhas Kotha, Christopher Brix, J Zico Kolter, Krishnamurthy Dvijotham, and Huan Zhang. 2023. Provably bounding neural network preimages. Advances in Neural Information Processing Systems 36 (2023), 80270–80290

    2023

  31. [39]

    Yann LeCun, Corinna Cortes, and CJ Burges. 2010. MNIST handwritten digit database. (2010). http://yann.lecun.com/ exdb/mnist

    2010

  32. [40]

    Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, Mykel J Kochenderfer, et al. 2021. Algorithms for verifying deep neural networks. Foundations and Trends® in Optimization 4, 3-4 (2021), 244–404

    2021

  33. [41]

    Sirui Lu, Lu-Ming Duan, and Dong-Ling Deng. 2020. Quantum adversarial machine learning. Physical Review Research 2, 3 (2020), 033212

    2020

  34. [42]

    Luca Marzari, Davide Corsi, Ferdinando Cicalese, and Alessandro Farinelli. 2023. The #DNN-Verification problem: Counting Unsafe Inputs for Deep Neural Networks. In International Joint Conference on Artificial Intelligence (IJCAI) . 217–224

    2023

  35. [43]

    Luca Marzari, Davide Corsi, Enrico Marchesini, Alessandro Farinelli, and Ferdinando Cicalese. 2024. Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees. In Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Con...

    2024

  36. [44]

    Luca Marzari, Isabella Mastroeni, and Alessandro Farinelli. 2025. Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation. In ECAI 2025. IOS Press

    2025

  37. [45]

    Isabella Mastroeni. 2024. Abstract domain adequacy. Int. J. Softw. Tools Technol. Transf. 26, 6 (2024), 747–765. https://doi.org/10.1007/S10009-024-00774-X 30 Nicola Assolini, Luca Marzari, Isabella Mastroeni, and Alessandra Di Pierro

    2024 doi

  38. [46]

    Isabella Mastroeni. 2025. Abstract Local Completeness. In Verification, Model Checking, and Abstract Interpretation , Krishna Shankaranarayanan, Sriram Sankaranarayanan, and Ashutosh Trivedi (Eds.). Springer, 3–25

    2025

  39. [47]

    Andrea Matic, Maureen Monnet, Jeanette Miriam Lorenz, Balthasar Schachtner, and Thomas Messerer. 2022. Quantum- classical convolutional neural networks in radiological image classification. In 2022 IEEE International Conference on Quantum Computing and Engineering (QCE) . 56–6...

    2022

  40. [48]

    Denny Mattern, Darya Martyniuk, Henri Willems, Fabian Bergmann, and Adrian Paschke. 2021. Variational quanvolu- tional neural networks with enhanced image encoding. arXiv preprint arXiv:2106.07327 (2021)

    2021 arXiv

  41. [49]

    Marvin L. Minsky. 1967. Computation: finite and infinite machines . Englewood Cliffs, N.J. : Prentice-Hall

    1967

  42. [50]

    Mitarai, M

    K. Mitarai, M. Negoro, M. Kitagawa, and K. Fujii. 2018. Quantum circuit learning. Phys. Rev. A 98 (Sep 2018), 032309. Issue 3. https://doi.org/10.1103/PhysRevA.98.032309

    2018 doi

  43. [51]

    Moore, R

    Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud. 2009. Introduction to Interval Analysis. Society for Industrial and Applied Mathematics. https://doi.org/10.1137/1.9780898717716

    2009 doi

  44. [52]

    Mikko Mottonen, Juha J Vartiainen, Ville Bergholm, and Martti M Salomaa. 2004. Transformation of quantum states using uniformly controlled rotations. arXiv preprint quant-ph/0407010 (2004)

    2004 arXiv

  45. [53]

    Nidhi Munikote. 2024. Comparing Quantum Encoding Techniques. arXiv:2410.09121 [quant-ph] https://arxiv.org/ abs/2410.09121

    2024 arXiv

  46. [54]

    Nielsen and Isaac L

    Michael A. Nielsen and Isaac L. Chuang. 2010. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press

    2010

  47. [55]

    Pedregosa, G

    F. Pedregosa, G. Varoquaux, A. Gramfort, V. Michel, B. Thirion, O. Grisel, M. Blondel, P. Prettenhofer, R. Weiss, V. Dubourg, J. Vanderplas, A. Passos, D. Cournapeau, M. Brucher, M. Perrot, and E. Duchesnay. 2011. Scikit-learn: Machine Learning in Python. Journal of Machine Le...

    2011

  48. [56]

    Simon Perdrix. 2008. Quantum Entanglement Analysis Based on Abstract Interpretation. In Static Analysis, 15th International Symposium, SAS 2008, Valencia, Spain, July 16-18, 2008. Proceedings (Lecture Notes in Computer Science, Vol. 5079), María Alpuente and Germán Vidal (Eds....

    2008 doi

  49. [57]

    Luca Pulina and Armando Tacchella. 2010. An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In Computer Aided Verification (Lecture Notes in Computer Science, Vol. 6174) , Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heide...

    2010 doi

  50. [58]

    Rath and H

    M. Rath and H. Date. 2024. Quantum data encoding: a comparative analysis of classical-to-quantum mapping techniques and their impact on machine learning accuracy. EPJ Quantum Technology 11 (2024), 72. https://doi.org/10.1140/epjqt/ s40507-024-00285-3

    2024 doi

  51. [59]

    Quantum Mechanics and Path Integrals,

    P Richard. 1965. Feynman AR Hibbs, “. Quantum Mechanics and Path Integrals, ” ISBN-10 70206503 (1965)

    1965

  52. [60]

    Svore, and Nathan Wiebe

    Maria Schuld, Alex Bocharov, Krysta M. Svore, and Nathan Wiebe. 2020. Circuit-centric quantum classifiers. Phys. Rev. A 101 (Mar 2020), 032308. Issue 3. https://doi.org/10.1103/PhysRevA.101.032308

    2020 doi

  53. [61]

    Maria Schuld, Ilya Sinayskiy, and Francesco Petruccione. 2015. An introduction to quantum machine learning. Contemporary Physics 56, 2 (2015), 172–185

    2015

  54. [62]

    Maria Schuld, Ryan Sweke, and Johannes Jakob Meyer. 2021. Effect of data encoding on the expressive power of variational quantum-machine-learning models. Phys. Rev. A 103 (Mar 2021), 032430. Issue 3. https://doi.org/10.1103/ PhysRevA.103.032430

    2021

  55. [63]

    Jinjing Shi, Zimeng Xiao, Heyuan Shi, Yu Jiang, and Xuelong Li. 2025. QuanTest: Entanglement-Guided Testing of Quantum Neural Network Systems. ACM Trans. Softw. Eng. Methodol. 34, 2, Article 48 (Jan. 2025), 32 pages. https://doi.org/10.1145/3688840

    2025 doi

  56. [64]

    Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. 2019. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3, POPL (2019), 1–30

    2019

  57. [65]

    Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus

  58. [66]

    John van de Wetering. 2020. ZX-calculus for the working quantum computer scientist. arXiv:2012.13966 [quant-ph] https://arxiv.org/abs/2012.13966

    2020 arXiv

  59. [67]

    Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18) . 1599–1614

    2018

  60. [68]

    Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. 2021. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems 34 (2021), 29909–29921

    2021

  61. [69]

    Tianhao Wei, Hanjiang Hu, Luca Marzari, Kai S Yun, Peizhi Niu, Xusheng Luo, and Changliu Liu. 2025. Modelverification. jl: a comprehensive toolbox for formally verifying deep neural networks. In Proceedings of the 37th International Conference on Computer Aided Verification . ...

    2025

  62. [70]

    Maximilian Wendlinger, Kilian Tscharke, and Pascal Debus. 2024. A comparative analysis of adversarial robustness for quantum and classical machine learning models. In 2024 IEEE International Conference on Quantum Computing and Engineering (QCE), Vol. 1. IEEE, 1447–1457

    2024

  63. [71]

    Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2020. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824 (2020)

    2020 arXiv

  64. [72]

    Nengkun Yu and Jens Palsberg. 2021. Quantum abstract interpretation. In Proceedings of the 42nd ACM SIGPLAN Inter- national Conference on Programming Language Design and Implementation (Virtual, Canada) (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 542–5...

    2021

  65. [73]

    Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. 2018. Efficient neural network robustness certification with general activation functions. Advances in neural information processing systems 31 (2018)

    2018

  66. [74]

    Xiyue Zhang, Benjie Wang, and Marta Kwiatkowska. 2024. Provable preimage under-approximation for neural networks. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Springer, 3–23

    2024

  67. [2006]

    In Advances in Computer Science - ASIAN 2006

    Combination of Abstractions in the ASTRÉE Static Analyzer. In Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Revised Selected Papers (Lecture Notes in Computer Science, V...

    2006 doi

  68. [2013]

    arXiv preprint arXiv:1312.6199 (2013)

    Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)

    2013 arXiv

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.