Leanstral 1.5: dimostrazioni in abbondanza per tutti

Dal suo lancio, Leanstral ha offerto un approccio aperto e pratico all’ingegneria delle dimostrazioni in Lean 4. Oggi rilasciamo Leanstral 1.5, un modello gratuito con licenza Apache-2.0, 119B parametri totali e solo 6B parametri attivi, che offre un miglioramento delle prestazioni tale da rendere la verifica formale più potente e accessibile che mai.

Leanstral 1.5 satura miniF2F, risolve 587/672 problemi di PutnamBench, e raggiunge un nuovo stato dell’arte del %87 su FATE-H e del 34% su FATE-X. Oltre ai benchmark, verifica proprietà complesse del codice e scopre bug precedentemente sconosciuti in repository open-source, dimostrando che metodi formali rigorosi possono essere sia efficaci sia pratici per l’uso nel mondo reale.

Addestramento di Leanstral

Leanstral 1.5 segue un processo in tre fasi: mid-training, supervised fine-tuning e reinforcement learning con CISPO. Leanstral 1.5 sfrutta un addestramento estensivo su due ambienti RL:

Nell’ambiente multiturn, al modello viene fornito l’enunciato di un teorema e deve dimostrarlo o confutarlo. Il modello invia una dimostrazione, riceve il feedback del compilatore Lean e affina il proprio approccio a ogni tentativo. Se la dimostrazione compila, ha successo; altrimenti il ciclo continua finché il modello risolve il problema o esaurisce il proprio budget.

Nell’ambiente code agent, Leanstral opera come una persona sviluppatrice in un filesystem grezzo: modifica file, esegue comandi bash e usa il language server di Lean per ispezionare obiettivi, errori e informazioni sui tipi in tempo reale. Questo gli consente di affrontare attività di lungo orizzonte, come completare dimostrazioni parziali in un repository, costruire lemmi ausiliari e proseguire attraverso più cicli di compattazione del contesto. Il modello impara a navigare l’intero workflow di ingegneria delle dimostrazioni e viene infine verificato dal nostro fork di SafeVerify per la correttezza, data una lista di teoremi target.

Valutazione

Valutiamo Leanstral sui seguenti benchmark:

• miniF2F è un benchmark cross-system per la matematica formale, che spazia da problemi elementari a sfide di livello IMO, testando diverse capacità dimostrative in algebra, combinatoria e teoria dei numeri.

• PutnamBench è composto da 672 problemi della Putnam Mathematical Competition, che richiedono ragionamento profondo e lunghe catene dimostrative per risolvere problemi matematici complessi.

• FATE-H e FATE-X sono benchmark di algebra astratta rispettivamente per problemi di livello graduate e PhD, che testano il ragionamento avanzato in aree come teoria dei gruppi, teoria degli anelli e teoria dei moduli.

• FLTEval si basa su pull request reali dal repository dell’Ultimo Teorema di Fermat, testando l’ingegneria pratica delle dimostrazioni con complessità realistica.

Saturiamo completamente miniF2F, raggiungendo il 100% sia sul set di validazione sia su quello di test. Su PutnamBench e FATE-H/X, confrontiamo Leanstral 1.5 con Goedel-Architect senza guida in linguaggio naturale, Seed-Prover 1.5 nella sua impostazione high e AxProverBase. Leanstral raggiunge un nuovo stato dell’arte su FATE-H/X, risolvendo rispettivamente 87 e 34 problemi. Su PutnamBench supera Seed-Prover 1.5 high di 7 problemi a un costo molto inferiore: circa 4 $ per problema, contro una stima di almeno 300 $ per Seed-Prover, la cui impostazione high viene eseguita con un budget di 10 giorni-H20 per problema. Gli unici prover classificati più in alto operano in condizioni diverse: alcuni ricevono una guida alla dimostrazione in linguaggio naturale, altri hanno costi di esecuzione molto più elevati, come Aleph Prover a 54–68 $ per problema.

Leanstral 1.5 mostra il più forte test-time scaling che abbiamo osservato in un modello di ragionamento formale. La figura sotto traccia Pass@8 su PutnamBench mentre aumentiamo il budget di token per tentativo da 25k a 4M: le prestazioni crescono in modo fluido e monotono lungo tutto il percorso, da 44 problemi risolti a 50k a 244 a 200k, 493 a 1M e 587 a 4M. Invece di fermarsi quando una dimostrazione si prolunga, Leanstral continua a ragionare, modificare file e rivedere attraverso milioni di token, convertendo direttamente quel budget in problemi risolti: lo stesso comportamento alla base della dimostrazione sugli alberi AVL qui sotto, eseguita per oltre 2,7 milioni di token attraverso 22 compattazioni.

Con questo rilascio, rendiamo anche FLTEval completamente open source. Leanstral 1.5 porta il pass@1 sul benchmark da 21,9 a 28,9 e il pass@8 da 31,9 a 43,2, superando il 39,6 di Opus 4.6 a un settimo del costo. Inoltre amplia il proprio vantaggio rispetto a modelli open-source 3–10× più grandi, come mostrato nella figura sotto.

Casi di studio sulla verifica del codice

Pur essendo addestrato principalmente per la matematica, Leanstral 1.5 dimostra forti capacità nella verifica del codice. Presentiamo 2 casi di studio critici per dimostrarne l’impatto.

Alberi AVL: dimostrare la complessità temporale

Gli alberi AVL sono alberi di ricerca binari autobilancianti che mantengono un’altezza O(log n) tramite ribilanciamento durante inserimenti ed eliminazioni. Leanstral 1.5 ha dimostrato queste garanzie di complessità temporale per un’implementazione reale, un’attività che ha richiesto induzione strutturale per rispecchiare la struttura ricorsiva dell’albero, una gestione accurata del tracciamento temporale monadico e un’analisi esaustiva dei casi per i percorsi di ribilanciamento. Attraverso oltre 2,7 milioni di token e 22 compattazioni, Leanstral ha espanso sistematicamente ogni livello della monade TimeM, esponendo i calcoli sottostanti nonostante il loro intreccio con il flusso di controllo. Ha stabilito un limite quasi stretto di 48 passaggi per unità di altezza più una costante per l’inserimento, quindi ha collegato l’altezza alla dimensione dell’albero tramite una relazione logaritmica, fornendo dimostrazioni complete e verificate che inserimento ed eliminazione sono effettivamente O(log n).

Scoperta di bug: individuare difetti nascosti

Per testare le capacità di Leanstral nell’individuazione dei bug, abbiamo costruito una pipeline automatizzata: Aeneas traduce codice Rust in Lean, mentre Leanstral inferisce l’intento dell’utente e genera proprietà di correttezza a partire dal codice. Leanstral tenta quindi di dimostrare ciascuna proprietà in quattro tentativi. Se tutti falliscono, prova invece a dimostrarne la negazione, anche in questo caso con quattro tentativi. Su 57 repository testati, questo processo ha segnalato 47 proprietà violate, di cui 11 riferite a bug reali, 5 dei quali mai segnalati prima su GitHub.

Uno di questi bug si trovava nella funzione di segno per la decodifica zigzag della libreria datrs/varinteger. Con input Std.U64.MAX, l’espressione (value + 1) andava in overflow, causando crash in modalità debug e corruzione silenziosa in modalità release: un caso limite che testing e fuzzing in genere non rileverebbero. La pipeline di Leanstral lo ha intercettato automaticamente, dimostrando che la verifica formale può già essere applicata a codebase reali e trovare bug che alcuni metodi tradizionali trascurano.

Per iniziare

Leanstral 1.5 ha una licenza Apache-2.0 . I pesi sono disponibili su Huggingface e sono inoltre già disponibili come endpoint API gratuito con il nome leanstral-1-5. Consigliamo di usarlo in Mistral Vibe. Per iniziare il Suo percorso, ottenga una API Key e:

1. Configurare Mistral Vibe

uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setup

2. Installare Leanstral 1.5

/leanstall
exit

3. Avviare l’agent

vibe --agent lean

4. Installare Lean LSP MCP (facoltativo)

Si consiglia vivamente di installare Lean LSP MCP aggiungendo quanto segue al file ~/.vibe/config.toml

[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

Se non sono presenti server MCP esistenti, potrebbe essere necessario rimuovere mcp_servers = [].

5. Iniziare a dimostrare

Chieda a Leanstral di affrontare un teorema, eseguire il debug di una dimostrazione o contribuire a un repository. È così semplice.