Scenario-Based Synthesis of Barrier Certificates for the Verification of Quantum Circuits

Bachelor's Thesis in Computer Science — Sapienza Università di Roma Facoltà di Ingegneria dell'Informazione, Informatica e Statistica

Author: Marco Casu (marco.casu.job@gmail.com) Advisor: Prof. Paolo Zuliani Academic Year: 2024/2025

📄 Full thesis (Italian): src/Thesis.pdf

---

Abstract

Real quantum circuits are highly sensitive to noise, which makes it hard to formally guarantee that a prepared qubit register evolves as intended. This thesis adapts barrier certificates — a formalism from dynamical systems and control theory used to prove safety properties of critical systems — to quantum circuits, in order to verify that a circuit evolves as desired despite uncertainty in the initial state.

The core contribution is a scenario-based synthesis method: candidate barrier certificates are searched for by sampling the state space and solving a linear program, using a parametrized template built from a linear combination of trigonometric (harmonic) functions. Once a candidate is found, it is checked against the formal definition of a barrier certificate using the dReal SMT solver over nonlinear real arithmetic.

The results show that while the harmonic template is expressive enough to model a wide range of quantum gates, it becomes computationally expensive to verify with an SMT solver as the number of terms grows, due to the trigonometric terms involved. The thesis closes by outlining several directions for future work, including alternative templates (spherical harmonics, generalized harmonic templates), extending the method to noisy dynamics, and using neural networks as barrier certificates.

Repository Structure

.
├── src/                         # LaTeX source of the thesis (Sapthesis class)
│   ├── Thesis.tex
│   ├── Thesis.pdf               # Compiled thesis
│   └── chapter/                 # Individual chapters
│
├── Quantum_Verification/        # Main implementation: synthesis + SMT verification
│   ├── main.py                  # Entry point — defines systems/gates and runs synthesis
│   ├── find_candidate.py        # Sampling + scenario-based candidate search
│   ├── synthesize_bc.py         # Synthesis loop (search candidate ⇄ verify ⇄ refine)
│   ├── verify.py                # Builds SMT2 constraints and calls dReal
│   ├── lib/                     # Core library (gates, templates, linear program, sampling, utils)
│   ├── samples/                 # Cached Sobol/random samples per system
│   └── candidate/               # Synthesized barrier certificate candidates
│
├── Quantum_Verification_Noise/  # Variant of the above extended to noisy dynamics
│   └── ...                      # Same structure, with adaptive-delta SMT verification
│
├── Neural_Network/               # Exploratory work: neural networks as barrier certificates
│   ├── main.py                  # Training loop for a barrier-certificate network
│   ├── nn_model.py               # Fully-connected network + custom BC loss
│   ├── lipschitz_bound.py       # Upper bound on the network's Lipschitz constant
│   └── utils/                    # Sphere/cube sampling helpers
│
├── Presentation/                 # Thesis defense slides (odp/pptx/pdf) and flowchart
├── BC_lipschitziana.pdf          # Notes on Lipschitz-based barrier certificates
└── COSE DA FARE.txt              # Personal TODO notes (Italian)

How It Works

1. Model the circuit as a dynamical system (lib/system.py, lib/gate.py): a quantum gate is represented as a unitary matrix acting on a qubit state vector, together with a starting region Z0 and an unsafe region ZU expressed as probability-of-measurement bounds.
2. Sample the state space (lib/generate_samples.py) using Sobol or random sampling over the unit sphere (valid quantum states).
3. Search for a candidate barrier certificate (find_candidate.py, lib/linprog.py): the candidate is a linear combination of harmonic (cos/sin) terms whose coefficients are found by solving a linear program built from the sampled scenarios (scipy.optimize.linprog).
4. Verify the candidate formally (verify.py): the candidate's constraints are encoded as an SMT2 problem over nonlinear real arithmetic and checked with the dReal SMT solver.
5. Refine on counterexamples: if verification fails, the returned counterexample points are added to the sample set and the loop restarts (synthesize_bc.py).

Quantum_Verification_Noise/ follows the same pipeline but accounts for uncertainty/noise in the dynamics, with an adaptively shrinking delta for the SMT queries as iterations progress.

Neural_Network/ explores an alternative approach where the barrier certificate is a small fully-connected network trained end-to-end, using a spectral-norm-based upper bound on its Lipschitz constant to reason about generalization beyond the sampled points.

Requirements

• Python 3.x
• dReal SMT solver — the code expects the binary at /opt/dreal/4.21.06.2/bin/dreal (adjust the path in verify.py if installed elsewhere)
• Python packages:
  • numpy
  • scipy
  • dreal (Python bindings)
  • torch (only needed for the Neural_Network experiments)

No requirements.txt is currently included in the repository; install the packages above with pip.

Thesis Contents

Chapter	Topic
1	Introduction: history of quantum computing, quantum mechanics fundamentals, qubits and quantum gates
2	Barrier certificates for quantum circuits
3	Linear combination of harmonics (the template)
4	SMT verification of the constraints with dReal
5	The synthesis procedure and algorithm
6	Case studies (verified and non-verified systems)
7	Future work: alternative templates, Fourier series / spherical harmonics, noisy dynamics, neural networks as barrier certificates, alternatives to SMT verification