ByteDance prezentuje Seed-Prover: Przełom w automatycznym dowodzeniu twierdzeń matematycznych

W miarę jak modele językowe (LLM) zyskują na zdolności do rozumowania matematycznego, ich aplikacje wciąż napotykają istotne bariery. Dotychczasowe próby wykorzystania uczenia ze wzmocnieniem (RL) do trenowania tych modeli były hamowane przez trudność w weryfikacji poprawności dowodów generowanych w języku naturalnym. Wymagało to żmudnego, ręcznego sprawdzania każdego kroku logicznego, co ograniczało skalę i efektywność uczenia.

Alternatywą są języki formalne, takie jak Lean, które oferują automatyczną weryfikację poprawności. Jednak nawet w tym obszarze, obecne provery oparte na LLM mają swoje ograniczenia. Provery krok po kroku generują kod przyrostowo, ale wymagają specyficznego wsparcia i często brakuje im zdolności do rozumowania na wyższym poziomie abstrakcji.

Nowe podejście ByteDance

Odpowiedzią na te wyzwania jest Seed-Prover, opracowany przez ByteDance Seed Team. To model rozumowania, który koncentruje się na dowodzeniu w stylu lematycznym, czyli na budowaniu kompletnych dowodów w oparciu o wcześniej ustalone lematy. Zamiast tradycyjnych, sekwencyjnych generacji krok po kroku, Seed-Prover iteracyjnie udoskonala dowody, wykorzystując informacje zwrotne z Lean, istniejące lematy oraz mechanizm autosumaryzacji. To innowacyjne podejście stawia lematy w centrum procesu rozumowania.

Seed-Prover wykorzystuje trzy specjalistyczne strategie wnioskowania w czasie testowym, które umożliwiają głębokie i szerokie metody rozumowania. Pozwoliło to systemowi na rozwiązywanie problemów na poziomie Międzynarodowej Olimpiady Matematycznej (IMO).

Ważnym uzupełnieniem jest Seed-Geometry, silnik do rozumowania geometrycznego, stworzony z myślą o przezwyciężaniu ograniczeń Lean w obsłudze geometrii. Integracja Seed-Prover z Lean odbywa się za pomocą wieloetapowego i wielozadaniowego uczenia ze wzmocnieniem, bazującego na VAPO.

Trening i wydajność

Zestaw danych treningowych Seed-Prover łączy otwarte źródła z wewnętrznymi problemami formalnymi. Inteligentny system generujący problemy tworzy uproszczone warianty trudnych zadań, wykluczając jednocześnie te, które są zbyt proste (z wskaźnikiem dowodzenia powyżej 25%). Backend Seed-Geometry jest zdolny do generowania problemów na dużą skalę, identyfikując ponad 230 milionów unikalnych zadań w ciągu siedmiu dni, co świadczy o ośmiokrotnej poprawie efektywności wyszukiwania.

Wyniki Seed-Prover są imponujące. W symulacji IMO 2025 system w pełni rozwiązał 5 z 6 problemów. Seed-Geometry natychmiastowo rozwiązał Problem 2, a Seed-Prover znalazł dowody dla pozostałych problemów, używając różnych ustawień wnioskowania. Na podstawie historycznych zadań IMO, system udowodnił 121 z 155 zadań, osiągając 78,1% sukcesu we wszystkich poziomach trudności. W tym 47 z 55 łatwych, 47 z 56 średnich i 27 z 44 trudnych zadań. Szczegółowe wyniki obejmują 72 z 85 w algebrze, 42 z 55 w teorii liczb i 7 z 14 w kombinatoryce.

Na benchamrku MiniF2F, Seed-Prover osiągnął 99,6% wskaźnika dowodzenia dla zestawów walidacyjnych i testowych w średnich ustawieniach, rozwiązując trudne problemy takie jak IMO 1990 P3. Wyniki PutnamBench pokazują znaczną poprawę, z 201 rozwiązań do 331 z 657, co jest znaczącym skokiem wydajności w porównaniu do poprzednich systemów rozumowania matematycznego na poziomie licencjackim.

Mimo sukcesów, Seed-Prover nadal napotyka na wyzwania, szczególnie w rozumowaniu kombinatorycznym. Na CombiBench system rozwiązał 30 ze 100 problemów, co choć przewyższa istniejące metody, wskazuje na obszary wymagające dalszych badań. Na MiniCTX-v2 osiągnięto 81,8% sukcesu, pokazując silną generalizację poza problemy konkursowe, przewyższając bazową linię 44,3% dla o4-mini.

Perspektywy i wnioski

Wprowadzenie Seed-Geometry i Seed-Prover przez ByteDance Seed Team stanowi kamień milowy w dziedzinie formalnego rozumowania, scalając możliwości dużych modeli językowych z rygorem języków formalnych. Seed-Geometry zapewnia przyspieszoną weryfikację i ulepszone mechanizmy wyszukiwania, podczas gdy Seed-Prover stosuje iteracyjne udoskonalanie i złożone strategie wnioskowania w czasie testowym. Zdolność do rozwiązania 5 z 6 problemów finału IMO 2025 świadczy o praktycznej skuteczności tych metod w elitarnych konkursach matematycznych. Przyjęcie języków formalnych, takich jak Lean, umożliwia szybką weryfikację dowodów, która jest bardziej ekonomiczna niż praca ludzkich ekspertów i bardziej niezawodna niż ocena przez modele LLM.

Przyszłe badania będą koncentrować się na dalszym łączeniu systemów formalnych z LLM, aby sprostać otwartym problemom i hipotezom matematycznym.