LeanBET: Formally-verified surface area calculations in Lean

Cet article présente LeanBET, une chaîne d'analyse de surface spécifique BET (Brunauer–Emmett–Teller) entièrement exécutable et formellement vérifiée, implémentée en Lean 4, qui garantit l'exactitude mathématique tout en obtenant un accord numérique quasi parfait avec l'implémentation de référence BETSI établie.

L'essentiel

Imaginez que vous essayez de mesurer la surface d'une éponge, mais que cette éponge est constituée de trous invisibles et microscopiques. Les scientifiques utilisent une méthode appelée BET (du nom de trois scientifiques) pour estimer cette surface en observant comment un gaz adhère à l'éponge. C'est un outil standard en chimie, mais c'est un peu comme essayer de résoudre un puzzle dont l'image sur la boîte est floue.

Voici le problème : pour obtenir la réponse, les scientifiques doivent sélectionner une plage spécifique de points de données issus de leur expérience et tracer une ligne droite les reliant. Le problème est que différentes personnes (ou différents programmes informatiques) peuvent choisir des plages légèrement différentes. L'un pourrait dire : « Utilisons les 10 points du milieu », tandis qu'un autre dirait : « Non, utilisons les 12 points du milieu. » Cela conduit à des réponses différentes pour la même éponge, provoquant confusion et manque de confiance dans les résultats.

Pour résoudre cela, une équipe a créé un programme informatique appelé BETSI qui vérifie automatiquement chaque plage de données possible pour trouver la « meilleure ». C'est comme avoir un robot qui essaie chaque combinaison possible de pièces de puzzle pour trouver celle qui s'emboîte parfaitement. Cependant, même les robots peuvent comporter des bugs, ou des hypothèses cachées qui les rendent erronés de manière subtile.

Voici "LeanBET" : Le Robot Démontré par les Mathématiques

Les auteurs de cet article ont construit une nouvelle version de ce robot en utilisant un outil informatique spécial appelé Lean 4. Imaginez Lean 4 non pas seulement comme un langage de programmation, mais comme un professeur de mathématiques ultra-exigeant qui ne vous laisse jamais faire une erreur sans preuve.

Voici comment ils ont procédé, en utilisant quelques analogies simples :

1. Le Système à « Deux Cerveaux » (Polymorphisme)

Habituellement, lorsque vous écrivez un programme informatique, vous utilisez des « nombres à virgule flottante » (comme les nombres sur une calculatrice). Ils sont rapides mais légèrement imparfaits car les ordinateurs ne peuvent pas maintenir une précision infinie. Lorsque vous faites des preuves mathématiques, vous utilisez des « nombres réels » (parfaits, à précision infinie), mais vous ne pouvez pas les exécuter sur un ordinateur.

Les auteurs ont résolu ce problème en construisant un robot métamorphe.

• Cerveau A (La Preuve) : Lorsqu'ils doivent prouver que les mathématiques sont justes, le robot porte un costume de « Nombre Réel ». Il effectue des mathématiques théoriques parfaites pour prouver que la logique est impeccable.
• Cerveau B (L'Exécution) : Lorsqu'ils doivent exécuter le programme sur de vraies données, le robot change de costume pour un costume de « Virgule Flottante ». Il s'exécute rapidement sur de vrais ordinateurs.
• La Magie : Parce que le robot est construit de la même manière dans les deux costumes, si le « Cerveau Preuve » déclare que la logique est parfaite, le « Cerveau Exécution » est garanti de suivre les mêmes règles. C'est comme prouver qu'un pont est sûr avec des mathématiques parfaites, puis construire le pont réel avec de l'acier véritable, en sachant que la conception tient la route.

2. La « Recette vs La Cuisine » (La Dérivation comme Spécification)

En science normale, vous écrivez une recette (la théorie mathématique) sur papier, puis un chef (le programmeur) essaie de la cuisiner dans la cuisine (le logiciel). Parfois, le chef ajoute une pincée de sel ici ou là, ou mal interprète une étape, et le plat a un goût différent de la recette.

Dans LeanBET, la recette et la cuisson se déroulent dans la même pièce. La « dérivation mathématique » (la recette) est écrite directement dans le code. L'ordinateur vérifie que le code est la recette. Si le code dit « ajouter du sel », la preuve mathématique vérifie que « l'ajout de sel » est exactement ce que la théorie exige. Il n'y a aucun écart entre la théorie et la pratique.

3. L'« Inspecteur Strict » (Vérification Formelle)

L'article affirme que leur programme ne se contente pas de deviner la réponse ; il transporte avec lui un certificat de correction.

• Logiciel Standard : Vous exécutez le programme, il vous donne un nombre, et vous espérez qu'il est juste.
• LeanBET : Vous exécutez le programme, il vous donne un nombre, et il vous remet aussi un document prouvé mathématiquement disant : « J'ai vérifié chaque étape, j'ai suivi chaque règle, et ce nombre est la seule réponse correcte basée sur les données que vous m'avez fournies. »

Que Ont-ils Découvert ?

Ils ont testé leur nouveau « Robot Démontré par les Mathématiques » contre l'ancien « Robot Standard » (BETSI) en utilisant 19 ensembles de données différents (comme 19 éponges différentes).

• Le Résultat : Pour 18 éponges sur 19, les deux robots ont donné exactement la même réponse jusqu'à la plus petite décimale.
• Le Seul Bug : Pour une éponge (appelée UiO-66), il y avait une différence infime (0,03 %). Les auteurs admettent ne pas être encore sûrs de la raison, mais c'est une erreur très faible comparée au bruit habituel des expériences.

La Conclusion

Cet article ne porte pas sur l'invention d'une nouvelle façon de mesurer les éponges. Il s'agit de construire une version fiable de la méthode existante. Ils ont pris un outil scientifique standard, l'ont reconstruit dans un environnement de « preuve mathématique », et ont montré qu'il fonctionne aussi bien que les anciens outils, mais avec la garantie qu'il n'a commis aucune erreur logique.

C'est comme passer d'une carte ordinaire à un GPS qui non seulement vous indique l'itinéraire, mais prouve également, étape par étape, que cet itinéraire est le plus court et le plus sûr possible, sans détours cachés.

Résumé technique

Résumé technique de "LeanBET : Calculs de surface spécifique formellement vérifiés dans Lean"

Énoncé du problème
La méthode Brunauer–Emmett–Teller (BET) constitue le cadre standard pour estimer la surface spécifique à partir d'isothermes d'adsorption de gaz. Cependant, la mise en œuvre pratique implique une subjectivité significative, en particulier dans le choix de la plage de pression relative pour la régression linéaire. Bien que des critères de cohérence (critères de Rouquerol) existent pour filtrer les régions valides, plusieurs intervalles de pression satisfont souvent ces règles, entraînant une variabilité des surfaces spécifiques rapportées entre différents laboratoires et implémentations logicielles. Les efforts précédents visant à standardiser ce processus, tels que l'algorithme BETSI (BET Surface Identification), reposent sur des logiciels numériques à usage général (Python). Bien que BETSI réduise la subjectivité grâce à une énumération exhaustive, il reste un algorithme numérique où des hypothèses d'implémentation cachées ou des erreurs subtiles ne peuvent être formellement exclues, laissant les garanties scientifiques de la sortie non vérifiées.

Méthodologie
Les auteurs présentent LeanBET, un pipeline d'analyse BET entièrement exécutable et formellement vérifié, implémenté dans le proveur de théorèmes Lean 4. L'approche intègre du code exécutable et des preuves mathématiques au sein d'un seul environnement, en utilisant une conception numérique polymorphe pour combler le fossé entre le calcul et la vérification :

• Polymorphisme : L'algorithme est écrit en utilisant un type générique α contraint par une classe de types BETLike. Cela permet d'instancier la même structure de code sur des nombres à virgule flottante (Float) pour une exécution efficace sur des données expérimentales réelles et sur des nombres réels (Real) pour des preuves mathématiques non computables.
• Dérivation comme spécification : La dérivation algébrique de l'équation linéarisée BET n'est pas simplement une motivation, mais sert de spécification formelle. Le code est construit pour refléter cette dérivation, garantissant que la transformation exécutable correspond au modèle théorique.
• Flux de travail : Le pipeline exécute les étapes suivantes, chacune couplée à une preuve formelle :
  1. Énumération des fenêtres : Génère systématiquement toutes les sous-listes contiguës de l'isotherme contenant au moins deux points de données.
  2. Linéarisation : Transforme les points de données $(p, n)$ en la forme linéarisée BET $p/[n(1-p)]$.
  3. Régression linéaire : Effectue une régression par moindres carrés sur chaque fenêtre pour extraire la pente, l'ordonnée à l'origine et $R^2$.
  4. Contrôles d'admissibilité : Filtre les candidats selon les critères de Rouquerol (monotonie de $n(1-p)$, positivité des paramètres $C$ et $n_m$, et cohérence de la pression de monocouche).
  5. Sélection du genou : Résout les égalités entre fenêtres valides en sélectionnant celle ayant le plus grand indice de fin, brisant les égalités supplémentaires avec la plus petite erreur en pourcentage.

Contributions clés

1. Vérification formelle du pipeline BETSI : L'article fournit la première implémentation vérifiée par machine de l'intégralité du flux de travail BETSI. Il prouve que le code exécutable satisfait les définitions mathématiques de la théorie BET et des critères de sélection spécifiques.
2. Preuves de correction et de complétude : Les auteurs prouvent formellement :
   • Théorèmes A.1 & A.2 : L'équation de l'isotherme BET est dérivée des hypothèses du modèle de couches, et l'étape de linéarisation est algébriquement correcte.
   • Théorème A.3 : L'énumération des fenêtres est correcte (seules les fenêtres valides sont générées) et complète (aucune fenêtre contiguë valide n'est omise).
   • Théorèmes A.4 & A.5 : L'étape de régression retourne un véritable minimiseur des moindres carrés, et les paramètres physiques extraits ($n_m$, $C$) sont en accord avec leurs définitions théoriques.
   • Théorèmes A.6 & A.7 : Les contrôles d'admissibilité et la stratégie de sélection basée sur le genou satisfont strictement leurs spécifications formelles.
3. Implémentation polymorphe : Le travail démontre un modèle pratique pour l'informatique scientifique dans Lean, où la correction est prouvée sur des nombres réels idéalisés tandis que l'exécution s'effectue sur l'arithmétique à virgule flottante, évitant ainsi le besoin de langages de vérification séparés.

Résultats
L'implémentation LeanBET a été évaluée par rapport à l'implémentation de référence BETSI basée sur Python, en utilisant un ensemble de référence de 19 isothermes d'adsorption.

• Accord numérique : LeanBET est en accord avec la référence BETSI à la précision machine pour 18 des 19 isothermes.
• Discrépance : Pour le jeu de données UiO-66, un écart d'environ 0,03 % (0,36 m²/g) a été observé. Les auteurs notent que la cause de cet écart spécifique reste indéterminée, mais soulignent qu'il est nettement inférieur aux incertitudes expérimentales typiques.
• Statut de vérification : Toutes les preuves ont compilé avec succès, fournissant des garanties vérifiées par machine que la sortie de l'algorithme adhère aux contraintes mathématiques spécifiées.

Signification
L'article affirme que LeanBET démontre qu'un flux de travail pratique d'informatique scientifique peut être construit dans un proveur de théorèmes sans sacrifier l'accord numérique avec les implémentations de référence établies. La contribution principale n'est pas un nouvel algorithme, mais une garantie formellement vérifiée de correction. En reliant le pipeline exécutable à des énoncés mathématiques vérifiés par machine, le travail s'attaque à la crise de la reproductibilité dans l'analyse BET en éliminant l'ambiguïté concernant l'adhésion de l'implémentation à la théorie sous-jacente et aux critères de sélection. Les auteurs positionnent cela comme une étape visant à combler le fossé entre les dérivations théoriques et les implémentations logicielles en science des matériaux.