Pięć. Dziesięć agentów domyka stuletni problem matematyczny
Piąty fakt jest badawczy, ale nie jest ciekawostką — to pierwszy w tej serii przykład formalnego dowodu wygenerowanego przez wiele współpracujących agentów i sprawdzonego przez niezależne jądro weryfikacyjne. Firma ewaluacyjna Vals AI poinformowała dwudziestego ósmego września, że dziesięć agentów opartych na Claude Sonnet 5.5, pracujących z maksymalnym wysiłkiem przez około piętnaście godzin i wymieniających tysiąc dwieście siedemdziesiąt wiadomości na wspólnej tablicy, wytworzyło dowód w języku Lean dla problemu Thomsona przy siedmiu elektronach. Chodzi o wykazanie, że pentagonalna bipiramida jest jedynym układem minimalizującym energię Coulomba dla siedmiu ładunków na sferze — problem, którego ścisły dowód globalny opierał się przez ponad stulecie. Powstały plik liczy siedemnaście tysięcy osiemset dziewięćdziesiąt pięć linii i korzysta wyłącznie ze standardowych aksjomatów Lean. Dowód został przyjęty przez Lean i dodatkowo sprawdzony przez niezależne jądro nanoda, które zaakceptowało czterdzieści siedem tysięcy osiemset pięćdziesiąt cztery deklaracje. Argument dzieli wszystkie konfiguracje według najmniejszego iloczynu skalarnego pary i zamyka każdą gałąź certyfikatem semidefinite programming sprawdzanym w jądrze. Kod, praca i skrypty weryfikacyjne są w publicznym repozytorium.
Źródło: vals-ai
Trzeba jednak nazwać wprost granice tego wyniku. Vals AI jest komercyjnym dostawcą ewaluacji, więc opis jest zarazem materiałem promocyjnym; dowód jest twardy i sprawdzalny maszynowo, ale jego wartość dla ogólnych zdolności modelu pozostaje ograniczona, bo zadanie było zaprojektowane pod weryfikację formalną. Osobno ten sam ośrodek udostępnił nowy benchmark MysteryMechanism, w którym agent dostaje anonimowe zmienne, dwie obserwacje i ograniczony budżet eksperymentów, po czym musi odtworzyć ukryte prawo matematyczne. Na dwustu dwudziestu dwóch mechanizmach z biologii, fizyki, chemii i ekologii prowadzi GPT-6 Astra z wynikiem pięćdziesiąt trzy przecinek piętnaście procent. Najważniejszy wniosek z tego drugiego testu nie dotyczy jednak kolejności, lecz sufitu obliczeń: podnoszenie wysiłku rozumowania powyżej pewnego progu podnosi koszt zadania nawet dwudziestokrotnie, nie dając przy tym żadnego przyrostu trafności, a jedynym wyjątkiem jest sytuacja, w której dodatkowe obliczenia zmieniają stawianą hipotezę (Vals AI i AlphaSignal, 28–29.09).
Źródło: vals-ai, alphasignal