DeepSeekMath-V2: Przełom w matematyce wspomaganej AI. Model osiąga 118/120 punktów na Putnam 2024

W dziedzinie sztucznej inteligencji nastąpił istotny postęp w zakresie rozumowania matematycznego. DeepSeek AI zaprezentowało DeepSeekMath-V2, duży model językowy (LLM) o otwartych wagach, którego głównym przeznaczeniem jest dowodzenie twierdzeń w języku naturalnym z funkcją autoweryfikacji. Model, bazujący na architekturze DeepSeek-V3.2-Exp-Base i działający jako mieszanina ekspertów (MoE) z 685 miliardami parametrów, jest dostępny na platformie Hugging Face na licencji Apache 2.0.

Wyniki DeepSeekMath-V2 w testach benchmarkowych są imponujące. Model osiągnął poziom „złotego medalu” na Międzynarodowej Olimpiadzie Matematycznej (IMO) 2025 oraz Chińskiej Olimpiadzie Matematycznej (CMO) 2024. Szczególnie spektakularny jest wynik na amerykańskim konkursie Putnam 2024, gdzie DeepSeekMath-V2 zdobył 118 na 120 możliwych punktów, co przewyższa dotychczasowy najlepszy wynik ludzki (90 punktów).

Dlaczego sama odpowiedź numeryczna to za mało?

Obecne modele rozumowania matematycznego często opierają się na uczeniu ze wzmocnieniem, gdzie nagradzana jest jedynie poprawna odpowiedź końcowa. Takie podejście, choć pozwoliło na szybkie osiągnięcie nasycenia w konkursach z krótkimi odpowiedziami, ma swoje ograniczenia. Zespół badawczy DeepSeek wskazuje na dwa kluczowe problemy:

1. Poprawna odpowiedź numeryczna nie gwarantuje poprawnego rozumowania. Błędy algebraiczne mogą się wzajemnie niwelować, prowadząc do właściwego wyniku mimo wadliwych kroków.
2. Wiele zadań, w tym dowody olimpijskie i dowodzenie twierdzeń, wymaga kompletnego argumentu wyrażonego językiem naturalnym. W takich przypadkach nie ma jednej końcowej odpowiedzi numerycznej, co uniemożliwia zastosowanie standardowych systemów nagród.

W związku z tym DeepSeekMath-V2 skupia się na optymalizacji jakości dowodu, a nie wyłącznie na poprawności odpowiedzi. System ocenia kompletność i logiczną spójność rozumowania, wykorzystując tę ocenę jako główny sygnał uczenia.

Trening weryfikatora przed generatorem

Kluczową innowacją jest podejście „najpierw weryfikator”. Zespół DeepSeek opracował weryfikator oparty na LLM, który analizuje problem i przedstawiony dowód, a następnie generuje opisową analizę w języku naturalnym oraz dyskretną ocenę jakości (0, 0.5, 1). Początkowe dane do uczenia ze wzmocnieniem pochodzą z konkursów Art of Problem Solving. Zebrano 17 503 problemy wymagające dowodów z olimpiad i testów selekcyjnych, stanowiące bazę dla „zimnego startu” uczenia ze wzmocnieniem. Kandydatury dowodów generowane są przez model rozumujący DeepSeek-V3.2, który iteracyjnie udoskonala własne rozwiązania, produkując wiele niedoskonałych, lecz bogatych w detale dowodów. Eksperci ludzcy oceniają te dowody pod kątem rygoru i kompletności.

Weryfikator jest trenowany za pomocą Group Relative Policy Optimization (GRPO), gdzie nagroda składa się z dwóch komponentów: nagrody za format (zgodność z ustalonym szablonem) i nagrody za wynik (kara za różnicę między przewidywanym a eksperckim wynikiem). Ten etap treningu pozwala weryfikatorowi na spójne ocenianie dowodów w stylu olimpijskim.

Weryfikacja weryfikatora: rola metaweryfikatora

Mimo solidnego treningu, weryfikator mógłby „oszukać system”, generując poprawny wynik końcowy, jednocześnie fabrykując problemy w analizie. Aby temu zapobiec, wprowadzono metaweryfikator. Jego zadaniem jest ocena wierności analizy weryfikatora w stosunku do problemu i dowodu, sprawdzając spójność między opisem a ostateczną oceną. Metaweryfikator również jest trenowany za pomocą GRPO, a jego wynik wpływa na nagrodę dla podstawowego weryfikatora. Dzięki temu znacząco poprawiono jakość analiz (z 0.85 do 0.96).

Samoweryfikujący się generator dowodów i sekwencyjne udoskonalanie

Po wytrenowaniu silnego weryfikatora, przystąpiono do treningu generatora dowodów. Generator, przyjmując problem, nie tylko tworzy rozwiązanie, ale także własną analizę zgodną z kryteriami weryfikatora. Nagroda dla generatora składa się z trzech sygnałów: oceny weryfikatora, zgodności samocenionego wyniku z wynikiem weryfikatora oraz oceny metaweryfikacji. Dzięki temu generator jest motywowany do tworzenia dowodów, które są akceptowane przez weryfikatora i do uczciwej oceny własnych niedociągnięć.

DeepSeek wykorzystuje również limit kontekstu 128 tysięcy tokenów. W przypadku trudnych problemów, generator często nie jest w stanie naprawić wszystkich błędów za jednym razem. Wówczas system przeprowadza sekwencyjne udoskonalanie, iteracyjnie poprawiając dowód i analizę, aż do wyczerpania budżetu kontekstowego. W miarę doskonalenia generatora, pojawia się problem kosztownego ręcznego etykietowania coraz trudniejszych dowodów. Wprowadzono zatem zautomatyzowaną linię etykietowania, która wykorzystuje zwielokrotnioną weryfikację, pozwalając na utrzymanie świeżości danych treningowych.

Wyniki i osiągnięcia

DeepSeekMath-V2 został poddany wszechstronnej ewaluacji. W wewnętrznych testach 91 problemów na poziomie Chinese National Mathematical Olympiad (CNML), model DeepSeekMath-V2 osiągnął najwyższy średni wynik weryfikatora we wszystkich kategoriach (algebra, geometria, teoria liczb, kombinatoryka, nierówności), przewyższając Gemini 2.5 Pro i GPT 5 Thinking High. Na liście krótkich dowodów IMO 2024, sekwencyjne udoskonalanie z autoweryfikacją poprawiło metryki jakości w miarę wzrostu liczby iteracji.

Najważniejsze osiągnięcia DeepSeekMath-V2 to:

• IMO 2025: rozwiązanie 5 z 6 problemów, poziom złotego medalu.
• CMO 2024: pełne rozwiązanie 4 problemów oraz częściowe kredyty za jeden, poziom złotego medalu.
• Putnam 2024: rozwiązanie 11 z 12 problemów w całości, z drobnymi błędami w pozostałym, co dało 118 z 120 punktów, znacznie powyżej najlepszego wyniku ludzkiego.

Kluczowe wnioski

DeepSeekMath-V2 stanowi znaczący krok w kierunku weryfikowalnego rozumowania matematycznego. Innowacyjne podejście do treningu, z weryfikatorem i metaweryfikatorem oceniającymi rygor dowodów, a nie tylko ostateczne odpowiedzi, skutecznie wypełnia lukę między poprawnością wyniku a poprawnością rozumowania. Fakt, że ten model jest otwarty (open weights) i osiąga tak wybitne rezultaty na poziomie konkursów olimpijskich, jest dowodem na praktyczną wykonalność samoweryfikowalnego rozumowania matematycznego w AI.
DeepSeekMath-V2 jest z pewnością ważnym krokiem w rozwoju sztucznej inteligencji, otwierającym nowe perspektywy dla automatycznego dowodzenia twierdzeń i rozwiązywania złożonych problemów matematycznych.