Runtime Verification

This document describes how the MQT Debugger can be used to verify the correctness of quantum programs at runtime on real quantum computers. This is achieved by splitting the program into multiple slices based on the assertions and then translating the assertions into a set of measurements that are performed on the quantum device. After running the program and collecting measurement outcomes, the results can be passed to the MQT Debugger once again to check whether the assertions are satisfied.

Translating assertion programs into executable slices is done by the SimulationState::compile method. However, Python bindings and a full Python framework are available to automate this process. The remainder of this document will focus on the Python framework and its usage. For further information, please refer to @rovara2025runtimeverification.

Run Preparation

This process prepares a quantum program, given in OpenQASM format with equality and superposition assertions, for execution on a quantum device. This is done by translating each assertion in the program into a set of measurements that can be performed on the quantum device. As measurements may collapse the quantum state, execution cannot continue after such a newly introduced measurement in all cases. Therefore, the program is split into multiple slices, each containing a set of translated assertions and the instructions that are executed before them. By only collecting assertions with measurements that do not interfere with each other in the same slice, the program can be executed on a quantum device without any issues.

The run preparation method also applies slice optimization to reduce the overhead introduced by these slices. This is done by specifically searching for assertions that are compatible with each other and can be executed in the same slice. The more assertions can be executed in the same slice, the less overhead is introduced by the slicing process.

Run preparation is done by executing the mqt.debugger.check module with the prepare option, using:

python -m mqt.debugger.check prepare ...

Additionally, the prepare option requires the path to the OpenQASM file containing the quantum program. After execution, a new directory will be created that contains all generated slices as individual OpenQASM files. The path to this directory can be specified using the --output option.

An example execution command is:

python -m mqt.debugger.check prepare my_program.qasm --output slices

Verification

The generated slices should be executed on a quantum computer over multiple shots. The larger the number of shots, the more accurate the results will be. The result of this execution should be stored in a single json file for each slice that contains a list of dictionaries with one entry per shot. The dictionaries should map the names of all measured qubits to their measurement outcomes. An example of such a file is:

[
  {
    "test_q0": 0,
    "test_q1": 1,
    "test_q2": 0
  },
  {
    "test_q0": 0,
    "test_q1": 1,
    "test_q2": 1
  }
  // ...
]

For each slice, verification can then be performed by executing the mqt.debugger.check module with the check option, using:

python -m mqt.debugger.check check ...

The check option requires the path to the json file containing the measurement results. It also requires the path to the slices generated by the run preparation through the --dir option. The index of the specific slice to be verified should be specified using the --slice option.

The verification procedure also takes noise-conditions of the quantum device into account. To accurately investigate the results in the presence of noise, the --calibration option allows the user to specify a calibration file. The calibration file, given in json format, contains device-specific error data that is used during verification. An example of such a file with all supported fields is given here:

{
  "error_rate_1q": 0.001,
  "error_rate_2q": 0.01,
  "error_rate_measurement": 0.01,
  "specific_gate_errors": {
    "cx": 0.001,
    "rx": 0.0001
  }
}

As the framework uses statistical tests to verify the results, the -p argument can be used to specify a p-value threshold. Assertions are considered failed only if the p-value computed by the verification procedure is below this threshold.

A full example command for verification is:

python -m mqt.debugger.check --calibration calibration.json check --dir slices --slice 1 --p-value 0.05 results.json

Shot Estimation

Using a device calibration and a program containing assertions, the verification framework can also attempt to estimate a sufficient number of shots to be performed for good results. While this is only an estimate, it can help to reduce the resources needed for the verification process.

This is done by executing the mqt.debugger.check module with the shots option, using:

python -m mqt.debugger.check shots ...

This method requires a quantum program containing translated assertions to be passed as an argument. Importantly, this program should be the starting program after the run preparation step. This is because different slices might require more or fewer shots. Once again, the --calibration option is used to specify the calibration file and the -p option can be used to specify a p-value threshold.

Shot estimation is performed by running a set number of simulated trials. The number of trials can be specified using the --trials option. Once a number of shots is found that reaches the desired p-value threshold in a large enough fraction of trials, the process stops and the number of shots is printed. The desired fraction of trials that should reach the p-value threshold can be specified using the --accuracy option.

A full example command for shot estimation is:

python -m mqt.debugger.check --calibration calibration.json shots my_program.qasm --trials 1000 --accuracy 0.95 -p 0.05