저희가 만드는 것들입니다.
Aria Language
양자 회로를 위한 작고 읽기 쉬운 언어. 하나의 소스로 실행하고, 학습하고, OpenQASM 2.0이나 기계 검증된 Lean 4로 내보냅니다.
Aria 살펴보기 →최적화Aria-Opt
MILP / QUBO 모델을 Aria로 한 번 작성하면 HiGHS, CBC, SCIP, CP-SAT 또는 자체 시뮬레이티드 바이퍼케이션 솔버로 보냅니다. 개발 중이며, 주요 상용 솔버에서 익숙한 파라미터 이름과 모델 의미 체계를 그대로 따릅니다.
Aria-Opt 보기 →라이선스Quantum Toolkit (Sqetch)
Aria 런타임 위의 라이선스 툴킷: 최적화 패스, QML, 오류 정정, Lean 4 및 Rocq 내보내기, 금융 랩.
툴킷 보기 →응용Finance & Trading
합성 OHLC 데이터, GBDT·DNN·QNN 기반 국면 분류, 합성 시계열에 대한 워크포워드 백테스트.
금융 보기 →회로는 한 번만 작성하세요. 나머지는 Aria가 맡습니다.
- libtorch가 필요 없는 순수 Rust 런타임
- OpenQASM 또는 Lean 4로 내보내기
- 선택형 Python 바인딩과 에디터 지원
다음 릴리스더 빠른 시뮬레이션, 그리고 멀티 QPU 에뮬레이션: 양자 광 네트워크로 연결된 여러 QPU를 하나의 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양자 회로가 조종할 수 있는 이미지 생성기를 만들었습니다.
열여섯 개의 숫자로 조종되는 이미지 생성기입니다. 지금은 작은 고전 신경망이 그 숫자를 고르지만, 앞으로는 양자 회로가 대신하도록 할 계획입니다.
생성기 보기 →어떻게 동작하는지에 대해 쓴 글들.
양자 신호 처리의 형식화: Lean 4로 증명한 역정리
양자 신호 처리의 역 기본 정리 — 모든 허용 가능한 다항식 쌍은 어떤 위상 열로 실현된다 — 가 Aria와 함께 배포되는 Lean 4 증명 트리에서 sorry 없이 기계 검증되었습니다.
→Aria Language읽을 수 있는 회로에서 기계가 검증한 정리까지
aria export --lean은 회로와 그 주석을 Lean 4 정리로 바꿉니다. 무엇이 내보내지는지, 아직 열려 있던 증명을 어떻게 닫았는지, 그리고 증명 트리가 어디에 있는지 설명합니다.
→Aria Language신뢰할 수 있는 회로 최적화기
Aria는 자체 런타임을 함께 제공합니다. 회로 최적화기는 세 개의 작은 패스로 게이트를 재작성하며, 각 패스는 단위 테스트를 거치고, 의존하는 자기 역원 항등식은 Lean 4로 증명되어 있습니다.
→