DeepSeekMath-V2: Verso un Ragionamento Matematico Auto-Verificabile
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
November 27, 2025
Autori: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
cs.AI
Abstract
I grandi modelli linguistici hanno compiuto progressi significativi nel ragionamento matematico, che funge da importante banco di prova per l'IA e potrebbe influenzare la ricerca scientifica se ulteriormente perfezionato. Scalando il ragionamento con l'apprendimento per rinforzo che premia le risposte finali corrette, i LLM sono migliorati da scarse prestazioni alla saturazione di competizioni di ragionamento quantitativo come AIME e HMMT in un anno. Tuttavia, questo approccio presenta limitazioni fondamentali. Perseguire una maggiore accuratezza delle risposte finali non affronta un problema chiave: risposte corrette non garantiscono un ragionamento corretto. Inoltre, molti compiti matematici come la dimostrazione di teoremi richiedono una derivazione rigorosa passo-passo piuttosto che risposte numeriche, rendendo inapplicabili i premi per la risposta finale. Per spingere i limiti del ragionamento profondo, riteniamo necessario verificare la completezza e il rigore del ragionamento matematico. L'auto-verifica è particolarmente importante per scalare il calcolo al momento del test, specialmente per problemi aperti senza soluzioni note. Verso un ragionamento matematico auto-verificabile, investigiamo come addestrare un verificatore accurato e fedele basato su LLM per la dimostrazione di teoremi. Addestriamo quindi un generatore di dimostrazioni utilizzando il verificatore come modello di ricompensa, incentivando il generatore a identificare e risolvere il maggior numero possibile di problemi nelle proprie dimostrazioni prima di finalizzarle. Per mantenere il divario generazione-verifica man mano che il generatore diventa più forte, proponiamo di scalare il calcolo di verifica per etichettare automaticamente nuove dimostrazioni difficili da verificare, creando dati di addestramento per migliorare ulteriormente il verificatore. Il nostro modello risultante, DeepSeekMath-V2, dimostra forti capacità di dimostrazione di teoremi, raggiungendo punteggi di livello oro alle IMO 2025 e CMO 2024 e un quasi perfetto 118/120 al Putnam 2024 con calcolo scalato al momento del test.
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.