신뢰할 수 있는 회로 최적화기

Aria는 런타임(omega-* 크레이트)을 같은 저장소에 함께 담고 있으므로, 이 글에서 다루는 내용은 모두 github.com/Anzaetek/aria-quantum-language-oss-public의 언어와 함께 배포됩니다.

세 개의 패스, 변화가 없을 때까지 반복

omega-core의 최적화기는 게이트 수가 더 줄지 않을 때까지 세 가지 작업을 반복합니다.

상쇄되는 것을 제거합니다. 같은 큐비트에 연속으로 적용된 두 자기 역원 게이트(H·H, X·X, CX·CX)를 제거하고, 항등 게이트와 각도가 0인 회전도 함께 제거합니다.
회전을 병합합니다. 같은 큐비트에서 같은 축을 중심으로 인접한 회전들은 각도를 합한 하나의 회전이 됩니다.
교환하여 둘 다 더 많이 만들어 냅니다. 대수적으로 허용되는 곳에서 단일 큐비트 게이트를 다중 큐비트 게이트 너머로 이동시켜, 다음 라운드에서 새로운 상쇄와 병합이 드러나게 합니다.

의도적으로 작게 만들었습니다. 무거운 최적화기가 주는 것의 대부분을 담아내면서도, 모든 규칙이 검증할 수 있을 만큼 단순합니다.

검사하고, 그다음 증명합니다

각 패스는 자신이 재작성하는 회로에 대한 단위 테스트를 갖고 있으며, 모든 예제 회로는 독립적인 오라클과 끝에서 끝까지 수치적으로 대조됩니다. 따라서 결과를 바꾸는 재작성이 있으면 테스트 스위트가 실패합니다. 상쇄 패스의 바탕이 되는 자기 역원 항등식(H, X, Y, Z, CNOT)은 Aria와 함께 배포되는 Lean 4 트리(proofs/lean4/QuantumProofs/Gates.lean)에서 증명되어 있으며, 다른 패스들이 의존하는 게이트 행렬과 회로 의미론도 그 옆에 있습니다.

런타임의 나머지 부분

같은 크레이트들이 최적화기와 나란히 놓인 다음 기능도 제공합니다.

기울기. 한 번의 패스로 파라미터 기울기를 구하는 정확한 adjoint 미분, 그리고 손실이 잡음이 많거나 미분 불가능할 때를 위한 CMA-ES.
동적 회로. 모든 백엔드에서의 회로 중간 측정, 조건부 게이트, 리셋. 리셋 의미론도 형식화되어 있습니다(ResetModel.lean).
관측량. 연산자 산술로 Pauli 합을 구성하고, 한 번의 시뮬레이션으로 여러 관측량을 동시에 평가합니다.

왜 중요한가

속도는 기본 조건입니다. 빠른 시뮬레이터는 많습니다. 런타임에 정말 필요한 것은 회로를 재작성해도 계산 결과가 조용히 바뀌지 않는다는 보장입니다. 테스트와 증명이 바로 그것을 위해 있습니다.