Po raz pierwszy system sztucznej inteligencji zaprojektowany do sprawdzania dowodów matematycznych zidentyfikował zasadniczy błąd w recenzowanej pracy naukowej z fizyki. To odkrycie dokonane przez Josepha Toby-Smitha z Uniwersytetu w Bath uwydatnia rosnące obawy: ile podobnych błędów może istnieć w istniejącej literaturze naukowej? To wydarzenie pokazuje potencjał narzędzi do automatycznej recenzji w zakresie transformacji publikacji akademickich i poprawy wiarygodności wyników badań naukowych.
Powstanie formalnej weryfikacji
Weryfikacja formalna, czyli proces rygorystycznego testowania spójności matematycznej i logicznej, staje się coraz bardziej powszechna w matematyce. Specjalistyczne oprogramowanie, takie jak język Lean zastosowany w tym przypadku, może zidentyfikować niespójności i luki w dowodach, które mogą przeoczyć weryfikatorzy. Podejście to ma na celu nie tylko identyfikację błędów, ale jest również postrzegane jako sposób na rozwiązanie szczególnie trudnych problemów, takich jak nierozwiązana hipoteza ABC, w której nawet eksperci nie są zgodni co do słuszności proponowanych rozwiązań.
Fizyka pod mikroskopem
Tooby-Smith zastosował formalną weryfikację w artykule z 2006 roku na temat potencjalnej stabilności modelu dwóch dubletów Higgsa (2HDM), szeroko cytowanej pracy z fizyki cząstek elementarnych. Celem było zintegrowanie artykułu z PhysLib – projektem mającym na celu stworzenie sformalizowanej bazy danych zawierającej badania fizyczne, podobnej do odnoszącej sukcesy biblioteki MathsLib dla matematyki. Sztuczna inteligencja pokazała, że kluczowy warunek przedstawiony w oryginalnej pracy nie gwarantował stabilnego rozwiązania, jak twierdzili autorzy.
Odkrycie nie było celową próbą zdyskredytowania dzieła. Jak wyjaśnia Tooby-Smith, celem zespołu było „formalne ćwiczenie” polegające na stworzeniu solidnej biblioteki sformalizowanej fizyki. Jednakże wykryty błąd rodzi ważne pytanie: jeśli dobrze cytowany artykuł może zawierać taki błąd, ile innych może być równie błędnych?
Dlaczego to jest ważne?
Fizyka opiera się na rygorze matematycznym, ale fizycy często przedkładają wyniki nad wyczerpujące szczegóły. W przeciwieństwie do matematyków, którzy zazwyczaj podają wyraźne etapy dowodu, fizycy mogą pominąć pozornie drobne szczegóły, które, jak pokazuje ten przypadek, mogą podważyć ważność twierdzenia. Ta różnica w praktyce oznacza, że artykuły fizyczne są potencjalnie bardziej podatne na niezbadane błędy.
Przyszłość weryfikacji naukowej
Konsekwencje tego odkrycia są znaczące. Choć jest mało prawdopodobne, aby błąd ten dyskredytował późniejszą pracę cytującą artykuł (obecnie przygotowywana jest korekta), wzmacnia on argument za włączeniem weryfikacji formalnej do standardowego procesu publikacji.
Kevin Buzzard z Imperial College w Londynie zwraca uwagę, że formalizacja już zmieniła matematykę i nie ma powodu, dla którego fizyka teoretyczna nie mogłaby odnieść korzyści z tego samego podejścia. Problem polega jednak na stworzeniu wystarczająco dużego korpusu sformalizowanych danych fizycznych, aby skutecznie szkolić modele sztucznej inteligencji. „W idealnej sytuacji potrzebowalibyśmy miliona linii kodu fizycznego… jeśli maszyny nie rozumieją fizyki wystarczająco dobrze, najpierw będzie to wymagało pracy ręcznej” – mówi Buzzard.
Automatyczna weryfikacja może stać się ważnym narzędziem zapewniającym dokładność naukową. Choć początkowe wysiłki mogą być czasochłonne, długoterminowe korzyści wynikające z bardziej wiarygodnych zapisów naukowych są niezaprzeczalne.
