읽을 수 있는 회로에서 기계가 검증한 정리까지

Aria는 회로를 Lean 4로 내보낼 수 있습니다. 그러면 프로그램에 대한 주장이 기계가 검사할 수 있는 정리가 됩니다. 증명 트리는 Aria 저장소 안의 proofs/lean4/QuantumProofs에 함께 배포되며, sorry가 없습니다. 즉 가정으로 남겨 둔 것이 하나도 없습니다.

무엇이 내보내지는가

회로에는 Assert, Prove, Ensures, Requires, Invariant, ResourceBound 같은 주석을 붙일 수 있습니다. aria export --lean은 회로와 주석을 다음 내용을 담은 Lean 파일로 바꿉니다.

• n개 큐비트 위의 정의로 표현된 회로,
• denote를 통한 유니터리 행렬로서의 의미,
• 주석 하나당 정리 하나.

인식되는 회로(Bell, GHZ, QFT, QPE, Grover)의 경우 내보낸 파일은 공유 트리에 대해 증명이 닫힙니다. 예를 들어 Generated/GateModel/Bell_Spec.lean은 Bell 쌍에 대해 aria export --gate-model이 출력하는 그대로이며, 실제로 증명됩니다.

가장 오래 걸린 증명들

한동안 이 정리 중 몇 개는 스텁이었습니다. 컴파일은 되지만 증명된 것은 없었습니다. 이들을 닫는 작업은 새로운 수학이 아니라 대부분 정리와 포장의 문제였습니다.

QFT는 유니터리입니다. 양자 푸리에 변환은 n차 단위근으로 만들어진 행렬이고, QFT.lean의 qft_correct는 회로가 정확히 그 행렬을 계산한다고 말합니다. 유니터리성은 항등식 하나로 귀결됩니다. ω^(jk)와 ω^(lk)의 공액을 곱해 k에 대해 합하면 j = l일 때 n, 그 외에는 0이 됩니다. 비대각 성분은 공비가 1이 아닌 등비급수이므로 합이 0이고, 대각 성분은 1이 n개 더해진 값입니다.

블록 인코딩. 블록 인코딩 정리는 예전에는 자리표시자였습니다. 이제는 실제 불변량을 서술합니다. 유니터리의 왼쪽 위 블록이 A/α를 ε 이내로 근사한다는 것이고, 덕분에 이후 블록 인코딩을 구성하는 패스들이 구체적으로 인용할 대상이 생겼습니다.

QPE와 Grover. 둘 다 증인(witness)이 필요했습니다. 위상 추정에는 k/2^n 형태의 위상, 탐색에는 Grover 각도 arcsin(1/√N)입니다. 증인 자체는 쉬웠습니다. 진짜 작업은 QFT 아래에서 위상이 일관되게 순환한다는 보조정리였고, 이는 위의 단위근 항등식에서 자연스럽게 따라 나왔습니다.

트리에 그 밖에 무엇이 있는가

내보낸 회로 외에도 같은 트리에서 런타임 자체의 일부를 형식화합니다. 게이트 행렬과 adjoint, 리셋 의미론, 스태빌라이저 모델, MPS 절단 오차, HHL과 QSVT 구조, 그리고 별도 글에서 다룬 양자 신호 처리의 정방향 정리와 역정리가 포함됩니다.

직접 써 보기

$ aria export examples/aria/bell.aria --circuit Bell --lean
$ cd proofs/lean4 && lake build

첫 명령은 Lean 파일을 쓰고, 두 번째 명령은 그것을 트리에 대해 검사합니다.