LongTails: agent AI udowodnił ponad 30 nowych twierdzeń optymalizacji

Weryfikacja w Lean 4

Najważniejszą cechą systemu jest automatyczne sprawdzanie każdego dowodu w języku formalnej weryfikacji Lean 4. To zabezpieczenie przed znanym problemem: model może wygenerować rozumowanie, które brzmi przekonująco, ale zawiera błąd albo dotyczy innego zadania. LongTails startuje od formalnego opisu warunków i celu, a potem sprawdza, czy dowód z nimi się zgadza.

Badacze uzyskali około 100 twierdzeń zapisanych formalnie, w tym 50 poprawiających gwarancje znane z wcześniejszych prac. Zespół planuje opublikować kolejne 35 twierdzeń jako samodzielne wyniki matematyczne. Udowodnienie jednego twierdzenia zajmuje programowi średnio od 3 do 7 godzin.

Znaczenie praktyczne

Optymalizacja polega na wyszukiwaniu najlepszej opcji spośród wielu możliwych, na przykład najszybszej, najtańszej czy najdokładniejszej. Takie twierdzenia pokazują, jak szybko działa dana metoda i w jakich warunkach, co pozwala z góry oszacować liczbę potrzebnych obliczeń. Na optymalizacji opiera się trening sieci neuronowych, od systemów rekomendacji po duże modele językowe, więc wydajniejsze algorytmy mogą skrócić czas treningu, obniżyć koszty i zużycie energii w centrach danych. Metody te stosuje się też w logistyce, projektowaniu lekkich i wytrzymałych konstrukcji, sieciach energetycznych, poszukiwaniu nowych materiałów i zarządzaniu ryzykiem inwestycyjnym.

Kod LongTails jest otwarty, więc inne zespoły mogą z niego korzystać. Jeden z uczestników projektu przyznał, że w kilka dni framework osiągnął więcej, niż on sam w całej karierze, i trudno mu określić własne uczucia, choć uważa to za bardzo ekscytujące. Zespół zamierza dowodzić kolejnych twierdzeń, zwiększać złożoność problemów i sprawdzać algorytmy w praktycznych zastosowaniach.