Wywiady opublikowane 19 października przez The Daily Californian pokazały różne oceny wpływu AI na matematykę, jakie przedstawili Richard Borcherds i Robin Huang z UC Berkeley. Wcześniejsza analiza A. Bastounis, F. Circelli i A. C. Hansen, opublikowana 6 października, wskazała rozbieżności między fragmentami tekstowego dowodu OpenAI a jego formalizacją w Lean. Autorzy nie twierdzą, że dowód zapisany słownie jest błędny.
Wcześniej NeoTeo opisywało publikację wyników matematycznych wygenerowanych przez wewnętrzny model OpenAI. Obecna sprawa dotyczy tego, jak zapisano jeden z przedstawionych przez firmę dowodów.
Matematycy z Berkeley różnią się w ocenie AI
Borcherds, profesor matematyki i laureat Medalu Fieldsa z 1998 roku, przewidywał, że jeśli obecne tempo rozwoju się utrzyma, w ciągu kilku lat ludzie mogą stać się zbędni w badaniach matematycznych. Robin Huang, doktorantka matematyki na ostatnim roku studiów, była mniej przekonana o obecnej użyteczności AI. Jak relacjonował The Daily Californian, korzystała z tych narzędzi we własnych badaniach, ale oceniała je jako mało sprawne i nieefektywne. To odmienne opinie rozmówców, nie wspólne stanowisko matematyków.
Co OpenAI twierdzi o swoim wyniku
8 września OpenAI ogłosiło, że jego system wykazał możliwość powstania osobliwości w skończonym czasie w trójwymiarowym, nieściśliwym płynie poddanym działaniu gładkiej siły zewnętrznej. Według firmy płyn zaczyna w spoczynku, a jego energia pozostaje skończona. OpenAI stwierdziło, że wynik odpowiada punktom C i D w sformułowaniu problemu Instytutu Matematycznego Claya. Firma opublikowała opis wyniku i jego formalizację w Lean.
Konkretna rozbieżność w formalizacji Lean
Lean to język formalny i asystent dowodzenia, w którym twierdzenie i jego dowód można zapisać w postaci sprawdzanej przez komputer. W przykładzie z lematu 8.6 autorzy analizy porównali oszacowania dotyczące tych samych pochodnych wyniku. Tekstowy dowód OpenAI wymaga czterech dodatkowych pochodnych funkcji wejściowej, natomiast przywołane oszacowanie w Lean wymaga pięciu.
| Wersja oszacowania | Dodatkowe pochodne funkcji wejściowej |
| Dowód zapisany słownie, lemat 8.6 | 4 |
| Oszacowanie przywołane w Lean | 5 |
Autorzy wskazali również różnice w oszacowaniu strumienia ciśnienia. Wersja tekstowa zależy od wielkości B_R, a wyrażenie w Lean uwzględnia także A_R, przez co obu oszacowań trudno bezpośrednio porównać. Szczegóły obu przykładów opisali w swojej analizie formalizacji.
Kompilacja w Lean sprawdza, czy formalny zapis dowodzi zakodowanego twierdzenia. Sama nie potwierdza, że zakodowane twierdzenie i argument odpowiadają treści tekstu matematycznego. Analiza wskazuje więc konkretny problem z wiernością formalizacji; jej autorzy nie stwierdzają, że tekstowy dowód OpenAI jest niepoprawny.
