기술 요약: ConQEC – 양자 오류 정정 코드 구현을 위한 컨콜릭 테스팅(Concolic Testing)

1. 문제 정의

양자 오류 정정 코드(QECC) 구현은 측정된 신드롬(syndrome)이 디코더 호출, 복구 동작 및 논리적 검사를 구동하는 하이브리드 소프트웨어-제어 시스템으로서 기능한다. 기존의 형식 검증 기술은 수학적 의무를 증명할 수 있고 일반적인 양자 테스팅은 최종 실패를 드러낼 수 있지만, 개발자들은 구체적인 결함을 생성하고 QECC 복구 경로가 참조 모델(reference)로부터 어느 지점에서 처음으로 벗어났는지 설명할 수 있는 확장 가능한 테스팅 워크플로우가 부족한 실정이다.

현재의 접근 방식들은 두 가지 주요 한계에 직면해 있다:

1. 확장성(Scalability): 일반적인 양자 컨콜릭 테스팅(예: QCT)은 진폭 기반 제약 모델에 의존한다. 양자 상태 공간을 추적하는 것은 물리 큐비트의 수에 따라 기하급적으로 증가하며, 이는 수천 개의 큐비트를 포함하는 현대적 구현(예: IBM의 Condor 프로세서)에 적용하기에는 불가능하다.
2. 진단 유용성(Diagnostic Utility): 기존 도구들은 종종 최종적인 논리적 실패(pass/fail)만을 보고한다. 이들은 구현체가 기대 동작으로부터 언제, 어디서 벗어났는지(신드롬 추출, 디코더 결정, 또는 복구 동작 중 어느 단계인지) 격리할 수 있는 재현 가능한 "목격자(witness)"를 제공하지 못한다.

2. 방법론: ConQEC 프레임워크

ConQEC는 QECC 구현을 위해 특별히 설계된 최초의 컨콜릭 테스팅 프레임워크이다. 이 프레임워크는 진폭 수준의 상태 추론에서 **심볼릭 복구 경로 제약(symbolic repair-path constraints)**으로 초점을 전환함으로써 확장성과 진단 요구 사항을 해결한다.

핵심 설계 원칙

• FSDR(Fault–Syndrome–Decoder–Recovery) 복구 경로: ConQEC는 테스트를 단순한 최종 결과가 아닌 단계별 실행 경로로 취급한다. 버그는 참조 계약(reference contract)에 대한 "쌍을 이룬 재현(paired replay)"을 통해 단계별 목격자를 생성한 후에만 버그로 인정된다.
• 복구 경로 수준의 심볼릭 인코딩: 진폭 수준의 시뮬레이션 대신, ConQEC는 다음을 심볼릭하게 인코딩한다:
  • 파울리 결함(Pauli Faults): 주입 지점에 대한 심볼릭 불리언 지표($\hat{f}_i$)로 표현된다.
  • 신드롬 서술어(Syndrome Predicates): 결함이 체크 비트를 어떻게 반전시키는지 나타내는 아핀 패리티 표현식($s_c(\hat{f}) = \beta_c \oplus \bigoplus \hat{f}_i$)으로 모델링된다.
  • 디코더 및 복구 관계(Decoder and Recovery Relations): 신드롬을 결정과 복구 동작으로 매핑하는 관계 $D(\sigma, d)$ 및 $R(\sigma, d, r)$로 모델링된다.
• 쌍을 이룬 재현(Paired Replay): 프레임워크는 솔버(SMT)를 통해 후보 파울리 결함을 생성한 후, 이를 구현체와 참조 계약 모두에서 구체적으로 실행한다. 커버리지와 버그 수용은 이 재현을 통해 결함의 효과를 검증하고 첫 번째 이탈 지점을 식별한 후에만 인정된다.

컨콜릭 루프(The Concolic Loop)

1. 심볼릭 생성: 시스템은 합법적인 결함 공간과 복구 경로 서술어에 대한 제약 모델을 구축한다. 특정 목표(예: 특정 신드롬 도달, 특정 디코더 분기 트리거, 또는 구현체와 참조 간의 차이 발견)를 타겟팅하기 위한 쿼리를 구성한다.
2. 후보 구체화(Candidate Materialization): 솔버는 심볼릭 결함 지표에 대한 값을 제공하여, 구체적인 파울리 결함(예: $X@q_0$)을 구체화한다.
3. 쌍을 이룬 검증: 구체화된 결함은 구현체와 참조 계약 상에서 각각 재현된다.
4. 목격자 구성: 재현 결과 실패($\omega = \text{FAIL}$) 또는 단계별 이탈($\delta \neq \perp$)이 발견되면, ConQEC는 FSDR 버그 목격자를 구성한다. 이 목격자에는 주입된 결함, 관찰된 신드롬, 디코더 결정, 복구 동작, 오라클 결과 및 가장 이른 이탈 단계가 포함된다.

버그 분류

ConQEC는 가장 이른 이탈 단계에 따라 버그를 다섯 가지 클래스로 국지화한다:

1. 신드롬 추출 오류: 잘못된 체크/검출기 값.
2. 측정 레지스터 오용: 오래되거나 뒤바뀐 레지스터 읽기.
3. 디코더 오디스패치(Misdispatch): 올바른 신드롬이 잘못된 디코더 암(arm)에 매핑됨.
4. 처리되지 않은 신드롬: 도달 가능한 신드롬이지만 핸들러가 없음.
5. 복구 계약 위반: 올바른 디코더 결정이 이루어졌으나 복구 적용이 잘못되었거나 최종 체크에 실패함.

3. 주요 기여

1. ConQEC 프레임워크: QECC 구현을 위해 설계된 최초의 컨콜릭 테스팅 프레임워크로, 테스트를 FSDR 복구 경로로 모델링하고 재현 기반의 목격자를 반환한다.
2. 확장 가능한 복구 경로 생성: 지수적인 진폭 수준의 추론을 피하는 심볼릭 인코딩 방법을 사용하여, 수천 개의 큐비트를 가진 QECC에 대해서도 타겟팅된 결함을 생성할 수 있게 한다.
3. 실증적 평가: 생성된 소스 레벨 QECC 패밀리(Repetition, Surface/Toric, Tanner/LDPC, Color codes) 및 공개 아티팩트(Tesseract, PyMatching)에 대한 포괄적인 평가를 통해, 시드된 버그를 탐지하고 대규모 시스템에서 결함 국지화 목격자를 제공하는 능력을 입증하였다.

4. 실험 결과

평가는 128 코어와 2.0 TiB 메모리를 갖춘 서버에서 QSE 백엔드와 Z3 솔버를 사용하여 수행되었다.

• 결함 국지화 (RQ1): ConQEC는 생성 예산 $B=4$에서 13개 설정 및 5개 버그 클래스에 걸친 195/195 실험 케이스의 시드된 버그를 성공적으로 국지화했다. 반면, 무작위 결함 테스팅은 동일한 예산에서 약 15.7/195개의 목격자만을 발견했으며, 일반적인 브랜치 순서 탐색은 0개를 발견했다. ConQEC는 최대 1,500개의 물리 큐비트를 가진 시스템에서도 결함을 국지화했다.
• 의미론적 커버리지 (RQ2): ConQEC는 "어려운" 안정기 의무(예: 두 결함이 서로 상쇄되는 페어 마스크 커버리지)를 커버하는 데 있어 무작위 테스팅을 크게 앞질렀다. $n=1000$ 큐비트에 대해, 무작위 테스팅은 0.10%의 커버리지를 보인 반면, ConQEC는 예산 $B=500$에서 페어 마스크 의무의 약 49.9%를 커버했다.
• 규모 및 비용 (RQ3): 프레임워크는 3,000 큐비트(Repetition code) 및 거리 $d=41$(Surface code)의 소스 레벨 캠페인까지 확장 가능했다. 주요 병목 지점은 SMT 솔빙/쿼리 생성이었으며, 쌍을 이룬 재현 단계는 전체 실행 시간의 0.004% 미만을 차지했다.
• 공개 아티팩트 적용 가능성 (RQ4): ConQEC는 Tesseract Stim 코퍼스와 PyMatching 회귀 테스트를 포함한 공개 아티팩트에서 재현 기반의 증거를 성공적으로 제시하였으며, 논리적 불일치와 디코더 경계 회귀를 식별해 냈다.

5. 의의 및 주장

본 논문은 ConQEC가 기존의 형식 검증 및 일반 양자 테스팅 도구가 제공할 수 없는 확장 가능하고 진단적인 테스팅 워크플로우를 제공한다고 주장한다.

• 개발자 중심의 디버깅: 재현 가능한 FSDR 목격자를 반환함으로써, ConQEC는 "블랙박스" 형태의 실패를 국지화된 디버깅 아티팩트로 변환한다(예: "신드롬 $(1,0)$에 대해 디코더가 $X@q_0$ 대신 $X@q_1$을 선택함").
• 확장성: 진폭 수준의 상태 추적을 추상화하고 신드로 디코딩 및 복구의 이산적 로직에 집중함으로써, ConQEC는 이론적인 QECC 검증과 수천 큐비트 시스템을 위한 실질적인 소프트웨어 테스팅 사이의 간극을 메운다.
• 상호 보완성: 저자들은 ConQEC가 형식 검증 도구(QSE 또는 QECV와 같은)와 상호 보완적이라고 규정한다. 형식 도구가 정확성을 증명한다면, ConQEC는 구현상의 버그를 위한 구체적인 테스트 케이스와 디버깅 증거를 생성하며, 대규모 소프트웨어 스택에 적합한 "예산 기반" 테스팅 프레임워크 내에서 작동한다.

본 논문은 자신의 심볼릭 모델이 노출된 서술어에 의존하며 전이 목표(transition objectives)를 위해 명시적인 디코더/복구 관계가 필요하다는 점을 인정하며 적절한 범위를 유지한다. 이는 모든 양자 소프트웨어 테스팅 문제를 해결하겠다는 것이 아니라, 특히 QECC 복구 파이프라인의 고유한 과제를 타겟팅하는 것이다.