自動化による証明が可能になった

私は以前からCoqやLeanのような依存型言語に特別な思い入れがありました。これらの言語は、任意に微妙な不変条件をエンコードし強制できる型システムを提供する可能性を秘めています。通常の言語では、せいぜいコメントになるようなもので、チームの規模が大きくなるにつれてすぐに失われてしまいます。すると、微妙な誤解が生じ、コンポーネントがうまくかみ合わなくなります。多くの場合、それらのコンポーネントは十分な大きさまで成長しており、問題に気づいたときには、どちらかを調整することは疲れる見込みとなります。おそらく、依存型型は誘惑的に、それらの不変条件を形式的に記述し、機械にチェックさせることができるでしょう。 （追伸：Coqは名前を変えました！何年も前のプリンストンでのCoqカンファレンスで、英語圏でCoqという名前のプログラミング言語を持つことは障害になると提案したことを覚えています。当時の聴衆は同意しなかったと思います。また、Tyrion Lannisterの演説のように聞こえる講演が多く、CoqとHoareがたくさんあったと冗談を言いました。そのショーの最終シーズンと、我々の集合的な記憶喪失の前に起こったため、完全に的外れでしたが、面白くてタイムリーなジョークでした。） 問題は常に、型システムの強力さには証明の労力が伴うということでした。本当に単純なことを証明するのに丸一日費やしたことを確かに証言できます。証明を行うことは実際には非常に楽しいです。挑戦的で、インタラクティブで、明確な目標があります。しかし、特に私のように、自分が何をしているのかわからない場合、それは非常に時間がかかります。また、何時間もの労力を費やした末に、証明しようとしている目標が実際には偽であったことに気づくという、周期的な、腹立たしい経験もあります。この分野での古典的な結果は、seL4プロジェクトからのレトロスペクティブであり、プロジェクトがエンジニアがかなりの経験を積むのに十分な大きさであったにもかかわらず、設計と実装に費やした時間の約10倍の時間を証明に費やしたことがわかりました。彼らは、Cコードよりも20倍以上の証明コード行数を持つことになりました。そのオーバーヘッドにより、依存型言語でのプログラミングは非常にニッチなものになりました。 それはまた、人々がそれを自動化しようと駆り立てました。私がかすかに知っている試みはF*で、システムはSMTソルバーに義務を自動的に discharge させようとします。これは単純なケースでは確かに機能しますが、SMTソルバーを宇宙に飛ばして数時間実行させるようなものを簡単に作成でき、それがいつ終わるのか疑問に思わせます。これらの言語を頻繁に使用する人々は、ソルバーを満足させるものが何であるかについての第六感を発達させ、それに基づいてすべてを構築する必要があることを私は見てきました。それは助けになりますが、ある程度は問題を神秘主義に変換します。あなたは複雑で気まぐれな神に仕えることになります。 重要な事実は、少なくとも理論上は、ステートメントが正しい場合、その証明の内容は無関係であり、その存在だけが重要です。これは、2つの複雑な要因があるため、完全には真実ではありません。第一に、seL4グループが「証明エンジニアリング」と呼んだもの：コードの変更後に証明を再調整する労力を減らすように証明を構造化する必要性。第二に、十分に複雑な証明は、型チェッカーを爆発させ、膨大なメモリを消費させる可能性があります。 私たちは今、LLMを持っており、証明の無関係性と組み合わせることで、非常に有能な形式の証明自動化を約束します。十分な自動化があれば、証明エンジニアリングについてそれほど心配する必要はないかもしれません。型チェッカーを爆発させることを避ける必要がありますが、私の限定的なテストでは、LLMはそれを回避できます。潜在的に、LLMは依存型システムを劇的に実用的にします。 私はこれを試してみたかったので、Zstandardについても興味があったため、LeanでZstandard解凍器を構築しました。Zstandardは、gzipを置き換える標準的な圧縮ユーティリティの競争に勝っているようです。これは別のLZ77スタイルの圧縮機ですが、より優れたエントロピーコーディングと、非常に印象的な解凍速度を達成できる慎重な設計を提供します。bzip2ほど美しくなることは決してありませんが、Burrows-Wheeler変換の輝かしいエレガンスは、実質的な実用的な利点の前にあまり意味をなしません。 [グラフの説明] Zstandard, bzip2, gzip, lzma (XZ/LZMA2) の圧縮トレードオフ（64 MiBのLean/mathlibソースを使用） スペース節約率（右に行くほど圧縮率が高い） 解凍スループット（MiB/秒、対数スケール）（高いほど速い） （測定は標準参照コンピューター、つまり著者が当時使用していたコンピューターで行われました。また、y軸の対数スケールに注意してください。gzipとZstandardは独自の速度クラスにあります。これはAppleマシンであり、Appleのgzipは特に最適化されています。他の場所ではgzipは遅いと予想してください。） Zstandard（Yann Collet作、Jarek Dudaによる画期的なANS作業を基盤）にはRFCがありますが、非常に簡潔です。解凍器を実装するために必要なすべての情報が含まれていますが、圧縮にすでにかなり精通していない限り、何が起こっているのかを理解するために数回読み直す必要があると思います。少なくとも、セクション4.1を6回読み直してから、まともな理解を得られたと感じました。このプロセスの遅すぎる段階で、同僚のNigel Taoが、私が管理できるよりも優れたZstandardの解説を書いていることを発見しました。したがって、Zstandardを理解したい場合は、それを読むべきです。私は、最も興味深い部分であるエントロピーエンコーダーの説明と、Leanに関するいくつかの普及活動を混ぜて説明するつもりです。 エントロピーエンコーダーの仕事は、非均一な確率を持つシンボルのセットが与えられたときに、それらのシンボルのシーケンスを最小限のビット数でエンコードすることです。古典的なエントロピーコーダーはハフマンエンコーダーです。ハフマンエンコーダーは、シンボルを葉ノードとする二分木を構築し、ハフマンは非常に単純なアルゴリズムが最適なプレフィックスツリーを生成することを示しました。シンボルのリストを取得し、確率が最も低い2つを見つけ、それらを子とするツリーノードを形成します。そのツリーノードは、2つの子の合計である確率を持ち、次に、シンボルが2つ少ないセットでアルゴリズムを繰り返しますが、今度はツリーノードが混在します。明らかに、このアルゴリズムの各ステップは要素のセットのサイズを1つ減らすため、終了し、最適なツリーを生成します。ハフマンツリーは、次のnビット（nは最長のコードの長さ）をインデックスとするテーブルを作成できるため、非常に高速です。テーブルエントリは、デコードしたシンボルと、巻き戻す必要があるビット数を示します。ハフマンツリーの欠点は、各シンボルに整数ビットしか使用できないことです。シンボルがあり、-log2(p) = 2.3 の場合、理想的にはそれをエンコードするために2.3ビットを使用したいでしょう。しかし、ハフマンは3ビットに丸めるか、それ以下に丸めることを強制し、他のシンボルにそれ以上のビットを消費させることを強制します。 Zstandardはハフマンツリーを使用しますが、FSEと呼ばれるより高圧縮のエントロピーエンコーダーも備えています。FSEはステートマシンです。シンボルよりも状態が多く、各シンボルは、ストリームでの出現確率を反映する状態のフラクションを受け取ります。したがって、50%の時間出現すると予想されるシンボルがある場合、それは状態の約50%を受け取ります。各状態には3つの値があります。その状態のシンボル、その状態でビットストリームから読み取るビット数、および次の状態を取得するためにこれらのビットに追加されるベースライン状態番号です。さて、思い出せば、ハフマンツリーの問題は整数ビットしか使用できなかったことでしたが、これらの状態も整数ビットを読み取ります。しかし、トリックは、指定されたシンボルに対して1.5ビットを読み取ることを目指している場合、その状態の半分は1ビットを読み取り、半分は2ビットを読み取ることです。そうすれば、平均して目標に到達します。状態のテーブルは送信されません。RFC