arXiv subjects

Paolo Zuliani

Publications and source records attributed to Paolo Zuliani.

At least 19 recordsLinked to original sources

arXiv2026

Verified Linear Programming through Tolerance-Aware Precision Boosting

Linear programming plays a fundamental role in computer science, with applications in optimization, formal verification, SMT solving, and numerous other domains. When exactness guarantees are required, numerical inaccuracies arising from floating-point arithmetic can compromise soundness, whereas exact rational arithmetic often incurs significant computational overhead. In this paper, we investigate the numerical stability of the simplex algorithm and establish conditions under which a precision-boosting floating-point implementation provably produces the same pivot decisions and final basis as an exact rational implementation, from which the final result is reconstructed and certified exactly. Our analysis shows that correctness depends on both arithmetic precision and a careful handling of numerical tolerances. Based on these results, we develop a tolerance-aware, precision-boosting simplex algorithm with formal correctness guarantees. Finally, we introduce a delta-complete termination criterion that allows the algorithm to terminate once certified upper and lower bounds on the optimal objective differ by at most a user-specified threshold delta, providing a certified, user-controlled optimality gap.

math.OC↗

arXiv2026

A Hybrid Classical-Quantum Annealing Algorithm for the TSP

Hybrid quantum-classical algorithms can help mitigating the physical limitations of current quantum devices, particularly the low qubit count and the reduced topological connectivity. In this paper, we propose a hybrid technique to solve a well-known NP-hard optimization problem: the Traveling Salesperson Problem (TSP). Our approach is based on a graph contraction technique that removes most of the dimensionality of the original problem instance, producing a sub-TSP of a size suitable to be efficiently solved by a quantum device. The performance of our approach is first demonstrated on classical quantum simulation using Path Integral Monte Carlo, and then run on a D-Wave quantum annealer.

quant-ph↗

arXiv2025

LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

Ensuring the safety of AI-enabled systems, particularly in high-stakes domains such as autonomous driving and healthcare, has become increasingly critical. Traditional formal verification tools fall short when faced with systems that embed both opaque, black-box AI components and complex stochastic dynamics. To address these challenges, we introduce LUCID (Learning-enabled Uncertainty-aware Certification of stochastIc Dynamical systems), a verification engine for certifying safety of black-box stochastic dynamical systems from a finite dataset of random state transitions. As such, LUCID is the first known tool capable of establishing quantified safety guarantees for such systems. Thanks to its modular architecture and extensive documentation, LUCID is designed for easy extensibility. LUCID employs a data-driven methodology rooted in control barrier certificates, which are learned directly from system transition data, to ensure formal safety guarantees. We use conditional mean embeddings to embed data into a reproducing kernel Hilbert space (RKHS), where an RKHS ambiguity set is constructed that can be inflated to robustify the result to out-of-distribution behavior. A key innovation within LUCID is its use of a finite Fourier kernel expansion to reformulate a semi-infinite non-convex optimization problem into a tractable linear program. The resulting spectral barrier allows us to leverage the fast Fourier transform to generate the relaxed problem efficiently, offering a scalable yet distributionally robust framework for verifying safety. LUCID thus offers a robust and efficient verification framework, able to handle the complexities of modern black-box systems while providing formal guarantees of safety. These unique capabilities are demonstrated on challenging benchmarks.

eess.SY↗

arXiv2025

Verification of Quantum Circuits through Barrier Certificates using a Scenario Approach

In recent years, various techniques have been explored for the verification of quantum circuits, including the use of barrier certificates, mathematical tools capable of demonstrating the correctness of such systems. These certificates ensure that, starting from initial states and applying the system's dynamics, the system will never reach undesired states. In this paper, we propose a methodology for synthesizing such certificates for quantum circuits using a scenario-based approach, for both finite and infinite time horizons. In addition, our approach can handle uncertainty in the initial states and in the system's dynamics. We present several case studies on quantum circuits, comparing the performance of different types of barrier certificate and analyzing which one is most suitable for each case.

cs.LO↗

arXiv2025

High-level quantum algorithm programming using Silq

Quantum computing, with its vast potential, is fundamentally shaped by the intricacies of quantum mechanics, which both empower and constrain its capabilities. The development of a universal, robust quantum programming language has emerged as a key research focus in this rapidly evolving field. This paper explores Silq, a recent high-level quantum programming language, highlighting its strengths and unique features. We aim to share our insights on designing and implementing high-level quantum algorithms using Silq, demonstrating its practical applications and advantages for quantum programming.

quant-ph↗

arXiv2024

Verification of Quantum Circuits through Discrete-Time Barrier Certificates

Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.

quant-ph↗

arXiv2024

T-Count Optimizing Genetic Algorithm for Quantum State Preparation

Quantum state preparation is a crucial process within numerous quantum algorithms, and the need for efficient initialization of quantum registers is ever increasing as demand for useful quantum computing grows. The problem arises as the number of qubits to be initialized grows, the circuits required to implement the desired state also exponentially increase in size leading to loss of fidelity to noise. This is mainly due to the susceptibility to environmental effects of the non-Clifford T gate, whose use should thus be reduced as much as possible. In this paper, we present and utilize a genetic algorithm for state preparation circuits consisting of gates from the Clifford + T gate set and optimize them in T-Count as to reduce the impact of noise. Whilst the method presented here does not always produce the most accurate circuits in terms of fidelity, it can generate high-fidelity, non-trivial quantum states such as quantum Fourier transform states. In addition, our algorithm does automatically generate fault tolerantly implementable solutions where the number of the most error prone components is reduced. We present an evaluation of the algorithm when trialed against preparing random, Poisson probability distribution, W, GHZ, and quantum Fourier transform states. We also experimentally demonstrate the scalability issues as qubit count increases, which highlights the need for further optimization of the search process.

quant-ph↗

arXiv2024

Automated Verification of Silq Quantum Programs using SMT Solvers

We present SilVer (Silq Verification), an automated tool for verifying behaviors of quantum programs written in Silq, which is a high-level programming language for quantum computing. The goal of the verification is to ensure correctness of the Silq quantum program against user-defined specifications using SMT solvers. We introduce a programming model that is based on a quantum RAM-style computer as an interface between Silq programs and SMT proof obligations, allowing for control of quantum operations using both classical and quantum conditions. Additionally, users can employ measurement flags within the specification to easily specify conditions that measurement results require to satisfy for being a valid behavior. We provide case studies on the verification of generating entangled states and multiple oracle-based algorithms.

quant-ph↗

arXiv2024

Vagus nerve stimulation: Laying the groundwork for predictive network-based computer models

Vagus Nerve Stimulation (VNS) is an established palliative treatment for drug resistant epilepsy. While effective for many patients, its mechanism of action is incompletely understood. Predicting individuals' response, or optimum stimulation parameters, is challenging. Computational modelling has informed other problems in epilepsy but, to our knowledge, has not been applied to VNS. We started with an established, four-population neural mass model (NMM), capable of reproducing the seizure-like dynamics of a thalamocortical circuit. We extended this to include 18 further neural populations, representing nine other brain regions relevant to VNS, with connectivity based on existing literature. We modelled stimulated afferent vagal fibres as projecting to the nucleus tractus solitarius (NTS), which receives input from the vagus nerve in vivo. Bifurcation analysis of a deterministic version of the model showed higher background NTS input made the model monostable at a fixed point (FP), representing normal activity, while lower inputs produce bistability between the FP and a limit cycle (LC), representing the seizure state. Adding noise produced transitions between seizure and normal states. This stochastic model spent decreasing time in the seizure state with increasing background NTS input, until seizures were abolished, consistent with the deterministic model. Simulated VNS stimulation, modelled as a 30 Hz square wave, was summed with the background input to the NTS and was found to reduce total seizure duration in a dose-dependent manner, similar to expectations in vivo. We have successfully produced an in silico model of VNS in epilepsy, capturing behaviour seen in vivo. This may aid understanding therapeutic mechanisms of VNS in epilepsy and provides a starting point to (i) determine which patients might respond best to VNS, and (ii) optimise individuals' treatments.

q-bio.NC↗

arXiv2024

Safe Reach Set Computation via Neural Barrier Certificates

We present a novel technique for online safety verification of autonomous systems, which performs reachability analysis efficiently for both bounded and unbounded horizons by employing neural barrier certificates. Our approach uses barrier certificates given by parameterized neural networks that depend on a given initial set, unsafe sets, and time horizon. Such networks are trained efficiently offline using system simulations sampled from regions of the state space. We then employ a meta-neural network to generalize the barrier certificates to state space regions that are outside the training set. These certificates are generated and validated online as sound over-approximations of the reachable states, thus either ensuring system safety or activating appropriate alternative actions in unsafe scenarios. We demonstrate our technique on case studies from linear models to nonlinear control-dependent models for online autonomous driving scenarios.

eess.SY↗

arXiv2023

Verification of Quantum Systems using Barrier Certificates

Various techniques have been used in recent years for verifying quantum computers, that is, for determining whether a quantum computer/system satisfies a given formal specification of correctness. Barrier certificates are a recent novel concept developed for verifying properties of dynamical systems. In this article, we investigate the usage of barrier certificates as a means for verifying behaviours of quantum systems. To do this, we extend the notion of barrier certificates from real to complex variables. We then develop a computational technique based on linear programming to automatically generate polynomial barrier certificates with complex variables taking real values. Finally, we apply our technique to several simple quantum systems to demonstrate their usage.

quant-ph↗

arXiv2022

Formal Verification of Quantum Programs: Theory, Tools and Challenges

Over the past 27 years, quantum computing has seen a huge rise in interest from both academia and industry. At the current rate, quantum computers are growing in size rapidly backed up by the increase of research in the field. Significant efforts are being made to improve the reliability of quantum hardware and to develop suitable software to program quantum computers. In contrast, the verification of quantum programs has received relatively less attention. Verifying programs is especially important in the quantum setting due to how difficult it is to program complex algorithms correctly on resource-constrained and error-prone quantum hardware. Research into creating verification frameworks for quantum programs has seen recent development, with a variety of tools implemented using a collection of theoretical ideas. This survey aims to be a short introduction into the area of formal verification of quantum programs, bringing together theory and tools developed to date. Further, this survey examines some of the challenges that the field may face in the future, namely the development of complex quantum algorithms.

cs.LO↗

arXiv2022

Matrix Representation of Arbitrarily Controlled Quantum Gates

Controlled operations allow for the entanglement of quantum registers. In particular, a controlled-$U$ gate allows an operation, $U$, to be applied to the target register and entangle the results to certain values in the control register. This can be generalised by making use of the classical notion of conditional statements, where if a value (or state) satisfies some condition then a sequence of operations can be performed. A method is introduced to represent these generalised controlled operations that are based on classical conditional statements. Throughout examples are given to highlight the use of introduced gates.

quant-ph↗

arXiv2021

Quantum Computer Benchmarking via Quantum Algorithms

We present a framework that utilizes quantum algorithms, an architecture aware quantum noise model and an ideal simulator to benchmark quantum computers. The benchmark metrics highlight the difference between the quantum computer evolution and the simulated noisy and ideal quantum evolutions. We utilize our framework for benchmarking three IBMQ systems. The use of multiple algorithms, including continuous-time ones, as benchmarks stresses the computers in different ways highlighting their behaviour for a diverse set of circuits. The complexity of each quantum circuit affects the efficiency of each quantum computer, with increasing circuit size resulting in more noisy behaviour. Furthermore, the use of both a continuous-time quantum algorithm and the decomposition of its Hamiltonian also allows extracting valuable comparisons regarding the efficiency of the two methods on quantum systems. The results show that our benchmarks provide sufficient and well-rounded information regarding the performance of each quantum computer.

quant-ph↗

arXiv2021

Modelling and Simulating the Noisy Behaviour of Near-term Quantum Computers

Noise dominates every aspect of near-term quantum computers, rendering it exceedingly difficult to carry out even small computations. In this paper we are concerned with the modelling of noise in Noisy Intermediate-Scale Quantum (NISQ) computers. We focus on three error groups that represent the main sources of noise during a computation and present quantum channels that model each source. We engineer a noise model that combines all three noise channels and simulates the evolution of the quantum computer using its calibrated error rates. We run various experiments of our model, showcasing its behaviour compared to other noise models and an IBM quantum computer. We find that our model provides a better approximation of the quantum computer's behaviour than the other models. Following this, we use a genetic algorithm to optimize the parameters used by our noise model, bringing the behaviour of the model even closer to the quantum computer. Finally, a comparison between the pre and postoptimization parameters reveals that, according to our model, certain operations can be more or less erroneous than the hardware-calibrated parameters show.

quant-ph↗

arXiv2021

A Comparison of Quantum Walk Implementations on NISQ Computers

This paper explores two circuit approaches for quantum walks: the first consists of generalised controlled inversions, whereas the second one effectively replaces them with rotation operations around the basis states. We show the theoretical foundation of the rotational implementation. The rotational approach nullifies the large amount of ancilla qubits required to carry out the computation when using the inverter implementation. Our results concentrate around the comparison of the two architectures in terms of structure, benefits and detriments, as well as the computational resources needed for each approach. We show that the inverters approach requires exponentially fewer gates than the rotations but almost half the number of qubits in the system. Finally, we execute a number of experiments using an IBM quantum computer. The experiments show the effects of noise in our circuits. Small two-qubit quantum walks evolve closer to our expectations, whereas for a larger number of steps or state space the evolution is severely affected by noise.

quant-ph↗

arXiv2019

Automated Synthesis of Safe Digital Controllers for Sampled-Data Stochastic Nonlinear Systems

We present a new method for the automated synthesis of digital controllers with formal safety guarantees for systems with nonlinear dynamics, noisy output measurements, and stochastic disturbances. Our method derives digital controllers such that the corresponding closed-loop system, modeled as a sampled-data stochastic control system, satisfies a safety specification with probability above a given threshold. The proposed synthesis method alternates between two steps: generation of a candidate controller pc, and verification of the candidate. pc is found by maximizing a Monte Carlo estimate of the safety probability, and by using a non-validated ODE solver for simulating the system. Such a candidate is therefore sub-optimal but can be generated very rapidly. To rule out unstable candidate controllers, we prove and utilize Lyapunov's indirect method for instability of sampled-data nonlinear systems. In the subsequent verification step, we use a validated solver based on SMT (Satisfiability Modulo Theories) to compute a numerically and statistically valid confidence interval for the safety probability of pc. If the probability so obtained is not above the threshold, we expand the search space for candidates by increasing the controller degree. We evaluate our technique on three case studies: an artificial pancreas model, a powertrain control model, and a quadruple-tank process.

eess.SY↗

arXiv2018

Full version: An evaluation of estimation techniques for probabilistic reachability

We evaluate numerically-precise Monte Carlo (MC), Quasi-Monte Carlo (QMC) and Randomised Quasi-Monte Carlo (RQMC) methods for computing probabilistic reachability in hybrid systems with random parameters. Computing reachability probability amounts to computing (multidimensional) integrals. In particular, we pay attention to QMC methods due to their theoretical benefits in convergence speed with respect to the MC method. The Koksma-Hlawka inequality is a standard result that bounds the approximation of an integral by QMC techniques. However, it is not useful in practice because it depends on the variation of the integrand function, which is in general difficult to compute. The question arises whether it is possible to apply statistical or empirical methods for estimating the approximation error. In this paper we compare a number of interval estimation techniques based on the Central Limit Theorem (CLT), and we also introduce a new approach based on the CLT for computing confidence intervals for probability near the borders of the [0,1] interval. Based on our analysis, we provide justification for the use of the developed approach and suggest usage guidelines for probability estimation techniques.

cs.LO↗