← すべてのインサイト

Ariaをオープンソース化：ひとつの言語で、あらゆるモダリティを

Aria Language →aria · oss · quantum · lean4 · rust

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

ひとつのランタイム、5つのモダリティ

すべてのエンジンは同じトレイト omega_core::executor::Backend を実装しているため、物理系の選択はフラグひとつで済み、書き直しは不要です。各モダリティには専用の言語表現があり、自社実装だけでなく、必ず独立した外部実装と照合して検証しています。

モダリティ記述形式エンジン照合対象
量子ビット.aria、OpenQASM 2密な状態ベクトル（CPU · CUDA · Metal · OpenCL · libtorch）· MPS テンソルネットワーク（GPU SVD）· 保証付き打ち切り誤差を持つ Pauli 伝播Qiskit Aer, quimb, ppvm
量子ディットDITQASM（混合基数）厳密な混合基数状態ベクトル · MPSmqt.qudits, QuickQudits
フェルミオン（Majorana）FermionicQASM 1.0、OpenFermion ラダー形式テキスト切り捨て質量の証明書付き Majorana 伝播 · 粒子数固定セクター · Jordan–Wigner 変換による任意の量子ビットエンジンへの変換ffsim, OpenFermion-FQE
光子（DV、CV）.opticqasm、CV プログラム一方向クラスター状態エグゼキュータを備えた Fock 空間フォトニクス · 打ち切り Fock 空間上の連続変数Perceval, piquasso
スタビライザーOpenQASM 2Clifford タブロー · スタビライザーランク（厳密位相 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 バックエンドは feature フラグで有効化され、デバイスがない場合は CPU エンジンにフォールバックします。libtorch はオプトインのバックエンド（tch）であり、依存関係ではありません。

学習し、検証し、証明する

aria train は、純 Rust シミュレータ上でパラメータシフト法または厳密な随伴（adjoint）勾配を使って symbolic[k] の角度を最適化します。標準デモでは VQE によって H₂ の基底状態エネルギーを再現します。aria tune は TPE と枝刈りでメタパラメータを探索します。

すべてのサンプルには、外部オラクルとの数値照合が付いています。閉形式のアルゴリズムがある場合はそれと、ない場合は差分状態ベクトルと比較します。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 状態から学習可能なアンザッツ、Lean エクスポートまでを、すべてのコマンドを示しながら順に解説しています。GRAMMAR.md は完全なリファレンスです。VS Code、Neovim、tree-sitter 向けのエディタサポートは editors/ にあります。