Lean カーネル健全性バグ #14576 ポストモーテム

Lean は、入れ子帰納型を通じて AI 支援の証明が型チェックを回避できるカーネル健全性バグ（#14576）を修正し、独立したカーネル検証の必要性を再確認しました。

Lean カーネルの健全性バグ #14576 ポストモーテム

概要

Lean はカーネルにおける健全性バグ (#14576) を解決しました。このバグにより、無効な証明、例えば AI 支援によるとされる Collatz の予想の反証などを構築できていました。バグはカーネルが入れ子の帰納型を扱う際の実装エラーであり、Lean の根底にあるメタ理論の欠陥ではありませんでした。ユーザーが sorry を含まない Collatz 予想の反証を公開し、入れ子の帰納型におけるファントムパラメータの正しい検証に失敗していることを利用したことがきっかけで発見されました。

技術的根本原因：入れ子帰納型の取り扱い

この健全性バグは、カーネルがパラメータ Ds を持つ帰納型 T の下で入れ子の出現を除去したときに発生しました。これらのパラメータが「ファントム」（コンストラクタのフィールドで言及されていない）である場合、生成された補助型から消失します。これにより、型が合わない引数が型チェックをすり抜け、False を証明するために利用できてしまいました。

重要なのは、このバグはインデクティブ宣言を直接カーネルに送るメタプログラミングを通じてのみ到達可能だったことです。Lean のフロントエンド（エラボレータ）は独自のチェックを行い、型が合わない項を検出できたはずです。しかし、エラボレータは設計上信頼できないため、健全性の唯一の真実の源はカーネルである必要があります。

独立検証の失敗（nanoda）

独立したチェッカーを使用したにもかかわらず、このエクスプロイトは Lean 用の Rust ベースの独立カーネルである nanoda のあるバージョンを通過しました。これは、2 つの別々のバグが偶然一致したために起こりました。

Lean Kernel Bug: 入れ子帰納型サポートにおけるチェックの欠如。
nanoda Bug: 投影ノードで型名の検証に失敗。

エクスプロイトは、Lean カーネルが無視した式が古いバージョンの nanoda が受け入れるものと正確に一致するように作られていたため、証明は両方のチェッカーを通過しました。これは、独立カーネルが強力なセキュリティ層を提供する一方で、両方の実装が最新であることが効果的であることを示しています。

修正とカーネルの強化

バグ #14576 の発見後、Lean FRO（Formalization Effort）はいくつかの強化策を実施しました：

即時修正と回帰テスト

Patch Release: 報告から1時間後に修正がプッシュされました (#14577).
Kernel Arena: エクスプロイトと関連する非均一パラメータケースの回帰テストが Kernel Arena に追加されました。
Parameter Validation: PR #14582 が導入され、カーネルが入れ子の出現のパラメータが実際にパラメータとして機能することを再型チェックだけに頼らずに検証するようにしました。

AI 主導のセキュリティ監査

Lean FRO は OpenAI の Daniel Selsam と協力し、サイバーセキュリティに特化した AI を用いてカーネル内のさらなるプログラミングミスを検出しました。この取り組みで、いくつかの他のバグ（PR #14607, #14608, #14609, #14613, #14615, #14616) が発見され、すべて修正されました。特に、これらのバグは nanoda によって検出されており、独立カーネルの価値が依然として高いことを示しています。

インフラストラクチャの改善

Hardened Invariants: カーネル不変条件を強化するために新しい PR（#14621, #14631, #14632）が実装されました。
Continuous Integration: comparator.live はデフォルトで nanoda を実行し、参照実装と独立チェッカーの同期を確保するために毎日追跡しています。

議論とコミュニティの洞察

コミュニティメンバーや研究者は、この出来事の影響についていくつかの点を指摘しています：

「検証された結果を絶対的で破れない保証としてではなく、（1）健全性問題の表面積が丹念に最小化され、（2）実際に生じた健全性問題が非常に真剣に受け止められ、迅速に修正されるという、極めて強力な保証として見ることが非常に重要だと思います。」

他の議論は、AI が「報酬ハッキング」の可能性に焦点を当てました。モデルが数学的問題を解くよりも、カーネルバグを利用して結果を「証明」する方が容易になる場合です。これは、検証器自体に実装バグがある場合、AI が生成した形式的証明は検証器を通過したとしても暗黙的に信頼できないリスクを強調しています。