DeepSeek wprowadza DeepSeek-Prover-V2, przełomowy model językowy o dużej skali (LLM) o otwartym kodzie źródłowym, starannie stworzony dla złożonej domeny formalnego dowodzenia twierdzeń w ramach Lean 4. Ten nowatorski model wykorzystuje rekurencyjny potok dowodzenia twierdzeń, wykorzystując moc najnowocześniejszego modelu bazowego DeepSeek-V3 firmy DeepSeek. Lean 4, najnowsza iteracja programu do dowodzenia twierdzeń Lean, jest interaktywnym asystentem dowodów opracowanym przez Microsoft Research. Ten zaawansowany język programowania funkcyjnego i interaktywny system dowodzenia twierdzeń umożliwia matematykom i informatykom konstruowanie formalnych dowodów z niezrównaną weryfikacją maszynową.
Projekt oznacza monumentalny krok w kierunku wypełnienia luki między formalnym i nieformalnym rozumowaniem matematycznym. Wykorzystując inherentne możliwości ogólnego przeznaczenia LLM, ma na celu skuteczne zajęcie się wysoce ustrukturyzowaną domeną formalnego dowodzenia twierdzeń. Zespół badawczy DeepSeek utrzymuje, że ich innowacyjne podejście odzwierciedla procesy poznawcze stosowane przez ludzkich matematyków podczas konstruowania dowodów, skrupulatnie dzieląc złożone twierdzenia na bardziej zarządzalne i zrozumiałe komponenty.
Rozszerzenie ramy oceny: wprowadzenie ProverBench
W znaczącym ruchu, aby zwiększyć rygor swoich badań, zespół DeepSeek znacznie rozszerzył swoją ramę oceny dzięki wprowadzeniu ProverBench, zupełnie nowej kolekcji benchmarków starannie zaprojektowanej specjalnie do kompleksowej oceny możliwości formalnego dowodzenia twierdzeń. Ta kompleksowa kolekcja służy jako cenne źródło do oceny wydajności LLM w kontekście matematyki formalnej.
"Oprócz konwencjonalnych benchmarków z dumą przedstawiamy ProverBench, starannie wyselekcjonowaną kolekcję 325 sformalizowanych problemów, aby wzbogacić nasz proces oceny. Ta kolekcja zawiera 15 starannie wybranych problemów pochodzących bezpośrednio z ostatnich konkursów American Invitational Mathematics Examination (AIME), szczególnie z lat 24-25" – wyjaśnili badacze.
Włączenie problemów AIME do zestawu danych ProverBench jest szczególnie godne uwagi, ponieważ wprowadza zestaw trudnych i dobrze ugruntowanych problemów matematycznych, które są powszechnie uznawane w społeczności matematycznej. Zapewnia to standardową i rygorystyczną podstawę do oceny wydajności DeepSeek-Prover-V2 i porównywania go z innymi podejściami.
Obiecujące wstępne wyniki: rozwiązywanie problemów AIME
Wstępne wyniki uzyskane z rygorystycznych testów na tych trudnych problemach AIME ujawniły wyjątkowo obiecującą wydajność starannie zaprojektowanego specjalistycznego modelu dowodzenia twierdzeń. Zespół DeepSeek z dumą informuje, że DeepSeek-Prover-V2 zademonstrował swoją sprawność, skutecznie rozwiązując imponujące 6 z 15 problemów AIME, które mu przedstawiono. Dla porównania, ogólnego przeznaczenia model DeepSeek-V3, stosując techniki głosowania większościowego, zdołał skutecznie rozwiązać 8 problemów.
Te odkrycia podkreślają potencjał zarówno specjalistycznych, jak i ogólnego przeznaczenia LLM w rozwiązywaniu złożonych problemów matematycznych. Podczas gdy model ogólnego przeznaczenia wykazywał nieco wyższy wskaźnik sukcesu w tym konkretnym benchmarku, specjalistyczny model dowodzenia twierdzeń zademonstrował swoją biegłość w formalnym rozumowaniu matematycznym.
Naśladowanie ludzkiej konstrukcji dowodu: podejście łańcucha myśli
"Biorąc pod uwagę dobrze udokumentowane wyzwania, z którymi często spotykają się modele ogólnego przeznaczenia, próbując stworzyć kompletne dowody Lean, strategicznie poinstruowaliśmy DeepSeek-V3, aby generował tylko szkic dowodu wysokiego poziomu, celowo pomijając zawiłe szczegóły. Wynikowy łańcuch myśli wieńczy twierdzenie Lean składające się z sekwencji stwierdzeń, z których każde jest skrupulatnie zakończone zastępczym miejscem sorrry, skutecznie wskazując podcel, który należy rozwiązać. To innowacyjne podejście elegancko odzwierciedla ludzki styl tworzenia dowodów, w którym złożone twierdzenie jest inkrementalnie redukowane do sekwencji bardziej zarządzalnych lematów" – wyjaśnił zespół DeepSeek.
To innowacyjne podejście do generowania szkiców dowodów wysokiego poziomu jest zgodne z tym, jak matematycy często podchodzą do złożonych dowodów. Koncentrując się na ogólnej strukturze i kluczowych krokach, model może skutecznie kierować późniejszym udoskonalaniem i ukończeniem dowodu.
Metodyczna strategia: indywidualne adresowanie każdego komponentu dowodu
System następnie skrupulatnie stosuje metodyczną i ustrukturyzowaną strategię, aby odnieść się do każdego indywidualnego komponentu dowodu. To systematyczne podejście zapewnia, że każdy aspekt dowodu jest starannie rozważony i adresowany w logiczny i spójny sposób. System tworzy wysoce ustrukturyzowane podejście do dowodzenia twierdzeń, opierając się na wcześniej ustalonych wynikach, aby zapewnić solidną podstawę dla każdego kolejnego kroku.
"Wykorzystując podcele generowane przez DeepSeek-V3, przyjmujemy strategię rekurencyjnego rozwiązywania, aby systematycznie rozwiązywać każdy pośredni krok dowodu. Wyodrębniamy wyrażenia podcelów ze stwierdzeń have, aby zastąpić je oryginalnymi celami w danych problemach, a następnie włączamy poprzednie podcele jako założenia. Ta konstrukcja umożliwia rozwiązywanie kolejnych podcelów przy użyciu pośrednich wyników wcześniejszych kroków, promując w ten sposób bardziej zlokalizowaną strukturę zależności i ułatwiając rozwój prostszych lematów" – szczegółowo wyjaśnili badacze.
Rekurencyjna strategia rozwiązywania jest kluczowym aspektem zdolności systemu do radzenia sobie ze złożonymi dowodami. Dzieląc problem na mniejsze, bardziej zarządzalne cele, system może skutecznie zastosować swoje możliwości rozumowania do każdego indywidualnego komponentu.
Optymalizacja zasobów obliczeniowych: specjalistyczny model z 7B parametrami
Aby skutecznie optymalizować zasoby obliczeniowe i zapewnić wydajne przetwarzanie, system strategicznie wykorzystuje mniejszy, wysoce wyspecjalizowany model z 7B parametrami do przetwarzania rozłożonych lematów. To podejście jest kluczowe dla skutecznego zarządzania wymaganiami obliczeniowymi związanymi z rozległymi wyszukiwaniami dowodów, zapewniając, że system może działać wydajnie, nie będąc przytłoczonym złożonością przestrzeni wyszukiwania. Podejście ostatecznie wieńczy automatycznie wyprowadzony kompletny dowód, gdy wszystkie rozłożone kroki zostaną pomyślnie rozwiązane.
"Algorytmiczny framework działa w dwóch odrębnych etapach, wykorzystując dwa uzupełniające się modele: DeepSeek-V3 do dekompozycji lematów i model z 7B prover do ukończenia odpowiednich szczegółów formalnego dowodu" – opisali badacze.
To dwuetapowe podejście pozwala systemowi wykorzystać mocne strony zarówno dużego modelu ogólnego przeznaczenia, jak i mniejszego specjalistycznego modelu. Duży model służy do generowania szkiców dowodów wysokiego poziomu, podczas gdy mniejszy model służy do wypełniania szczegółów i ukończenia formalnego dowodu.
Synteza danych rozumowania formalnego: naturalna ścieżka
Ta starannie zaprojektowana architektura skutecznie ustanawia naturalną i intuicyjną ścieżkę do syntezy danych rozumowania formalnego, płynnie łącząc rozumowanie matematyczne wysokiego poziomu ze ścisłymi i rygorystycznymi вимогами formalnej weryfikacji. Ta integracja jest niezbędna do zapewnienia niezawodności i wiarygodności wyników systemu.
"Selekcjonujemy podzbiór trudnych problemów, które pozostają nierozwiązane przez model z 7B prover w sposób kompleksowy, ale dla których wszystkie zdekomponowane podcele zostały pomyślnie rozwiązane. Komponując dowody wszystkich подцелей, konstruujemy kompletny formalny dowód dla oryginalnego problemu" – wyjaśnili badacze.
To podejście pozwala systemowi uczyć się na swoich błędach i poprawiać swoją zdolność do rozwiązywania złożonych problemów. Identyfikując konkretne подцели, które powodują trudności, system może skoncentrować swoje wysiłki na poprawie wydajności w tych obszarach.
Obawy i wyzwania: szczegóły implementacji pod obserwacją
Pomimo niezaprzeczalnych osiągnięć technicznych zademonstrowanych przez DeepSeek-Prover-V2, niektórzy eksperci w tej dziedzinie zgłosili istotne obawy dotyczące niektórych szczegółów implementacji. Elliot Glazer, wysoko ceniony wiodący matematyk w Epoch AI, zwrócił uwagę na potencjalne problemy, które wymagają dalszego zbadania.
Kilka obaw dotyczących artykułu DeepSeek-Prover-V2. Potencjalnie błędnie sformalizowane przykłady, a dyskusja na temat Lean zulip sugeruje, że dowody PutnamBench to nonsens i używają domyślnego przepraszam (prawdopodobnie ukrytego w taktyce apply?), co nie zostało zgłoszone w ich pętli odczytu-oceny-drukowania.
Te obawy wyraźnie podkreślają ciągłe wyzwania związane z formalną przestrzenią weryfikacji, w której nawet najmniejsze i pozornie nieistotne szczegóły implementacji mogą mieć nieproporcjonalnie duży wpływ na ogólną ważność i niezawodność wyników. Proces formalnej weryfikacji wymaga niezachwianej dbałości o szczegóły i skrupulatnego przestrzegania ustalonych standardów.
Potencjał błędnie sformalizowanych przykładów i możliwość ukrytych taktyk "sorry" w dowodach PutnamBench rodzą ważne pytania dotyczące rygoru i kompletności procesu weryfikacji. Te obawy podkreślają potrzebę ciągłego nadzoru i niezależnej weryfikacji wyników.
Dostępność i zasoby: demokratyzacja dostępu do formalnego dowodzenia twierdzeń
DeepSeek udostępnił swój Prover-V2 w dwóch różnych rozmiarach modeli, dostosowanych do różnorodnego zakresu zasobów obliczeniowych i celów badawczych. Pierwsza wersja to model z 7B parametrami zbudowany na bazie ich poprzedniego Prover-V1.5-Base, charakteryzujący się wydłużoną długością kontekstu do 32K tokenów. Druga wersja to znacznie większy model z 671B parametrami wytrenowany na DeepSeek-V3-Base. Oba modele są teraz łatwo dostępne na HuggingFace, wiodącej platformie do udostępniania i współpracy nad modelami uczenia maszynowego.
Oprócz samych modeli DeepSeek udostępnił również pełny zestaw danych ProverBench, zawierający 325 starannie sformalizowanych problemów do celów oceny, na HuggingFace. Ten kompleksowy zestaw danych zapewnia badaczom i programistom cenne źródło do oceny wydajności swoich modeli i porównywania ich z DeepSeek-Prover-V2.
Udostępniając te zasoby bezpłatnie, DeepSeek demokratyzuje dostęp do formalnej technologii dowodzenia twierdzeń i wspiera współpracę w społeczności badawczej. To podejście open-source prawdopodobnie przyspieszy postęp w tej dziedzinie i doprowadzi do nowych przełomów w automatycznym rozumowaniu i weryfikacji.
To wydanie daje badaczom i programistom zasoby potrzebne do zagłębiania się w możliwości i ograniczenia tej technologii. Zapewniając otwarty dostęp do modeli i zestawu danych ProverBench, DeepSeek zachęca do dalszej eksploracji i wspólnych wysiłków, aby rozwiać obawy zgłoszone przez ekspertów w tej dziedzinie. To oparte na współpracy podejście jest kluczem do rozwiązania złożoności formalnego dowodzenia twierdzeń i utrwalenia niezawodności tych przełomowych postępów.