AutoQ

KO | EN

gitlite — search

#hacktoberfest #ai #llm #rust #linux #macos #windows #cli #kubernetes #vue #pytorch #security #ios #open-source

(★ 29)

No description available.

AutoQ Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# AutoQ 2.0: An automata-based C++ tool for quantum program verification.

AutoQ 2.0 is a command-line utility written in C++ for verifying partial correctness of quantum programs automatically based on non-deterministic finite tree automata (NFTA) along with the concept of Hoare-style proof systems.

Consider a triple \{ $P$ \} $C$ \{ $Q$ \}, where $P$ and $Q$ are the pre- and post-condition recognizing sets of pure quantum states and $C$ is a quantum program. Note that we don't consider mixed states in this work. Let $\mathcal L(x)$ denote the language (set) of all quantum states satisfying the condition $x$ and $C(L)$ denote the output set of quantum states generated by the quantum program $C$ transforming the initial set of quantum states $L$. Then essentially, AutoQ 2.0 simply checks whether each quantum state in $\mathcal L(P)$ reaches some state in $\mathcal L(Q)$ *up to a nonzero complex factor* after being transformed by the program $C$, i.e., whether $\forall \ket{s} \in C(\mathcal L(P)),\ \exists c\in\mathbb C\setminus\\{0\\}$ such that $c\ket{s}\in \mathcal L(Q)$. We may denote it by $C(\mathcal L(P)) \subseteq_{uts} \mathcal L(Q)$, where $uts$ is short for up to scaling.

The following is a simple illustration of the usage.
```
OPENQASM 3;
include "stdgates.inc";
qubit[2] qb; // quantum bits

//    L(P): {|00>, 0.5|00> + 0.5|01> + 0.5|10> + 0.5|11>}
x qb[0];
//          {|10>, 0.5|10> + 0.5|11> + 0.5|00> + 0.5|01>}
x qb[1];
//          {|11>, 0.5|11> + 0.5|10> + 0.5|01> + 0.5|00>}
h qb[1];
// C(L(P)): {|10>/√2 - |11>/√2, |10>/√2 + |00>/√2}
/******************************************************/
//  L(Q_1): {|10>/√2 - |11>/√2, |10>/√2 + |00>/√2} -> pass
//  L(Q_2): {|10>/√2 - |11>/√2, |10>/√2 - |00>/√2} -> fail
```
The program starts from an initial set of quantum states $\mathcal L(P)$. Immediately after executing each gate, AutoQ 2.0 computes the resulting transformation of the quantum states and stores it for use by the next gate. At the end of the quantum program, AutoQ 2.0 checks whether the set $\mathcal L(Q)$ contains the set $C(\mathcal L(P))$. In the above example, if we take the postcondition $Q_1$ such that $\mathcal L(Q_1) = C(\mathcal L(P))$, the verification passes. If we take another postcondition $Q_2$ such that there is some quantum state $\ket{10}/\sqrt2 + \ket{00}/\sqrt2 \in C(\mathcal L(P))$ but $\not\in \mathcal L(Q_2)$, the verification fails.

Please see the introductory [video](https://www.youtube.com/watch?v=1pO6bBvEaLM) for more examples on its usage. You can also check the folder ![benchmarks](https://raw.githubusercontent.com/fmlab-iis/AutoQ/main/benchmarks) for all the files used to produce the experimental results.

---

## Installation and Compilation

Currently, for Linux (Ubuntu/Debian), macOS, and WSL2, the dependency of AutoQ can be built with the command `./install-dependencies.sh`. If you want to use a system-installed Z3 instead of the bundled library, change `option(USE_SYSTEM_Z3 ... OFF)` to `ON` in the top-level `CMakeLists.txt` before building. After the configuration, please run the following command.
```
make
make test
```
The first command `make` compiles the source code with compiler optimizations enabled, while the second command `make test` runs several unit tests to verify the correctness of the implementation. Under normal circumstances, you should see 12 green check marks on the `Commits` page for the latest commit. This indicates that the continuous integration (CI) workflow in GitHub Actions has verified that both `make` and `make debug` produce no errors and that `make test` passes successfully on Ubuntu, macOS, and WSL2.

If you need to compile the library for debugging, you can replace `make` with `make debug`.

---

## Command-Line Execution
The following help message lists four modes, each of which can be accessed by typing its corresponding subcommand. Each subcommand also provides its own usage instructions via the `-h` option.
```
$ ./build/cli/autoq -h
AutoQ 2.0: An automata-based C++ tool for quantum program verification.
Usage: autoq [OPTIONS] [SUBCOMMAND]

Options:
  -h,--help                   Print this help message and exit.
  -v,--version                Print the full Git commit hash ID.

Subcommands:
  ex                          Execute a quantum circuit with a given precondition.
  ver                         Verify the execution result against a given postcondition.
  eq                          Check equivalence of two given quantum circuits.
  print                       Print the set of quantum states.
```

The most frequently used mode in our papers is `ver` for verifying quantum programs.
```
$ ./build/cli/autoq ver -h
Verify the execution result against a given postcondition.
Usage: autoq ver [OPTIONS] pre.hsl circuit.qasm post.hsl

Positionals:
  pre.hsl                     the precondition file
  circuit.qasm                the OpenQASM 2.0 or 3.0 circuit file
  post.hsl                    the postcondition file

Options:
  -h,--help                   Print this help message and exit.
  --loopsum                   Summarize loops using symbolic execution.
  -l,--latex                  Print the statistics for tables in LaTeX.
```
One noteworthy feature of this tool is its support for loop summarization in circuits that use the specific syntax `for int i in [x:y] { C }`, as described in the [QASM format documentation](./docs/qasm_description.md). To enable the loop summarization algorithm, include the `--loopsum` flag when using the `ex` or `ver` subcommands.

This is one example usage.
```
$ ./build/cli/autoq ver benchmarks/all/Grover/03/pre.hsl benchmarks/all/Grover/03/circuit.qasm benchmarks/all/Grover/03/post.hsl
The quantum program has [5] qubits and [52] gates. The verification process [OK] in [0.1s] with [77MB] memory usage.
```

---

## Input File Formats

* Quantum States 
Preconditions, postconditions, and loop invariants are all sets of quantum states. We use the `*.hsl` format (short for high-level specification language) which extends Dirac notation to describe sets of quantum states. The detailed grammar is described in the [hsl format description](./docs/hsl_description.md).

* Quantum Programs 
Our program currently supports $X$, $Y$, $Z$, $H$, $T$, $T^\dagger$, $S$, $S^\dagger$, $R_x(\pi/2)$, $R_y(\pi/2)$, $CX$, $CZ$, $CCX$, $SWAP$ quantum gates. The supported version of OpenQASM can be 2.0 or 3.0, but the supported syntax is very limited. Please refer to the [qasm format description](./docs/qasm_description.md) for more details.

---

## Citation
Please cite the following papers if you use this tool for your research.

* <summary>
 <a href="https://dl.acm.org/doi/10.1145/3704868">P. A. Abdulla, Y.-G. Chen, Y.-F. Chen, L. Holík, O. Lengál, J.-A. Lin, F.-Y. Lo, and W.-L. Tsai, “Verifying Quantum Circuits with Level-Synchronized Tree Automata,” in Proceedings of the ACM on Programming Languages 9 (POPL), 2025, pp. 923–953.</a>
</summary>

```bibtex
@article{10.1145/3704868,
  title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata},
  author = {Abdulla, Parosh Aziz and Chen, Yo-Ga and Chen, Yu-Fang and Hol\'{\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej and Lin, Jyun-Ao and Lo, Fang-Yi and Tsai, Wei-Lun},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {POPL},
  year = {2025},
  pages = {923--953},
  doi = {10.1145/3704868}
}
```

* <summary>
 <a href="https://link.springer.com/chapter/10.1007/978-3-031-90660-2_5">Y.-F. Chen, K.-M. Chen, M.-H. Hsieh, W.-J. Huang, O. Lengál, J.-A. Lin, and W.-L. Tsai, “AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2025, pp. 87–108</a>
</summary>

```bibtex
@InProceedings{10.1007/978-3-031-90660-2_5,
  author = {Chen, Yu-Fang and Chung, Kai-Min and Hsieh, Min-Hsiu and Huang, Wei-Jia and Leng{\'a}l, Ond{\v{r}}ej and Lin, Jyun-Ao and Tsai, Wei-Lun},
  booktitle = {International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
  title = {AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs},
  year = {2025},
  pages = {87--108},
  doi = {10.1007/978-3-031-90660-2_5}
}
```

---

## Contact

If you have any questions or suggestions, feel free to [create an issue](https://github.com/fmlab-iis/AutoQ/issues) or contact us via alan23273850@gmail.com.

AutoQ

AutoQ Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

AutoQ

AutoQ Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README