LeanBET: Formally-verified surface area calculations in Lean

Dit artikel presenteert LeanBET, een volledig uitvoerbare en formeel geverifieerde Brunauer-Emmett-Teller (BET)-oppervlakteanalysepiplijn geïmplementeerd in Lean 4 die wiskundige correctheid garandeert terwijl het een bijna perfecte numerieke overeenkomst bereikt met de gevestigde BETSI-referentie-implementatie.

De kern

Stel je voor dat je probeert het oppervlak van een spons te meten, maar de spons bestaat uit onzichtbare, microscopische gaatjes. Wetenschappers gebruiken een methode genaamd BET (vernoemd naar drie wetenschappers) om dit oppervlak te schatten door te observeren hoe gas aan de spons plakt. Het is een standaardtool in de chemie, maar het is een beetje als proberen een puzzel op te lossen waarbij de afbeelding op de doos wazig is.

Hier is het probleem: Om het antwoord te krijgen, moeten wetenschappers een specifiek bereik van datapunten uit hun experiment kiezen en er een rechte lijn doorheen trekken. Het probleem is dat verschillende mensen (of verschillende computerprogramma's) mogelijk iets verschillende bereiken kiezen. Iemand zou kunnen zeggen: "Laten we de middelste 10 punten gebruiken," terwijl een ander zegt: "Nee, gebruik de middelste 12." Dit leidt tot verschillende antwoorden voor dezelfde spons, wat verwarring en een gebrek aan vertrouwen in de resultaten veroorzaakt.

Om dit op te lossen, heeft een team een computerprogramma gemaakt genaamd BETSI dat automatisch elk mogelijk bereik van data controleert om het "beste" te vinden. Het is alsof je een robot hebt die elke mogelijke combinatie van puzzelstukjes probeert om die ene te vinden die perfect past. Zelfs robots kunnen echter bugs hebben, of verborgen aannames die hen op subtiele manieren foutief maken.

Presentatie van "LeanBET": De wiskundig bewezen robot

De auteurs van dit artikel hebben een nieuwe versie van deze robot gebouwd met een speciaal computergereedschap genaamd Lean 4. Denk aan Lean 4 niet alleen als een programmeertaal, maar als een superstreng wiskundeleraar die je nooit een fout laat maken zonder bewijs.

Hier is hoe ze het deden, met enkele eenvoudige analogieën:

1. Het "Twee-Hersenen" Systeem (Polymorfisme)

Normaal gesproken gebruik je bij het schrijven van een computerprogramma "drijvende-kommagetallen" (zoals de getallen op een rekenmachine). Deze zijn snel maar iets rommelig omdat computers geen oneindige precisie kunnen vasthouden. Wanneer je wiskundige bewijzen doet, gebruik je "reële getallen" (perfecte, oneindige precisie), maar die kun je niet op een computer uitvoeren.

De auteurs losten dit op door een vormveranderende robot te bouwen.

• Hersenen A (Het Bewijs): Wanneer ze moeten bewijzen dat de wiskunde klopt, draagt de robot een "Reële Getallen"-pak. Het doet perfecte, theoretische wiskunde om te bewijzen dat de logica foutloos is.
• Hersenen B (De Uitvoering): Wanneer ze het programma op echte data moeten draaien, wisselt de robot naar een "Drijvende-Komma"-pak. Het draait snel op echte computers.
• De Magie: Omdat de robot in beide pakken op dezelfde manier is gebouwd, is gegarandeerd dat als het "Bewijs-Hersenen" zegt dat de logica perfect is, het "Uitvoerings-Hersenen" dezelfde regels zal volgen. Het is alsof je het ontwerp van een brug met perfecte wiskunde veilig bewijst, en vervolgens de daadwerkelijke brug bouwt met echt staal, wetende dat het ontwerp standhoudt.

2. Het "Recept versus het Koken" (Afleiding als Specificatie)

In de normale wetenschap schrijf je een recept (de wiskundetheorie) op papier, en probeert een chef-kok (de programmeur) het daarna in de keuken (de software) te bereiden. Soms voegt de chef hier en daar een snufje zout toe, of begrijpt een stap verkeerd, en smaakt het gerecht anders dan het recept.

In LeanBET gebeuren het recept en het koken in dezelfde kamer. De "wiskundige afleiding" (het recept) wordt direct in de code geschreven. De computer controleert dat de code het recept is. Als de code zegt "voeg zout toe", verifieert het wiskundebewijs dat "zout toevoegen" precies is wat de theorie vereist. Er is geen kloof tussen theorie en praktijk.

3. De "Strenge Inspecteur" (Formele Verificatie)

Het artikel beweert dat hun programma niet alleen het antwoord raadt; het draagt een certificaat van correctheid bij zich.

• Standaard Software: Je voert het programma uit, het geeft je een getal, en je hoopt dat het klopt.
• LeanBET: Je voert het programma uit, het geeft je een getal, en het geeft je ook een wiskundig bewezen document dat zegt: "Ik heb elke stap gecontroleerd, ik heb elke regel gevolgd, en dit getal is het enige correcte antwoord op basis van de data die je me hebt gegeven."

Wat Vonden Ze?

Ze testten hun nieuwe "Wiskundig Bewezen Robot" tegen de oude "Standaard Robot" (BETSI) met 19 verschillende datasets (zoals 19 verschillende sponzen).

• Het Resultaat: Voor 18 van de 19 sponzen gaven de twee robots exact hetzelfde antwoord tot op het kleinste decimaal.
• De Eén Glitch: Voor één spons (genaamd UiO-66) was er een klein verschil (0,03%). De auteurs geven toe dat ze nog niet zeker weten waarom, maar het is een zeer kleine fout in vergelijking met de gebruikelijke ruis in experimenten.

De Conclusie

Dit artikel gaat niet over het uitvinden van een nieuwe manier om sponzen te meten. Het gaat over het bouwen van een betrouwbare versie van de bestaande manier. Ze namen een standaard wetenschappelijke tool, herbouwden deze in een "wiskundig bewezen" omgeving, en toonden aan dat het net zo goed werkt als de oude tools, maar dan met de garantie dat er geen logische fouten zijn gemaakt.

Het is alsof je upgradet van een gewone kaart naar een GPS die je niet alleen de route vertelt, maar ook stap-voor-stap bewijst dat de route de kortste en veiligste mogelijke is, zonder verborgen omwegen.

Technische samenvatting

Technische Samenvatting van "LeanBET: Formeel geverifieerde berekeningen van het oppervlak in Lean"

Probleemstelling
De Brunauer–Emmett–Teller (BET)-methode is het standaardkader voor het schatten van het specifieke oppervlak uit gasadsorptie-isothermen. De praktische implementatie houdt echter aanzienlijke subjectiviteit in, met name bij het selecteren van het relatieve drukbereik voor lineaire regressie. Hoewel consistentiecriteria (Rouquerol-criteria) bestaan om geldige gebieden te filteren, voldoen vaak meerdere drukintervallen aan deze regels, wat leidt tot variabiliteit in gerapporteerde oppervlakten tussen verschillende laboratoria en software-implementaties. Eerdere pogingen om dit proces te standaardiseren, zoals het BET Surface Identification (BETSI)-algoritme, vertrouwen op algemene numerieke software (Python). Hoewel BETSI de subjectiviteit vermindert door exhaustieve enumeratie, blijft het een numeriek algoritme waarbij verborgen implementatieaannames of subtiele fouten niet formeel kunnen worden uitgesloten, waardoor de wetenschappelijke garanties van de output ongeverifieerd blijven.

Methodologie
De auteurs presenteren LeanBET, een volledig uitvoerbare en formeel geverifieerde BET-analysepiplijn geïmplementeerd in de Lean 4-theoremaprover. De aanpak integreert uitvoerbare code met wiskundige bewijzen binnen één omgeving, waarbij gebruik wordt gemaakt van een polymorf numeriek ontwerp om de kloof tussen berekening en verificatie te overbruggen:

• Polymorfisme: Het algoritme is geschreven met een generiek type α dat wordt beperkt door een BETLike-typeclass. Dit stelt dezelfde codestructuur in staat om te worden geïnstantieerd over drijvende-kommagetallen (Float) voor efficiënte uitvoering op echte experimentele data en over reële getallen (Real) voor niet-berekenbare wiskundige bewijzen.
• Afleiding als specificatie: De algebraïsche afleiding van de gelijnde BET-vergelijking is niet slechts een motivatie, maar dient als de formele specificatie. De code is zo opgebouwd dat deze deze afleiding weerspiegelt, waardoor wordt gegarandeerd dat de uitvoerbare transformatie overeenkomt met het theoretische model.
• Werkstroom: De pijplijn voert de volgende stappen uit, elk gekoppeld aan een formeel bewijs:
  1. Venstereenumeratie: Genereert systematisch alle aaneengesloten sublijsten van de isotherm die ten minste twee datapunten bevatten.
  2. Linearisatie: Transformeert datapunten $(p, n)$ naar de gelijnde BET-vorm $p/[n(1-p)]$.
  3. Lineaire regressie: Voert een kleinste-kwadratenregressie uit op elk venster om helling, intercept en $R^2$ te extraheren.
  4. Toelaatbaarheidscontroles: Filtert kandidaten op basis van Rouquerol-criteria (monotonie van $n(1-p)$, positiviteit van parameters $C$ en $n_m$, en consistentie van het monolaagdruk).
  5. Knie-selectie: Lost gelijke standen op tussen geldige vensters door het venster met de grootste eindindex te selecteren, en breekt verdere gelijke standen met de kleinste procentuele fout.

Belangrijkste bijdragen

1. Formele verificatie van de BETSI-pijplijn: Het artikel biedt de eerste machinegecontroleerde implementatie van de volledige BETSI-werkstroom. Het bewijst dat de uitvoerbare code voldoet aan de wiskundige definities van de BET-theorie en de specifieke selectiecriteria.
2. Bewijzen van soundness en volledigheid: De auteurs bewijzen formeel:
   • Stelling A.1 & A.2: De BET-isothermvergelijking is afgeleid uit aannames van het lagenmodel, en de linearisatiestap is algebraïsch correct.
   • Stelling A.3: De venstereenumeratie is sound (alleen geldige vensters worden gegenereerd) en volledig (geen enkel geldig aaneengesloten venster wordt gemist).
   • Stelling A.4 & A.5: De regressiestap retourneert een ware kleinste-kwadraten-minimalisator, en de geëxtraheerde fysische parameters ($n_m$, $C$) komen overeen met hun theoretische definities.
   • Stelling A.6 & A.7: De toelaatbaarheidscontroles en de op de knie gebaseerde selectiestrategie voldoen strikt aan hun formele specificaties.
3. Polymorfe implementatie: Het werk demonstreert een praktisch patroon voor wetenschappelijk rekenen in Lean, waarbij correctheid wordt bewezen over geïdealiseerde reële getallen terwijl uitvoering plaatsvindt over drijvende-kommarekenkunde, waardoor de noodzaak van aparte verificatietalen wordt vermeden.

Resultaten
De LeanBET-implementatie werd geëvalueerd tegen de referentie-implementatie van BETSI op basis van Python, met behulp van een benchmarkset van 19 adsorptie-isothermen.

• Numerieke overeenstemming: LeanBET komt overeen met de BETSI-referentie tot machineprecisie voor 18 van de 19 isothermen.
• Afwijking: Voor de UiO-66-dataset werd een afwijking van ongeveer 0,03% (0,36 m²/g) waargenomen. De auteurs merken op dat de oorzaak van deze specifieke afwijking onbepaald blijft, maar benadrukken dat deze aanzienlijk kleiner is dan typische experimentele onzekerheden.
• Verificatiestatus: Alle bewijzen compileerden succesvol, waardoor machinegecontroleerde garanties worden geboden dat de output van het algoritme voldoet aan de gespecificeerde wiskundige beperkingen.

Betekenis
Het artikel stelt dat LeanBET aantoont dat een praktische werkstroom voor wetenschappelijk rekenen kan worden gebouwd in een theoremaprover zonder in te leveren op numerieke overeenstemming met gevestigde referentie-implementaties. De primaire bijdrage is geen nieuw algoritme, maar een formeel geverifieerde garantie van correctheid. Door de uitvoerbare pijplijn te koppelen aan machinegecontroleerde wiskundige uitspraken, adresseert het werk de reproduceerbaarheidcrisis in BET-analyse door ambiguïteit te elimineren met betrekking tot de naleving van de implementatie aan de onderliggende theorie en selectiecriteria. De auteurs positioneren dit als een stap naar het overbruggen van de kloof tussen theoretische afleidingen en software-implementaties in de materiaalkunde.