기술 요약: AutoQ 2.0: 양자 회로 검증에서 양자 프로그램 검증으로

1. 문제 정의

양자 프로그램은 분기와 루프와 같은 고전적 제어 흐름 구조를 통합함으로써 양자 회로를 확장합니다. 양자 회로 (AutoQ 1.0 의 영역) 는 게이트의 정적 시퀀스를 정의하는 데 충분하지만, 반복 - 성공 (RUS) 알고리즘 및 약측정 기반 그로버 검색과 같은 고급 양자 알고리즘은 큐비트 측정에서 얻은 고전적 값에 기반한 동적 제어가 필요합니다.

이러한 프로그램을 검증하는 것은 회로 전용 검증에는 존재하지 않는 상당한 도전을 제시합니다:

• 측정 및 정규화: 측정은 양자 상태를 붕괴시키고 제어 흐름을 주도하는 고전적 값 (0 또는 1) 을 생성합니다. 이 과정은 종종 확률 진폭의 정규화를 요구하며, 이는 형식적 추론을 복잡하게 만듭니다.
• 제어 흐름 추론: 루프와 분기를 검증하는 것은 측정 결과에 따라 진화하는 상태 공간을 처리해야 하며, 이는 기존 자동화 도구에게는 어려운 작업입니다.
• 자동화 도구의 부재: 고전적 프로그램용 (예: Dafny, KeY) 및 일부 양자용 (예: CoqQ, Qbricks) 연역적 검증 도구가 존재하지만, 이들은 완전한 자동화가 부족하거나 상당한 수동 노력 (예: 복잡한 에르미트 연산자 제공 또는 광범위한 증명 탐색) 을 요구합니다. 기존 자동화 도구는 주로 회로 동등성이나 특정 매개변수화된 프로그램에 초점을 맞추어 양자 프로그램의 제어 흐름에 대한 일반적인 지원을 결여하고 있습니다.

2. 방법론

AutoQ 2.0 은 이전 회로 검증 프레임워크를 확장하여 완전한 양자 프로그램을 지원함으로써 이러한 도전을 해결합니다. 핵심 방법론은 레벨 동기화 트리 오토마타 (LSTAs) 와 새로운 추론 테스트 (entailment testing) 접근법에 기반합니다.

2.1 형식 모델: 레벨 동기화 트리 오토마타 (LSTAs)

이 도구는 전제 조건, 사후 조건, 그리고 루프 불변식을 양자 상태 집합을 나타내는 LSTAs 로 표현합니다.

• 구조: LSTAs 는 양자 상태를 완벽한 이진 트리로 인코딩하도록 설계된 심볼릭 트리 오토마타로, 분기는 계산 기저 상태를 나타내고 잎은 복소수 확률 진폭을 나타냅니다.
• 동기화: LSTAs 의 핵심 특징은 "선택 (choice)" 메커니즘입니다. 동일한 트리 레벨에서의 전이는 공통 선택 집합을 공유해야 합니다. 이는 표준 트리 오토마타가 표현할 수 없는 얽힌 상태와 중첩을 LSTAs 가 간결하게 표현할 수 있게 하며, 오직 유효한 분기 조합 (공유 선택을 가진 것) 만 생성되도록 보장합니다.
• 입력 형식: 사용자는 유효한 양자 상태 집합을 인식하는 오토마타를 정의하는 .lsta 파일로 전제 조건, 사후 조건, 루프 불변식을 지정합니다.

2.2 검증 프레임워크

검증 과정은 자동화되며 연역적 스타일을 따릅니다:

1. 프로그램 실행: 도구는 전제 조건을 나타내는 LSTA 에 대해 양자 게이트 (예: $H$, $CX$, $T$) 를 실행합니다.
2. 측정 및 분기 처리:
   • 측정 $M_i = b$가 발생하면, LSTA 는 결과 $b=0$ 및 $b=1$에 해당하는 두 개의 복사본으로 분할됩니다.
   • 알고리즘은 일치하지 않는 분기의 확률 진폭을 0 으로 설정하여 트리를 업데이트합니다 (예: $M_1=0$인 경우, $x_1$ 아래의 $1$-서브트리의 진폭을 0 으로 설정).
   • 중요하게도, 도구는 이 단계에서 진폭을 정규화하지 않습니다. 실행 중 복잡한 산술 연산을 피하기 위해 원시 진폭을 보존하며, 정규화 검사는 최종 추론 테스트로 미룹니다.
   • 분기 문은 참과 거짓 경로에 대한 결과 LSTAs 를 계산한 후 그 합집합을 취함으로써 처리됩니다.
3. 루프 처리:
   • while 루프의 경우, 사용자는 LSTA 로서 루프 불변식을 제공해야 합니다.
   • 도구는 불변식이 귀납적인지 검증합니다: 이는 루프 전에 도달 가능한 모든 상태를 커버해야 하며, 불변식 (루프 계속 조건에 기반) 에 루프 본문을 실행한 결과 상태가 여전히 불변식에 의해 커버되어야 합니다.
   • 루프 종료 시의 상태는 루프 종료 조건에 기반한 불변식에 의해 과대 추정됩니다.
4. 추론 테스트 (스케일링까지):
   • 마지막 단계는 도달 가능한 상태 집합 (LSTA $R$로 표현됨) 이 사후 조건 (LSTA $Q$) 에 포함되는지 확인합니다.
   • 실행 중 정규화 인자가 무시되었으므로, 도구는 특수한 스케일링까지의 추론 (entailment up to scaling) ($|=_{uts}$) 관계를 사용합니다.
   • $A |=_{uts} B$는 $A$의 모든 트리가 $B$의 트리의 선형 스케일 버전인 경우 (즉, $T_A = r \cdot T_B$, 여기서 $r$은 0 이 아닌 스칼라) 성립합니다.
   • 이 검사는 LSTAs 를 레벨별로 탐색하여 상태와 항을 매핑하고, 최종적으로 글로벌 제약 조건을 만족하는 스케일링 인자 $r$의 존재를 검증하기 위해 SMT 솔버 (Z3) 를 호출하는 그래프 탐색 알고리즘을 사용하여 수행됩니다.

3. 주요 기여

• 양자 프로그램으로의 확장: AutoQ 2.0 은 루프와 분기를 포함하는 양자 프로그램에 대한 자동화된 연역적 검증을 제공하는 최초의 도구로, AutoQ 1.0 의 회로 전용 범위를 넘어섰습니다.
• 자동화된 측정 처리: 이 도구는 측정 결과에 기반하여 LSTAs 를 분할하고 수동 개입 없이 결과 상태 공간을 관리하는 알고리즘을 도입합니다.
• 정규화 없는 검증: 스케일링까지의 비정규화 상태로 작동하는 추론 테스트를 설계함으로써, 도구는 실행 단계에서 진폭을 정규화하는 계산적 복잡성을 피하여 효율성을 크게 향상시킵니다.
• LSTA 기반 불변식: 이 프레임워크는 LSTAs 를 사용하여 루프 불변식을 표현함으로써, 반복 알고리즘에 필요한 복잡한 양자 상태를 간결하게 표현할 수 있게 합니다.
• 확장성: LSTAs 의 간결성과 효율적인 SMT 해결을 활용하여 이 접근법은 보고된 벤치마크에서 최대 100 개의 큐비트를 가진 프로그램의 검증을 지원합니다.

4. 실험 결과

저자들은 AutoQ 2.0 을 두 가지 범주의 고급 양자 프로그램에 대해 평가했습니다:

1. 반복 - 성공 (RUS) 알고리즘: 비표준 양자 게이트 (예: $(2X + \sqrt{2}Y + Z)/\sqrt{7}$와 같은 특정 유니타리) 생성에 사용됩니다.
   • 결과: 모든 RUS 벤치마크가 즉시 (0.0 초) 검증되었습니다.
2. 약측정 기반 그로버 검색: 솔루션 수에 대한 사전 지식이 필요하지 않은 그로버 알고리즘의 변형입니다.
   • 결과: 도구는 약 11 초 (101 큐비트 사례의 경우) 에서 20 분 (초록에서 100 큐비트 사례에 대해 언급되었으나, 표에서는 101 큐비트에서 11 초로 나타남; 초록은 아마도 특정 구성을 참조하거나 설정 시간을 포함하는 것으로 보임) 내에 최대 100 개의 큐비트 (구체적으로 표에서는 101 큐비트) 를 가진 인스턴스를 성공적으로 검증했습니다. 검증 시간은 큐비트 및 게이트 수에 따라 합리적으로 확장됩니다.

실험은 AMD EPYC 7742 프로세서와 1,152 GiB RAM 이 장착된 서버에서 수행되었습니다.

5. 중요성 및 주장

이 논문은 AutoQ 2.0 이 현재 이러한 높은 수준의 자동화로 양자 프로그램을 검증할 수 있는 유일한 도구라고 주장합니다. 증명 보조기 (significant human effort 요구) 에 의존하거나 회로 동등성에만 초점을 맞추는 기존 도구와 달리, AutoQ 2.0 은 제어 흐름과 측정을 자동으로 처리함으로써 형식적 검증 이론과 실용적 양자 프로그래밍 간의 격차를 해소합니다.

저자들은 이 도구를 복잡한 양자 알고리즘의 형식적 검증으로 향하는 중요한 단계로 위치시키며, 단순한 양자 회로로 표현할 수 없는 프로그램에 대한 자동화된 연역적 검증이 가능함을 입증했습니다. 그들은 현재 구현이 중첩되지 않은 제어 흐름과 순수 상태를 처리하지만, 향후 작업은 불변식 생성 자동화와 더 복잡한 루프에서 발생하는 혼합 상태에 대한 지원 확장을 목표로 한다고 겸손하게 언급합니다.