Towards the Correctness of Quantum Program Implementation

Yan, Peng

Towards the Correctness of Quantum Program Implementation

Yan, Peng

Permalink

Publication Type:: Thesis
Issue Date:: 2024

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download thesisAdobe PDF (1.23 MB)

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Yan, Peng
dc.date.accessioned	2024-06-18T02:36:13Z
dc.date.available	2024-06-18T02:36:13Z
dc.date.issued	2024
dc.identifier.uri	http://hdl.handle.net/10453/179543
dc.description	University of Technology Sydney. Faculty of Engineering and Information Technology.	en_US.UTF-8
dc.description.abstract	With the rapid advancement of quantum computing hardware, numerous quantum programming languages are continually proposed to facilitate the implementation of quantum algorithms. This research focuses on enhancing the correctness of quantum programs from the perspective of formal verification, given the counter-intuitive nature of quantum mechanics and environmental noise challenges. Two formal verification approaches are explored to validate the correctness of quantum programs. The first approach extends classical incorrectness logic to the quantum domain, establishing a logical foundation for statically detecting bugs in quantum programming. The proposed quantum incorrectness logic is based on an intuitive explanation derived from a reachability standpoint. Based on under-approximation relations, the formulation of the incorrectness triple is found to be dual to quantum Hoare logic. The corresponding proof system is sound, complete, and decidable. The second approach introduces approximate quantum coupling as a key tool for studying relational reasoning in quantum programs. This novel proof system generalizes the widely used approximate probabilistic coupling in probabilistic programs, addressing an open question regarding projective predicates in quantum contexts. The application of approximate relational logic aids in assessing the robustness of quantum programs between ideal specifications and imperfect implementations. The practical utility of these approaches is demonstrated through case studies involving quantum teleportation, Grover's search, the repeat-until-success algorithm, the approximation of unitary gates, and the bit flip code. Notably, the formal verification of the low-depth approximation of the quantum Fourier transform is provided through approximate relational reasoning, showcasing the effectiveness of the proposed methodologies.	en_US.UTF-8
dc.format	Thesis (PhD)
dc.language.iso	en_US	en_US.UTF-8
dc.relation	https://opus.lib.uts.edu.au/bitstream/10453/179543/1/thesis.pdf
dc.rights	info:eu-repo/semantics/openAccess
dc.rights	The author owns the copyright in this thesis including all reproduction and reuse rights for the work. The work may not be altered without the permission of the copyright owner. Attribution is essential when quoting or paraphrasing from this thesis.
dc.rights	© 2024 Peng Yan
dc.rights	au.edu.uts.lib/cph
dc.title	Towards the Correctness of Quantum Program Implementation	en_US.UTF-8
dc.type	Thesis
utslib.copyright.status	open_access	*

Abstract:

With the rapid advancement of quantum computing hardware, numerous quantum programming languages are continually proposed to facilitate the implementation of quantum algorithms. This research focuses on enhancing the correctness of quantum programs from the perspective of formal verification, given the counter-intuitive nature of quantum mechanics and environmental noise challenges. Two formal verification approaches are explored to validate the correctness of quantum programs. The first approach extends classical incorrectness logic to the quantum domain, establishing a logical foundation for statically detecting bugs in quantum programming. The proposed quantum incorrectness logic is based on an intuitive explanation derived from a reachability standpoint. Based on under-approximation relations, the formulation of the incorrectness triple is found to be dual to quantum Hoare logic. The corresponding proof system is sound, complete, and decidable. The second approach introduces approximate quantum coupling as a key tool for studying relational reasoning in quantum programs. This novel proof system generalizes the widely used approximate probabilistic coupling in probabilistic programs, addressing an open question regarding projective predicates in quantum contexts. The application of approximate relational logic aids in assessing the robustness of quantum programs between ideal specifications and imperfect implementations. The practical utility of these approaches is demonstrated through case studies involving quantum teleportation, Grover's search, the repeat-until-success algorithm, the approximation of unitary gates, and the bit flip code. Notably, the formal verification of the low-depth approximation of the quantum Fourier transform is provided through approximate relational reasoning, showcasing the effectiveness of the proposed methodologies.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/179543