カーネルの健全性バグ #14576 の事後分析

カーネルの健全性バグ #14576 の事後分析 2026年8月1日 Leanカーネルにおける健全性バグ（#14576）が、7月27日の週に報告され修正されました。この件はZulipやソーシャルメディア（X、LinkedIn、Mastodonなど）で注目を集めました。 何が起こったのか 7月25日、Ramana KumarはAI支援によって生成されたコラッツ予想の、Sorry（証明不可能）ではない「反証」を含むリポジトリを公開しました。これは、カーネルがネストされた帰納型を処理する際のバグを悪用していたため、有効な証明ではありませんでした。7月28日、Kiran GopinathanはこれをFalseの短い証明に還元し、issue #14576 を開きました。報告から1時間後に私たちは修正をプッシュしました（#14577）。Joachim Breitnerがレビューし改善を提案し、マージされました。新しいパッチリリースが公開されています。 バグの詳細 カーネルがパラメータDsを持つ帰納型Tの下にあるネストされた出現を消去する際、これらのパラメータがファントム型（コンストラクタフィールドに現れない）である場合、生成される補助型から消え、型チェックをすり抜けてしまいます。その位置に型が不正な引数を使用することで、カーネルにFalseの証明を受け入れさせることが可能でした。このバグは、帰納型宣言を直接カーネルに送信するメタプログラミングを通じてのみ到達可能です。フロントエンドは引数をチェックし、型が不正な項を捕捉します。これはLeanのメタ理論の欠陥ではなく、実装上のバグです。 なぜnanodaはそれを検知できなかったのか 元のコラッツリポジトリは、主要な外部チェッカーであるnanodaの1週間前のバージョンでもテストされていました。nanodaはChris BaileyによってRustで実装された、Leanの独立したカーネル（証明/型チェッカー）です。驚くべきことに、2つの無関係なバグが関与していました。公式カーネルには、前述のようにネストされた帰納型サポートにチェックが欠けていました。nanodaはその箇所をチェックしていましたが、プロジェクションノードでの型名を検証していませんでした。nanodaのバグはJeremy Chenによって報告され、Leanのバグが報告される1週間前に修正されました。証明は、カーネルが決して検査しない式が古いnanodaによって受け入れられたものになるように構築されていました。Ramanaはタイミングは偶然だと考えていますが、モデルがnanodaの報告を見ていた可能性を排除できません。Joachimは、このタイミングの偶然性は、このバグを見つけられる強力なモデルが利用可能であったためだという仮説を提唱しました。 実際の結果：独立したカーネルでのチェックは依然として機能します。なぜなら、2つの実装に2つの異なるバグが必要だったからです。しかし、それに依存しているユーザーは、両方の最新バージョンが必要です。 lean4leanはカーネルバグの影響を受けます。なぜなら、その帰納型の処理は参照実装のポートであるためです。 検証 Mario Carneiroのlean4leanは、Leanの型理論のLeanによる形式化であり、カーネルがそれを実装しているという証明です。作業は進行中であり、整合性の証明はまだ帰納型をカバーしていません。検証されるべき実装は、公式カーネルと同じバグの影響を受けていました。このバグは、この部分の検証を完了しようとしたときに発見されたでしょう。 メタプログラミングの削除について 議論の中での提案の1つは、この攻撃が表現できないようにメタプログラミングを削除または制限することです。これは誤解です。エラボレーターは設計上信頼されていません。健全性は、信頼されていないコンポーネントが悪意のある項の構築を拒否することに依存できません。悪意のある証明を提出したい攻撃者は、.oleanファイルを直接書き込んだり、メモリを変更したりすることもできます。これらはすべてエラボレーターを完全にバイパスします。カーネルは、それ自身のプロセス内で、型が不正な宣言を自身で拒否する必要があります。この懸念事項の分離と独立性は、証明項の主な利点の1つです。 FROは何をしているのか 悪用およびArthur Adjedjによって提起された関連する非一様パラメータのケースの回帰テストは、Kernel Arenaにあります。フォローアップPR（#14582）により、カーネルはネストされた出現のパラメータが、単に再型チェックするだけでなく、実際にパラメータとして振る舞うことをチェックするようになります。OpenAIのDaniel Selsamは、サイバーセキュリティに特化したAIを使用してLean FROを支援し、Leanカーネル内の他のプログラミングミスを発見しました。それらはすべて修正されました。それらはすべてnanodaによって捕捉されました。これらのバグもメタプログラミング経由でのみ到達可能です。PR: #14607, #14608, #14609, #14613, #14615, #14616。カーネルの不変条件も強化しました。PR: #14621, #14631, #14632。 comparator.liveは現在デフォルトでnanodaを実行しており、nanodaは毎日追跡されているため、lean-evalとcomparatorはアップストリームの修正後に最新の状態に保たれます。私たちは、さらなるバグを発見し、新しいカーネルを開発し、理論または検証済みカーネルに取り組むことができる専門家と連絡を取り、支援しています。 謝辞 この投稿に関するレビューと提案をしてくれたJoachim BreitnerとSebastian Ullrichに感謝します。