Anzaetek Quantum — 今日出荷されているもの

現時点の Anzaetek Quantum スタックをそのまま記録します。この記事は意図的にスコープを狭めています — 今後来るものではなく、今日出荷されているものだけを列挙します。このページに載っていない機能はビルドにも入っていません。

2 つのレイヤ

スタックは 2 層構成です。オープンソースのランタイム (omega-functions) と、その上に載るクローズドソースのツールキット (Quantum) です。

ランタイム — オープンソース、Apache-2.0。github.com/Anzaetek/omega-functions-public。本日公開。実行レイヤ — 4 つのシミュレーションバックエンド、PQC 認証サーバ、C FFI、WASM サンドボックス、CLI。

Quantum ツールキット — クローズドソース。回路レイヤ — シンボルパラメータと注釈付きの IR、最適化パス、フォーマットエクスポータ、QML スタック、誤り訂正符号、Lean 4 / Rocq へのスペック抽出パイプライン。オープンランタイムにコンパイルされます。

回路言語

Quantum ツールキットの AST は Pauli、Clifford、T、回転、制御、フォトニックの各系統にわたる 30 以上のゲート種別をカバーします。パラメータはシンボリック (ParamExpr: シンボル、Pi、二項演算、関数呼び出し) にでき、これが可変アルゴリズムを特殊ケースなしに駆動する要です。注釈 — Assert、Prove、Ensures、Requires、Invariant、ResourceBound — が回路点に正当性主張を結び付け、Lean / Rocq エクスポータが何を証明すべきかを知ります。

Rust 内でインラインに構築するための circuit! proc-macro があります。

circuit!(bell, 2, 2 => { h 0; cx 0,1; measure_all; })

パイプ・テンソル積の合成代数 (>>、|、repeat、inverse) で部品から大きな回路を組み立てます。

最適化 — 13 パス

恒等除去、隣接ゲート相殺、随伴対相殺 (QFT >> IQFT をゼロゲートに畳み込む)、回転結合、可換性に基づく並べ替え、ゲート分解、T-merge、Clifford テーブル上での FastTMerge、arXiv:2407.08695 の F₂ ガウス消去カーネル探索を含む PhasePolyDedup、BBMerge、InternalHOpt、Clifford+T パイプライン、オプションの Tket2 連携。推測ではなく quantum-core に実際に出荷されており、それぞれ単体テストが添付されています。

フォーマットエクスポータ — 8 種

OpenQASM 2.0、OPTICQASM 1.0、JSON、.qc、omega-IR (ランタイムへの直接渡し)、C ABI FFI、Lean 4、Rocq/Coq。Lean 4 と Rocq の出力は、回路と注釈をプローバが検査する定理文に変換します。

QML

quantum-qml は中回路射影測定とリセットに対応した状態ベクトルシミュレータ、tch-rs 経由で PyTorch と統合する QuantumLayer、tch のオートグラッドを通じて流れるパラメータシフト勾配、勾配が取れないケースのための純 Rust CMA-ES 最適化器、arXiv:2505.05249 の代理 (surrogate) トレーナから成ります。

今日出荷されている回路ビルダは標準 (Bell、GHZ、QFT、QPE)、Trotter ステップ (1 次・2 次、H₂、Ising、Heisenberg)、フォトニックメッシュ (Clements、MZI)、QSVT と LCU ブロックエンコーディング、QML エンコーディング層 (角度、IQP、ハードウェア効率) をカバーします。

誤り訂正

反復符号 [[n,1,n]]、Steane [[7,1,3]]、表面符号 [[d²,1,d]]、そして論理回路をエンコード済み回路に持ち上げる add_error_correction 変換。表面符号シンドローム用の MWPM デコーダを備えます。

アルゴリズム例

コンパイル・実行され、サンプルディレクトリとテスト行列の一部です。

• Shor — 15、21、35 の因数分解。1 カウント量子ビットの半古典バリアント。Shor-DLP (離散対数)。p = 97 における構造的 EC 点加算回路、secp256k1 サイズの素数 (256–521 ビット) での表面符号物理リソース見積り。
• QFT / QPE — 標準と反復 (Kitaev の 1-ancilla)、堅牢位相推定例。
• HHL — スタブではない完全な線形方程式ソルバー例。
• Grover — 2/3 量子ビット検索と状態ベクトル検証。
• ブロックエンコーディングと LCU — 対角ブロックエンコーディングと LCU のデモ。
• 量子ウォーク、Deutsch–Jozsa、Bernstein–Vazirani、Simon、swap test、テレポーテーション、スーパーデンス符号化。
• QAOA — パラメータシフト勾配降下 + CMA-ES バリアントを伴う MaxCut。オープンランタイムのサンドボックス上で実行する WASM ゲストとして出荷。
• VQE — 基準エネルギーの H₂ 基底状態例、WASM ゲストとしても提供。

Aria DSL とリソース推定

Aria は、さまざまなパラメータでインスタンス化できる回路テンプレートを記述する表面 DSL です。quantum_core::ast::aria のパーサがテンプレートの AriaProgram を生成し、AriaProgram::instantiate(name, ¶ms) がテンプレートを具体的な Circuit に下げます — ループ展開、オラクルのインライン化、シンボルパラメータ配列の解決。5 つの .aria サンプルすべてがパース → インスタンス化のラウンドトリップを通過します。

quantum_core::resource モジュールは論理 ResourceEstimate 計数と表面符号 PhysicalEstimate 外挿、そしてオラクル実装だけが異なるアルゴリズム変種を比較するためのオラクルスケッチ層を提供します。

Lean 4 へのスペック抽出

quantum spec extract --aria --all --out