자료유형  

 학위논문

Control Number  

0017164274

International Standard Book Number  

9798384493778

Dewey Decimal Classification Number  

004

Main Entry-Personal Name  

Tao, Runzhou.

Publication, Distribution, etc. (Imprint  

[S.l.] : Columbia University., 2024

Publication, Distribution, etc. (Imprint  

Ann Arbor : ProQuest Dissertations & Theses, 2024

Physical Description  

143 p.

General Note  

Source: Dissertations Abstracts International, Volume: 86-04, Section: B.

General Note  

Advisor: Gu, Ronghui.

Dissertation Note  

Thesis (Ph.D.)--Columbia University, 2024.

Summary, Etc.  

요약Real applications of near-term quantum computing are around the corner and quantum software is a key component. Unlike classical computing, quantum software is under the threat of both quantum hardware errors and human bugs due to the unintuitiveness of quantum physics theory. Therefore, trustworthiness and reliability are critical for the success of quantum computation. However, most traditional methods to ensure software reliability, like testing, do not transfer to quantum at scale because of the destructive and probabilistic nature of quantum measurement and the exponential-sized state space.In this thesis, I introduce a series of frameworks to ensure the trustworthiness of quantum computing software by automated formal verification. First, I present Giallar, a fully-automated verification toolkit for quantum compilers to formally prove that the compiler is bug-free. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, I implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. The evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.Second, I introduce Gleipnir, an error analysis framework for quantum programs that enable scalable and adaptive verification of quantum error through the application of tensor networks. Giallar introduces the (\uD835\uDF0C, \uD835\uDEFF)-diamond norm, an error metric constrained by a quantum predicate consisting of the approximate state \uD835\uDF0C and its distance \uD835\uDEFF to the ideal state \uD835\uDF0C. This predicate (\uD835\uDF0C, \uD835\uDEFF) can be computed adaptively using tensor networks based on Matrix Product States. Giallar features a lightweight logic for reasoning about error bounds in noisy quantum programs, based on the (\uD835\uDF0C, \uD835\uDEFF)-diamond norm metric. The experimental results show that Giallar is able to efficiently generate tight error bounds for real-world quantum programs with 10 to 100 qubits, and can be used to evaluate the error mitigation performance of quantum compiler transformations.Finally, I present QSynth, a quantum program synthesis framework that synthesizes verified recursive quantum programs, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes 10 quantum unitary programs including quantum arithmetic programs, quantum eigenvalue inversion, quantum teleportation and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.

Subject Added Entry-Topical Term  

Computer science.

Subject Added Entry-Topical Term  

Quantum physics.

Subject Added Entry-Topical Term  

Theoretical physics.

Index Term-Uncontrolled  

Quantum software

Index Term-Uncontrolled  

Giallar

Index Term-Uncontrolled  

Qiskit compiler

Index Term-Uncontrolled  

Quantum programs

Added Entry-Corporate Name  

Columbia University Computer Science

Host Item Entry  

Dissertations Abstracts International. 86-04B.

Electronic Location and Access  

로그인을 한후 보실 수 있는 자료입니다.

Control Number  

joongbu:657962