読める回路から、機械が検証した定理へ

Aria は回路を Lean 4 にエクスポートできます。これにより、プログラムについての主張が、機械が検証できる定理になります。証明ツリーは Aria リポジトリ内の proofs/lean4/QuantumProofs に同梱されており、sorry を含みません。つまり、仮定として置いているものは何もありません。

何がエクスポートされるのか

回路には Assert、Prove、Ensures、Requires、Invariant、ResourceBound といったアノテーションを付けられます。aria export --lean は回路とそのアノテーションを、次の内容を持つ Lean ファイルに変換します。

• n 量子ビット上の定義としての回路
• denote によるユニタリ行列としての意味
• アノテーションごとにひとつの定理

認識される回路（Bell、GHZ、QFT、QPE、Grover）については、エクスポートされたファイルが共有ツリーに対して証明を完結させます。たとえば Generated/GateModel/Bell_Spec.lean は、Bell ペアに対して aria export --gate-model が出力するものそのままであり、実際に証明が通ります。

最も時間がかかった証明

一時期、これらの定理のいくつかはスタブでした。コンパイルは通るものの、何も証明していなかったのです。それらを閉じる作業の大半は、新しい数学ではなく、既知の結果を整理して組み込むことでした。

QFT はユニタリである。 量子フーリエ変換は n 乗根（1 の n 乗根）から構成される行列であり、QFT.lean の qft_correct は、回路がまさにその行列を計算することを述べています。ユニタリ性はひとつの恒等式に帰着します。ω^(jk) と ω^(lk) の複素共役の積を k について和をとると、j = l のとき n、それ以外では 0 になるというものです。非対角成分では公比が 1 でない等比級数なので和は 0 になり、対角成分では 1 が n 個並ぶので n になります。

ブロックエンコーディング。 ブロックエンコーディングの定理は以前はプレースホルダーでした。現在は本来の不変条件、すなわちユニタリの左上ブロックが A/α を ε 以内で近似することを述べており、ブロックエンコーディングを構築する後続のパスが具体的に参照できるものになっています。

QPE と Grover。 どちらにも証拠（witness）が必要でした。位相推定では k/2^n の形の位相、Grover 探索では角度 arcsin(1/√N) です。証拠そのものは簡単でしたが、QFT のもとで位相が整合的に巻き付くという補題が本当の難所であり、これは上述の 1 の n 乗根の恒等式から導かれました。

ツリーに含まれるその他の内容

エクスポートされた回路のほかに、同じツリーはランタイム自体の構成要素も形式化しています。ゲート行列とその随伴、リセットのセマンティクス、スタビライザーモデル、MPS の打ち切り誤差、HHL と QSVT の構造、そして量子信号処理の順定理と逆定理です。最後のものについては別の記事で紹介しています。

試してみる

$ aria export examples/aria/bell.aria --circuit Bell --lean
$ cd proofs/lean4 && lake build

最初のコマンドが Lean ファイルを書き出し、2 つ目のコマンドがそれをツリーに対して検証します。