Voor het eerst heeft een AI-aangedreven systeem dat is ontworpen om wiskundige bewijzen te verifiëren een fundamentele fout geïdentificeerd in een peer-reviewed natuurkundig artikel. De ontdekking, gedaan door Joseph Tooby-Smith van de Universiteit van Bath, benadrukt een groeiende zorg: hoeveel soortgelijke fouten kunnen er bestaan in de bestaande wetenschappelijke literatuur? Dit evenement onderstreept het potentieel van geautomatiseerde verificatietools om academisch publiceren opnieuw vorm te geven en de betrouwbaarheid van wetenschappelijke bevindingen te verbeteren.
De opkomst van formele verificatie
Formele verificatie – het proces van het rigoureus controleren van wiskundige en logische consistentie – wordt steeds gebruikelijker in de wiskunde. Gespecialiseerde software, zoals de Lean-taal die in dit geval wordt gebruikt, kan tegenstrijdigheden en gaten in bewijzen opsporen die menselijke beoordeling misschien over het hoofd zou zien. Deze aanpak gaat niet alleen over het opsporen van fouten; het wordt gezien als een manier om notoir moeilijke problemen aan te pakken, zoals het onopgeloste ABC-vermoeden, waarbij zelfs experts het oneens zijn over de geldigheid van voorgestelde oplossingen.
Natuurkunde onder de microscoop
Tooby-Smith paste formele verificatie toe op een artikel uit 2006 over de stabiliteit van het potentieel van de twee Higgs-doubletmodellen (2HDM), een veel geciteerd werk in de deeltjesfysica. Het doel was om het artikel te integreren in PhysLib, een project gericht op het creëren van een geformaliseerde database van natuurkundig onderzoek, gemodelleerd naar de succesvolle MathsLib voor wiskunde. De AI onthulde dat een belangrijke voorwaarde uit het originele artikel geen stabiele oplossing garandeerde, zoals beweerd door de auteurs.
De ontdekking was geen opzettelijke poging om het werk in diskrediet te brengen. Zoals Tooby-Smith uitlegt, streefde het team naar een ‘aanvinkvakjesoefening’ om een betrouwbare bibliotheek van geformaliseerde natuurkunde op te bouwen. De fout die aan het licht is gekomen, roept echter een cruciale vraag op: als een goed geciteerd artikel zo’n fout zou kunnen bevatten, hoeveel andere zouden dan soortgelijke gebreken kunnen vertonen?
Waarom dit belangrijk is
De natuurkunde is afhankelijk van wiskundige nauwkeurigheid, maar natuurkundigen geven vaak prioriteit aan resultaten boven uitputtende details. In tegenstelling tot wiskundigen, die doorgaans expliciete bewijsstappen leveren, kunnen natuurkundigen ogenschijnlijk kleine details weglaten die, zoals dit geval aantoont, de geldigheid van een stelling kunnen ondermijnen. Dit verschil in de praktijk betekent dat natuurkundeartikelen mogelijk kwetsbaarder zijn voor niet-onderzochte fouten.
De toekomst van wetenschappelijke validatie
De implicaties van deze ontdekking zijn aanzienlijk. Hoewel het onwaarschijnlijk is dat de fout downstream-werk waarin het artikel is geciteerd ongeldig maakt (er is al een erratum aan de gang), versterkt het het argument voor het integreren van formele verificatie in het standaard publicatieproces.
Kevin Buzzard van Imperial College London merkt op dat formalisering de wiskunde al heeft getransformeerd, en er is geen reden waarom de theoretische natuurkunde niet van dezelfde aanpak zou kunnen profiteren. De uitdaging ligt echter in het opbouwen van een corpus van geformaliseerde natuurkundige gegevens dat groot genoeg is om AI-modellen effectief te kunnen trainen. “In het ideale geval hebben we een miljoen regels natuurkunde nodig… als de machines in eerste instantie niet zo goed zijn in natuurkunde, dan zal er in het begin handmatig werk zijn”, zegt Buzzard.
Geautomatiseerde verificatie staat op het punt een essentieel instrument te worden voor het garanderen van wetenschappelijke nauwkeurigheid. Hoewel de initiële inspanning arbeidsintensief kan zijn, vallen de langetermijnvoordelen van een betrouwbaarder wetenschappelijk verslag niet te ontkennen.
