DeepSeekMath-V2: Op weg naar zelf-verifieerbaar wiskundig redeneren

Samenvatting

Grote taalmodellen hebben aanzienlijke vooruitgang geboekt in wiskundig redeneren, wat een belangrijke testomgeving vormt voor AI en wetenschappelijk onderzoek zou kunnen beïnvloeden bij verdere ontwikkeling. Door redeneervaardigheid op te schalen met reinforcement learning dat correcte eindantwoorden beloont, zijn LLM's in één jaar tijd verbeterd van slechte prestaties tot het verzadigen van kwantitatieve redeneerwedstrijden zoals AIME en HMMT. Deze aanpak kent echter fundamentele beperkingen. Het najagen van hogere nauwkeurigheid van eindantwoorden lost een kernprobleem niet op: correcte antwoorden garanderen geen correcte redenering. Bovendien vereisen veel wiskundige taken, zoals stellingbewijzen, rigoureuze stap-voor-stap-afleiding in plaats van numerieke antwoorden, waardoor beloningen voor eindantwoorden onbruikbaar worden. Om de grenzen van diep redeneren te verleggen, menen wij dat het noodzakelijk is om de volledigheid en strengheid van wiskundige redenering te verifiëren. Zelfverificatie is vooral belangrijk voor het opschalen van rekenkracht tijdens testtijd, met name voor open problemen zonder bekende oplossingen. Richting zelfverifieerbaar wiskundig redeneren onderzoeken we hoe een accurate en betrouwbare LLM-gebaseerde verifier voor stellingbewijzen kan worden getraind. Vervolgens trainen we een bewijsgenerator met de verifier als beloningsmodel, en stimuleren we de generator om zoveel mogelijk problemen in hun eigen bewijzen te identificeren en op te lossen voordat deze worden gefinaliseerd. Om de kloof tussen generatie en verificatie in stand te houden naarmate de generator sterker wordt, stellen we voor om de verificatie-rekenkracht op te schalen om automatisch nieuwe, moeilijk te verifiëren bewijzen te labelen, waardoor trainingsdata ontstaat om de verifier verder te verbeteren. Ons resulterende model, DeepSeekMath-V2, toont sterke stellingbewijscapaciteiten, behaalt gouden scores op de IMO 2025 en CMO 2024 en een bijna perfecte 118/120 op de Putnam 2024 met opgeschaalde rekenkracht tijdens testtijd.

English

Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.

DeepSeekMath-V2: Op weg naar zelf-verifieerbaar wiskundig redeneren

DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning

Samenvatting

Support