Nuovo modello AI firmato DeepSeek: ecco DeepSeekMath-V2, progettato per elevare la qualità e la verificabilità del ragionamento matematico prodotto dai grandi modelli linguistici (LLM). A differenza degli approcci tradizionali che si concentrano solo sul risultato finale, questo nuovo sistema punta a garantire rigore logico e completezza dei passaggi, affrontando uno dei limiti strutturali più complessi nell’ambito della matematica automatizzata.
Ciclo generazione-verifica: come funziona il modello
Negli ultimi anni, il reinforcement learning ha permesso ai modelli di avvicinarsi ai punteggi massimi in competizioni come AIME e HMMT, riducendo margini di errore sul risultato numerico. Tuttavia, un valore corretto non implica necessariamente un ragionamento solido e verificabile, elemento cruciale soprattutto per problemi aperti o derivazioni formali.
Per questo motivo, DeepSeekMath-V2 integra un sistema di auto-verifica, progettato per controllare la completezza di ogni passaggio e stimolare il modello a correggere autonomamente eventuali errori prima della finalizzazione della dimostrazione.
Secondo il portale European Central Station, il cuore del modello è un circuito generativo che combina un proof generator e un verificatore specializzato nella prova dei teoremi. Il verificatore non si limita a controllare l’esattezza del risultato, ma valuta la struttura logica dell’intera dimostrazione, diventando il “reward model” del generatore.
In questo modo, ogni dimostrazione prodotta viene analizzata, affinata e corretta in tempo reale, mentre la scalabilità del verificatore permette di aumentare progressivamente la complessità dei controlli. Questo approccio consente al sistema di affrontare anche prove particolarmente articolate, che richiedono calcoli intensivi e precisione estrema.
I risultati ottenuti da DeepSeekMath-V2 nelle principali competizioni matematiche confermano le potenzialità del modello: punteggi gold all’IMO 2025 e al CMO 2024, e un impressionante 118/120 nel Putnam 2024, grazie a compute scalato in fase di test. Ulteriori valutazioni condotte su IMO-ProofBench, sviluppato dal team DeepMind dietro DeepThink IMO-Gold, attestano la capacità del sistema nella dimostrazione rigorosa dei teoremi.
La versione DeepSeekMath-V2 è basata su DeepSeek-V3.2-Exp-Base ed è disponibile su HuggingFace con licenza Apache 2.0. Tutti i dettagli sul ciclo generazione-verifica, sui dataset e sul processo di addestramento sono pubblicati su GitHub, insieme al paper tecnico e al codice completo.