ترغب بنشر مسار تعليمي؟ اضغط هنا

QUANTIFY: A framework for resource analysis and design verification of quantum circuits

140   0   0.0 ( 0 )
 نشر من قبل Alexandru Paler
 تاريخ النشر 2020
والبحث باللغة English




اسأل ChatGPT حول البحث

Quantum resource analysis is crucial for designing quantum circuits as well as assessing the viability of arbitrary (error-corrected) quantum computations. To this end, we introduce QUANTIFY, which is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind, and it includes the necessary methods to handle Toffoli+H and more generalised controlled quantum gates, too. Key features of QUANTIFY include: (1) analysis and optimisation methods which are compatible with the surface code, (2) choice between different automated (mixed polarity) Toffoli gate decompositions, (3) semi-automatic quantum circuit rewriting and quantum gate insertion methods that take into account known gate commutation rules, and (4) novel optimiser types that can be combined with different verification methods (e.g. truth table or circuit invariants like number of wires). For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits. Experimental results show that the frameworks performance scales to circuits with thousands of qubits.



قيم البحث

اقرأ أيضاً

100 - Gilad Gour , Andreas Winter 2019
We show that the generalization of the relative entropy of a resource from states to channels is not unique, and there are at least six such generalizations. We then show that two of these generalizations are asymptotically continuous, satisfy a vers ion of the asymptotic equipartition property, and their regularizations appear in the power exponent of channe
Despite the pursuit of quantum advantages in various applications, the power of quantum computers in neural network computations has mostly remained unknown, primarily due to a missing link that effectively designs a neural network model suitable for quantum circuit implementation. In this article, we present the co-design framework, namely QuantumFlow, to provide such a missing link. QuantumFlow consists of novel quantum-friendly neural networks (QF-Nets), a mapping tool (QF-Map) to generate the quantum circuit (QF-Circ) for QF-Nets, and an execution engine (QF-FB). We discover that, in order to make full use of the strength of quantum representation, it is best to represent data in a neural network as either random variables or numbers in unitary matrices, such that they can be directly operated by the basic quantum logical gates. Based on these data representations, we propose two quantum friendly neural networks, QF-pNet and QF-hNet in QuantumFlow. QF-pNet using random variables has better flexibility, and can seamlessly connect two layers without measurement with more qbits and logical gates than QF-hNet. On the other hand, QF-hNet with unitary matrices can encode 2^k data into k qbits, and a novel algorithm can guarantee the cost complexity to be O(k^2). Compared to the cost of O(2^k)in classical computing, QF-hNet demonstrates the quantum advantages. Evaluation results show that QF-pNet and QF-hNet can achieve 97.10% and 98.27% accuracy, respectively. Results further show that for input sizes of neural computation grow from 16 to 2,048, the cost reduction of QuantumFlow increased from 2.4x to 64x. Furthermore, on MNIST dataset, QF-hNet can achieve accuracy of 94.09%, while the cost reduction against the classical computer reaches 10.85x. To the best of our knowledge, QuantumFlow is the first work to demonstrate the potential quantum advantage on neural network computation.
We provide evidence that commonly held intuitions when designing quantum circuits can be misleading. In particular we show that: a) reducing the T-count can increase the total depth; b) it may be beneficial to trade CNOTs for measurements in NISQ cir cuits; c) measurement-based uncomputation of relative phase Toffoli ancillae can make up to 30% of a circuits depth; d) area and volume cost metrics can misreport the resource analysis. Our findings assume that qubits are and will remain a very scarce resource. The results are applicable for both NISQ and QECC protected circuits. Our method uses multiple ways of decomposing Toffoli gates into Clifford+T gates. We illustrate our method on addition and multiplication circuits using ripple-carry. As a byproduct result we show systematically that for a practically significant range of circuit widths, ripple-carry addition circuits are more resource efficient than the carry-lookahead addition ones. The methods and circuits were implemented in the open-source QUANTIFY software.
142 - Mingsheng Ying 2021
In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are m odelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); (iii) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.
A major hurdle to the deployment of quantum linear systems algorithms and recent quantum simulation algorithms lies in the difficulty to find inexpensive reversible circuits for arithmetic using existing hand coded methods. Motivated by recent advanc es in reversible logic synthesis, we synthesize arithmetic circuits using classical design automation flows and tools. The combination of classical and reversible logic synthesis enables the automatic design of large components in reversible logic starting from well-known hardware description languages such as Verilog. As a prototype example for our approach we automatically generate high quality networks for the reciprocal $1/x$, which is necessary for quantum linear systems algorithms.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا