Mistral ha appena reso disponibile Leanstral 1.5, un Large Language Model pensato per la verifica formale e rilasciato con licenza Apache 2.0. Il dato che salta subito all’occhio non sono soltanto i numeri da primato su benchmark consolidati, quanto l’architettura del modello: 119 miliardi di parametri totali, di cui solo 6 miliardi attivi per ciascuna inference. Un rapporto che nei fatti riconfigura i confini del deployment on-premise per tool di proof engineering, perché consente di eseguire localmente carichi che fino a poco tempo fa avrebbero richiesto cluster dedicati.

Il modello satura praticamente il benchmark miniF2F (un test di teoremi matematici), risolve 587 dei 672 problemi del PutnamBench – la temuta competizione universitaria nordamericana – e stabilisce nuovi riferimenti su FATE-H (87%) e FATE-X (34%), due metriche pensate per valutare le capacità di verifica su codice reale. Non si tratta di esercizi di stile: nei test su 57 repository open source, Leanstral 1.5 ha individuato 5 bug precedentemente sconosciuti, dimostrando un’efficacia concreta nel validare specifiche software e correttezza di implementazioni.

L’addestramento ha seguito un percorso in tre fasi: mid-training su corpus specialistici, supervised fine-tuning e reinforcement learning tramite l’algoritmo CISPO (Contextual Inference with Self-Play Optimization, una variante pensata per domini formali). Il risultato è un modello che eccelle non solo nel theorem proving automatico, ma anche nell’"agentic proof engineering", dove il sistema esplora attivamente lo spazio delle dimostrazioni come farebbe un matematico umano.

Cosa significa tutto questo per chi valuta il deployment on-premise? Il punto di forza è il basso numero di parametri attivi. Sei miliardi è una soglia che oggi può essere gestita da una singola GPU consumer o da una workstation ben dimensionata, senza necessità di ricorrere a servizi cloud. Per team che operano su codice proprietario, software crittato o in ambienti con vincoli di residenza dati, la possibilità di eseguire un verificatore formale senza mai esporre sorgenti all’esterno è un vantaggio dirompente. La licenza Apache 2.0, inoltre, elimina incertezze legali e consente fork, modifiche e integrazioni senza restrizioni.

Mistral non ha ancora diffuso requisiti hardware precisi, ma il profilo di risorse avvicina Leanstral 1.5 a modelli che già oggi vengono serviti su singole GPU con 16-24 GB di VRAM, sfruttando anche la quantization qualora servisse ridurre ulteriormente l’impronta. L’aspetto più interessante, forse, è che l’intero flusso di verifica rimane confinato all’infrastruttura aziendale, allineandosi alle politiche di sicurezza che rendono il cloud un’opzione percorribile solo in parte. In un’epoca in cui la sovranità del dato non è più una bandierina ma un requisito contrattuale, modelli del genere segnano un cambio di passo concreto per gli strumenti di sviluppo.