Preuve automatique de théorèmes sur les réels pour raisonner sur les circuits quantiques

école doctorale

équipe

MOSEL-VERIDIS

contexte

Quantum computers continue to increase the number of qubits they can handle on various hardware. This induces a need for quantum computing languages independent of the hardware. A quantum circuit is a graphical representation of a quantum program that achieves this abstraction. The quantum computing research community is actively pursuing research in this domain [1]. In particular the question of reliably establishing the equivalence of two circuits is a major concern, as it opens the way to hardware-dependent optimization techniques from abstract programs [2]. Currently, most equivalence results are proved with pen-and-paper and in an ad-hoc way [3], but the community has started to consider more reliable approaches based on proof assistants and automated reasoning tools (ATPs) for quantum circuits (QC) equivalence as well as other verification tasks relating to quantum computing [4, 5, 6, 7]. ATPs are softwares specialized on formal reasoning, able to verify the satisfiability of logical formulas for various logics, so as to prove mathematical theorems. They are ubiquitous in (non-quantum) formal methods, but are ill-equipped to face some major challenges posed by QC equivalence. • A first challenge is the deformability of QC, that follows from laws such as distributivity and associativity. • Another challenge is the lack of automated procedures to handle the transcendental operations that are commonplace in QC transformations, involving non-polynomial arithmetic over the reals with trigonometric and exponential functions. The first challenge is a well-known issue in the ATP community. Indeed, associativity and commutativity must be handled with care as they create many ways of representing the same problem that tend to clutter solvers in an exponentially explosive way. Distributivity is of a similar nature (it is one of the causes of the exponential growth of propositional formulas when converted to one normal form or the other). Many an ATP technique has been adapted to handle such rules in an ad-hoc way, with mitigated success [8, 9]. However, a relatively recent technique from rewriting-based theorem proving can cope better with such properties than existing ones. Instead of focusing on depth-first search, it builds graph datastructures called E-graphs representing known equivalences that iteratively grow by applying rewriting rules in a breadth-first manner until the desired equivalence is found or a limit reached. This approach shows promising results to handle QC deformations [10], but the research in this direction is still in its preliminary stage. Regarding the second challenge, only very few ATPs include techniques that can handle transcendental real arithmetic. MetiTarski [11] is one, and it specializes in proving inequations by approximating the transcendental functions with Taylor series. Other techniques focus on formulas that are stable under perturbation (i.e, that remain true with the addition or removal of an arbitrarily small ϵ) by relying on interval arithmetic [12]. All of these are ill-suited to address QC equivalence problems that do not care for stability under perturbations and cannot be verified with approximations only.

spécialité

Informatique

laboratoire

LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications