LeanBET: Formally-verified surface area calculations in Lean

Dieser Beitrag stellt LeanBET vor, eine vollständig ausführbare und formal verifizierte Pipeline zur BET-Oberflächenanalyse (Brunauer–Emmett–Teller), die in Lean 4 implementiert ist, mathematische Korrektheit garantiert und eine nahezu perfekte numerische Übereinstimmung mit der etablierten BETSI-Referenzimplementierung erzielt.

Das Wesentliche

Stellen Sie sich vor, Sie versuchen, die Oberfläche eines Schwamms zu messen, doch dieser Schwamm besteht aus unsichtbaren, mikroskopischen Poren. Wissenschaftler verwenden eine Methode namens BET (benannt nach drei Wissenschaftlern), um diese Fläche zu schätzen, indem sie beobachten, wie sich Gas an dem Schwamm anlagert. Es ist ein Standardwerkzeug in der Chemie, doch es ist ein wenig wie der Versuch, ein Puzzle zu lösen, bei dem das Bild auf der Schachtel verschwommen ist.

Hier liegt das Problem: Um die Antwort zu erhalten, müssen Wissenschaftler einen spezifischen Bereich von Datenpunkten aus ihrem Experiment auswählen und eine gerade Linie durch diese ziehen. Das Problem besteht darin, dass verschiedene Personen (oder verschiedene Computerprogramme) möglicherweise leicht unterschiedliche Bereiche auswählen. Eine Person könnte sagen: „Lassen Sie uns die mittleren 10 Punkte verwenden", während eine andere sagt: „Nein, verwenden Sie die mittleren 12." Dies führt zu unterschiedlichen Ergebnissen für denselben Schwamm, was Verwirrung stiftet und das Vertrauen in die Ergebnisse erschüttert.

Um dies zu beheben, entwickelte ein Team ein Computerprogramm namens BETSI, das automatisch jeden möglichen Datenbereich prüft, um den „besten" zu finden. Es ist, als hätte man einen Roboter, der jede mögliche Kombination von Puzzlestücken durchspielt, um diejenige zu finden, die perfekt passt. Doch selbst Roboter können Fehler enthalten oder versteckte Annahmen haben, die sie auf subtile Weise falsch machen.

Hier kommt „LeanBET" ins Spiel: Der mathematisch verifizierte Roboter

Die Autoren dieser Arbeit bauten eine neue Version dieses Roboters mit einem speziellen Computerwerkzeug namens Lean 4. Betrachten Sie Lean 4 nicht nur als Programmiersprache, sondern als einen überstrengen Mathematiklehrer, der Ihnen niemals einen Fehler ohne Beweis durchgehen lässt.

So haben sie es getan, unter Verwendung einiger einfacher Analogien:

1. Das „Zwei-Gehirn"-System (Polymorphismus)

Normalerweise verwenden Sie beim Schreiben eines Computerprogramms „Gleitkommazahlen" (wie die Zahlen auf einem Taschenrechner). Diese sind schnell, aber etwas ungenau, da Computer keine unendliche Präzision halten können. Bei mathematischen Beweisen verwendet man „reelle Zahlen" (perfekt, unendliche Präzision), doch diese lassen sich nicht auf einem Computer ausführen.

Die Autoren lösten dies, indem sie einen gestaltwandelnden Roboter bauten.

• Gehirn A (Der Beweis): Wenn sie beweisen müssen, dass die Mathematik korrekt ist, trägt der Roboter einen „Reelle-Zahlen"-Anzug. Er führt perfekte, theoretische Mathematik aus, um zu beweisen, dass die Logik fehlerfrei ist.
• Gehirn B (Die Ausführung): Wenn sie das Programm auf echten Daten ausführen müssen, wechselt der Roboter in einen „Gleitkommazahl"-Anzug. Er läuft schnell auf tatsächlichen Computern.
• Die Magie: Da der Roboter in beiden Anzügen auf die gleiche Weise gebaut ist, garantiert das „Beweis-Gehirn", dass das „Ausführungs-Gehirn" dieselben Regeln befolgt, wenn es sagt, die Logik sei perfekt. Es ist, als würde man die Sicherheit einer Brückenkonstruktion mit perfekter Mathematik beweisen und dann die tatsächliche Brücke aus echtem Stahl bauen, in dem Wissen, dass das Design standhält.

2. Das „Rezept versus das Kochen" (Ableitung als Spezifikation)

In der normalen Wissenschaft schreiben Sie ein Rezept (die mathematische Theorie) auf Papier, und dann versucht ein Koch (der Programmierer), es in der Küche (der Software) zuzubereiten. Manchmal fügt der Koch hier oder dort eine Prise Salz hinzu oder versteht einen Schritt falsch, und das Gericht schmeckt anders als das Rezept.

Bei LeanBET finden Rezept und Kochen im selben Raum statt. Die „mathematische Ableitung" (das Rezept) wird direkt in den Code geschrieben. Der Computer prüft, dass der Code das Rezept ist. Wenn der Code sagt „Salz hinzufügen", verifiziert der mathematische Beweis, dass „Salz hinzufügen" genau das ist, was die Theorie verlangt. Es gibt keine Lücke zwischen Theorie und Praxis.

3. Der „Strengen Inspektor" (Formale Verifikation)

Die Arbeit behauptet, dass ihr Programm nicht nur die Antwort rät; es trägt ein Zertifikat der Korrektheit bei sich.

• Standard-Software: Sie führen das Programm aus, es liefert eine Zahl, und Sie hoffen, dass sie richtig ist.
• LeanBET: Sie führen das Programm aus, es liefert eine Zahl, und es übergibt Ihnen auch ein mathematisch bewiesenes Dokument mit der Aussage: „Ich habe jeden Schritt überprüft, ich habe jede Regel befolgt, und diese Zahl ist die einzig korrekte Antwort basierend auf den Daten, die Sie mir gegeben haben."

Was haben sie herausgefunden?

Sie testeten ihren neuen „mathematisch verifizierten Roboter" gegen den alten „Standard-Roboter" (BETSI) unter Verwendung von 19 verschiedenen Datensätzen (wie 19 verschiedene Schwämme).

• Das Ergebnis: Bei 18 von 19 Schwämmen gaben die beiden Roboter exakt dieselbe Antwort bis auf die kleinste Dezimalstelle.
• Der eine Fehler: Bei einem Schwamm (genannt UiO-66) gab es einen winzigen Unterschied (0,03 %). Die Autoren geben zu, dass sie noch nicht sicher sind, warum, doch es ist ein sehr kleiner Fehler im Vergleich zum üblichen Rauschen in Experimenten.

Das Fazit

Diese Arbeit handelt nicht davon, eine neue Methode zur Messung von Schwämmen zu erfinden. Es geht darum, eine vertrauenswürdige Version der bestehenden Methode zu bauen. Sie nahmen ein Standardwissenschaftliches Werkzeug, bauten es in einer „mathematisch bewiesenen" Umgebung neu auf und zeigten, dass es genauso gut funktioniert wie die alten Werkzeuge, jedoch mit der Garantie, dass es keine logischen Fehler gemacht hat.

Es ist wie der Upgrade von einer normalen Landkarte zu einem GPS, das Ihnen nicht nur die Route anzeigt, sondern auch Schritt für Schritt beweist, dass die Route die kürzeste und sicherste mögliche ist, ohne versteckte Umwege.

Technische Zusammenfassung

Technische Zusammenfassung von "LeanBET: Formal verifizierte Oberflächenberechnungen in Lean"

Problemstellung
Die Brunauer–Emmett–Teller (BET)-Methode ist der Standardrahmen zur Schätzung der spezifischen Oberfläche aus Gasadsorptionsisothermen. Die praktische Umsetzung beinhaltet jedoch erhebliche Subjektivität, insbesondere bei der Auswahl des relativen Druckbereichs für die lineare Regression. Zwar existieren Konsistenzkriterien (Rouquerol-Kriterien), um gültige Bereiche zu filtern, doch erfüllen häufig mehrere Druckintervalle diese Regeln, was zu Variabilität der berichteten Oberflächenwerte zwischen verschiedenen Laboren und Softwareimplementierungen führt. Bisherige Bemühungen zur Standardisierung dieses Prozesses, wie der BET Surface Identification (BETSI)-Algorithmus, verlassen sich auf allgemeine numerische Software (Python). Obwohl BETSI die Subjektivität durch erschöpfende Enumeration reduziert, bleibt es ein numerischer Algorithmus, bei dem versteckte Implementierungsannahmen oder subtile Fehler nicht formal ausgeschlossen werden können, wodurch die wissenschaftlichen Garantien der Ausgabe unverifiziert bleiben.

Methodik
Die Autoren präsentieren LeanBET, eine vollständig ausführbare und formal verifizierte BET-Analysepipeline, die im Lean-4-Theorembeweiser implementiert ist. Der Ansatz integriert ausführbaren Code mit mathematischen Beweisen in einer einzigen Umgebung und nutzt ein polymorphes numerisches Design, um die Lücke zwischen Berechnung und Verifikation zu schließen:

• Polymorphie: Der Algorithmus wird mit einem generischen Typ α geschrieben, der durch eine BETLike-Typklasse eingeschränkt ist. Dies ermöglicht es, dieselbe Codestruktur über Gleitkommazahlen (Float) für eine effiziente Ausführung mit realen experimentellen Daten und über reelle Zahlen (Real) für nicht-berechenbare mathematische Beweise zu instanziieren.
• Ableitung als Spezifikation: Die algebraische Ableitung der linearisierten BET-Gleichung dient nicht nur als Motivation, sondern als formale Spezifikation. Der Code ist so konstruiert, dass er dieser Ableitung entspricht, wodurch sichergestellt wird, dass die ausführbare Transformation dem theoretischen Modell entspricht.
• Arbeitsablauf: Die Pipeline führt die folgenden Schritte durch, wobei jeder Schritt mit einem formalen Beweis gekoppelt ist:
  1. Fenster-Enumeration: Systematische Generierung aller zusammenhängenden Teillisten der Isotherme, die mindestens zwei Datenpunkte enthalten.
  2. Linearisierung: Transformation der Datenpunkte $(p, n)$ in die linearisierte BET-Form $p/[n(1-p)]$.
  3. Lineare Regression: Durchführung einer Ausgleichsrechnung nach der Methode der kleinsten Quadrate für jedes Fenster, um Steigung, Achsenabschnitt und $R^2$ zu extrahieren.
  4. Zulässigkeitsprüfungen: Filterung von Kandidaten basierend auf den Rouquerol-Kriterien (Monotonie von $n(1-p)$, Positivität der Parameter $C$ und $n_m$ sowie Konsistenz des Monolayer-Drucks).
  5. Knie-Auswahl: Auflösung von Gleichständen unter den gültigen Fenstern durch Auswahl des Fensters mit dem größten Endindex; bei weiteren Gleichständen wird der kleinste prozentuale Fehler herangezogen.

Hauptbeiträge

1. Formale Verifikation der BETSI-Pipeline: Der Artikel bietet die erste maschinell geprüfte Implementierung des gesamten BETSI-Arbeitsablaufs. Er beweist, dass der ausführbare Code den mathematischen Definitionen der BET-Theorie und den spezifischen Auswahlkriterien entspricht.
2. Korrektheits- und Vollständigkeitsbeweise: Die Autoren beweisen formal:
   • Satz A.1 & A.2: Die BET-Isothermengleichung wird aus Annahmen des Schichtenmodells abgeleitet, und der Linearisierungsschritt ist algebraisch korrekt.
   • Satz A.3: Die Fenster-Enumeration ist korrekt (nur gültige Fenster werden generiert) und vollständig (kein gültiges zusammenhängendes Fenster wird übersehen).
   • Satz A.4 & A.5: Der Regressionsschritt liefert einen wahren Minimierer der kleinsten Quadrate, und die extrahierten physikalischen Parameter ($n_m$, $C$) stimmen mit ihren theoretischen Definitionen überein.
   • Satz A.6 & A.7: Die Zulässigkeitsprüfungen und die auf dem Knie basierende Auswahlstrategie erfüllen ihre formalen Spezifikationen strikt.
3. Polymorphe Implementierung: Die Arbeit demonstriert ein praktisches Muster für wissenschaftliches Rechnen in Lean, bei dem die Korrektheit über idealisierte reelle Zahlen bewiesen wird, während die Ausführung über Gleitkommaarithmetik erfolgt, wodurch die Notwendigkeit separater Verifikationssprachen entfällt.

Ergebnisse
Die LeanBET-Implementierung wurde anhand eines Benchmark-Satzes von 19 Adsorptionsisothermen gegen die referenzielle Python-basierte BETSI-Implementierung evaluiert.

• Numerische Übereinstimmung: LeanBET stimmt mit der BETSI-Referenz für 18 der 19 Isothermen bis zur Maschinenpräzision überein.
• Abweichung: Beim UiO-66-Datensatz wurde eine Abweichung von ungefähr 0,03 % (0,36 m²/g) beobachtet. Die Autoren stellen fest, dass die Ursache dieser spezifischen Abweichung unbestimmt bleibt, betonen jedoch, dass sie deutlich kleiner ist als typische experimentelle Unsicherheiten.
• Verifikationsstatus: Alle Beweise wurden erfolgreich kompiliert und liefern maschinell geprüfte Garantien, dass die Ausgabe des Algorithmus den spezifizierten mathematischen Einschränkungen entspricht.

Bedeutung
Der Artikel behauptet, dass LeanBET zeigt, wie ein praktischer wissenschaftlicher Arbeitsablauf in einem Theorembeweiser aufgebaut werden kann, ohne die numerische Übereinstimmung mit etablierten Referenzimplementierungen zu opfern. Der primäre Beitrag ist kein neuer Algorithmus, sondern eine formal verifizierte Garantie der Korrektheit. Durch die Verknüpfung der ausführbaren Pipeline mit maschinell geprüften mathematischen Aussagen adressiert die Arbeit die Reproduzierbarkeitskrise in der BET-Analyse, indem sie Mehrdeutigkeiten bezüglich der Einhaltung der zugrundeliegenden Theorie und der Auswahlkriterien durch die Implementierung beseitigt. Die Autoren positionieren dies als einen Schritt zur Überbrückung der Lücke zwischen theoretischen Ableitungen und Softwareimplementierungen in den Materialwissenschaften.