LeanBET: Formally-verified surface area calculations in Lean

本論文は、数学的正当性を保証しつつ確立された BETSI 参照実装とほぼ完全な数値的合致を達成する Lean 4 で実装された、完全に実行可能かつ形式的に検証された Brunauer–Emmett–Teller (BET) 表面積分析パイプラインである LeanBET を提示する。

要約

スポンジの表面積を測定しようとしていると想像してください。ただし、そのスポンジは目に見えない微細な穴でできているとします。科学者たちは、ガスがスポンジにどのように付着するかを観察することでこの面積を推定するために、BET（3 人の科学者の名前にちなんで名付けられた）と呼ばれる手法を使用します。これは化学における標準的なツールですが、箱の絵がぼやけたパズルを解こうとするようなものです。

ここで問題があります。答えを得るために、科学者たちは実験から特定のデータ点の範囲を選び、それらを通る直線を描かなければなりません。問題は、異なる人々（または異なるコンピュータプログラム）がわずかに異なる範囲を選ぶ可能性があることです。ある人は「中央の 10 点を使おう」と言い、別の人は「いいえ、中央の 12 点を使おう」と言うかもしれません。これにより、同じスポンジに対して異なる答えが導き出され、結果に対する混乱と信頼の欠如を引き起こします。

これを解決するために、チームは「最良」の範囲を見つけるためにデータのあらゆる可能な範囲を自動的にチェックするBETSIというコンピュータプログラムを作成しました。これは、完璧に合うピースを見つけるために、あらゆる可能なパズルの組み合わせを試すロボットを持っているようなものです。しかし、ロボットであってもバグがあったり、微妙な誤りを引き起こす隠れた前提があったりする可能性があります。

「LeanBET」の登場：数学的に証明されたロボット

この論文の著者たちは、Lean 4と呼ばれる特別なコンピュータツールを用いて、このロボットの新しいバージョンを構築しました。Lean 4 を単なるプログラミング言語ではなく、証明なしに間違いを許さない超厳格な数学の先生と考えてみてください。

以下に、いくつかの単純なアナロジーを用いて、彼らがどのように行ったかを示します。

1. 「二重脳」システム（多相性）

通常、コンピュータプログラムを書くときは、「浮動小数点数」（電卓に表示されるような数値）を使用します。これらは高速ですが、コンピュータが無限の精度を保持できないため、わずかに不正確です。数学的証明を行う際には、「実数」（完璧で無限の精度）を使用しますが、それらをコンピュータ上で実行することはできません。

著者たちは、変形するロボットを構築することでこれを解決しました。

• 脳 A（証明）： 数学が正しいことを証明する必要があるとき、ロボットは「実数」のスーツを着ます。完璧で理論的な数学を行い、論理が欠陥がないことを証明します。
• 脳 B（実行）： 実際のデータでプログラムを実行する必要があるとき、ロボットは「浮動小数点数」のスーツに切り替えます。実際のコンピュータ上で高速に実行します。
• 魔法： ロボットが両方のスーツで同じように構築されているため、「証明脳」が論理が完璧であると述べるならば、「実行脳」も同じ規則に従うことが保証されます。これは、完璧な数学で橋の設計が安全であることを証明し、その後、実際の鋼鉄で橋を建設する際に、その設計が耐えられることを知っているようなものです。

2. 「レシピ対調理」（導出を仕様として）

通常の科学では、紙の上にレシピ（数学理論）を書き、その後、シェフ（プログラマー）がキッチン（ソフトウェア）でそれを調理しようとします。時にはシェフがここに少し塩を加えたり、そこに少し加えたり、あるいは手順を誤解したりして、出来上がった料理がレシピとは異なる味になることがあります。

LeanBETでは、レシピと調理が同じ部屋で行われます。「数学的導出」（レシピ）がコードに直接記述されます。コンピュータは、コードがまさにレシピそのものであることを確認します。コードが「塩を加える」と述べる場合、数学的証明は「塩を加える」ことが理論が要求するものと完全に一致することを検証します。理論と実践の間にギャップはありません。

3. 「厳格な検査官」（形式的検証）

この論文は、彼らのプログラムが単に答えを「推測」するのではなく、正しさの証明書を伴って運ぶと主張しています。

• 標準ソフトウェア： プログラムを実行すると、数値が返され、それが正しいことを願うしかありません。
• LeanBET： プログラムを実行すると、数値が返され、さらに「すべてのステップを確認し、すべての規則に従い、この数値はあなたが提供したデータに基づいて唯一の正しい答えである」と数学的に証明された書類も手渡されます。

彼らは何を見つけましたか？

彼らは、19 組の異なるデータセット（19 種類の異なるスポンジのようなもの）を使用して、新しい「数学的に証明されたロボット」を古い「標準ロボット」（BETSI）と比較しました。

• 結果： 19 個のスポンジのうち 18 個について、2 つのロボットは最も小さな小数点まで完全に同じ答えを出しました。
• 1 つの glitches： 1 つのスポンジ（UiO-66 と呼ばれる）では、わずかな違い（0.03%）がありました。著者たちは、なぜそうなのかはまだ確信が持てないと認めていますが、これは実験における通常のノイズと比較して非常に小さな誤差です。

結論

この論文は、スポンジを測定する新しい方法を発明することについてではありません。既存の方法の信頼できるバージョンを構築することについてです。彼らは標準的な科学ツールを取り、それを「数学的証明」環境内で再構築し、それが古いツールと同じように機能するだけでなく、論理的な間違いを犯していないという保証があることを示しました。

これは、単なる地図から、ルートだけでなく、隠れた迂回路なしに、そのルートが最短かつ最安全であることをステップバイステップで証明する GPS へとアップグレードするようなものです。

技術概要

「LeanBET: Lean における形式検証された表面積計算」の技術的概要

問題定義
Brunauer–Emmett–Teller（BET）法は、ガス吸着等温線から比表面積を推定するための標準的な枠組みである。しかし、実用的な実装には、特に線形回帰のための相対圧力範囲の選択において、重大な主観性が伴う。一貫性基準（Rouquerol 基準）は有効な領域をフィルタリングするために存在するが、複数の圧力区間がこれらの規則を満たすことが多く、異なる実験室やソフトウェア実装間で報告される表面積に変動が生じる。BET 表面同定（BETSI）アルゴリズムなどのこのプロセスを標準化しようとする以前の取り組みは、汎用数値ソフトウェア（Python）に依存している。BETSI は網羅的な列挙を通じて主観性を低減するが、それは数値アルゴリズムであり、隠れた実装上の仮定や微妙な誤りを形式的に排除することができず、出力の科学的保証は未検証のままとされている。

手法
著者らは、Lean 4 定理証明器で実装された、完全に実行可能かつ形式検証された BET 分析パイプラインであるLeanBETを提示する。このアプローチは、単一の環境内で実行可能コードと数学的証明を統合し、計算と検証の間のギャップを埋めるために多態的数値設計を利用する：

• 多態性：アルゴリズムは、BETLike 型クラスによって制約された汎用型 α を用いて記述されている。これにより、同じコード構造が、実実験データでの効率的な実行のために浮動小数点数（Float）上で、また非計算可能な数学的証明のために実数（Real）上でインスタンス化される。
• 導出を仕様として：BET 線形化方程式の代数的導出は、単なる動機付けではなく、形式的仕様として機能する。コードはこの導出を反映するように構築されており、実行可能な変換が理論モデルと一致することを保証する。
• ワークフロー：パイプラインは、それぞれが形式的証明とペアになった以下のステップを実行する：
  1. ウィンドウ列挙：少なくとも 2 つのデータ点を含む等温線のすべての連続部分リストを体系的に生成する。
  2. 線形化：データ点 $(p, n)$ を線形化された BET 形式 $p/[n(1-p)]$ に変換する。
  3. 線形回帰：各ウィンドウに対して最小二乗回帰を実行し、傾き、切片、および $R^2$ を抽出する。
  4. 許容性チェック：Rouquerol 基準（$n(1-p)$ の単調性、パラメータ $C$ と $n_m$ の正性、および単分子層圧力の一貫性）に基づいて候補をフィルタリングする。
  5. ニー選択：有効なウィンドウ間の同着を、最大の終端インデックスを持つウィンドウを選択することで解決し、さらに同着がある場合は最小のパーセント誤差で解決する。

主な貢献

1. BETSI パイプラインの形式検証：本論文は、完全な BETSI ワークフローの最初の機械検証実装を提供する。実行可能コードが BET 理論の数学的定義と特定の選択基準を満たすことを証明する。
2. 健全性と完全性の証明：著者らは以下を形式的に証明する：
   • 定理 A.1 および A.2：BET 等温線方程式は層モデルの仮定から導出され、線形化ステップは代数的に正しい。
   • 定理 A.3：ウィンドウ列挙は健全（有効なウィンドウのみが生成される）かつ完全（有効な連続ウィンドウが漏れることはない）である。
   • 定理 A.4 および A.5：回帰ステップは真の最小二乗最小化子を返し、抽出された物理パラメータ（$n_m$、$C$）はそれらの理論的定義と一致する。
   • 定理 A.6 および A.7：許容性チェックとニーに基づく選択戦略は、その形式的仕様を厳密に満たす。
3. 多態的実装：この研究は、正しさが理想化された実数上で証明されながら、実行は浮動小数点演算で行われる、Lean における科学計算の実用的なパターンを実証する。これにより、別個の検証言語の必要性を回避している。

結果
LeanBET の実装は、19 個の吸着等温線からなるベンチマークセットを用いて、参照となる Python ベースの BETSI 実装に対して評価された。

• 数値的合意：LeanBET は、19 個の等温線のうち18 個において、BETSI 参照値と機械精度で一致する。
• 不一致：UiO-66データセットについては、約0.03%（0.36 m²/g）の偏差が観測された。著者らは、この特定の偏差の原因は未確定であると指摘しつつも、それが典型的な実験的不確かさよりも著しく小さいことを強調している。
• 検証ステータス：すべての証明が正常にコンパイルされ、アルゴリズムの出力が指定された数学的制約に準拠していることを機械検証された保証として提供した。

重要性
本論文は、LeanBET が、確立された参照実装との数値的合意を犠牲にすることなく、定理証明器内で実用的な科学計算ワークフローを構築できることを実証していると主張する。主な貢献は新しいアルゴリズムではなく、正しさの形式的検証保証である。実行可能パイプラインを機械検証された数学的命題にリンクさせることで、この研究は、実装が基礎となる理論および選択基準に準拠していることに関する曖昧さを排除することにより、BET 分析における再現性危機に対処する。著者らはこれを、材料科学における理論的導出とソフトウェア実装の間のギャップを埋めるための一歩として位置づけている。