We present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilities for symbolic reasoning. The extension allows to specify relational properties, i.e., relationships between states before and after executing a circuit. We present a number of use cases where we used AutoQ to fully automatically verify crucial properties of several quantum circuits, which have, to the best of our knowledge, so far been proved only with human help.
CITATION STYLE
Chen, Y. F., Chung, K. M., Lengál, O., Lin, J. A., & Tsai, W. L. (2023). AutoQ: An Automata-Based Quantum Circuit Verifier. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13966 LNCS, pp. 139–153). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-37709-9_7
Mendeley helps you to discover research relevant for your work.