Aria 오픈소스 공개: 하나의 언어, 모든 모달리티

Aria는 Apache-2.0 라이선스의 오픈소스로 github.com/Anzaetek/aria-quantum-language-oss-public에 공개되어 있습니다. 자체 CLI, 순수 Rust 런타임, 검증된 예제 회로 43개, 그리고 Lean 4 정확성 증명이 함께 들어 있습니다.

핵심 아이디어는 하나의 소스, 여러 타깃입니다. 회로는 백엔드에 독립적인 IR로 파싱된 뒤, 실행되고, symbolic[k] 각도를 학습하며, OpenQASM 2.0, JSON 또는 Lean 4로 내보내집니다.

circuit Bell() {
    qreg q[2]
    creg c[2]
    apply H on q[0]
    apply CX on q[0], q[1]
    measure q[0] -> c[0]
    measure q[1] -> c[1]
}

$ aria run examples/aria/bell.aria --circuit Bell --statevector
|00>  +0.707107+0.000000i
|11>  +0.707107+0.000000i

하나의 런타임, 다섯 가지 모달리티

모든 엔진은 같은 트레이트 omega_core::executor::Backend를 구현하므로, 어떤 물리를 다룰지는 플래그 하나로 정해지며 코드를 다시 쓸 필요가 없습니다. 각 모달리티는 고유한 언어 표면을 가지며, 우리 자체 구현만이 아니라 항상 독립적인 외부 구현과 대조하여 검증합니다.

모달리티	표기 방식	엔진	대조 검증 대상
큐비트	`.aria`, OpenQASM 2	밀집 상태벡터 (CPU · CUDA · Metal · OpenCL · libtorch) · MPS 텐서 네트워크 (GPU SVD) · 인증된 절단 한계를 가진 Pauli 전파	Qiskit Aer, quimb, ppvm
큐디트	DITQASM (혼합 기수)	정확한 혼합 기수 상태벡터 · MPS	mqt.qudits, QuickQudits
페르미온 (Majorana)	FermionicQASM 1.0, OpenFermion 사다리 연산자 텍스트	누락 질량 인증서를 가진 Majorana 전파 · 고정 입자 수 섹터 · 임의의 큐비트 엔진으로의 Jordan–Wigner 변환	ffsim, OpenFermion-FQE
광자 (DV, CV)	`.opticqasm`, CV 프로그램	단방향 클러스터 상태 실행기를 갖춘 Fock 공간 광학 · 절단된 Fock 공간 위의 연속변수	Perceval, piquasso
스태빌라이저	OpenQASM 2	Clifford 테이블로 · 스태빌라이저 랭크 (정확 위상 CH 형식)	Stim

이 모달리티들 위에서 aria-qec가 표면 코드와 Steane 코드, 횡단 게이트, 매직 상태 증류, 디코더를 위의 어느 엔진에서든 실행합니다.

명령줄에서 백엔드 선택

$ aria run qft.aria --circuit QFT --int n=3 --backend sim        # pure-Rust statevector (default)
$ aria run bell.aria --circuit Bell --shots 4096 --backend mps   # tensor network
$ aria run bell.aria --circuit Bell --expectation "Z0 Z1" --backend pauliprop
$ aria run qft.aria --circuit QFT --int n=3 --backend gpu        # Metal / CUDA / OpenCL
$ aria run qft.aria --circuit QFT --int n=3 --backend remote --url http://host:8080
$ omega-run --backend {stabilizer,sr,qudit,sector,mp,photonics,cv} …

GPU 백엔드는 기능 플래그로 켜고 끌 수 있으며, 장치가 없으면 CPU 엔진으로 자동 전환됩니다. libtorch는 선택적으로 켜는 백엔드(tch)이며 필수 의존성이 아닙니다.

학습, 검증, 증명

aria train은 순수 Rust 시뮬레이터 위에서 파라미터 시프트 또는 정확한 adjoint 기울기로 symbolic[k] 각도를 최적화합니다. 대표 데모는 VQE로 H₂ 바닥 상태 에너지를 복원합니다. aria tune은 TPE와 가지치기(pruning)로 메타 파라미터를 탐색합니다.

모든 예제에는 외부 오라클과 대조하는 수치 검사가 붙어 있습니다. 닫힌 형식의 알고리즘이 있으면 그것을, 없으면 차분 상태벡터를 기준으로 삼습니다. CI가 그 결과를 단언하고, 게이트 집합은 뮤테이션 테스트를 거칩니다(게이트 뮤턴트 797개, 각도 뮤턴트 286개).

인식되는 회로(Bell, GHZ, QFT, QPE, Grover)는 sorry가 없는 Lean 4 정리로 내보내집니다. 증명 루트에는 별도 글에서 다룬 QSP 정방향 정리와 역정리도 포함되어 있습니다. 일반적인 임의 회로 대응처럼 아직 증명되지 않은 부분은 애매하게 넘기지 않고 LIMITATIONS.md에 보류 항목으로 명시해 두었습니다.

직접 써 보기

$ cargo build -p aria-cli
$ aria run examples/aria/qft.aria --circuit QFT --int n=3 --statevector

TUTORIAL.md는 Bell부터 학습 가능한 안자츠(ansatz)와 Lean 내보내기까지 모든 명령을 보여 주며 안내하고, GRAMMAR.md는 전체 문법 레퍼런스입니다. VS Code, Neovim, tree-sitter용 에디터 지원은 editors/에 있습니다.