Il 30 aprile 2025, DeepSeek ha rilasciato senza preavviso il modello di intelligenza artificiale Prover-V2, specializzato nella dimostrazione automatica di teoremi matematici. Questo rilascio, avvenuto sulla piattaforma Hugging Face, è stato effettuato senza un annuncio ufficiale, suscitando interesse e curiosità nella comunità tecnologica.
Prover-V2 è un modello linguistico di grandi dimensioni progettato specificamente per affrontare problemi complessi di logica e matematica formale. Basato sull’architettura Mixture-of-Experts (MoE), il modello vanta 671 miliardi di parametri, con un’architettura che consente l’attivazione di un numero selezionato di esperti per ottimizzare l’efficienza computazionale.
Il modello è stato addestrato utilizzando un processo di “cold-start” che ha coinvolto il modello DeepSeek-V3 per decomporre problemi complessi in sotto-obiettivi, facilitando così la dimostrazione dei teoremi. Questo approccio ha permesso a Prover-V2 di raggiungere prestazioni notevoli, come evidenziato nei benchmark standardizzati.
Prover-V2 ha ottenuto risultati significativi in vari test di benchmark. Ad esempio, ha raggiunto una percentuale di successo dell’88,9% nel MiniF2F-test e ha risolto 49 problemi su 658 nel PutnamBench. Inoltre, ha affrontato con successo 6 dei 15 problemi provenienti dalle recenti competizioni AIME, dimostrando la sua capacità di gestire problemi matematici complessi.
Per arricchire ulteriormente la valutazione, DeepSeek ha introdotto ProverBench, una raccolta di 325 problemi formalizzati, che include anche problemi selezionati dalle competizioni AIME degli anni 2024-2025. Questa iniziativa mira a fornire una valutazione più completa delle capacità del modello.
Il rilascio di Prover-V2 senza un annuncio ufficiale può essere interpretato come una strategia per testare la completezza tecnica del modello e raccogliere feedback dalla comunità di sviluppatori prima del lancio ufficiale del prossimo modello di generazione, DeepSeek-R2. Questo approccio consente a DeepSeek di affinare ulteriormente le capacità del modello e di rispondere alle esigenze della comunità scientifica e tecnologica.