인사이트
어떻게 동작하는지에 대해 쓴 글들.
증명, 컴파일러, 런타임, 그리고 그 위의 언어까지. 각 구성 요소가 어떻게 동작하는지 설명합니다.
Aria Language
양자 신호 처리의 형식화: Lean 4로 증명한 역정리
양자 신호 처리의 역 기본 정리 — 모든 허용 가능한 다항식 쌍은 어떤 위상 열로 실현된다 — 가 Aria와 함께 배포되는 Lean 4 증명 트리에서 sorry 없이 기계 검증되었습니다.
→Aria Language읽을 수 있는 회로에서 기계가 검증한 정리까지
aria export --lean은 회로와 그 주석을 Lean 4 정리로 바꿉니다. 무엇이 내보내지는지, 아직 열려 있던 증명을 어떻게 닫았는지, 그리고 증명 트리가 어디에 있는지 설명합니다.
→Aria Language신뢰할 수 있는 회로 최적화기
Aria는 자체 런타임을 함께 제공합니다. 회로 최적화기는 세 개의 작은 패스로 게이트를 재작성하며, 각 패스는 단위 테스트를 거치고, 의존하는 자기 역원 항등식은 Lean 4로 증명되어 있습니다.
→Aria LanguageAria 오픈소스 공개: 하나의 언어, 모든 모달리티
읽기 쉬운 양자 회로 언어 Aria가 Apache-2.0 라이선스로 github.com/Anzaetek/aria-quantum-language-oss-public 에 공개되었습니다. 하나의 소스가 큐비트, 큐디트, 페르미온, 광자, 스태빌라이저 엔진에서 실행되고, 순수 Rust로 학습되며, OpenQASM 2.0 또는 기계 검증된 Lean 4로 내보내집니다.
→