arXiv Science⌕ Search

arXiv subjects

Benoît Valiron

Publications and source records attributed to Benoît Valiron.

At least 37 records · Page 2Linked to original sources
arXiv2022

Decoding techniques applied to the compilation of CNOT circuits for NISQ architectures

Current proposals for quantum compilers require the synthesis and optimization of linear reversible circuits and among them CNOT circuits. Since these circuits represent a significant part of the cost of running an entire quantum circuit, we aim at reducing their size. In this paper we present a new algorithm for the synthesis of CNOT circuits based on the solution of the syndrome decoding problem. Our method addresses the case of ideal hardware with an all-to-all qubit connectivity and the case of near-term quantum devices with restricted connectivity. For both cases, we present benchmarks showing that our algorithm outperforms existing algorithms.

quant-ph↗
arXiv2022

Reducing the Depth of Linear Reversible Quantum Circuits

In quantum computing the decoherence time of the qubits determines the computation time available and this time is very limited when using current hardware. In this paper we minimize the execution time (the depth) for a class of circuits referred to as linear reversible circuits, which has many applications in quantum computing (e.g., stabilizer circuits, CNOT+T circuits, etc.). We propose a practical formulation of a divide and conquer algorithm that produces quantum circuits that are twice as shallow as those produced by existing algorithms. We improve the theoretical upper bound of the depth in the worst case for some range of qubits. We also propose greedy algorithms based on cost minimization to find more optimal circuits for small or simple operators. Overall, we manage to consistently reduce the total depth of a class of reversible functions, with up to 92% savings in an ancilla-free case and up to 99% when ancillary qubits are available.

quant-ph↗
arXiv2022

Gaussian Elimination versus Greedy Methods for the Synthesis of Linear Reversible Circuits

Linear reversible circuits represent a subclass of reversible circuits with many applications in quantum computing. These circuits can be efficiently simulated by classical computers and their size is polynomially bounded by the number of qubits, making them a good candidate to deploy efficient methods to reduce computational costs. We propose a new algorithm for synthesizing any linear reversible operator by using an optimized version of the Gaussian elimination algorithm coupled with a tuned LU factorization. We also improve the scalability of purely greedy methods. Overall, on random operators, our algorithms improve the state-of-the-art methods for specific ranges of problem sizes: the custom Gaussian elimination algorithm provides the best results for large problem sizes (n > 150) while the purely greedy methods provide quasi optimal results when n < 30. On a benchmark of reversible functions, we manage to significantly reduce the CNOT count and the depth of the circuit while keeping other metrics of importance (T-count, T-depth) as low as possible.

quant-ph↗
arXiv2021

Categorical Semantics of Reversible Pattern-Matching

This paper is concerned with categorical structures for reversible computation. In particular, we focus on a typed, functional reversible language based on Theseus. We discuss how join inverse rig categories do not in general capture pattern-matching, the core construct Theseus uses to enforce reversibility. We then derive a categorical structure to add to join inverse rig categories in order to capture pattern-matching. We show how such a structure makes an adequate model for reversible pattern-matching.

cs.LO↗
arXiv2021

Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data -- qubits -- into classical data -- booleans -- . We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios\&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics.

cs.LO↗
arXiv2021

Hybrid quantum-classical circuit simplification with the ZX-calculus

We present a complete optimization procedure for hybrid quantum-classical circuits with classical parity logic. While common optimization techniques for quantum algorithms focus on rewriting solely the pure quantum segments, there is interest in applying a global optimization process for applications such as quantum error correction and quantum assertions. This work, based on the pure-quantum circuit optimization procedure by Duncan et al., uses an extension of the formal graphical ZX-calculus called ZX-ground as an intermediary representation of the hybrid circuits to allow for granular optimizations below the quantum-gate level. We define a translation from hybrid circuits into diagrams that admit the graph-theoretical focused-gFlow property, needed for the final extraction back into a circuit. We then derive a number of gFlow-preserving optimization rules for ZX-ground diagrams that reduce the size of the graph, and devise an strategy to find optimization opportunities by rewriting the diagram guided by a Gauss elimination process. Then, after extracting the circuit, we present a general procedure for detecting segments of circuit-like ZX-ground diagrams which can be implemented with classical gates in the extracted circuit. We have implemented our optimization procedure as an extension to the open-source python library PyZX.

quant-ph↗
arXiv2021

Proceedings 17th International Conference on Quantum Physics and Logic

This volume contains the proceedings of the 17th International Conference on Quantum Physics and Logic (QPL 2020), which was held June 2-6, 2020. Quantum Physics and Logic is an annual conference that brings together researchers working on mathematical foundations of quantum physics, quantum computing, and related areas, with a focus on structural perspectives and the use of logical tools, ordered algebraic and category-theoretic structures, formal languages, semantical methods, and other computer science techniques applied to the study of physical behavior in general. Work that applies structures and methods inspired by quantum theory to other fields (including computer science) is also welcome.

cs.LO↗
arXiv2021

Reasoning about Recursive Quantum Programs

Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling.

cs.LO↗
arXiv2020

Synthesizing quantum circuits via numerical optimization

We provide a simple framework for the synthesis of quantum circuits based on a numerical optimization algorithm. This algorithm is used in the context of the trapped-ions technology. We derive theoretical lower bounds for the number of quantum gates required to implement any quantum algorithm. Then we present numerical experiments with random quantum operators where we compute the optimal parameters of the circuits and we illustrate the correctness of the theoretical lower bounds. We finally discuss the scalability of the method with the number of qubits.

cs.ET↗
arXiv2020

Quantum circuit synthesis using Householder transformations

The synthesis of a quantum circuit consists in decomposing a unitary matrix into a series of elementary operations. In this paper, we propose a circuit synthesis method based on the QR factorization via Householder transformations. We provide a two-step algorithm: during the first step we exploit the specific structure of a quantum operator to compute its QR factorization, then the factorized matrix is used to produce a quantum circuit. We analyze several costs (circuit size and computational time) and compare them to existing techniques from the literature. For a final quantum circuit twice as large as the one obtained by the best existing method, we accelerate the computation by orders of magnitude.

cs.ET↗
arXiv2019

Realizability in the Unitary Sphere

In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.

cs.LO↗
arXiv2018

From Symmetric Pattern-Matching to Quantum Control (Extended Version)

One perspective on quantum algorithms is that they are classical algorithms having access to a special kind of memory with exotic properties. This perspective suggests that, even in the case of quantum algorithms, the control flow notions of sequencing, conditionals, loops, and recursion are entirely classical. There is however, another notion of control flow, that is itself quantum. The notion of quantum conditional expression is reasonably well-understood: the execution of the two expressions becomes itself a superposition of executions. The quantum counterpart of loops and recursion is however not believed to be meaningful in its most general form. In this paper, we argue that, under the right circumstances, a reasonable notion of quantum loops and recursion is possible. To this aim, we first propose a classical, typed, reversible language with lists and fixpoints. We then extend this language to the closed quantum domain (without measurements) by allowing linear combinations of terms and restricting fixpoints to structurally recursive fixpoints whose termination proofs match the proofs of convergence of sequences in infinite-dimensional Hilbert spaces. We additionally give an operational semantics for the quantum language in the spirit of algebraic lambda-calculi and illustrate its expressiveness by modeling several common unitary operations.

cs.LO↗
arXiv2017

The Vectorial $λ$-Calculus

We describe a type system for the linear-algebraic $λ$-calculus. The type system accounts for the linear-algebraic aspects of this extension of $λ$-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed $λ$-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.

cs.LO↗
arXiv2016

Concrete resource analysis of the quantum linear system algorithm used to compute the electromagnetic scattering cross section of a 2D target

We provide a detailed estimate for the logical resource requirements of the quantum linear system algorithm (QLSA) [Phys. Rev. Lett. 103, 150502 (2009)] including the recently described elaborations [Phys. Rev. Lett. 110, 250504 (2013)]. Our resource estimates are based on the standard quantum-circuit model of quantum computation; they comprise circuit width, circuit depth, the number of qubits and ancilla qubits employed, and the overall number of elementary quantum gate operations as well as more specific gate counts for each elementary fault-tolerant gate from the standard set {X, Y, Z, H, S, T, CNOT}. To perform these estimates, we used an approach that combines manual analysis with automated estimates generated via the Quipper quantum programming language and compiler. Our estimates pertain to the example problem size N=332,020,680 beyond which, according to a crude big-O complexity comparison, QLSA is expected to run faster than the best known classical linear-system solving algorithm. For this problem size, a desired calculation accuracy 0.01 requires an approximate circuit width 340 and circuit depth of order $10^{25}$ if oracle costs are excluded, and a circuit width and depth of order $10^8$ and $10^{29}$, respectively, if oracle costs are included, indicating that the commonly ignored oracle resources are considerable. In addition to providing detailed logical resource estimates, it is also the purpose of this paper to demonstrate explicitly how these impressively large numbers arise with an actual circuit implementation of a quantum algorithm. While our estimates may prove to be conservative as more efficient advanced quantum-computation techniques are developed, they nevertheless provide a valid baseline for research targeting a reduction of the resource requirements, implying that a reduction by many orders of magnitude is necessary for the algorithm to become practical.

quant-ph↗
arXiv2014

Quipper: Concrete Resource Estimation in Quantum Algorithms

Despite the rich literature on quantum algorithms, there is a surprisingly small amount of coverage of their concrete logical design and implementation. Most resource estimation is done at the level of complexity analysis, but actual concrete numbers (of quantum gates, qubits, etc.) can differ by orders of magnitude. The line of work we present here is a formal framework to write, and reason about, quantum algorithms. Specifically, we designed a language, Quipper, with scalability in mind, and we are able to report actual resource counts for seven non-trivial algorithms found in the quantum computer science literature.

cs.PL↗
arXiv2014

Quantum Oracles in Constant Depth with Measurement-Based Quantum Computation

This paper shows that, in measurement-based quantum computation, it is possible to write any quantum oracle implementing a classical function in constant depth. The result is shown through the equivalence between MBQC and the circuit model where arbitrary rotations along $Z$ axis and unbounded fan-outs are elementary operations. A corollary of this result is that disjunction can be implemented exactly in constant-depth, answering an open question of Høyer and Špalek.

quant-ph↗
arXiv2014

Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is described, and several examples based on Church numerals are presented.

cs.LO↗