パリティ回路のサイズ下界をLeanで形式化する

この論文をやさしく読む

ひとことで言うと

入力ビットの偶奇を求める計算には、深さを一定に制限すると大きな回路が必要になるという既知の結果を、証明支援系Leanで形式化しています。

何に役立つ？

回路計算量の基礎定理を、機械で検査できる形で再利用するための土台になります。下界だけでなく、対数深さなら多項式サイズで計算できる構成も含みます。

この研究の面白いところ

論理式とDAG回路を扱い、定数深さの限界と対数深さの構成をつなげて、二つの計算量クラスの違いを形式化したモデル内で示します。

どこまで分かった？

Håstadの既知の下界の形式化であり、新たに同じ下界を発見したという主張ではありません。dは固定で2以上、下界は十分大きなnについての結果です。Leanによる検査は著者の報告で、この紹介でソースを実行検証したわけではありません。

v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。

アブストラクトの日本語訳

スイッチング補題を用いて、HåstadによるPARITYの下界をLeanで形式化する。固定した任意のd≥2について、n入力のPARITYを計算する、計算深さが高々dの論理式および有向非巡回グラフ（DAG）回路は、十分大きなすべてのnに対してexp(Ω_d(n^(1/(d−1))))のサイズを必要とする。これは指数内の定数を除いて古典的な上界と一致し、PARITYが非一様AC⁰に属さないことを意味する。 さらに、PARITYに対して、多項式サイズ、対数深さ、入力数が有界なゲートを持つ論理式の族を構成し、形式化したモデルでNC¹がAC⁰の部分集合ではないことの具体例を与える。Leanのソースコードはhttps://github.com/formalcs/circuit-complexityで公開されており、Lean 4.33.1とmathlib 4.33.1で検査されている。

v1の要旨から自動生成。本文の精読・人による確認は未実施。