Quantum program validation
The main principle behind software testing is to verify the runtimes of the expected system properties. These program validation and verification techniques cannot simply be transposed to quantum programs, however. Because of the physics at work inside quantum computers, the value of a unit of data cannot be read at runtime without destroying it. The non-deterministic nature of quantum computing also makes scaling up test strategies impossible. Therefore, for any future quantum programming scenario to be realistic, new and innovative code verification methods will have to be developed.
Over the past several years, CEA-List has been developing a formal-proof-based quantum program verification tool called Qbricks. In Qbricks, a quantum program’s expected specifications can be written explicitly. The tool’s automated and interactive proof features provide verification that the program behaves according to specifications on all possible input data.
Extending the analysis to hybrid programming
Our most recent research focuses on extending this principle to hybrid programs, in which classical and quantum data interact.
There is abundant research on hybrid computing in the literature. The quantum variational eigensolver (QVE) algorithm and other algorithms that combine classical and quantum computing components or that embed quantum computing in classical structures have been amply studied.
In addition, in the general case, the quantum phase estimation (QPE) algorithm, Shor’s quantum factoring algorithm, and most other purely quantum algorithms perform better when broken down into simpler components and hybridized. In large-scale quantum computing, even purely quantum primitives are implemented in a hybrid manner—a prerequisite for error detection and correction.
We started by extending equivalency verification—crucial to validating program compilation and optimization from purely quantum computing to different classes of hybrid computing.
To address the general case, however, the symbolic program representation system used in Qbricks will need to be overhauled. This research is ongoing and encouraging results have been obtained on symbolic circuit execution experiments.
New code verification and debugging methods will be required for any realistic future quantum programming scenario
