Approximate Relational Reasoning for Quantum Programs

Yan, P; Jiang, H; Yu, N

Approximate Relational Reasoning for Quantum Programs

Yan, P Jiang, H Yu, N

Permalink

Publisher:: Springer Nature
Publication Type:: Chapter
Citation:: Computer Aided Verification, 2024, 14683 LNCS, pp. 495-519
Issue Date:: 2024-01-01

Open Access

Copyright Clearance Process

Recently Added
In Progress
Open Access

This item is open access.

Adobe PDF

Download Published versionAdobe PDF (735.19 kB)

View on publisher's site

View statistics

Full metadata record

Field	Value	Language
dc.contributor.author	Yan, P
dc.contributor.author	Jiang, H
dc.contributor.author	Yu, N https://orcid.org/0000-0003-1188-3032
dc.date.accessioned	2024-09-02T04:48:26Z
dc.date.available	2024-09-02T04:48:26Z
dc.date.issued	2024-01-01
dc.identifier.citation	Computer Aided Verification, 2024, 14683 LNCS, pp. 495-519
dc.identifier.isbn	9783031656323
dc.identifier.uri	http://hdl.handle.net/10453/180588
dc.description.abstract	Quantum computation is inevitably subject to imperfections in its implementation. These imperfections arise from various sources, including environmental noise at the hardware level and the introduction of approximate implementations by quantum algorithm designers, such as lower-depth computations. Given the significant advantage of relational logic in program reasoning and the importance of assessing the robustness of quantum programs between their ideal specifications and imperfect implementations, we design a proof system to verify the approximate relational properties of quantum programs. We demonstrate the effectiveness of our approach by providing the first formal verification of the renowned low-depth approximation of the quantum Fourier transform. Furthermore, we validate the approximate correctness of the repeat-until-success algorithm. From the technical point of view, we develop approximate quantum coupling as a fundamental tool to study approximate relational reasoning for quantum programs, a novel generalization of the widely used approximate probabilistic coupling in probabilistic programs, answering a previously posed open question for projective predicates.
dc.language	en
dc.publisher	Springer Nature
dc.relation.ispartof	Computer Aided Verification
dc.relation.ispartofseries	Lecture Notes in Computer Science
dc.relation.isbasedon	10.1007/978-3-031-65633-0_22
dc.rights	info:eu-repo/semantics/openAccess
dc.subject.classification	Artificial Intelligence & Image Processing
dc.subject.classification	46 Information and computing sciences
dc.title	Approximate Relational Reasoning for Quantum Programs
dc.type	Chapter
utslib.citation.volume	14683 LNCS
pubs.organisational-group	University of Technology Sydney
pubs.organisational-group	University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	University of Technology Sydney/All Manual Groups
pubs.organisational-group	University of Technology Sydney/All Manual Groups/Centre for Quantum Software and Information (QSI)
pubs.organisational-group	University of Technology Sydney/All Manual Groups/Centre for Quantum Software and Information (QSI)/Associate Member
utslib.copyright.status	open_access	*
dc.rights.license	This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0). To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/
dc.date.updated	2024-09-02T04:48:25Z
pubs.publication-status	Published
pubs.volume	14683 LNCS

Abstract:

Quantum computation is inevitably subject to imperfections in its implementation. These imperfections arise from various sources, including environmental noise at the hardware level and the introduction of approximate implementations by quantum algorithm designers, such as lower-depth computations. Given the significant advantage of relational logic in program reasoning and the importance of assessing the robustness of quantum programs between their ideal specifications and imperfect implementations, we design a proof system to verify the approximate relational properties of quantum programs. We demonstrate the effectiveness of our approach by providing the first formal verification of the renowned low-depth approximation of the quantum Fourier transform. Furthermore, we validate the approximate correctness of the repeat-until-success algorithm. From the technical point of view, we develop approximate quantum coupling as a fundamental tool to study approximate relational reasoning for quantum programs, a novel generalization of the widely used approximate probabilistic coupling in probabilistic programs, answering a previously posed open question for projective predicates.

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

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