Machine-Checked Arithmetic Bit Complexity of the Kannan-Bachem Smith Normal Form in Lean 4

あなたは、すべての本が数字で構成された巨大で複雑なパズルである図書館の、熟練したアーキビスト（記録保管係）であると想像してください。時には、その下に隠された、より単純なパターンを見つけ出すために、パズルのページを並べ替える必要があります。これは、整数のグリッド（行列と呼ばれます）を扱う数学の一分野である線形代数の世界です。行列をスプレッドシートのように考えてみてください。名前の乱雑なリストをアルファベット順に並べ替えてパターンを見つけるように、数学者はこれらの数字のグリッドを「スミス標準形」へと整理しようとします。これは、数字が列に沿ってどんどん大きくなり、かつ各数字が次の数字を完璧に割り切るような、非常にクリーンで対角線上のバージョンです。

しかし、ここには落とし穴があります。数字を整理する方法を説明するのは簡単ですが、実際にその計算を行うことは悪夢となり得ます。行や列を入れ替えて整理していくうちに、中の数字が爆発的に大きくなり、コンピュータをクラッシュさせたり、計算に100万年かかったりしてしまうのです。何十年もの間、数学者たちはこれらのグリッドを整理する方法（カナン・バッヘム・アルゴリズムと呼ばれる手法）を知っていましたが、そのプロセスが無限ループに陥ったり、数字が制御不能に増大したりしないことを、絶対的な確信を持って証明する必要がありました。この論文は、単に「それは機能する」と言うだけでなく、それが機能するというデジタルで揺るぎない証明を構築し、それにどれだけの「計算エネルギー」がかかるかを正確にカウントするという、その空白を埋めるものです。

デジタルなダブルチェック

この論文において、ワシントン大学のJunye Jiは、整数の行列を整理するための巧妙なレシピであるカナン・バッヘム・アルゴリズムを取り上げ、Lean 4というツールを用いた機械検証による証明を構築しています。Lean 4を、数学の証明が論理的に完全に堅牢でない限り、決して受け入れない超厳格なロボット司書だと考えてください。もしあなたが「おそらく」や「たぶんこうなるはず」といった曖昧なことを紛れ込ませようとすれば、ロボットはドアを叩きつけます。Jiは単にコードを書いたのではありません。コードが常に終了し、決してクラッシュせず、毎回正確な答えを出すことを、ロボットに検証させたのです。

目標は、任意の非ゼロ整数からなる正方行列に対して、このアルゴリズムが、そこに至るまでの正確な手順を追跡しながら、クリーンな対角線状の「スミス標準形」へと変換できることを証明することでした。その結果は、単なる「はい、機能します」というメモではありません。最終的な整理されたグリッド、そこへ至る「順方向」のマップ、そして元の状態に戻るための「逆方向」のマップを含む、完全かつ検証済みのパッケージです。それは、巨大な数字の森の中で迷わないよう、ロボットによって検証された宝の地図と帰還チケットの両方を持っているようなものです。

「ピボット」のダンスと減少する数字

アルゴリズムの核心は、「安定化（stabilization）」と呼ばれるダンスです。部屋の片付けをしているところを想像してください。あなたは床の特定の場所（「ピボット」）を選び、その行と列にある他のすべてを消し去ろうとします。時として、数学的な処理が複雑になり、すべてを完璧に消し去ることができない場合があります。そのようなとき、アルゴリズムは諦めるのではなく、現在のピボットをより小さな数字（「真の約数」）に置き換えるという特別な操作を行います。

論文は、ある決定的な事実を証明しています。この特別な操作が行われるたびに、ピボットのビット数（バイナリとしての「サイズ」）は厳密に小さくなるということです。これは、重い岩を軽い小石と交換することが許されるゲームのようなもので、一度小石に替えたら、二度と重い岩に替えることはできません。この「小さくする」作業を永遠に続けることはできないため（最終的にはゼロに到達します）、ゲームは必ず終了します。著者らは、この「下降」が保証されていることを証明しました。つまり、アルゴリズムが無限ループに陥ることは決してないということです。

コストの計測：「トレース」

この研究の最もエキサイティングな部分の一つは、コストの数え方です。通常、アルゴリズムが「速い」と言うとき、数秒かかるだろうと推測するだけかもしれません。しかしここでは、著者らはバイナリ演算の観点から正確な算術コストを知りたいと考えました。彼らは、コンピュータが行ったあらゆる微細な数学的操作（加算、乗算、除算）をリストアップした、いわば「レシート」のような「フラット・トレース（flat trace）」を作成しました。

彼らは、このレシートの総コストが多項式レートで増大することを証明しました。平たく言えば、入力となる行列が巨大になったとしても、それを解くのにかかる時間は無限大に爆発することはありません。それは予測可能で管理可能な方法で増大します。彼らは、この増大の具体的な「次数」さえも計算しました。論文によかに 따르면、コストは、実行された作業に対しては2,150,687、出力のサイズに対しては98,990という次数を持つ多項式によって制限されています。

これらの数字は恐ろしく大きく見えるかもしれませんが、著者らはそれらが何を意味するかを非常に慎重に説明しています。これらは「シャープな」指数（例えば、$n^2$ステップかかる、と言うようなもの）ではありません。これらは**保守的な証拠（conservative witnesses）**です。橋を建設するとき、100トンの荷重に耐えられると計算しても、念のために1,000トン耐えられるように設計するようなものです。これらの巨大な数字は、数学界における「1,000トン」であり、たとえ現実世界のパフォーマンスがもっと優れていたとしても、アルゴリズムが安全で効率的であることを保証するものです。

何が残されたのか？

この論文が「行わなかったこと」を知っておくことも重要です。著者らは、自分たちの証明の境界について非常に明確でした。彼らは算術演算（数学そのもの）のみをカウントしました。コンピュータがデータをメモリにロードする時間、結果をプリントする時間、あるいはプログラミング言語自体のオーバーヘッドについてはカウントしていません。また、これが行列を整理する上で「最速」の方法であることも証明していません。彼らは、この特定の方法が安全であり、確実に終了し、計算された多項式の限界を超えないことを証明したに過ぎません。

最終的な判定

では、結論は何でしょうか？この論文は、**形式検証（formal verification）**の勝利です。数十年前からある複雑な数学的レシピを取り上げ、あらゆるステップをチェックするためにロボットに渡したのです。ロボットは、そのレシピが常に機能し、常に終了し、システムを壊すほど巨大な数字を作り出さないことを確認しました。それは、整理された行列、変換マップ、そしてそこに至るためにどれだけの作業を行ったかという数学的に証明された保証を含む、「正しさの証明書」を提供しています。

好奇心旺盛なティーンエイジャーにとって、これは、ルービックキューブを解くだけでなく、「どんなにバラバラの状態から始まっても、決して途中で止まらず、キューブを壊さず、決まった回数の動き以内で解く」という法的契約書まで書くロボットを作る様子を見ているようなものです。数学における「おそらく」を、想像しうる最も厳格な裁判官によって検証された「間違いなく」へと変えるのです。