Immagine AI

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.

Di Fantasy