Not Letting Proofs Die: xLaDe, a Lean 4 Ecosystem Framework

現代の数学およびソフトウェア工学の世界では、コンピュータが絶対的な正当性をチェックできる方法で証明やプログラムを書こうとする動きが広がっています。複雑な議論の間違いを人間の目で見つけ出す代わりに、研究者は「証明助手（プルーフ・アシスタント）」と呼ばれる特化したソフトウェアツールを使用します。これらのプログラムは厳格な編集者のように機能し、結果が疑いようのない真実であることを保証するために、あらゆる論理的ステップを検証します。Lean 4のようなシステムは、この作業のために普及しており、大規模なチームが検証済みの数学ライブラリや安全なソフトウェアを構築することを可能にしています。しかし、これらのツールは常に更新され、改善され続けています。ある設計図に基づいて建てられた家が、明日もし建設ルールが変わったら立っていられなくなる可能性があるのと同様に、今日完璧に動作する数学的証明も、ソフトウェアのバージョンが変われば明日には動作しなくなる可能性があります。これは科学の長期的な歴史において問題を引き起こします。もしツールが進化しすぎると、今日行われた作業が将来、再現不可能になったり理解不能になったりする可能性があるからです。

アンドラ・プラデーシュ中央大学の研究チームは、ソフトウェアの変化を止めるのではなく、その周囲に保護層を構築することによって、この課題に対処する新しい方法を提案しました。彼らは、その創造物を「xLaDe（Experimental Lean 4 Advanced Development Ecosystem：実験的Lean 4高度開発エコシステム）」と呼んでいます。xLaDeは、既存のツールを時間の経過とともに凍結させたり、変化しないよう強制したりするのではなく、既存のツールの上の層に位置する、洗練された記録・管理システムとして機能します。その目的は、コアとなるソフトウェアを強固で変更不可能な基盤として扱い、その上の表面で研究者が自由に実験できるようにすることです。このフレームワークは、証明がどのように実行されたかという詳細（使用されたソフトウェアの特定のバージョン、依存関係、および環境の正確な条件）をすべて捕捉するように設計されており、たとえ基礎となるツールが進歩したとしても、数年後にその作業を再構築できるようにしています。

xLa解の核心となるアイデアは、システムの信頼できる心臓部と、その周囲で行われる実験的な作業との間の厳格な分離にあります。研究者はLeanソフトウェア自体を「イミュータブル（不変）なインフラストラクチャ」として扱っており、実験によって変更されることは決してありません。代わりに、xLaDeはオーケストレーション・レイヤー、つまり外部プロジェクトに触れることなくそれらを包み込む一連のツールとして機能します。このアプローチにより、科学者は数学的証明自体の完全性を損なうことなく、新しいアイデアをテストしたり、ワークフローを変更したり、作業の整理方法を試したりすることができます。もし実験が失敗したり破棄する必要が生じたりしても、跡を残したりプロジェクトの安定した部分に影響を与えたりすることなく、クリーンに削除することができます。この可逆性は極めて重要であり、研究者が自身の作業を永久に壊してしまうという恐怖を感じることなく、新しいことに挑戦することを促進します。

このシステムを使用可能にするために、チームはユーザーのメインインターフェースとして機能するコマンドラインツールを構築しました。このツールは異なる「モード」の運用を管理し、同じフレームワークが異なるニーズに応えられるようにしています。初心者向けの穏やかなガイダンスを提供するオンボーディング・モード、研究者が新しいワークフローやポリシーをテストできる実験モード、そして信頼性の高い長期利用のために設定を固定する安定モードがあります。安定モードでは、予期せぬ変更が発生しないように厳格なルールが適用され、研究結果の保存に理想的な状態となります。また、このツールは、実験が実行された時間や関与した特定のソフトウェアバージョンなどのメタデータを自動的に記録し、詳細な監査証跡を作成します。これにより、将来この作業を見る人が、どのように行われたかを正確に把握し、再現するために必要な情報を得られるようにしています。

研究者たちは、このフレームワークが実際に機能するかどうかを確認するために、2つの具体的な実験で検証を行いました。最初のテストでは、研究のために特別に作成された小規模で自己完結型のプロジェクトをxLaDeシステムの中にラップしました。彼らは、元のコードを一行も変更することなく、プロジェクトのビルドプロセスをフレームワーク経由で実行しました。システムは証明を正常にコンパイルし、結果を記録することに成功し、フレームワーク自体から完全に分離した状態で外部プロジェクトを管理できることを証明しました。2つ目のより厳格なテストでは、同じ手法を、チーム外の人物によって作成されたLean 4の完全に独立した教育コースに適用しました。このプロジェクトはxLaDeと事前の関係はありませんでした。フレームワークは、コースのファイルやLeanソフトウェアを修正することなく、コースを正常に統合し、ビルドプロセスを実行して、それが動作することを確認しました。これらの結果は、システムがユニバーサルなラッパーとして機能し、多様なプロジェクトを共通のルールに基づいて管理・再現できることを示唆しています。

セキュリティと信頼性はxLaDeの設計の中心です。研究者たちは、コンピュータの侵害やコードへのアクセス権を持つ悪意のある内部関係者といった、あらゆる脅威から保護することはできないと認めています。その代わりに、彼らは透明性と検証に焦点を当てています。システムはコードをホストするために複数のミラーを使用しており、一つのウェブサイトがダウンしてもプロジェクトが他の場所でアクセス可能であることを保証しています。また、デジタル指紋である暗号鍵とチェックサムを公開しており、これによりユーザーがダウンロードしたファイルが、著者の意図した通りのものであり、隠れた変更がないことを検証できます。このセキュリティモデルの重要な部分は、コアとなるLeanソフトウェアに対するあらゆる変更の試みを自動的に検出することです。もしスクリプトやユーザーが変更不可能な基盤を変更しようとした場合、システムは違反を検出し、プロセスを停止し、実験的なツールによって数学的証明の完全性が決して損なわれないようにします。

論文は、xLaDeがまだ実験的なプロジェクトであり完成した解決策ではないものの、形式検証の未来に向けた有望な道筋を提供していると結論付けています。それは、古いコードを新しいツールに強制的に適合させる「後方互換性」の問題を解決すると主張しているわけではありません。その代わりに、別の解決策、すなわち、コードが書かれた際の「文脈（コンテキスト）」を保存するという解決策を提示しています。環境を記録し、実験を第一級の研究成果物として扱うことで、このフレームワークはコミュニティが自信を持って過去の結果を再訪することを可能にします。著者らは、彼らの仕事はエコシステム研究を行うための「メソドロジー（手法）」であり、アイデアをテストし、失敗を記録し、成功したツールを共有するための構造化された方法を提供しているのだと強調しています。このアプローチを通じて、彼らは、証明助手の急速な進化が、その上に築かれた貴重な成果を失うことにならないような、持続可能な環境を構築することを目指しています。