An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.

Saved in:
Bibliographic Details
Title: An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
Authors: Chen, Yu-Fang1 (AUTHOR) yfc@iis.sinica.edu.tw, Chung, Kai-Min1 (AUTHOR) kmchung@iis.sinica.edu.tw, Lengál, Ondřej2 (AUTHOR) lengal@fit.vut.cz, Lin, Jyun-Ao3 (AUTHOR) jyalin@gmail.com, Tsai, Wei-Lun1,4 (AUTHOR) alan23273850@gmail.com, Yen, Di-De5 (AUTHOR) bottlebottle13@gmail.com
Source: Communications of the ACM. Jun2025, Vol. 68 Issue 6, p85-93. 9p.
Subjects: Quantum computing, Machine theory, Scalability, Qubits, Quantum gates
Abstract: As quantum computing progresses, scalable and precise verification of quantum circuits becomes essential. This work introduces an automata-based framework that uses tree automata to represent quantum state sets and applies transformers to model gate semantics. A prototype tool based on this framework successfully verified circuits with up to 320 qubits, outperforming existing tools. The approach also connects quantum verification with automata theory, suggesting new directions for applying formal methods in quantum computing.
Database: Engineering Source
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 185687578
AccessLevel: 6
PubType: Periodical
PubTypeId: serialPeriodical
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Chen%2C+Yu-Fang%22">Chen, Yu-Fang</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> yfc@iis.sinica.edu.tw</i><br /><searchLink fieldCode="AR" term="%22Chung%2C+Kai-Min%22">Chung, Kai-Min</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> kmchung@iis.sinica.edu.tw</i><br /><searchLink fieldCode="AR" term="%22Lengál%2C+Ondřej%22">Lengál, Ondřej</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> lengal@fit.vut.cz</i><br /><searchLink fieldCode="AR" term="%22Lin%2C+Jyun-Ao%22">Lin, Jyun-Ao</searchLink><relatesTo>3</relatesTo> (AUTHOR)<i> jyalin@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Tsai%2C+Wei-Lun%22">Tsai, Wei-Lun</searchLink><relatesTo>1,4</relatesTo> (AUTHOR)<i> alan23273850@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Yen%2C+Di-De%22">Yen, Di-De</searchLink><relatesTo>5</relatesTo> (AUTHOR)<i> bottlebottle13@gmail.com</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Communications+of+the+ACM%22">Communications of the ACM</searchLink>. Jun2025, Vol. 68 Issue 6, p85-93. 9p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Quantum+computing%22">Quantum computing</searchLink><br /><searchLink fieldCode="DE" term="%22Machine+theory%22">Machine theory</searchLink><br /><searchLink fieldCode="DE" term="%22Scalability%22">Scalability</searchLink><br /><searchLink fieldCode="DE" term="%22Qubits%22">Qubits</searchLink><br /><searchLink fieldCode="DE" term="%22Quantum+gates%22">Quantum gates</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: As quantum computing progresses, scalable and precise verification of quantum circuits becomes essential. This work introduces an automata-based framework that uses tree automata to represent quantum state sets and applies transformers to model gate semantics. A prototype tool based on this framework successfully verified circuits with up to 320 qubits, outperforming existing tools. The approach also connects quantum verification with automata theory, suggesting new directions for applying formal methods in quantum computing.
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=185687578
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1145/3725728
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 9
        StartPage: 85
    Subjects:
      – SubjectFull: Quantum computing
        Type: general
      – SubjectFull: Machine theory
        Type: general
      – SubjectFull: Scalability
        Type: general
      – SubjectFull: Qubits
        Type: general
      – SubjectFull: Quantum gates
        Type: general
    Titles:
      – TitleFull: An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Chen, Yu-Fang
      – PersonEntity:
          Name:
            NameFull: Chung, Kai-Min
      – PersonEntity:
          Name:
            NameFull: Lengál, Ondřej
      – PersonEntity:
          Name:
            NameFull: Lin, Jyun-Ao
      – PersonEntity:
          Name:
            NameFull: Tsai, Wei-Lun
      – PersonEntity:
          Name:
            NameFull: Yen, Di-De
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 06
              Text: Jun2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 00010782
          Numbering:
            – Type: volume
              Value: 68
            – Type: issue
              Value: 6
          Titles:
            – TitleFull: Communications of the ACM
              Type: main
ResultId 1