1. Bibliographic Information

1.1. Title

MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification

1.2. Authors

• Siwei Tan (Zhejiang University, Hangzhou, China)

• Dabin Xiang (Zhejiang University, Hangzhou, China)

• Liqiang Lu (Zhejiang University, Hangzhou, China)

• Junlin Lu (Peking University, Beijing, China)

• Qiuping Jiang (Ningbo University, Ningbo, China)

• Mingshuai Chen (Zhejiang University, Hangzhou, China)

• Jianwei Yin (Zhejiang University, Hangzhou, China)

  Note: Siwei Tan and Dabin Xiang contributed equally to this work. Liqiang Lu and Jianwei Yin are corresponding authors.

1.3. Journal/Conference

Published at ASPLOS '24, the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 3. ASPLOS is a highly reputable and influential conference in the fields of computer architecture, programming languages, and operating systems, indicating that the paper has undergone a rigorous peer-review process and presents significant contributions to these areas, particularly at the intersection with quantum computing.

1.4. Publication Year

2024

1.5. Abstract

Quantum Program Verification (QPV) presents significant challenges compared to classical computing due to inherent quantum properties like non-duplicability and state collapse upon measurement. Existing QPV methods, such as deductive verification, often lack scalability, while assertion-based approaches frequently require exhaustive assertions or offer low confidence in verifying correctness across all inputs.

This paper introduces MorphQPV, a novel, confident assertion-based verification methodology. The core innovation of MorphQPV lies in leveraging the concept of isomorphism in quantum programs. This implies a structure-preserving relation between the runtime states of a program. The methodology introduces a tracepoint pragma within assertion statements to label specific quantum states for verification and an assume-guarantee primitive to define the expected relationships between these states. To efficiently characterize the ground-truth relations between states, MorphQPV employs an isomorphism-based approximation technique. This approach effectively determines program states under various inputs without requiring repeated program executions. Finally, the verification process is framed as a constraint optimization problem, complemented by a confidence estimation model for rigorous analysis.

Experimental results demonstrate that MorphQPV significantly reduces the number of program executions by up to $107.9 \times$ when verifying a 27-qubit quantum lock algorithm. Furthermore, it improves the probability of success in debugging by $3.3 \times$ to $9.9 \times$ across five different benchmark quantum algorithms.

1.6. Original Source Link

Official Source: https://doi.org/10.1145/3620666.3651360 PDF Link: /files/papers/6936b57f3183ab0eea09e020/paper.pdf Publication Status: Officially published.

2. Executive Summary

2.1. Background & Motivation

The core problem the paper aims to solve is the significant challenge of Quantum Program Verification (QPV). Unlike classical programs, quantum programs operate on quantum states which possess unique properties such as superposition (a qubit can be in multiple states simultaneously), entanglement (qubits' states are correlated), and non-duplicability (the no-cloning theorem prevents perfect copying of an arbitrary unknown quantum state), and state collapse upon measurement. These properties make debugging and verifying quantum programs extremely difficult.

This problem is critically important in the current field because quantum computing is a promising technology with the potential for revolutionary speedups and low power consumption. As quantum programs become more complex, the inevitable presence of computational defects (bugs) necessitates advanced verification tools. The current low resolution rate of quantum program-related questions on platforms like Stack Overflow (21% compared to classical programs) highlights a significant gap in effective debugging and verification tools.

Prior approaches to QPV face several challenges:

• Deductive Verification: Relies on precise mathematical formulations and human expertise to identify inductive invariants (properties that hold true at specific points in a program's execution). This leads to poor scalability due to significant computational costs for discharging verification conditions (mathematical proofs of correctness) on classical computers.
• Runtime Assertion: A more lightweight method that tests programs with varying inputs. However, existing assertion methods suffer from:

  • Low Confidence: They can only validate assertions for a small subset of test inputs and lack the ability to generalize validation results to the entire input space.

  • Exhaustive Assertions: Some require testing numerous inputs exhaustively to achieve higher confidence, which becomes infeasible in the continuous Hilbert space of quantum states. For example, testing a 20-qubit QRAM program required $4.8 \times 10^6$ executions with prior methods.

  • Input-Dependent Verification: Current methods cannot characterize relations between states in an input-independent manner, leading to repetitive testing for each input.

  • Limited State Probing: Due to quantum collapse after measurement, they can only probe limited features of the state (e.g., purity, amplitudes), not the entire density matrix or complex relations between states.

    The paper's entry point or innovative idea is to leverage the isomorphism property inherent in quantum programs. Isomorphism implies a structure-preserving relation between the input and runtime states of a program. This insight allows MorphQPV to characterize program behavior under specific inputs and then infer behavior under alternative inputs, thereby extending verification results to the entire input space and achieving confident verification with a minimal number of program executions.

2.2. Main Contributions / Findings

The paper makes several primary contributions to the field of quantum program verification:

1. Multi-State Assertion for Enhanced Verification: MorphQPV introduces a novel multi-state assertion mechanism. This assertion type is designed to characterize relationships among a sequence of quantum states at different tracepoints (specific points in time) within a program. This significantly enhances both the efficiency and expressiveness of program verification by allowing complex, input-independent descriptions of program behavior, including relations between states at different times, which was a limitation of prior single-state assertions.

2. Isomorphism-Based Approximation for Runtime State Calculation: The paper proposes an innovative isomorphism-based approximation technique to calculate runtime quantum states. Instead of repeatedly executing the quantum program for each input, this method approximates the density matrix (mathematical description) of program states based on the input. This approximation effectively captures program behavior at a significantly lower computational cost, enabling input-independent characterization. The accuracy of this approximation is rigorously guaranteed by mathematical proof (Theorem 1 and 2).

3. Input-Independent Validation with Confidence Estimation: MorphQPV formulates the assertion validation as a constraint optimization problem. This approach allows for input-independent validation of assertions, capable of identifying counter-examples when bugs are present. Crucially, it integrates a confidence estimation model that analytically predicts the probability that the verification result holds true for all inputs. This provides a rigorous analytical framework for verifying program correctness.

   The key conclusions and findings are:

• Significant Reduction in Program Executions: Experiments demonstrate that MorphQPV drastically reduces the number of required program executions. For instance, it achieves a $107.9 \times$ reduction when verifying a 27-qubit quantum lock algorithm compared to baseline methods. For QRAM, it showed a $31,563.2 \times$ reduction in sampling inputs.

• Improved Debugging Success Probability: When debugging five benchmark algorithms, MorphQPV improves the probability of success by $3.3 \times$ to $9.9 \times$, consistently achieving a 100% success rate in identifying bugs, even for programs where other methods failed (e.g., 0% success rate for 9-qubit QL with NDD).

• Enhanced Expressiveness and Interpretability: MorphQPV provides full expressiveness for comparing mixed states and their evolution, supporting complex comparisons (e.g., greater than, less than) and comparisons between states at different times. It also offers counter-examples and intermediate state density matrices for better debugging insights, along with confidence estimation.

• Reduced Overhead: By minimizing actual quantum program executions and leveraging classical computation for approximation, MorphQPV achieves significant overhead optimization (e.g., from $2.8 \times 10^{10}$ to 488.0 operations for a 9-qubit Shor algorithm compared to NDD).

  These findings collectively address the challenges of scalability, confidence, and exhaustiveness in QPV, offering a robust and efficient methodology for ensuring the correctness of quantum programs.

3. Prerequisite Knowledge & Related Work

3.1. Foundational Concepts

To understand MorphQPV, a basic grasp of quantum computing fundamentals and program verification concepts is essential.

3.1.1. Qubits and Quantum States

In classical computing, information is stored in bits, which can be either 0 or 1. In quantum computing, information is stored in qubits. A qubit can represent 0, 1, or a superposition of both 0 and 1 simultaneously. This means it can be in a state like $α|0\rangle + β|1\rangle$, where $α$ and $β$ are complex probability amplitudes, and $|α|^2 + |β|^2 = 1$. The symbols $|0\rangle$ and $|1\rangle$ are standard notations for the basis states (computational basis).

3.1.2. Density Matrix ($\rho$)

The density matrix is a mathematical representation of a quantum state, especially useful for describing mixed states (probabilistic mixtures of pure states) and pure states (a single, well-defined quantum state).

• Pure State: A state that can be described by a single ket vector $|\psi\rangle$. Its density matrix is $\rho = |\psi\rangle\langle\psi|$, where $\langle\psi|$ is the bra vector (conjugate transpose of $|\psi\rangle$). For a pure state, $\rho^2 = \rho$ (idempotent) and its trace (sum of diagonal elements) is 1. The purity of a state is given by $Tr(\rho^2)$. For a pure state, $Tr(\rho^2) = 1$.
• Mixed State: A statistical ensemble of pure states. Its density matrix is a weighted sum of pure state density matrices: $\rho = \sum_i p_i |\psi_i\rangle\langle\psi_i|$, where $p_i$ is the probability of being in state $|\psi_i\rangle$, and $\sum_i p_i = 1$. For a mixed state, $Tr(\rho^2) < 1$. The density matrix is powerful because it allows a complete description of all properties of a quantum state.

3.1.3. Quantum Operations (Unitary Evolution)

The evolution of a quantum state over time or through quantum gates is described by a unitary operator (or unitary matrix) $U$. A unitary operator preserves the norm of quantum states and is reversible ($U^{-1} = U^\dagger$, where $\dagger$ denotes the conjugate transpose). If a quantum state is initially $\rho$, after applying a unitary $U$, it evolves to a new state $\rho'$: $ \rho' = U \rho U^\dagger \quad (1) $ Here, $U^\dagger$ is the conjugate transpose of $U$, meaning it transposes the matrix and then takes the complex conjugate of each element.

3.1.4. Quantum Measurement

Quantum measurement is the process of extracting information from qubits, converting quantum information into classical bits. It's the only way to read a quantum program's output.

• Projective Measurement: A common type of measurement described by a set of measurement operators $\{O_k\}$. These operators satisfy the completeness relation $\sum_k O_k^\dagger O_k = I$, where $I$ is the identity matrix.
• Expectation Value: The expectation value of measuring a quantum state $\rho$ with respect to an operator $O$ is given by: $ \mathbb{E}_O[\rho] = \mathrm{tr}(O\rho) \quad (2) $ where $\mathrm{tr}$ is the trace operator (sum of the diagonal elements of a matrix). This value represents the average outcome if the measurement were performed many times.
• State Collapse: After a measurement, the quantum state collapses to one of the eigenstates corresponding to the measurement outcome. The state $\rho$ evolves to a new state $\rho'$ after measurement with operator $O$: $ \rho' = \frac{O\rho O^\dagger}{\mathbb{E}_O[\rho]} \quad (3) $ This collapse means the original quantum state is generally altered, illustrating the non-duplicability (or no-cloning theorem) principle for unknown quantum states, which is a major hurdle for QPV.

3.1.5. Isomorphism

Mathematically, an isomorphism is a structure-preserving mapping between two mathematical structures of the same type that can be reversed by an inverse mapping. In simpler terms, it's a bijection (one-to-one and onto correspondence) that preserves operations or relations. A linear isomorphism is a type of isomorphism applied to vector spaces, characterized by additivity and homogeneity:

• additivity: $f(u+v) = f(u) + f(v)$
• homogeneity: $f(cu) = c f(u)$ where $c$ is a constant and u, v are elements in the input space of the linear isomorphism $f$. For quantum evolution, unitary operations are reversible, making them isomorphic transformations of quantum states. This property is key to MorphQPV's approximation technique, where $f(\sum_k c_k u_k) = \sum_k c_k f(u_k)$ (Equation 4), meaning the transformation of a linear combination of inputs is the linear combination of the transformed inputs.

3.1.6. Program Assertion

In classical software engineering, an assertion is a predicate (a Boolean-valued function) that expresses a condition that a program developer expects to be true at a specific point in the program's execution. If an assertion evaluates to false, it indicates a bug. MorphQPV extends this concept to quantum programs with tracepoints and assume-guarantee primitives, allowing for statements about the properties of quantum states and their relationships at different times during execution.

3.2. Previous Works

The paper contextualizes MorphQPV by discussing prior approaches to QPV, broadly categorizing them into deductive verification and runtime assertion.

3.2.1. Deductive Verification

This class of methods aims for formal proof of program correctness.

• Quantum Hoare Logic [57]: An extension of classical Hoare logic for quantum programs. It defines pre- and post-conditions for quantum operations, allowing for formal reasoning about program behavior.
• Semantic Models [34]: Uses formal mathematical models to describe the semantics (meaning) of quantum programs, enabling rigorous analysis.
• Verification Conditions: Deductive verification typically compiles correctness into a set of mathematical verification conditions that need to be discharged (proven true) by classical computers.
• Limitations:
  • Scalability: Discharging verification conditions incurs significant computational costs, making it poorly scalable for larger quantum programs.
  • Human Expertise: Often requires human expertise to identify suitable inductive invariants, limiting automation.
  • Verified Objects: As per Table 5, methods like KNA [34] and QHL [57] primarily verify expectation values, while Twist [55] focuses on purity. These are limited in scope compared to MorphQPV's ability to verify mixed states & evolution.

3.2.2. Runtime Assertion

These are lightweight methods that test programs under varying inputs and check conditions at runtime.

• Assertion Predicates: Assertions are defined as predicates about program state properties (e.g., purity [55], expectation [27, 28], amplitudes [20]).
• Validation Steps: Involve (a) stating the assertion, (b) characterizing the program (often by executing it), and (c) validating if the characterization satisfies the predicate.
• Case-by-Case Studies: Early applications were often tailored to specific cases [20].
• Dynamic Assertions on Hardware [27, 28]: Extended assertions to quantum hardware, enabling dynamic checks.
• Methods and their Limitations:
  • Stat [20]: Statistical assertions for validating patterns and finding bugs. Checks probability distributions. Limited interpretability.
  • Proj [27]: Projection-based measurement for runtime assertions. Checks if the state is in a specified state set. Limited to equal or in comparisons; cannot compare states at different times.
  • NDD [28, 29]: Non-destructive discrimination for systematic and precise/approximate assertions. Similar to Proj, limited to equal or in comparisons for mixed states. Shows poor confidence for programs with few counter-examples.
  • SR [13]: Symbolic reasoning for verification of nondeterministic quantum programs. Can verify mixed state and evolution. One of the few prior works capable of verifying nondeterministic programs and feedback circuits.
  • Quito [47]: A coverage-guided test generator for quantum programs, employing grid search on the input space. Suffers from exhaustive testing requirements, leading to massive program executions (e.g., $4.8 \times 10^6$ for QRAM), and often has low success rates for identifying phase errors as it only validates probability distributions.
  • Fuzz [46]: Fuzz testing for quantum programs, similar to classical fuzzing, searching for bugs through random inputs.
• Confidence Issues: A major limitation across existing runtime assertion works is low confidence in verifying overall program correctness for all inputs, as they typically only validate assertions for a small subset of test inputs. They lack mechanisms to generalize validation results to the entire input space.
• Gleipnir [39]: A framework for input-aware error analysis using tensor networks for approximation. MorphQPV distinguishes itself by eliminating simulation for each input.
• OSCAR [18]: Debugs variational quantum algorithms by constructing loss function landscapes in parameter space. MorphQPV constructs landscapes in the input space.

3.3. Technological Evolution

The evolution of program verification from classical to quantum computing highlights a shift from deterministic, clonable states to probabilistic, non-clonable, and collapsing states.

• Classical Program Verification: Established methods include formal methods (e.g., Hoare logic, model checking) for formal proofs and dynamic methods (e.g., testing, assertions) for runtime checks. These rely on the ability to inspect memory, duplicate states, and deterministically re-execute programs.
• Early Quantum Program Verification: Initially, attempts focused on adapting classical formal methods (like Hoare logic) to the quantum domain. While theoretically sound, these often faced practical limitations due to the computational complexity of quantum state spaces and the difficulty of formalizing quantum phenomena.
• Runtime Approaches for Quantum: Recognizing the simulation costs, researchers developed runtime assertion techniques, often aiming to verify specific properties (purity, amplitudes, expectation values) using quantum hardware or simulators. However, they struggled with the input generalization problem and confidence due to measurement-induced state collapse and the vastness of the quantum state space.
• MorphQPV's Place: MorphQPV represents an advancement by addressing the input generalization problem and confidence directly. It bridges the gap between the rigor of formal methods and the practicality of runtime assertions by introducing isomorphism as a key insight. This allows for a more comprehensive characterization of program behavior without exhaustive execution, marking a significant step towards more scalable and confident QPV.

3.4. Differentiation Analysis

Compared to the main methods in related work, MorphQPV offers several core differences and innovations:

• Input-Independent Verification:

  • Prior Works: Many (e.g., Proj [27], NDD [29], Quito [47]) require testing programs for each input or an exhaustive grid search, which is highly inefficient for the continuous Hilbert space. Bugs might only activate under specific, rarely tested inputs.
  • MorphQPV: Leverages isomorphism to build approximation functions that characterize the relation between inputs and runtime states for any input, based on a limited number of samples. This enables input-independent validation.

• Expressiveness of Assertions:

  • Prior Works: Assertions are often limited to single program states (e.g., Stat [20] for probability distribution, Twist [55] for purity, Proj [27] and NDD [29] for being in a specified state set). They struggle to check complex relations between states at different time points or complex inequalities.
  • MorphQPV: Introduces multi-state assertions with an assume-guarantee primitive that can specify complex relations between multiple states (density matrices) at different times. It can define predicates as classical functions involving the density matrix, allowing for full comparisons (equal, in, greater than, less than) and checking mixed states and evolution.

• Characterization of States:

  • Prior Works: Can only probe limited features of states due to quantum collapse (e.g., amplitudes in Stat [20], purity in Twist [55]). Obtaining full density matrices often requires expensive state tomography for each input.
  • MorphQPV: Its isomorphism-based approximation generates classical functions that approximate the density matrix of tracepoint states for any input. This effectively bypasses repeated full state tomography for every input.

• Confidence Estimation:

  • Prior Works: Exhibit low confidence in verifying overall program correctness because they cannot generalize results from tested inputs to the entire input space. Some (like Quito [47]) attempt exhaustive testing, but this is impractical. Most lack an analytical framework for confidence.
  • MorphQPV: Formulates verification as a constraint optimization problem and integrates a confidence estimation model (based on Beta distribution for approximation accuracy). This provides a rigorous, quantitative measure of how likely the verification result holds true for all inputs.

• Overhead and Scalability:

  • Prior Works: Methods like Quito [47] and NDD [29] (which requires synthesizing unitary gates) can incur astronomical overhead (e.g., $2.8 \times 10^{10}$ operations for 9-qubit Shor with NDD). Deductive methods also face scalability issues with increasing qubit count.
  • MorphQPV: Significantly reduces quantum program executions by using classical approximation. Its complexity is primarily determined by the number of input qubits rather than the overall program qubits, and approximation functions have linear complexity. This leads to substantial reductions in overhead (e.g., down to 488.0 operations for 9-qubit Shor) and improved scalability.

• Interpretability and Counter-Examples:

  • Prior Works: Some (e.g., Proj [27], NDD [29]) provide little to no information when an assertion fails. Stat [20] only outputs probability distribution.

  • MorphQPV: When a bug is found, it directly outputs the counter-example (the problematic input) and can provide the density matrix of program intermediate states, significantly enhancing debuggability and interpretability.

    In essence, MorphQPV innovates by providing a mathematically grounded, efficient, and confident way to verify quantum programs by intelligently leveraging the structural properties of quantum mechanics, moving beyond the limitations of purely empirical or exhaustively formal approaches.

4. Methodology

4.1. Principles

The core idea of MorphQPV is to leverage the inherent isomorphism property of quantum programs. This property implies a structure-preserving relationship between the program's input and its runtime quantum states. Because quantum operations (like unitary gates) are reversible and linear, they can be considered isomorphic transformations. This linearity allows MorphQPV to approximate the behavior of the program under any input by linearly combining the observed behaviors under a carefully selected set of sampled inputs.

The theoretical basis is rooted in the linearity of quantum mechanics. If a quantum program (or a segment of it between an input and a tracepoint) behaves as a linear operator (which unitary evolutions and measurements, when properly handled, do), then the output state for a linear combination of input states will be the same linear combination of the output states for the individual input states. This allows MorphQPV to "characterize" the program's behavior once and then "infer" the runtime states for new, unseen inputs without actually executing the quantum program repeatedly. This principle effectively transforms a computationally expensive quantum problem (repeated executions and tomography) into a more tractable classical problem (linear combination and optimization).

4.2. Core Methodology In-depth (Layer by Layer)

MorphQPV's verification workflow consists of three main steps: assertion statement, program characterization, and assertion validation.

4.2.1. Step 1: Assertion Statement

This step involves defining the expected behavior of the quantum program. MorphQPV extends classical assertion concepts to the quantum domain using tracepoints and an assume-guarantee primitive.

4.2.1.1. Tracepoint Pragma

To specify the exact quantum states to be verified, MorphQPV introduces a tracepoint pragma. A tracepoint acts as a label for a specific set of qubits at a particular time in the program's execution. A tracepointT_i is formally defined as: $ T_i \equiv (\{Q_i\}, time_i), Q_i \in Q \quad (5) $ Here: * $Q_i$: Represents the specific `qubit set` (a subset of all qubits $Q$ in the quantum program) whose state is being observed. * $time_i$: Denotes the `time` (e.g., instruction line number) at which the `density matrix` $\rho_{T_i}$ of the qubits $Q_i$ is to be captured or analyzed. Tracepoints are declared in a `QASM` (Quantum Assembly Language) program using a specific syntax. For example, `T index q[qubits]` could be a pragma. The paper provides an example for a `GHZ (Greenberger–Horne–Zeilinger) circuit`: ``` 1 h q[1]; 2 cx q[1], q[2]; 3 T 1 q[1,2]; // tracepoint T1 on qubits 1,2. 4 cx q[2], q[3]; ``` In this example, `T 1 q[1,2]` declares `tracepoint`T_1 on qubits q[1] and q[2] at $time=3$ (after the CX gate between q[1] and q[2]).

4.2.1.2. Assume-Guarantee Primitive

Assertions in MorphQPV are defined using an assume-guarantee primitive, inspired by classical parallel program verification. This primitive allows specifying expected relations between states at different tracepoints, not just properties of a single state. An assume-guarantee assertion is defined as: $ assert(T_i,T_j) \equiv assume:P_1(\rho_{T_i}), P_2(\rho_{T_j}), \ \text{guarantee}: P_3(\rho_{T_i},\rho_{T_j}), \quad (6) $ Here:

• assert(T_i, T_j): Declares an assertion involving states at tracepoints $T_i$ and $T_j$.

• assume:P_1(\rho_{T_i}), P_2(\rho_{T_j}): These are `predicates` (conditions) that are assumed to be true for the states $\rho_{T_i}$ and $\rho_{T_j}$. The assertion will only be validated for inputs where these assumptions hold. * `guarantee:`P_3(\rho_{T_i},\rho_{T_j}): This is the predicate that is expected to be true if the assumptions ($P_1, P_2$) are met and the program is correct.

• $P_k$: Each predicate $P_k$ is an inequality or objective function that takes density matrices as inputs. A predicate $P_k$ is considered true if and only if its value satisfies $P_k \le 0$. This formulation allows for flexible mathematical expressions, as density matrices are obtained on a classical computer.

  The advantages of this approach include:

• Input-Independent Description: It's a static statement describing program behavior, not tied to specific inputs.

• Multi-State Relations: Allows checking relations between states at different times, addressing a limitation of prior single-state assertions.

• Pruning Input Space: The assume conditions filter the input space, focusing validation efforts.

• Mid-Measurement and Feedback: Can handle programs with mid-measurement (measurements during execution) and feedback (classical control based on measurement results) by asserting on collapsed states.

4.2.1.3. Example: Quantum Teleportation Assertion

The paper illustrates this with quantum teleportation, which aims to transfer an unknown quantum state from a sender (Alice) to a receiver (Bob). As shown in Image 12.jpg (Figure 3 from the paper), tracepointT_1 labels Alice's input state (qubit $q_{alice}$ at time 1), and `tracepoint`T_2 labels Bob's output state (qubit $q_{bob}$ at time 10). The expected behavior is that if both input and output are pure states, the input state should equal the output state. The assertion is: $ assume: P_1(\rho_{T_1}) = |\rho_{T_1}\rho_{T_1}^\dagger - \rho_{T_1}|, \ \qquad P_2(\rho_{T_2}) = |\rho_{T_2}\rho_{T_2}^\dagger - \rho_{T_2}|, \ \mathrm{guarantee}: P_3(\rho_{T_1},\rho_{T_2}) = |\rho_{T_1} - \rho_{T_2}| $ Here:

• $P_1(\rho_{T_1}) \le 0$ means that the input state $\rho_{T_1}$ is a pure state (since $\|\rho\rho^\dagger - \rho\|$ equals 0 for pure states).

• $P_2(\rho_{T_2}) \le 0$ means that the output state $\rho_{T_2}$ is a pure state.

• $P_3(\rho_{T_1},\rho_{T_2}) \le 0$ means that the input state $\rho_{T_1}$ is equal to the output state $\rho_{T_2}$ (since $\|\rho_A - \rho_B\|$ equals 0 when $\rho_A = \rho_B$).

• $\| \cdot \|$ denotes the L2 norm of the matrix.

  A second example is given for validating phase differences with feedback (when $q_{alice}$ is measured 1), demonstrating the flexibility to check post-measurement conditions.

4.2.2. Step 2: Program Characterization

This step aims to capture the natural relation between the program's input $\rho_{\mathrm{in}}$ and the state $\rho_{T_i}$ at each tracepointT_i. This relation is formulated as an `approximation function`, $\rho_{T_i} = f(\rho_{\mathrm{in}})$, which can then be used to determine tracepoint states on a classical computer without repeated quantum executions. #### 4.2.2.1. Input Sampling The characterization process begins with `input sampling`. 1. **Execution**: The quantum program is run on quantum hardware or a simulator using a diverse set of `sampled inputs`. 2. **Tomography**: For each execution, `quantum state tomography` is applied to the qubits at each `tracepoint` to obtain their `density matrices`. This results in pairs $\langle \sigma_{\mathrm{in},i}, \sigma_{T,i} \rangle$, where $\sigma_{\mathrm{in},i}$ is the $i^{th}$ sampled input and $\sigma_{T,i}$ is the corresponding state at tracepoint $T$. 3. **Input Design**: The sampled inputs are crucial for accuracy. They should be `orthogonal` and cover a wide range of `eigenstates` to maximize variety. The paper utilizes circuits from the `orthogonal Clifford group` [6] to prepare these inputs. The Clifford group is more expressive than basis states for representing `superposition` and `entanglement`. 4. **Number of Samples ($N_{\text{sample}}$)**: The quantity of sampled inputs is determined by the desired `accuracy` of the approximation. #### 4.2.2.2. Isomorphism-based Approximation The core of the characterization lies in exploiting the `isomorphic property` of quantum evolution (as discussed in Section 3.1.5). Since the relationship between $\rho_{\mathrm{in}}$ and $\rho_T$ is linear and `structure-preserving` (due to unitary operations and linear operators in measurement/feedback), `MorphQPV` can build an approximation function. For an input $\rho_{\mathrm{in}}$ that can be expressed as a `linear combination` of the `sampled inputs` $\sigma_{\mathrm{in},i}$: $ \rho_{\mathrm{in}} = \sum_{i}\alpha_{i}\sigma_{\mathrm{in},i}. \quad (8) $ Here: * $\alpha_i$: Real-valued parameters. Mathematically, $\alpha_i$ can be seen as the `expectation` of the input $\rho_{\mathrm{in}}$ on the sampled input $\sigma_{\mathrm{in},i}$ (if $\sigma_{\mathrm{in},i}$ are chosen as measurement operators). More generally, they are coefficients of the linear combination. Then, the corresponding tracepoint state $\rho_T$ under this input can be approximated by the same linear combination of the observed tracepoint states $\sigma_{T,i}$: $ \rho_{\mathrm{T}} = \sum_{i}\alpha_{i}\sigma_{\mathrm{T},i}. \quad (9) $ This is derived from the `additivity` and `homogeneity` properties of the quantum evolution $F$: $ \rho_{\mathrm{T}} = F(\rho_{\mathrm{in}}) = F\left(\sum_{i}\alpha_{\mathrm{i}}\sigma_{\mathrm{in,i}}\right) = \sum_{i}\alpha_{\mathrm{i}}F(\sigma_{\mathrm{in},i}) = \sum_{i}\alpha_{\mathrm{i}}\sigma_{\mathrm{T},i}. $ Where $F(\sigma_{\mathrm{in},i}) = \sigma_{\mathrm{T},i}$ since these pairs are obtained from actual program executions. **Theorem 1 (Approximation function)**: The paper states that the function $\rho_{\mathrm{T}} = f(\rho_{\mathrm{in}})$ is an `under-approximation` of the real relation $F$ between input $\rho_{\mathrm{in}}$ and tracepoint state $\rho_{\mathrm{T}}$. The function is computed in two steps: 1. For input $\rho_{\mathrm{in}}$, it first approximates $\rho_{\mathrm{in}}$ by Equation 8 to obtain parameters $\{\alpha_i\}$. 2. In the second step, the tracepoint state under this input is computed according to Equation 9. This approximation holds even for programs with `non-overlapping qubits` between input and tracepoint, and programs with `mid-measurements` and `simple feedback` (where relations of qubit states are not always strictly isomorphic in the composite sense, but the linear operations still allow for this approximation). The detailed proof for this is provided in Appendix A. Image 5.jpg (Figure 4 from the paper) provides a visual example for a single-qubit program. If three orthogonal input states ($|{+}\rangle\langle{+}|$ on x-axis, $|{+}\rangle\langle{+i}|$ on y-axis, and $|1\rangle\langle 1|$ on z-axis) are sampled, and their corresponding tracepoint states $\sigma_{T,1}, \sigma_{T,2}, \sigma_{T,3}$ are recorded. For any new input $\rho_{\mathrm{in}}$, it's decomposed as $\rho_{\mathrm{in}} = \alpha_{1}|{+}\rangle\langle{+}| + \alpha_{2}|{+}\rangle\langle{+i}| + \alpha_{3}|1\rangle\langle 1|$ (where $\alpha_i$ are expectation values for these bases). Then, $\rho_T$ is computed as $\rho_T = \alpha_1\sigma_{T,1} + \alpha_2\sigma_{T,2} + \alpha_3\sigma_{T,3}$. This approximation significantly reduces the complexity of verification by moving from exponential-complexity quantum simulations/executions to linear-complexity classical computations. #### 4.2.2.3. Approximation Accuracy The `inaccuracy` of this approximation arises when the input state cannot be perfectly decomposed into a linear combination of the sampled inputs. **Theorem 2 (Approximation accuracy)**: For different inputs, there are two cases: 1. For inputs that can be accurately represented by Equation 8, the accuracy is $100\%$. 2. For inputs with eigenstates that cannot be represented by Equation 8, the average accuracy is $N_{\mathrm{sample}} / (2^{N_{\mathrm{in}}+1}) \times 100\%$. Here, `accuracy` is defined as the `Hilbert-Schmidt inner product` between the approximated tracepoint state $\rho_{\mathrm{approx}}$ and the real tracepoint state $\rho_{\mathrm{truth}}$ (obtained by executing the quantum program): $ \mathrm{acc} = tr(\sqrt{\rho_{\mathrm{approx}}\rho_{\mathrm{truth}}})^2 $ The proof of Theorem 2 is in Appendix A. It suggests that increasing $N_{\mathrm{sample}}$ exponentially expands the space of inputs for which the approximation is $100\%$ accurate and linearly increases the accuracy for other inputs. Image 6.jpg (Figure 5 from the paper) shows experimental validation of Theorem 2, where $N_{\mathrm{in}}$ is the number of qubits for the input. It compares experimental accuracy with theoretical values for 7-qubit and 15-qubit quantum teleportation programs. For inputs perfectly represented (Case 1), experimental accuracy is near 100% (with slight deviations due to tomography inaccuracy). For other inputs (Case 2), accuracy grows linearly with $N_{\mathrm{sample}}$, reaching maximum at $N_{\mathrm{sample}} = 2^{N_{\mathrm{in}}+1}$ (16 for $N_{\mathrm{in}}=3$, 64 for $N_{\mathrm{in}}=5$). #### 4.2.2.4. Pruning the Sample Space To improve the efficiency of characterization while maintaining accuracy, `MorphQPV` proposes three strategies for `pruning the sample space`: * **Strategy-adapt (Adaptive Sampling)**: This strategy adaptively determines the inputs for sampling. If the input space is a subspace of the whole quantum state, `eigendecomposition` can be applied. Only eigenvectors with large eigenvalues are used as sampled inputs, reducing $N_{\mathrm{sample}}$. For example, in a quantum neural network, top-eigenvectors from a training dataset can be used. * **Strategy-const (Constant Input Part)**: This strategy involves setting a part of the input state as constant. If a program's input consists of multiple parts, some qubits can be fixed, reducing the effective size of the input space to be sampled. For example, in a quantum adder $f(|x\rangle, |y\rangle) = |x+y\rangle$, keeping $|x\rangle$ constant focuses verification on different states of $|y\rangle$. * **Strategy-prop (Property-Specific Check)**: This strategy involves checking only a specific property of the state (e.g., probability distribution, expectation, purity) rather than the entire density matrix. If the assertion only validates properties that also satisfy additivity and homogeneity, `MorphQPV` can reduce the complexity of tomography by only measuring these specific properties, instead of full state tomography. ### 4.2.3. Step 3: Assertion Validation This final step involves checking whether the `characterized approximation functions` (e.g., $\rho_{T_1} = f_1(\rho_{\mathrm{in}})$) satisfy the predicates of the asserted `assume-guarantee` relation. This is formulated as a `constraint optimization problem`. #### 4.2.3.1. Constraint Optimization For an assertion $\text{assert}(T_1,T_2)$ with predicates $P_1, P_2, P_3$ (where $P_k \le 0$ means the predicate is true), the validation is transformed into the following `constraint optimization problem`: $ \underset{\rho_{T_1},\rho_{T_2}}{\mathrm{maximize}} P_3(\rho_{T_1},\rho_{T_2}), \\ \mathrm{subject~to} P_1(\rho_{T_1})\le 0,\\ P_2(\rho_{T_2})\le 0, \quad (10) $ Here: * `maximize`P_3(\rho_{T_1},\rho_{T_2}): The objective is to find the maximum possible value of the guarantee predicate $P_3$.

• subject toP_1(\rho_{T_1})\le 0, P_2(\rho_{T_2})\le 0: These are the `assume` conditions, ensuring that the optimization only considers input states that satisfy the assumptions. To make this problem solvable on a classical computer, the tracepoint states $\rho_{T_1}$ and $\rho_{T_2}$ are replaced by their `characterized approximation functions` $f_1(\rho_{\mathrm{in}})$ and $f_2(\rho_{\mathrm{in}})$: $ \underset{\rho_{\mathrm{in}}}{\mathrm{maximize}} P_3(f_1(\rho_{\mathrm{in}}),f_2(\rho_{\mathrm{in}})), \\ \mathrm{subject~to} P_1(f_1(\rho_{\mathrm{in}}))\le 0, \\ P_2(f_2(\rho_{\mathrm{in}}))\le 0. $ Since $\rho_{\mathrm{in}}$ is represented by the parameters $\{\alpha_i\}$ in the approximation function (from Equation 8), the optimization directly finds the values of $\{\alpha_i\}$ that maximize $P_3$. The `correctness` of the assertion is determined by the maximum value found: $ \mathrm{assert}(T_1,T_2)\equiv \mathrm{if}\max \{P_3(\{\alpha \})\} \le 0\to \mathrm{true} >0\to \mathrm{false.} $ If the maximum value of $P_3$ is $\le 0$, the assertion holds (true). If it's $> 0$, the assertion fails (false), and the $\rho_{\mathrm{in}}$ that yielded this maximum is the `counter-example` (the input that triggers the bug). Example for Quantum Teleportation (from Section 4, Equation 7): The verification aims to check: $ \begin{array}{rl} & {\underset {\rho_{\mathrm{in}}}{\mathrm{maximize}}\left\| \rho_{\mathrm{in}} - f_2(\rho_{\mathrm{in}})\right\| ,}\\ & {\mathrm{subject~to}\left\| \rho_{\mathrm{in}}\rho_{\mathrm{in}}^{\dagger} - \rho_{\mathrm{in}}\right\| \le 0,}\\ & {\left\| f_2(\rho_{\mathrm{in}})f_2(\rho_{\mathrm{in}})^{\dagger} - f_2(\rho_{\mathrm{in}})\right\| \le 0.} \end{array} $ Here, $f_1(\rho_{\mathrm{in}}) = \rho_{\mathrm{in}}$ (as $T_1$ labels the input state directly), and $f_2(\rho_{\mathrm{in}})$ is the approximation function for the output state at $T_2$. * The `objective function` is $\|\rho_{\mathrm{in}} - f_2(\rho_{\mathrm{in}})\|$, representing the difference between input and output states. * The `constraints` ensure that both the input $\rho_{\mathrm{in}}$ and the approximated output $f_2(\rho_{\mathrm{in}})$ are `pure states`. If the maximum value of this objective function is greater than zero, it means there's an input for which the teleportation fails (i.e., input $\neq$ output) even when both are pure states, indicating a bug. This optimization can be solved using standard solvers like `stochastic gradient descent [56]`, `genetic algorithm [24]`, or `quadratic programming [51]`. #### 4.2.3.2. Confidence Estimation The `approximation accuracy` (from Section 4.2.2.3) might not always be sufficient to identify subtle errors, especially in "corner cases." To address this, `MorphQPV` provides a quantitative method for `confidence estimation`. The `confidence` of the verification result (i.e., the probability that the result holds true for *all* inputs) is determined by the approximation accuracy and an `accuracy threshold` $\epsilon$ (defined to identify counter-examples). `1 - confidence` is the probability that a counter-example exists but is not identified because its approximation accuracy is below $\epsilon$. The distribution of `approximation accuracies` across various inputs is observed to follow a `Beta distribution` $B(\beta_1, \beta_2)$. Image 10.jpg (Figure 6 from the paper) shows this distribution. The parameters $\beta_1$ and $\beta_2$ of the Beta distribution are related to $N_{\mathrm{sample}}$ and $N_{\mathrm{in}}$ by: $ \frac{\beta_1}{\beta_1 + \beta_2} = \frac{N_{\mathrm{sample}}}{2^{N_{\mathrm{in}} + 1}} $ This corresponds to the average accuracy for Case 2 inputs from Theorem 2. The parameters $\beta_1$ and $\beta_2$ can be characterized by running a set of benchmarking inputs. The probability that the approximation accuracy `acc` of a `counter-example` is smaller than the `accuracy threshold` $\epsilon$, and thus not identified, is: $ P(acc < \epsilon) = \int_{0}^{\epsilon}B(x;\beta_{1},\beta_{2})dx, $ This is the integral of the `Beta probability function` $B(x;\beta_1,\beta_2)$ from `0` to $\epsilon$. **Theorem 3 (Confidence)**: The confidence that the program is correct when the validation does not find a counter-example is: $ \mathrm{confidence} = 1 - P(acc < \epsilon). \quad (11) $ This formula provides a `lower-bound estimation` of confidence, as it assumes only one counter-example. In reality, an erroneous program usually has multiple counter-examples, leading to higher actual confidence ($1 - P(acc < \epsilon)^{N_{c-e}}$, where $N_{c-e}$ is the number of counter-examples). This analytical framework allows programmers to estimate the overhead needed to achieve a desired confidence level. #### 4.2.3.3. MorphQPV Complexity The overall complexity of `MorphQPV` for verifying an assertion is influenced by: * $N_{\mathrm{in}}$: Number of qubits of the input. * $N_{T_1}, N_{T_2}$: Number of qubits involved in the two tracepoints. * $N_{\mathrm{sample}}$: Number of inputs executed in `input sampling`. * **Input Sampling (Characterization)**: * State tomography for a state with $N_T$ qubits has a complexity of $O(e^{N_T})$ [10]. * For $N_{\mathrm{sample}}$ inputs, the complexity is $O(N_{\mathrm{sample}}(e^{N_{T_1}} + e^{N_{T_2}}))$. * To ensure $100\%$ confidence, characterization requires $2^{N_{\mathrm{in}} + 1}$ sampled inputs. The upper-bound complexity for characterization is $O(2^{N_{\mathrm{in}}+1}(e^{N_{T_1}} + e^{N_{T_2}}))$. * **Assertion Validation**: * The optimization problem involves $N_{\mathrm{sample}}$ parameters $\{\alpha_i\}$. * If using a `quadratic programming solver`, it requires up to $O(N_{\mathrm{sample}}^3)$ iterations (as per [17], but the paper states $O(N_{\mathrm{sample}}^3)$ for number of iterations to find global maximization, which might be a typo for $N_{\mathrm{sample}}$ as the number of variables in QP problem typically has complexity related to $N^3$ or $N^{3.5}$ for variables $N$). * The paper actually states `up to`O(N_{\mathrm{sample}}^3)`number of iterations to find the global maximization` which is an odd way to state it. Assuming the number of variables is $N_{sample}$, the complexity of QP is polynomial, usually $O(N_{sample}^3)$ or $O(N_{sample}^{3.5})$. * The upper-bound complexity for validation is $O((2^{N_{\mathrm{in}}+1})^3)$. The key takeaway is that `MorphQPV`'s complexity is driven by $N_{\mathrm{in}}$ (input qubits) rather than the total number of qubits in the program, and by $N_{\mathrm{sample}}$, which can be controlled by desired confidence. This is a significant improvement over methods whose complexity scales exponentially with the *total* number of qubits or require exhaustive testing. # 5. Experimental Setup ## 5.1. Datasets `MorphQPV` was evaluated on five quantum algorithms, encompassing different types and complexities, chosen as benchmarks: * **Quantum Lock (QL) [30, 40]**: An important module for encrypting quantum program outputs by encoding a binary key. It outputs $|1\rangle$ only if the input matches the key, otherwise $|0\rangle$. A bug occurs if it outputs $|1\rangle$ for an unexpected key. This algorithm is also known as a phase kickback module, crucial for algorithms like Bernstein-Vazirani and Quantum Phase Estimation. * *Data Sample:* The input is a binary string (e.g., `001` as a key). * **Quantum Neural Network (QNN) [23]**: Used for classification tasks, specifically demonstrated with the Iris flower dataset. The QNN model consists of an encoder and layers of parameterized gates. * *Data Sample:* The `Iris dataset` consists of 100 flowers, each with 4 attributes (e.g., sepal length, sepal width, petal length, petal width) and 2 species (e.g., Setosa, Virginia). Attributes are encoded into the quantum state, and the `expectation value` on the Z-axis of a qubit determines the species prediction ($\mathbb{E}_Z(\rho) > 0$ for Setosa, $\mathbb{E}_Z(\rho) \le 0$ for Virginia). * **Quantum Random Access Memory (QRAM)**: A fundamental component for many quantum applications, allowing data access based on addresses, and information reuse without decoherence. * *Data Sample:* A QRAM table stores values $\theta_i \in [0, 2\pi]$ at addresses $i$. For $N$ addressing qubits, the table size is $2^N$. An input superposition state $\sum \lambda_i |i\rangle$ to addressing qubits queries information, outputting $\sum \lambda_i |\theta_i\rangle$ in a data qubit, where $|\theta_i\rangle = \cos\theta_i|0\rangle + \sin\theta_i|1\rangle$. * **Quantum Error Correction (QEC) [37]**: Algorithms designed to protect quantum information from `decoherence` and other errors. * **Shor's Algorithm [9]**: A famous quantum algorithm for integer factorization, demonstrating quantum speedup over classical algorithms. * **Cross Entropy Benchmarking (XEB) [2]**: A technique used to characterize the performance of quantum processors by measuring the probability of specific outcomes from randomly generated circuits. The number of input qubits and output qubits for these algorithms were set to their overall number of qubits for a fair comparison. These datasets are effective for validating the method's performance because they represent diverse quantum computational paradigms (encryption, machine learning, data access, fundamental quantum algorithms) and scale up in qubit count, allowing for testing of scalability and efficacy in different error scenarios. ## 5.2. Evaluation Metrics For every evaluation metric mentioned in the paper, here is a complete explanation: ### 5.2.1. Confidence * **Conceptual Definition**: `Confidence` in `QPV` is defined as the probability that the verification result (i.e., whether the program is correct or buggy) holds true for *all* possible inputs. A high confidence value indicates that the verification is highly reliable across the entire input space, not just for the inputs explicitly tested. * **Mathematical Formula**: $ \mathrm{confidence} = 1 - P(acc < \epsilon) \quad (11) $ * **Symbol Explanation**: * $\mathrm{confidence}$: The probability that the verification result holds for all inputs. * $P(acc < \epsilon)$: The probability that the `approximation accuracy` (`acc`) for a potential `counter-example` is less than a defined `accuracy threshold` $\epsilon$. If $acc < \epsilon$, the counter-example might not be identified by the validation process, leading to a false positive (program reported correct when it's buggy). * The probability $P(acc < \epsilon)$ is calculated as the integral of the `Beta probability function` $B(x;\beta_1,\beta_2)$ between range $[0, \epsilon]$: $ P(acc < \epsilon) = \int_{0}^{\epsilon}B(x;\beta_{1},\beta_{2})dx $ where $B(x;\beta_1,\beta_2)$ represents the Beta distribution of approximation accuracies, and $\beta_1, \beta_2$ are its parameters. * The paper notes this provides a `lower-bound estimation` of confidence, as it assumes only one counter-example. Real confidence is higher with multiple counter-examples. ### 5.2.2. Success Rate * **Conceptual Definition**: In the context of mutation testing, `success rate` is defined as the probability that a verification method correctly identifies a bug (or, more precisely, produces a valid verification result) when presented with a mutated (buggy) version of a program. * **Mathematical Formula**: The paper describes this conceptually. If $N_{\text{total}}$ test cases (programs with bugs) are generated, and $N_{\text{identified}}$ bugs are successfully identified by the method, then: $ \mathrm{Success~Rate} = \frac{N_{\text{identified}}}{N_{\text{total}}} \times 100\% $ * **Symbol Explanation**: * $N_{\text{identified}}$: The number of times a bug was correctly identified by the verification method. * $N_{\text{total}}$: The total number of buggy programs (test cases) evaluated. ### 5.2.3. Overhead * **Conceptual Definition**: `Overhead` quantifies the computational cost introduced by the verification process. In this paper, it's primarily measured by the `number of quantum operations` required to validate an assertion. This includes operations for `input sampling`, `state tomography`, and any additional gates or measurements introduced by the verification method itself. A lower overhead indicates a more efficient verification process. * **Mathematical Formula**: Not explicitly provided as a single formula, but calculated by summing the operations. For example, for NDD debugging a QL program, $10^3$ shots for 5 inputs implies $(1+1) \times 10^3 \times 5$ operations (where $1+1$ might imply a basic operation count per shot or per verification step). * **Symbol Explanation**: * `Number of quantum operations`: A direct count or estimation of the total quantum gate operations (e.g., single-qubit gates, two-qubit gates) and measurements performed during the verification process. * `Shots`: Repetitions of a quantum program execution to gather sufficient statistical data for measurement outcomes. ### 5.2.4. Approximation Accuracy * **Conceptual Definition**: `Approximation accuracy` measures how closely the `isomorphism-based approximation` of a tracepoint state $\rho_{\mathrm{approx}}$ matches the true tracepoint state $\rho_{\mathrm{truth}}$ (which would be obtained by a full, exact execution and tomography of the quantum program). * **Mathematical Formula**: The paper defines accuracy using the `Hilbert-Schmidt inner product`: $ \mathrm{acc} = tr(\sqrt{\rho_{\mathrm{approx}}\rho_{\mathrm{truth}}})^2 $ * **Symbol Explanation**: * $\mathrm{acc}$: The approximation accuracy, a value between 0 and 1 (or 0% and 100%). * $tr(\cdot)$: The `trace operator`, which sums the diagonal elements of a matrix. * $\sqrt{\cdot}$: The `matrix square root`. * $\rho_{\mathrm{approx}}$: The `density matrix` of the quantum state at a `tracepoint` as predicted by the `isomorphism-based approximation function`. * $\rho_{\mathrm{truth}}$: The `density matrix` of the true quantum state at the same `tracepoint`, ideally obtained from an exact quantum program execution and full quantum state tomography. ## 5.3. Baselines The paper compares `MorphQPV` against several representative prior works in quantum program verification, categorized into `assertion techniques` and `deductive verification methods`. ### 5.3.1. Assertion Techniques (Section 8) These are methods that use runtime checks or specific test inputs. * **Stat [20]**: `Statistical assertions`. Checks `probability distributions`. * **Proj [27]**: `Projection-based measurement`. Checks if the runtime state is within a specified set. * **NDD [28, 29]**: `Non-destructive discrimination`. Systematically checks for state properties, similar to `Proj`. * **SR [13]**: `Symbolic reasoning`. Verifies nondeterministic quantum programs. * **Quito [47]**: `Coverage-guided test generator`. Uses a `grid search` to determine test inputs. ### 5.3.2. Deductive Verification Methods (Appendix B) These methods aim for formal correctness proofs. * **KNA [34]**: `Kleene Algebra` based reasoning for quantum programs. * **Twist [55]**: Sound reasoning for `purity` and `entanglement` in quantum programs. * **QHL [57]**: `Quantum Hoare Logic`. * **Automa [8]**: An `automata-based framework` for verification and bug hunting in quantum circuits. These baselines were chosen because they represent the state-of-the-art in both runtime and formal verification paradigms, allowing for a comprehensive comparison across `expressiveness`, `confidence`/`success rate`, and `overhead`. # 6. Results & Analysis The evaluation of `MorphQPV` focuses on three key aspects: `expressiveness`, `success rate` (confidence), and `overhead`. The experiments use five benchmark quantum algorithms: `Quantum Lock (QL)`, `Quantum Neural Network (QNN)`, `Quantum Error Correction (QEC)`, `Shor's Algorithm (Shor)`, and `Cross Entropy Benchmarking (XEB)`. ## 6.1. Core Results Analysis ### 6.1.1. Case Study 1: Quantum Lock (QL) The `Quantum Lock` program is designed to output $|1\rangle$ only if the input matches a specific key; otherwise, it outputs $|0\rangle$. A bug would involve an unexpected key also leading to $|1\rangle$. Verifying this often requires searching a large input space. The paper provides the following assertion for `QL`: assume: P_1(P_T_1) = (p_T_1 != |key><0|||, output |0><0| This means: if the input state ($P_{T_1}$) is *not* the designated key state, then the output state ($P_{T_2}$) should be $|0\rangle\langle 0|$. A violation (i.e., $P_3 > 0$) indicates a bug. Image 7.jpg (Figure 7 from the paper) illustrates the number of program executions required by different methods to identify bugs in the `Quantum Lock` program as the number of qubits increases.  *该图像是一个图表，展示了不同量子程序在增加量子位（#qubit）时的执行次数（#executions）。三条曲线分别代表了Quito、NDD和MorphQPV，MorphQPV在27个量子位时相较于Quito减少了执行次数53.9倍，显示出其优越性。* The graph clearly shows `MorphQPV` drastically reducing the number of program executions compared to `Quito` and `NDD`. For a 21-qubit QL algorithm, `MorphQPV` requires around 8,974 executions, while `NDD` and `Quito` require $9.3 \times 10^5$ and $4.8 \times 10^5$ executions respectively. This translates to a $107.9 \times$ speedup over the baselines. The speedup is observed to grow exponentially with the number of qubits, highlighting `MorphQPV`'s scalability advantages in handling larger quantum programs. ### 6.1.2. Case Study 2: Quantum Neural Network (QNN) This case study uses a QNN model to classify Iris flowers (2 species, 4 attributes). `MorphQPV` is used to debug `gate pruning` and validate `prior knowledge`. #### 6.1.2.1. Verification of Gate Pruning Gate pruning (removing unimportant gates, e.g., $P_1, P_2$ in Figure 8) is a technique to mitigate noise. The goal is to ensure prediction doesn't change after pruning, or to identify incorrectly pruned gates. `MorphQPV` uses an assertion to compare states before and after pruning: assume: P_1(QNN^, p_T_1) = ||QNN^, p_T_1 QNN^, p_T_1^+ - QNN^, p_T_1|| // (simplified representation) guarantee: P_3(QNN^, p_T_i, QNN', p_T_i) = ||QNN^, p_T_i - QNN', p_T_i|| <= beta This assertion checks if the state at tracepoint $T_i$ (p_{T_i}) in the original QNN model ($QNN^*$) is `similar` to the state at the same tracepoint in the pruned QNN model (`QNN'`), within a distance threshold $\beta$. If an assertion toward the output fails, a binary search can pinpoint the incorrectly pruned gate. This is difficult for prior methods due to repeated tomography for varying inputs. #### 6.1.2.2. Verification of Prior Knowledge `MorphQPV` can verify biological prior knowledge, e.g., "flowers with sepal lengths in the range [4,6] cm belong to Setosa." An assertion is declared for this: assume: P_1(rho_T_5) = (4 <= rho_T_5[1][1] <= 6), when the word length is in [4,6]cm guarantee: P_2(rho_T_4) = (E_Z(rho_T_4) > 0); // the output should be Setosa Here, $\rho_{T_5}$ is the state of the fourth qubit (encoding sepal length), and $\rho_{T_4}$ is the output state. If the assertion fails (e.g., $\mathbb{E}_Z(\rho_{T_4}) \le 0$ for an input with sepal length in [4,6] cm), it implies the prior knowledge is incorrect or the QNN model does not adhere to it. This approach provides input-independent verification, overcoming the limitation of test datasets covering only a small proportion of the input space. ### 6.1.3. Case Study 3: Quantum Random Access Memory (QRAM) `QRAM` stores values $\theta_i$ at addresses $i$. For an input superposition state $\sum \lambda_i |i\rangle$, the data qubit should output $\sum \lambda_i |\theta_i\rangle$. The challenge is the vast superposition input space. An assertion for overall `QRAM` functionality: ``` assume: P_1(rho_T_1) = ||rho_T_1 - sum_{i,j=0}^{2^N} lambda_i lambda_j^* |i><j||, when input state is sum_{t=0}^{2^N} lambda_i|i> guarantee: P_2(rho_T_2) = ||rho_T_2 - sum_{i,j=0}^{2^N} lambda_i lambda_j^* |theta_i><theta_j||, the output state is sum_{t=0}^{2^N} lambda_i|theta_i> ``` Here, $\rho_{T_1}$ is the addressing qubit state at the start, and $\rho_{T_2}$ is the data qubit state at the end. If a bug is detected, a binary search strategy is employed: 1. Introduce an intermediate `tracepoint`T_3.

2. Assert correctness for the first half of addresses:

   assume: P_1(rho_T_1) = ||rho_T_1 - sum_{i,j=0}^{2^N/2} lambda_i lambda_j^* |i><j||,
   guarantee: P_2(rho_T_3) = ||rho_T_3 - sum_{i,j=0}^{2^N/2} lambda_i lambda_j^* |theta_i><theta_j||,
   

   If this assertion fails, the error is in the first half; otherwise, it's in the second half. This binary search effectively narrows down the error address.

Image 2.jpg (Figure 10 from the paper) presents the number of sampled inputs required to identify errors in QRAM.

该图像是图表，展示了在三种优化策略下不同量子比特（#qubit）条件下的样本输入数量（图2(a)）和实验的射击数量（图2(b)）。左侧图表中，baseline、strategy-adapt、strategy-const和strategy-prop四种策略的样本输入数量在不同量子比特时的变化情况，右侧图表则展示射击次数的对比。

MorphQPV achieves a $31,563.2 \times$ reduction in sampling inputs compared to Quito for QRAM, which is even more significant than for QL. This is attributed to QRAM having a larger superposition state input space, offering more optimization opportunities for MorphQPV's isomorphism-based approach.

6.1.4. Comparison With Prior Works

6.1.4.1. Expressiveness Analysis

The following are the results from Table 2 of the original paper:

Observations:

• Verified Object: MorphQPV and SR can verify Mixed state & Evolution, offering a comprehensive view. Stat is limited to Probability distribution, while Proj and NDD focus on Mixed states.

• Comparison Type: MorphQPV offers Full comparison capabilities (e.g., greater than, less than, equality, relations between states). Proj, NDD, and SR are limited to Equal & In comparisons. Stat has Part comparison ability.

• Interpretability: MorphQPV provides Full interpretability (counter-examples, intermediate density matrices, confidence). Stat offers Part (probability distribution of error state). Proj, NDD, and SR offer No interpretability in terms of explicit counter-examples or confidence.

• Debug circuit with feedback: MorphQPV and SR can fully debug circuits with mid-measurements and simple feedback. The other methods (Stat, Proj, NDD) require redefinition of predicates for different measurement results.

  The following are the results from Table 5 of the original paper:

  	KNA [34]	Twist [55]	QHL [57]	MorphQPV
  Verified object Compa- rison Interpr- etability	Expectation Equal or greater Part	Purity Equal No	Expectation Equal or greater Part	Mixed state & Evolution Full

Observations (Deductive Methods Comparison):

• Verified Object: MorphQPV verifies Mixed state & Evolution (full scope). Deductive methods are narrower: KNA and QHL check Expectation, Twist checks Purity. This limits their ability to catch various bug types (e.g., Twist cannot debug QNN or XEB if bugs don't change purity).
• Comparison Type: MorphQPV supports Full comparison. KNA and QHL support Equal or greater. Twist supports Equal.
• Interpretability: MorphQPV provides Full interpretability. Deductive methods like KNA and QHL offer Part interpretability (mathematical formulation) but generally cannot output counter-examples. Twist offers No interpretability.

6.1.4.2. Success Rate Analysis

The following are the results from Table 3 of the original paper:

The following are the results from Table 4 of the original paper:

Observations:

• MorphQPV: Achieves a perfect 100% success rate in identifying bugs across all five benchmark programs (QL, QNN, QEC, Shor, XEB) and all qubit sizes tested. This demonstrates its superior ability to reliably detect errors.

• Quito: Its success rate decreases exponentially as the number of qubits grows, especially for QL (36% for 3q, 0% for 9q) and XEB (100% for 3q, 37% for 9q). This is because Quito uses grid search and mainly validates probability distributions, missing phase errors. For QEC and Shor, its success rate is 0% for larger qubit counts.

• NDD: Shows high success rates (100%) for QEC, Shor, and XEB, as it can identify phase differences. However, it fails completely (0% success rate) for the 9-qubit QL program, highlighting its limitation when a program has only a single counter-example that it might miss. It also cannot debug QNN models, which require comparison of expectation values, a capability NDD lacks.

  The following are the results from Table 6 of the original paper (Deductive Methods Comparison):

  Bench- mark	Success rate (%)			Overhead (seconds)
  	Twist [55]	Automa [8]	Morph-QPV	Twist [55]	Automa [8]
  QPC	9g	98	100	0.3	0.3
  	10g	98	100	4.5	1.2
  	15g	99	100	156.5	3.1
  	20g	100	100	5.9 × 106	4.8
  SnorSNOR	30g	100	100	1.1	0.7
  	10g	100	100	23.2	6.9
  	15g	100	100	1.2 × 10-5	22.2
  	20g	100	100	6.1 × 104	65.5
  QNOVQNOV	5g	/	/	100	/
  	10g	/	/	100	/	/
  	15g	/	/	100	/	/
  	20g	/	/	100	/	/
  XRB	5g	/	100	100	0.7	/
  	10g	/	100	160	0.6	/
  	15g	/	100	160	/	/
  	20g	/	100	160	/	/

Observations:

• MorphQPV generally achieves 100% success rate.
• Twist and Automa also show high success rates for QEC and Shor. However, they are unable to debug QNN and XEB programs (indicated by /) because their verified objects (purity for Twist, expectation for Automa) do not capture the types of bugs present in these algorithms.

6.1.4.3. Overhead Analysis

The overhead is defined as the number of quantum operations required. Each program execution used $10^3$ shots.

Observations (from Table 4):

• MorphQPV: Consistently achieves a minimal overhead of $5.0 \times 10^3$ operations across all programs and qubit sizes. This significant reduction stems from its approximation function, which largely eliminates the need for repeated quantum executions after the initial sampling.
• NDD: Incurs extremely high overhead, especially for larger qubit counts. For example, for 9-qubit Shor, it requires $2.8 \times 10^{10}$ operations. This is due to its reliance on synthesizing unitary gates for sub-space projection, which scales exponentially with qubits.
• Quito: While having the minimum overhead among baselines ($5.0 \times 10^3$ for some cases, matching MorphQPV's initial sampling overhead), it comes at the cost of low confidence and success rate for many programs, as it only checks probability distributions.

Observations (from Table 6, Deductive Methods Comparison):

• Twist: Suffers from high computational cost, requiring $5.9 \times 10^6$ seconds (approximately 68 days) for a 20-qubit QEC program, as it relies on classical simulation.
• Automa: Shows smaller overhead than Twist due to its tree automata approach, but its complexity still increases exponentially with the number of qubits.
• MorphQPV: Its complexity is driven by the input qubits ($N_{\mathrm{in}}$) rather than total qubits, and the time-consuming input sampling can be parallelized, leading to overall efficiency.

6.1.5. Evaluation of Theorems

6.1.5.1. Evaluation of Theorem 1 (Approximation function)

Image 11.jpg(a) (Figure 11(a) from the paper) compares the computation time for obtaining intermediate program states using MorphQPV, quantum state tomography, and quantum process tomography.

该图像是图表，展示了不同量子比特下使用MorphQPV、状态与过程成像的计算时间对比，以及在不同量子比特和采样输入数量下的近似准确性。图(a)比较了在6、8和10个量子比特中获得中间程序状态所需的时间，图(b)显示了准确性与量子比特数和采样数的关系，公式为 $accuracy \propto \frac{N_a}{2^{n_{qubits}}}$。

The figure shows that MorphQPV achieves a dramatic reduction in computation time. For 10-qubit programs, MorphQPV is $74.3 \times$ faster than Qiskit simulation, $1.2 \times 10^4 \times$ faster than state tomography, and $7.3 \times 10^6 \times$ faster than process tomography. A 10-qubit process tomography can take 11.4 days, while MorphQPV takes less than 0.5 seconds. This validates the efficiency gain from MorphQPV's approximation, as it involves simple summation of density matrices classically, avoiding complex quantum operations and measurements.

6.1.5.2. Evaluation of Theorem 2 (Approximation accuracy)

Image 11.jpg(b) (Figure 11(b) from the paper) presents the average approximation accuracy under different numbers of qubits and sampled inputs. The accuracy curve closely follows Case 2 of Theorem 2, where accuracy grows linearly with the number of samples. The maximum number of sampled inputs to achieve 100% accuracy (i.e., $2^{N_{\mathrm{in}}+1}$) is consistent with the theorem. Experimental accuracy is often slightly higher than theoretical values, attributed to the Clifford group's expressiveness in input sampling.

6.1.5.3. Evaluation of Theorem 3 (Confidence Estimation)

Image 1.jpg (Figure 12 from the paper, but the image is titled "Figure 12. Evaluation of confidence estimation (Theorem 3)") compares the estimated confidence with the real success rate for 7-qubit programs with bugs introduced by mutation testing.

该图像是一个示意图，左侧(a)展示了一个因意外密钥而产生故障的4量子位锁，右侧(b)展示了在15量子位锁中验证结果的信心度随输入数量变化的曲线图，只有意外密钥能够帮助找到故障。

The graph shows that real success rates are generally above the theoretical confidence estimation. This validates Theorem 3, which provides a lower-bound estimation. Programs with fewer counter-examples (e.g., QEC) have curves closer to the estimated confidence, while programs with more counter-examples (e.g., Shor) show higher real success rates, as MorphQPV's confidence model is conservative.

6.1.6. Evaluation of Techniques

6.1.6.1. Evaluation of Space Pruning Strategies

Image 13.jpg (Figure 13 from the paper) shows the ablation study of space pruning strategies from Section 5.4.

• Figure 13(a) (Sampled Inputs Reduction): Strategy-adapt and Strategy-const significantly reduce the number of sampled inputs. Strategy-adapt (e.g., for 10-qubit QNN) reduces samples from 2048 to 90 ($22.8 \times$ reduction) while maintaining 95% accuracy by pruning unimportant eigenstates. Strategy-const (e.g., for 10-qubit Shor) achieves a $32.0 \times$ reduction by fixing half of the input qubits.
• Figure 13(b) (Shots Reduction): Strategy-prop achieves an $82.1 \times$ reduction in shots for 10-qubit programs. This is because it eliminates full state tomography when only specific properties (e.g., amplitudes) are relevant to the assertion, leading to fewer measurements. For a 6-qubit Shor program, it reduced shots by $63.0 \times$ when only amplitudes were involved.

6.1.6.2. Evaluation of Approximation Accuracy on Noisy Quantum Simulator

Image 14.jpg (Figure 14 from the paper) shows approximation accuracy on a noisy quantum simulator (IBM Cairo model) for 5-qubit and 15-qubit Shor and QNN algorithms.

When tracepoints are far apart (start and end of program), accuracy is low (e.g., 1.6% for 15-qubit QNN) due to accumulated decoherence errors. This is improved by injecting intermediate tracepoints. By injecting four intermediate tracepoints for 15-qubit QNN, accuracy improves from 1.6% to 13.6%. With nine intermediate tracepoints, it further rises to 65.0%. This demonstrates that breaking down the program into smaller, independently characterized segments helps maintain accuracy in noisy environments.

6.1.6.3. Ablation Study of Adopting Clifford Group

Image 15.jpg(a) (Figure 15(a) from the paper) compares using Clifford group states versus basis states for input sampling in 9-qubit algorithms.

Using the Clifford group for sampled inputs reduces the number of samples required for 100% accuracy by $64.0 \times$ compared to using basis states. For a fixed number of samples ($2^{10}$), the Clifford group improves accuracy from 10.9% to 93.1% ($82.2\%$ improvement). This is because Clifford states are more representative, showing entanglement and superposition.

6.1.6.4. Evaluation of Optimization Times Based on Different Solvers in Validation

Image 15.jpg(b) (Figure 15(b) from the paper) evaluates the optimization time of the constraint objective function using three different solvers: stochastic gradient descent [56], genetic algorithm [24], and quadratic programming [51].

The quadratic programming solver is the fastest for programs with fewer than 12 qubits, completing validation in under 12 minutes to find the global optimum. Optimization time increases polynomially with the number of sampled inputs. The paper notes that finding a local optimum is often sufficient for correctness determination, further reducing time.

6.2. Data Presentation (Tables)

The following are the results from Table 1 of the original paper:

The following are the results from Table 2 of the original paper:

The following are the results from Table 3 of the original paper:

The following are the results from Table 4 of the original paper:

The following are the results from Table 5 of the original paper:

The following are the results from Table 6 of the original paper:

The following are the results from Table 7 of the original paper:

6.3. Ablation Studies / Parameter Analysis

6.3.1. Evaluation of Theorems

The results for Theorem 1, 2, and 3, as discussed in Section 6.1.5, serve as ablation studies.

• Theorem 1: Demonstrates the computational efficiency of the isomorphism-based approximation by comparing its execution time against traditional simulation and tomography methods (Figure 11(a)). This validates the core efficiency gain of MorphQPV.
• Theorem 2: Shows how approximation accuracy is related to N_sample and N_in (Figure 11(b)), confirming the theoretical bounds and the impact of sampling on the precision of characterization.
• Theorem 3: Evaluates the confidence estimation model (Figure 12), showing that the theoretical lower bound for confidence is a reasonable predictor of real-world success rates in bug identification.

6.3.2. Evaluation of Space Pruning Strategies

(See Image 13.jpg and Section 6.1.6.1 for detailed analysis.) This study directly assesses the effectiveness of the proposed Strategy-adapt, Strategy-const, and Strategy-prop techniques in reducing overhead. These strategies collectively prune the number of sampled inputs and shots required for characterization, demonstrating that optimizing the sampling process is crucial for practical application.

6.3.3. Evaluation of Approximation Accuracy on Noisy Quantum Simulator

(See Image 14.jpg and Section 6.1.6.2 for detailed analysis.) This ablation study investigates the impact of noise and the effectiveness of intermediate tracepoints on approximation accuracy. It shows that while noise can significantly degrade accuracy over long quantum circuits, strategically injecting intermediate tracepoints to break down the characterization problem into smaller segments can effectively mitigate this degradation and improve accuracy, making MorphQPV more robust for real-world noisy quantum hardware.

6.3.4. Ablation Study of Adopting Clifford Group

(See Image 15.jpg(a) and Section 6.1.6.3 for detailed analysis.) This study compares the use of Clifford group states versus simple basis states for input sampling. It confirms that Clifford group states, due to their inherent entanglement and superposition, are significantly more representative and lead to higher approximation accuracy with fewer samples. This validates the importance of intelligent input selection in the characterization phase.

6.3.5. Runtime Comparison of Different Optimization Solvers

(See Image 15.jpg(b) and Section 6.1.6.4 for detailed analysis.) This analysis investigates the performance of different classical optimization solvers for the assertion validation step. It highlights that quadratic programming is efficient for smaller qubit counts, while other solvers might be more suitable for larger problems. This provides practical guidance for implementing the validation step, demonstrating that the choice of solver can impact the overall efficiency of MorphQPV.

7. Conclusion & Reflections

7.1. Conclusion Summary

The paper successfully introduces MorphQPV, a novel and confident assertion-based verification methodology for quantum programs. Its core innovation is the principled exploitation of isomorphism in quantum programs, enabling a structure-preserving relation between program inputs and runtime states.

The key contributions are:

1. Multi-state assertions are defined using tracepoint pragmas and an assume-guarantee primitive, allowing for expressive and input-independent specification of relations between quantum states at different points in time.

2. An isomorphism-based approximation technique is developed to characterize the ground-truth relations between states. This enables the calculation of runtime states for various inputs on classical computers without repeated quantum executions, backed by mathematical proofs of accuracy.

3. Input-independent validation is achieved by formulating the verification as a constraint optimization problem, capable of providing counter-examples when bugs are present. A novel confidence estimation model quantifies the reliability of verification results.

   Experimental results across five diverse quantum algorithms (QL, QNN, QRAM, QEC, Shor, XEB) demonstrate MorphQPV's significant advantages:

• Reduced Program Executions: Up to $107.9 \times$ reduction for a 27-qubit quantum lock algorithm and $31,563.2 \times$ reduction for QRAM compared to baselines.

• Improved Debugging Success Rate: Consistently achieves 100% success rate in bug identification, outperforming prior methods by $3.3 \times$ to $9.9 \times$.

• Lower Overhead: Drastically reduces the number of quantum operations compared to other assertion methods, achieving minimum overhead for many benchmarks.

• Enhanced Expressiveness and Interpretability: Offers full comparison types, debugs circuits with feedback, and provides counter-examples and confidence estimation.

  MorphQPV addresses fundamental challenges in QPV related to scalability, confidence, and the inherent properties of quantum mechanics, providing a more rigorous and efficient framework for ensuring the correctness of quantum programs.

7.2. Limitations & Future Work

While MorphQPV presents significant advancements, several limitations and areas for future work can be inferred:

1. Approximation Accuracy in Highly Noisy/Complex Systems: The isomorphism-based approximation relies on the linearity of quantum evolution. While the paper demonstrates robustness in noisy simulators by injecting intermediate tracepoints, its effectiveness might decrease in extremely noisy or complex systems where the linear model breaks down or requires an excessive number of intermediate tracepoints, increasing overhead. Quantifying the precise trade-off between intermediate tracepoints, noise levels, and achievable accuracy for arbitrary circuits could be a future direction.
2. Scalability of Characterization for Large Input Qubits: While MorphQPV's complexity is driven by N_in (input qubits) rather than total qubits, the $2^{N_{\mathrm{in}}+1}$ factor for $100\%$ confidence in sampling still represents an exponential scaling with N_in. For very large $N_{\mathrm{in}}$, even this initial sampling phase (with state tomography) could become a bottleneck. Further research into more advanced adaptive sampling techniques or more efficient tomography methods tailored to specific program structures could extend scalability.
3. Applicability to Non-Unitary/Non-Linear Operations: The underlying assumption of isomorphism relies on the linear nature of quantum operations. While the paper states it handles mid-measurements and simple feedback (which often involve conditional unitary operations, maintaining linearity), it might need further investigation for more complex non-linear quantum operations or error correction schemes that actively modify states in non-linear ways.
4. Optimality of Classical Solvers: The constraint optimization problem is solved using classical solvers. While quadratic programming performs well for smaller qubit counts, finding global optima for highly non-linear or large-scale problems can still be computationally intensive. Exploring quantum-inspired optimization algorithms or more specialized classical solvers for the specific structure of MorphQPV's objective functions could be beneficial.
5. Defining Assertions: The effectiveness of MorphQPV heavily relies on the programmer's ability to define meaningful assume-guarantee assertions. Identifying suitable tracepoints and formulating precise predicates ($P_k$) still requires human expertise, similar to classical assertion-based verification. Tools or methodologies to assist in automated assertion generation or suggesting relevant tracepoints could be a valuable extension.
6. Real-world Hardware Evaluation: While experiments on noisy simulators are provided, more extensive validation on diverse real-world quantum hardware (with varying noise profiles, qubit connectivity, and gate sets) would further solidify its practical utility.

7.3. Personal Insights & Critique

This paper presents a highly innovative approach to Quantum Program Verification by cleverly leveraging isomorphism. My key insights and critiques are:

1. The Power of Isomorphism: The central idea of exploiting isomorphism is brilliant. It transforms a fundamentally quantum challenge (verifying states that are hard to observe or duplicate) into a tractable classical problem (linear combination and optimization). This paradigm shift allows MorphQPV to efficiently generalize verification results from a limited set of quantum executions to the entire input space, which is a significant leap forward for QPV. The mathematical grounding in linearity makes this approach robust.

2. Bridging the Gap: MorphQPV effectively bridges the gap between the rigor of deductive verification (by providing confidence and counter-examples) and the practicality of runtime assertion (by being lightweight and dynamic). The assume-guarantee primitive and multi-state assertions offer a powerful way to specify complex program behaviors that were previously difficult to verify.

3. Confidence as a First-Class Metric: Explicitly providing a confidence estimation model is a crucial contribution. In the probabilistic world of quantum computing, knowing how confident one can be in a verification result is as important as the result itself. This analytical framework moves QPV beyond mere bug detection to a more rigorous, quantifiable assurance.

4. Practicality and Overhead Reduction: The demonstrated $107.9 \times$ reduction in quantum executions and $31,563.2 \times$ reduction in sampling inputs for QRAM is astonishing. This practical efficiency makes MorphQPV highly relevant for current and near-future NISQ (Noisy Intermediate-Scale Quantum) devices, where quantum resources are scarce and expensive. The pruning strategies further enhance this practicality.

5. Interpretability: The ability to provide counter-examples and intermediate density matrices for debugging is invaluable. This moves beyond simply stating "there's a bug" to "here's why and where the bug occurs," which significantly aids developers.

6. Potential for Broader Applications: The core principle of isomorphism-based approximation could potentially be applied beyond verification. For instance, it might inspire more efficient ways to characterize quantum devices, debug quantum machine learning models, or even inform compilation strategies by providing a classical approximation of quantum circuit behavior.

7. Critique - "Under-Approximation" Nuance: Theorem 1 states the approximation is an "under-approximation." While mathematically proven, the implications for verification (e.g., whether it could lead to false negatives in certain edge cases where the true state barely crosses a threshold but the under-approximation doesn't) warrant careful consideration. The paper addresses this with the confidence model and accuracy threshold, which is a good mitigation strategy.

8. Critique - Dependency on Tomography: The initial input sampling phase still relies on quantum state tomography, which is itself resource-intensive and error-prone, especially for many qubits. While Strategy-prop helps by reducing tomography to specific properties, the fundamental dependency on accurate state reconstruction at least once per sampled input (or intermediate tracepoint) remains. Improvements in robust and efficient tomography techniques will directly benefit MorphQPV.

   Overall, MorphQPV represents a substantial step forward in making Quantum Program Verification more practical, confident, and interpretable. Its insights into leveraging fundamental quantum properties for verification are likely to influence future research in this critical area.