{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:11:54Z","timestamp":1773097914068,"version":"3.50.1"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Near-term quantum computers are expected to work in an environment where each operation is noisy, with no error correction. Therefore, quantum-circuit optimizers are applied to minimize the number of noisy operations. Today, physicists are constantly experimenting with novel devices and architectures. For every new physical substrate and for every modification of a quantum computer, we need to modify or rewrite major pieces of the optimizer to run successful experiments. In this paper, we present QUESO, an efficient approach for automatically synthesizing a quantum-circuit optimizer for a given quantum device. For instance, in 1.2 minutes, QUESO can synthesize an optimizer with high-probability correctness guarantees for IBM computers that significantly outperforms leading compilers, such as IBM's Qiskit and TKET, on the majority (85%) of the circuits in a diverse benchmark suite.<\/jats:p>\n          <jats:p>\n            A number of theoretical and algorithmic insights underlie QUESO: (1) An algebraic approach for representing rewrite rules and their semantics. This facilitates reasoning about complex\n            <jats:italic>symbolic<\/jats:italic>\n            rewrite rules that are beyond the scope of existing techniques. (2) A fast approach for probabilistically verifying equivalence of quantum circuits by reducing the problem to a special form of\n            <jats:italic>polynomial identity testing<\/jats:italic>\n            . (3) A novel probabilistic data structure, called a\n            <jats:italic>polynomial identity filter<\/jats:italic>\n            (PIF), for efficiently synthesizing rewrite rules. (4) A beam-search-based algorithm that efficiently applies the synthesized symbolic rewrite rules to optimize quantum circuits.\n          <\/jats:p>","DOI":"10.1145\/3591254","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"835-859","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":37,"title":["Synthesizing Quantum-Circuit Optimizers"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-2279-5816","authenticated-orcid":false,"given":"Amanda","family":"Xu","sequence":"first","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1841-9565","authenticated-orcid":false,"given":"Abtin","family":"Molavi","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1605-5383","authenticated-orcid":false,"given":"Lauren","family":"Pick","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4479-7413","authenticated-orcid":false,"given":"Swamit","family":"Tannu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4577-175X","authenticated-orcid":false,"given":"Aws","family":"Albarghouthi","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.2562111"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341953"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2022.1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.68.012318"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_6"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434321"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.318.13"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.100.032328"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/QCE49297.2020.00036"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52482-1_11"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604138"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434318"},{"key":"e_1_2_1_16_1","unstructured":"2022. Toronto. https:\/\/quantum-computing.ibm.com\/services\/resources?system=ibmq_toronto \t\t\t\t  2022. Toronto. https:\/\/quantum-computing.ibm.com\/services\/resources?system=ibmq_toronto"},{"key":"e_1_2_1_17_1","unstructured":"IonQ. 2022. IonQ Aria. https:\/\/ionq.com\/posts\/july-25-2022-ionq-aria-part-one-practical-performance \t\t\t\t  IonQ. 2022. IonQ Aria. https:\/\/ionq.com\/posts\/july-25-2022-ionq-aria-part-one-practical-performance"},{"key":"e_1_2_1_18_1","unstructured":"IonQ. 2022. IonQ Native Gates. https:\/\/ionq.com\/docs\/getting-started-with-native-gates \t\t\t\t  IonQ. 2022. IonQ Native Gates. https:\/\/ionq.com\/docs\/getting-started-with-native-gates"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359630"},{"key":"e_1_2_1_20_1","volume-title":"Pyzx: Large scale automated diagrammatic reasoning. arXiv preprint arXiv:1904.04735.","author":"Kissinger Aleks","year":"2019","unstructured":"Aleks Kissinger and John van de Wetering . 2019 . Pyzx: Large scale automated diagrammatic reasoning. arXiv preprint arXiv:1904.04735. Aleks Kissinger and John van de Wetering. 2019. Pyzx: Large scale automated diagrammatic reasoning. arXiv preprint arXiv:1904.04735."},{"key":"e_1_2_1_21_1","unstructured":"Aleks Kissinger and John van de Wetering. 2019. Reducing T-count with the ZX-calculus. arXiv preprint arXiv:1903.10477. \t\t\t\t  Aleks Kissinger and John van de Wetering. 2019. Reducing T-count with the ZX-calculus. arXiv preprint arXiv:1903.10477."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535841"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781156"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737965"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99498-7_12"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814075"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908109"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41534-018-0072-4"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527330"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507739"},{"key":"e_1_2_1_33_1","volume-title":"Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities. CoRR, abs\/2111.11387","author":"Pointing Jessica","year":"2021","unstructured":"Jessica Pointing , Oded Padon , Zhihao Jia , Henry Ma , Auguste Hirth , Jens Palsberg , and Alex Aiken . 2021 . Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities. CoRR, abs\/2111.11387 (2021). Jessica Pointing, Oded Padon, Zhihao Jia, Henry Ma, Auguste Hirth, Jens Palsberg, and Alex Aiken. 2021. Quanto: Optimizing Quantum Circuits with Automatic Generation of Circuit Identities. CoRR, abs\/2111.11387 (2021)."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.22331\/q-2018-08-06-79"},{"key":"e_1_2_1_35_1","unstructured":"PyZX. 2023. PyZX Full API documentation. https:\/\/pyzx.readthedocs.io\/en\/latest\/api.html#pyzx.optimize.phase_block_optimize \t\t\t\t  PyZX. 2023. PyZX Full API documentation. https:\/\/pyzx.readthedocs.io\/en\/latest\/api.html#pyzx.optimize.phase_block_optimize"},{"key":"e_1_2_1_36_1","unstructured":"Google Quantum-AI. 2021. Quantum Computer Datasheet. (Accessed on 11\/22\/2021). \t\t\t\t  Google Quantum-AI. 2021. Quantum Computer Datasheet. (Accessed on 11\/22\/2021)."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.287.17"},{"key":"e_1_2_1_38_1","unstructured":"Rigetti. 2022. Rigetti Aspen-11. https:\/\/www.rigetti.com \t\t\t\t  Rigetti. 2022. Rigetti Aspen-11. https:\/\/www.rigetti.com"},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Mark Saffman. 2019. The next step in making arrays of single atoms. \t\t\t\t  Mark Saffman. 2019. The next step in making arrays of single atoms.","DOI":"10.1038\/d41586-019-00935-y"},{"key":"e_1_2_1_40_1","volume-title":"Souper: A synthesizing superoptimizer. arXiv preprint arXiv:1711.04422.","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas , Yang Chen , Peter Collingbourne , Jeroen Ketema , Gratian Lup , Jubi Taneja , and John Regehr . 2017 . Souper: A synthesizing superoptimizer. arXiv preprint arXiv:1711.04422. Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. 2017. Souper: A synthesizing superoptimizer. arXiv preprint arXiv:1711.04422."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.69.062321"},{"key":"e_1_2_1_42_1","unstructured":"Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W Cross Frederic T Chong and Ronghui Gu. 2019. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arXiv preprint arXiv:1908.08963. \t\t\t\t  Yunong Shi Runzhou Tao Xupeng Li Ali Javadi-Abhari Andrew W Cross Frederic T Chong and Ronghui Gu. 2019. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arXiv preprint arXiv:1908.08963."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab8e92"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1088\/2058-9565\/ab9acb"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2931037.2931074"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523431"},{"key":"e_1_2_1_47_1","volume-title":"PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated Corrections. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Wang Haojie","year":"2021","unstructured":"Haojie Wang , Jidong Zhai , Mingyu Gao , Zixuan Ma , Shizhi Tang , Liyan Zheng , Yuanzhi Li , Kaiyuan Rong , Yuanyong Chen , and Zhihao Jia . 2021 . PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated Corrections. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21) . USENIX Association, 37\u201354. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/wang Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. 2021. PET: Optimizing Tensor Programs with Partially Equivalent Transformations and Automated Corrections. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 37\u201354. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/wang"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1038\/nature25766"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41586-021-03557-5"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_1_51_1","unstructured":"Amanda Xu Abtin Molavi Lauren Pick Swamit Tannu and Aws Albarghouthi. 2022. Synthesizing Quantum-Circuit Optimizers. arxiv:cs.PL\/2211.09691. \t\t\t\t  Amanda Xu Abtin Molavi Lauren Pick Swamit Tannu and Aws Albarghouthi. 2022. Synthesizing Quantum-Circuit Optimizers. arxiv:cs.PL\/2211.09691."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7809285"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523433"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591254","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591254","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591254"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":53,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591254"],"URL":"https:\/\/doi.org\/10.1145\/3591254","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}