오픈소스 · Apache-2.0

Aria Language

양자 회로를 위한 작고 읽기 쉬운 언어입니다. 하나의 소스가 백엔드에 독립적인 IR로 파싱된 뒤, 실행되고, 파라미터를 학습하고, OpenQASM 2.0, JSON 또는 기계 검증된 Lean 4로 내보내집니다.

예제

커맨드라인에서 실행한 벨 쌍입니다.

회로는 평범한 텍스트입니다. aria 바이너리가 이를 나열하고, 파싱하고, 실행하고, 학습하고, 내보내고, 튜닝합니다.

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 bell.aria --circuit Bell --statevector
|00>  +0.707107+0.000000i
|11>  +0.707107+0.000000i

$ aria run bell.aria --circuit Bell --expectation "Z0 Z1"
<Z0 Z1> = 1.000000000000

왜 Aria인가

Aria로 회로를 작성하면 얻는 것.

타깃

필요한 형식으로 내보내기

같은 회로를 바로 실행하거나 OpenQASM 2.0, JSON, 또는 Lean 4 정확성 정리로 내보냅니다.

학습

있는 자리에서 학습

symbolic[k]로 학습 가능한 각도를 선언합니다. aria train이 libtorch 없이 순수 Rust로 파라미터 시프트 그래디언트를 써서 최적화하고, aria tune이 메타 파라미터를 탐색합니다.

런타임

시뮬레이터 선택

모든 백엔드가 하나의 트레이트를 구현합니다. 기본은 CPU 상태벡터이고, MPS, GPU(Metal, CUDA, OpenCL), libtorch, 원격 omega-server를 더할 수 있습니다.

검증

모든 예제를 검사

43개 예제 전부가 독립적인 고전 오라클과 수치적으로 대조 검증됩니다. Lean 4 증명에는 sorry가 없습니다.

모달리티

무엇을, 어떻게 시뮬레이션하는가.

모달리티마다 고유한 엔진이 있고, 각각은 Qiskit, Stim, ffsim, Perceval 같은 외부 참조 구현과 대조 검사됩니다.

큐비트CPU, CUDA, Metal, OpenCL, libtorch에서의 밀집 상태벡터; GPU 가속 SVD를 쓰는 MPS 텐서 네트워크; 인증된 절단 한계를 갖는 하이젠베르크 묘사의 파울리 전파.
큐디트DITQASM 회로를 위한 정확한 혼합 기수 상태벡터, 그리고 두 번째 엔진으로서의 MPS.
페르미온 (마요라나)누락 질량 인증서가 붙는 마요라나 전파; 입자 수가 고정된 정확한 섹터 엔진; 임의의 큐비트 엔진으로의 조던–위그너 변환. FermionicQASM 1.0 또는 OpenFermion 사다리 연산자 텍스트로 작성합니다.
광자 (CV와 DV)이산 변수: 단방향 클러스터 상태 실행기를 갖춘 OPTICQASM 회로용 Fock 공간 포토닉스. 연속 변수: 절단된 Fock 공간 위의 프로그램.
스태빌라이저빠른 기댓값 계산을 위한 클리포드 테이블로; 진폭, 내적, 파울리 행렬 원소를 위한 정확 위상 CH 형식의 스태빌라이저 랭크.

계산 방법

계산하는 방식들.

회로에 맞는 방법을 고르세요. 정확한 계산이 감당 가능한 곳에서는 정확하게, 그렇지 않은 곳에서는 인증된 근사로.

밀집 상태벡터CPU, CUDA, Metal, OpenCL 또는 libtorch에서 모든 기저 상태의 정확한 진폭을 계산합니다.
텐서 네트워크 (MPS)결합 차원이 제한된 행렬 곱 상태. 폭이 큐비트 수가 아니라 얽힘의 양에 따라 늘어납니다. 노이즈 MPS 경로를 포함합니다.
하이젠베르크 전파관측량을 파울리 또는 마요라나 합의 형태로 회로를 거슬러 밀어냅니다. 클리포드 회로에서는 정확하고, 그 밖에서는 버려진 가중치에 대한 인증된 한계와 함께 절단합니다.
스태빌라이저 방법빠른 기댓값을 위한 클리포드 테이블로; 정확한 진폭과 내적을 위한 CH 형식의 스태빌라이저 랭크.
Fock 공간 시뮬레이션이산 및 연속 변수 광학을 위한 광자 수 상태와 퍼머넌트 기반 진폭.
입자 수 섹터페르미온 회로를 입자 수가 고정된 부분 공간 안에서 정확하게 시뮬레이션합니다.
측정 기반 (단방향)게이트 모델과 나란히 제공되는 클러스터 상태 측정 패턴용 참조 실행기.
학습과 탐색변분 회로를 위한 파라미터 시프트 및 정확한 수반 그래디언트; 메타 파라미터를 위한 aria tune(가지치기가 있는 TPE); QUBO와 QAOA 정식화.

다음 릴리스

다음에 작업할 것들.

성능CPU와 GPU 백엔드 전반에서 더 빠른 시뮬레이션.
멀티 QPU 에뮬레이션양자 광 네트워크로 연결된 여러 QPU를 하나의 Aria 프로그램으로 에뮬레이션합니다.

저장소 안에는

저장소에 들어 있는 것.

43개의 예제 회로각 헤더에 하네스와 통과해야 할 검사가 명시되어 있습니다.
오류 정정 (aria-qec)횡단 게이트, 매직 상태 증류, 디코더를 갖춘 표면 코드와 Steane 코드. 어떤 백엔드에서도 동작합니다.
Lean 4 증명 트리인식되는 회로(Bell, GHZ, QFT, QPE, Grover)에 대한 정확성 정리.
에디터 지원VS Code, Neovim, tree-sitter용 문법과 선택형 Python 바인딩.
문서화된 한계LIMITATIONS.md, GATE-EXACTNESS.md, 그리고 측정된 CPU→GPU 전환 크기가 코드와 함께 제공됩니다.

인사이트

어떻게 동작하는지에 대해 쓴 글들.

Aria Language

함께 일하기

Aria 위에 무언가를 만드시나요? 필요한 것을 알려주세요.

contact@anzaetek.com

Aria Language

커맨드라인에서 실행한 벨 쌍입니다.

Aria로 회로를 작성하면 얻는 것.

필요한 형식으로 내보내기

있는 자리에서 학습

시뮬레이터 선택

모든 예제를 검사

무엇을, 어떻게 시뮬레이션하는가.

계산하는 방식들.

다음에 작업할 것들.

저장소에 들어 있는 것.

어떻게 동작하는지에 대해 쓴 글들.

양자 신호 처리의 형식화: Lean 4로 증명한 역정리

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

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

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

Aria 위에 무언가를 만드시나요? 필요한 것을 알려주세요.