Startup zajmujący się bezpieczeństwem AI o nazwie Resolution pokazał, jak automatycznie sformalizować matematyczne koncepty z teorii uczenia statystycznego - konkretnie pracę nad rozdzielczością singularności. Zespół połączył agenty AI, które podzieliły się na role: jedne robiły ołówkiem i papierem matematykę, inne pisały kod w systemie Lean, a pozostałe czuwały nad spójnością całego procesu.
Podejście Resolution ilustruje szerszą tendencję w AI badań: zamiast czekać, aż ludzie dowodzą twierdzeń, trenuje się modele do tego, aby same to robiły. Badacze zaczęli od stworzenia dwóch planów - zwykłego dla ludzi i szczegółowego 112-stronicowego podzielonego na atomowe kroki. Następnie agent orkiestrator kierował całym procesem, wymagając minimalnego nadzoru poza początkowym planem i umiejętnościami wyuczonymi z poprzednich projektów.
Za całą operację Resolution zapłacił około 135 tysięcy dolarów. To ma znaczenie dla AI alignment, bo zrozumienie geometrii landscape'u funkcji straty bezpośrednio związane jest z tym, jak modele się generalizują. Jeśli potrafilibyśmy automatycznie dowodzić bardziej skomplikowane twierdzenia dotyczące granic i warunków konwergencji, moglibyśmy lepiej przewidywać zachowanie dużych modeli języka - a to kluczowe dla ich bezpiecznego wdrażania.