AlphaProof Nexus od Google DeepMind rozwiązuje dziesięcioletnie problemy matematyczne za kilkaset dolarów

Google DeepMind opracował AlphaProof Nexus, przełomowy system, który autonomicznie rozwiązał dziewięć z 353 otwartych problemów matematycznych Erdősa, w tym dwa zagadnienia nierozwiązane przez 56 lat. Koszt obliczeń wyniósł zaledwie kilkaset dolarów na problem, jak wynika z badania opublikowanego przez zespół DeepMind.

System łączy model językowy Gemini 3.1 Pro z formalnym językiem weryfikacji matematycznej Lean, co pozwala na tworzenie rygorystycznych, sprawdzalnych maszynowo dowodów matematycznych.

Kluczowe wnioski

• AlphaProof Nexus rozwiązał 9 z 353 problemów Erdősa, 44 z 492 hipotez z Encyklopedii Ciągów Liczbowych oraz 15-letnie zagadnienie z geometrii algebraicznej.
• System wykorzystuje cztery typy agentów o rosnącej złożoności, ale najprostszy wariant (Agent A) również poradził sobie ze wszystkimi dziewięcioma problemami Erdősa.
• Koszty obliczeń wyniosły tylko kilkaset dolarów na problem dzięki efektywnemu połączeniu generowania dowodów przez LLM z weryfikacją kompilatora.
• Nawet nieudane próby dowodzenia okazały się wartościowe dla matematyków, pogłębiając zrozumienie badanych problemów.
• System jest już wykorzystywany w bieżących badaniach z optyki kwantowej i teorii grafów.

Architektura systemu: od prostoty do złożoności

AlphaProof Nexus składa się z czterech wariantów agentów o rosnącej złożoności. Najprostszy Agent A wykorzystuje niezależne pod-agenty działające na Gemini 3.1 Pro w pętlach: model językowy generuje kroki dowodu, kompilator Lean je weryfikuje, a komunikaty o błędach wracają do następnej próby.

Agent B dodaje zapytania do AlphaProof — systemu Google opartego na uczeniu ze wzmocnieniem dla matematyki olimpijskiej, który może wypełnić brakujące segmenty dowodu. Agent C wprowadza komponent ewolucyjny inspirowany AlphaEvolve, gdzie pod-agenci dzielą wspólną populację szkiców dowodów. Agenci oceniający zbudowani na Gemini 3.0 Flash punktują te szkice pod kątem prawdopodobieństwa i nowatorstwa, a następnie uszeregowują je systemem Elo.

Najbardziej wyposażony Agent D łączy wszystkie te możliwości i został użyty do problemów Erdősa. Jednak analiza post-hoc ujawniła zaskakujący wynik: najprostszy Agent A również potrafił udowodnić wszystkie dziewięć rozwiązanych problemów Erdősa, choć drożej przy najtrudniejszych zadaniach.

Sukces prostoty i perspektywy rozwoju

Badacze przypisują sukces prostego agenta dwóm czynnikom: szybkiej poprawie podstawowych modeli językowych i „sile sprzężenia zwrotnego kompilatora w ugruntowywaniu rozumowania LLM”. W pełni wyposażony agent wciąż ma przewagę w najtrudniejszych zadaniach, ale ta przewaga może się zmniejszyć wraz z rozwojem LLM.

Sukcesy systemu skupiają się w obszarach takich jak kombinatoryka, optymalizacja wypukła i teoria liczb, gdzie biblioteka matematyczna Lean Mathlib jest dojrzała, a problemy rozkładają się na możliwe do opanowania pod-cele. Większość problemów Erdősa pozostała poza zasięgiem, „nie mówiąc już o problemach wymagających rozległej nowej teorii”.

Mimo to badacze widzą wartość poza rozwiązanymi problemami. Matematycy współpracujący z systemem raportowali, że nawet nieudane próby dowodzenia pogłębiły ich zrozumienie problemu. Ponieważ szkice były formalne, eksperci mogli skupić się na nierozwiązanych pod-celach zamiast ponownie sprawdzać cały argument od początku.

System jest już wykorzystywany w bieżących badaniach z optyki kwantowej i teorii grafów. Wszystkie dowody w języku Lean oraz wybrane dowody w języku naturalnym są dostępne na GitHub. AlphaProof Nexus pokazuje, że połączenie zaawansowanych modeli językowych z formalną weryfikacją może otworzyć nowe możliwości w matematycznych badaniach, nawet przy relatywnie niskich kosztach obliczeniowych.