Leanが検証済みカーネルを出荷開始

Leanに検証済みカーネルが出荷されるようになりました

2026-10-15

AIエージェントは、私たちのソフトウェアにおける脆弱性を発見する上で非常に効果的です。これには、Lean証明アシスタントのカーネル（証明チェッカー）も含まれます。最近の2つのポストモーテム（8月1日、8月24日）を参照してください。私たちは公式カーネルを強化し、新しいカーネルを追加し、外部カーネルでLean開発の再検証を簡素化する新しいツールを構築しています。Lean v4.35.0にはlake checkコマンドが付属しています。このコマンドは、あなたの開発をエクスポートし、それを取り巻く全てのオーバーヘッドなしの公式Leanカーネルであるleancheckerで再検証します。プロセス全体はサンドボックス内で実行されます。lake check --inadvisably-no-sandboxを使用してサンドボックスを無効にすることもできます。Leanには現在、4つの追加カーネルが付属しています：nanoda、lean4lean、con-leche、およびcon-ron。lake check --paranoidコマンドを使用して、これら全てのカーネルで開発を再検証できます。このモードでは、メモリ破損を不正な回答ではなくチェックされたアボートに変換する、ハード化されたメモリ割り当て器で構築された公式カーネルのバリアントも実行します。

Con-lecheは、Leanで書かれ一貫性が証明された最初のLeanカーネルです。Lean FROでJoachim Breitnerの厳重な監督の下、Claude（FableおよびOpus）によって実装され、一貫性が証明されました。ここでの「一貫性」とは、con-lecheが受け入れる全ての環境が、Mario CarneiroのLeanの型理論のモデルに従って、集合論にモデルを持つことを意味します。証明のアイデアはこちらにまとめられています。証明自体は公式Leanカーネルによってチェックされ、モデルで使用される集合論の一貫性を仮定します。このアプローチは、カーネル実装におけるプログラミングミスという、バグのクラス全体を排除します。これはパフォーマンスのペナルティなしに実現されます。完全なMathlibエクスポートでは、con-lecheは公式カーネルの命令数の0.69倍を実行し、8スレッドを使用して約100秒でライブラリ全体をチェックします（PERF.mdを参照）。

しかし、con-lecheは万能ではありません。なぜなら、それを構築するために使用されたコンパイラやランタイムにバグが存在する可能性があるからです。この種のリスクを最小限に抑えるため、JoachimはAIを使用してcon-lecheをRustに翻訳し、その後Aeneasを使用してRustバージョンがcon-lecheのチェックアルゴリズムをリファインすることを証明しました。AeneasはLeanを使用してRustコードを検証するためのツールです。このカーネルはcon-ronと呼ばれます。重要な点は、con-lecheには形式的な一貫性証明があるため、残りの不整合バグはLeanのコンパイラまたはランタイム（bignumライブラリを含む）にある可能性が最も高いということです。同じバグがRustコンパイラまたはランタイムにも存在する可能性は非常に低いため、con-lecheとcon-ronの両方で証明をチェックすることにより、このクラスのバグに対する高いレベルの保護が得られます。

また、lean4leanの検証も数ヶ月以内に完了すると予想されており、その後、ディストリビューションには3つの検証済みカーネルが用意されることになります。lean4leanの検証は、その実装が公式のC++カーネル実装に非常に近いという点でも重要です。

Arthur Adjedjはカーネル改修計画（Issue #14977を参照）に取り組んでいます。Arthurはすでに計画を実装した複数のPRを提出しています。Joachimはそれらをレビューし、con-lecheが同じ変更を実装していることを確認し、改修中に新しい穴が導入されないようにその証明をパッチしています。ArthurはさらにシンプルなLeanカーネルにも取り組んでいます。目標は、それらの複雑さを軽減し、仕様の検証プロセスを簡素化することです。

まだ多くの作業が残っています。よりユーザーフレンドリーなlake checkコマンドを求めています。ユーザーがお気に入りのカーネルをlake checkにフックできるようにしたいと考えています。Lean Kernel Arenaには、新しく効率的なカーネルがいくつかあります。それらを簡単に使えるようにすべきです。コンパイラの一部を検証したいと考えています。スケーラビリティも現在大きな懸念事項です。AnthropicのFLTは1300万行を超え、Mathlibは250万行、Tau Cetiはすでに300万行を超えて急速に成長しています。The General Courtade–Kumar theoremリポジトリは5000万行を超えています。Leanコミュニティでは、10億行以上の範囲の数学ライブラリの提案が書かれているのを目にしています。外部カーネルの現在の方法は、このサイズの開発にはスケーリングしません。バイナリ出力形式と外部チェッカーによる増分チェックが必要です。Lean FROでは、これらの課題に取り組んでいます。それまでの間、ご自身のプロジェクトでlake check --paranoidを実行してください。カーネルがあなたの証明のいずれかで意見の相違を示した場合、contact@lean-fro.orgまでお知らせください。