信頼できる回路オプティマイザ

Aria はランタイム（omega-* クレート群）を同じリポジトリに同梱しているため、ここで紹介する内容は言語本体とともに github.com/Anzaetek/aria-quantum-language-oss-public で提供されています。

3 つのパスを、変化がなくなるまで繰り返す

omega-core のオプティマイザは、ゲート数が変わらなくなるまで、次の 3 つの処理をループで実行します。

打ち消し合うものを取り除く。 同じ量子ビット上で連続する 2 つの自己逆元ゲート（H·H、X·X、CX·CX）を削除し、恒等ゲートや角度 0 の回転も取り除きます。
回転をまとめる。 同じ量子ビット上で同じ軸まわりに隣接する回転を、角度を合計したひとつの回転に置き換えます。
交換して両方の機会を増やす。 代数的に許される範囲で単一量子ビットゲートを多量子ビットゲートの前後へ移動させ、次のラウンドで新たな打ち消しやマージが見つかるようにします。

意図的に小さく保っています。重量級のオプティマイザが与える効果の大半をこれで得られますし、どのルールも検証できるほど単純です。

テストし、そして証明する

各パスには、書き換え対象の回路に対するユニットテストが付いています。さらに、すべてのサンプル回路はエンドツーエンドで独立したオラクルと数値的に照合されるため、結果を変えてしまう書き換えがあればテストスイートが失敗します。打ち消しパスの根拠となる自己逆元の恒等式（H、X、Y、Z、CNOT）は、Aria に同梱の Lean 4 ツリー（proofs/lean4/QuantumProofs/Gates.lean）で証明されており、他のパスが依拠するゲート行列と回路セマンティクスも同じ場所にあります。

ランタイムのその他の機能

同じクレート群が、オプティマイザと並んで次の機能を提供します。

勾配。 1 パスでパラメータ勾配を求める厳密な随伴微分と、損失にノイズがある場合や微分不可能な場合のための CMA-ES。
動的回路。 すべてのバックエンドでの回路途中測定、条件付きゲート、リセット。リセットのセマンティクスも形式化されています（ResetModel.lean）。
オブザーバブル。 演算子の算術で Pauli 和を構築し、1 回のシミュレーションから複数のオブザーバブルを同時に評価できます。

なぜ重要なのか

速さは前提条件にすぎず、高速なシミュレータは数多くあります。ランタイムに本当に求められるのは、回路の書き換えによって計算内容が気づかないうちに変わってしまわないことです。テストと証明はそのためにあります。