インサイト
仕組みについて書いたもの。
証明、コンパイラ、ランタイム、そしてその上の言語。各要素がどう動くかを解説します。
Aria Language
量子信号処理を形式的に：Lean 4 による逆定理
量子信号処理の逆基本定理 — 許容される多項式の組はすべて、ある位相列によって実現される — が、Aria に同梱の Lean 4 証明ツリーで sorry なしに機械検証されています。
→Aria Language読める回路から、機械が検証した定理へ
aria export --lean は、回路とそのアノテーションを Lean 4 の定理に変換します。何がエクスポートされるのか、未完だった証明をどう閉じたのか、証明ツリーがどこにあるのかを紹介します。
→Aria Language信頼できる回路オプティマイザ
Aria は独自のランタイムを同梱しています。その回路オプティマイザは 3 つの小さなパスでゲートを書き換え、各パスはユニットテスト済みで、依拠する自己逆元の恒等式は Lean 4 で証明されています。
→Aria LanguageAriaをオープンソース化：ひとつの言語で、あらゆるモダリティを
読みやすい量子回路言語Ariaを、Apache-2.0ライセンスで github.com/Anzaetek/aria-quantum-language-oss-public に公開しました。ひとつのソースが量子ビット・量子ディット・フェルミオン・光子・スタビライザーの各エンジンで動き、純Rustで学習でき、OpenQASM 2.0や機械検証済みのLean 4へエクスポートできます。
→