검출기 오류 모델 (DEM)을 위한 준선형 동치성 검사

검출기 오류 모델 (Detector Error Model, DEM)은 양자 회로 내 오류 메커니즘의 구조적 표현으로, 회로 수준에서 결함 허용성 (fault-tolerance)을 포착할 수 있는 능력 덕분에 양자 컴파일 파이프라인에서 인기를 얻고 있습니다. DEM은 검출기 (detectors) 및 관측 가능량 (observables)을 대상으로 하는 명령어로 오류 메커니즘을 나열하며, 각 물리적 결함 채널 (physical fault channel)에 대해 결함이 발생할 확률, 해당 결함이 트리거하는 검출기, 그리고 뒤집는 관측 가능량을 명시합니다. 본 논문에서 우리는 DEM을 위한 등식 이론 (equational theory)과 그와 관련된 범주론적 의미론 (categorical semantics)을 개발합니다. 우리는 Giry 모나드 (Giry monad) 상의 대칭 단항 이론 (symmetric monoidal theory, 즉 PROP)으로 정식화된, DEM 항 (terms)에 대한 건전하고 (sound), 종료되며 (terminating), 결합적인 (confluent) 재작성 시스템 (rewriting system)을 제시합니다. 우리는 모든 DEM 항이 고유한 정규형 (normal form)을 가짐을 증명하며, 이는 $|E|$를 명령어의 수로, $k$를 대상 집합의 크기를 제한하는 상수로 할 때 준선형 시간 $O(k|E|\log|E|)$ 내에 효율적으로 계산될 수 있습니다. 이는 구조적 DEM 동치성을 위한 (Tanner 그래프를 통한) 완전한 불변량 (invariants) 집합을 제공합니다. 우리는 엄격한 정확성 보증을 갖춘 DEM 동치성에 대한 최초의 정적 결정 절차 (static decision procedure)를 제공합니다. 이는 비적응형 (non-adaptive) 양자 오류 정정 (Quantum Error Correction, QEC) 파이프라인에 대해 완전하며 (전체 디코더 동치성을 정확하게 결정함), 지수적 오버헤드 없이 부분 적응형 (partially-adaptive) 회로 (격자 수술 (lattice surgery), 분산 QEC 등)에 대해서도 건전하고 적용 가능한 결정 절차로 확장됩니다. 우리는 양자 컴파일러의 검증 및 최적화에 대한 적용 방안을 논의합니다.