Leanstral: base open-source per un vibe-coding affidabile

Gli agenti di AI si sono dimostrati strumenti altamente capaci nella generazione di codice. Tuttavia, man mano che spingiamo questi modelli verso domini ad alta criticità, dalla matematica di ricerca d'avanguardia al software mission-critical, incontriamo un collo di bottiglia della scalabilità: la revisione umana. Il tempo e le competenze specialistiche necessari per la verifica manuale diventano il principale impedimento alla velocità di sviluppo.

Immaginiamo una generazione più utile di agenti di coding, in grado sia di svolgere i propri compiti sia di dimostrare formalmente le proprie implementazioni rispetto a specifiche rigorose. Invece di eseguire il debugging della logica generata dalla macchina, le persone indicano ciò che desiderano. Oggi compiamo il primo grande passo verso questa visione.

Presentazione di Leanstral

Rilasciamo Leanstral, il primo agente di codice open-source progettato per Lean 4. Lean4 è un assistente alla dimostrazione capace di esprimere oggetti matematici complessi come gli spazi perfettoidi e specifiche software come le proprietà di frammenti Rust. A differenza dei sistemi di dimostrazione esistenti, che fungono da wrapper attorno a grandi modelli generalisti o si concentrano su singoli problemi matematici, Leanstral è progettato per essere altamente efficiente (con 6B parametri attivi) e addestrato per operare in repository formali realistici.

• Aperto e accessibile: rilasciamo i pesi di Leanstral con licenza Apache 2.0, in modalità agent all'interno di Mistral Vibe e tramite un endpoint API gratuito. Pubblicheremo inoltre un tech report che descrive nel dettaglio il nostro approccio di training, oltre a una nuova suite di valutazione, FLTEval, per portare le valutazioni oltre il focus sulla matematica da competizione.

• Efficiente e potente: utilizziamo un'architettura altamente sparsa per Leanstral e la ottimizziamo per attività di proof engineering. Sfruttando l'inferenza parallela con Lean come verificatore perfetto, Leanstral offre prestazioni elevate ed efficienza nei costi rispetto ai concorrenti closed-source esistenti.

• Estensibile via MCP: Leanstral supporta MCP arbitrari tramite Vibe ed è stato addestrato specificamente per raggiungere prestazioni massime con il diffuso lean-lsp-mcp. 

Valutazione

Per riflettere l'utilità in scenari realistici di proof engineering, sottoponiamo Leanstral a benchmark sul completamento di tutte le dimostrazioni formali e sulla definizione corretta di nuovi concetti matematici in ogni PR del progetto FLT, anziché su problemi matematici isolati. Confrontiamo Leanstral con agenti di coding leader (Claude Opus 4.6, Sonnet 4.6, Haiku 4.5) e modelli open-source (Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B).

Leanstral vs. modelli OSS

Leanstral-120B-A6B dimostra un vantaggio significativo in termini di efficienza rispetto ai suoi peer open-source molto più grandi. Mentre modelli come GLM5-744B-A40B e Kimi-K2.5-1T-32B faticano a scalare, fermando i propri punteggi FLTEval rispettivamente a circa 16.6 e 20.1, Leanstral li supera entrambi con una sola passata.

Anche Qwen3.5-397B-A17B, il concorrente OSS più forte mostrato, richiede 4 passate per raggiungere un punteggio di 25.4. Al contrario, Leanstral ottiene un punteggio superiore di 26.3 con metà di quell'investimento (pass@2) e continua a scalare linearmente, raggiungendo 29.3 allo stesso livello di costo.

Leanstral vs. famiglia Claude

Leanstral è un'alternativa ad alto valore alla suite Claude, offrendo prestazioni competitive a una frazione del prezzo: Leanstral pass@2 raggiunge un punteggio di 26.3, superando Sonnet di 2.6 punti, con un costo di esecuzione di soli $36, rispetto ai $549 di Sonnet. A pass@16, Leanstral raggiunge un punteggio di 31.9, superando nettamente Sonnet di 8 punti. Sebbene Claude Opus 4.6 resti leader in termini di qualità, comporta un costo impressionante di $1,650, 92 volte superiore rispetto all'esecuzione di Leanstral.

Nel nostro benchmarking abbiamo utilizzato Mistral Vibe come scaffold, senza modifiche specifiche per la valutazione.

Casi di studio

Rispondere a post Stack Exchange sulle modifiche nella versione più recente di Lean

Quando una nuova release di Lean introduce breaking change, migrare il codice può diventare un enorme grattacapo. Abbiamo fornito a Leanstral una domanda reale da Proof Assistants Stack Exchange su uno script che aveva misteriosamente smesso di compilare in Lean 4.29.0-rc6 (su cui non abbiamo eseguito training a causa della sua recente pubblicazione). Il responsabile era una tattica di rewrite (rw) che improvvisamente non riusciva più a trovare corrispondenze con pattern che coinvolgevano un semplice alias di tipo, inizialmente scritto come def T2 := List Bool.

Invece di procedere per tentativi, Leanstral si è messo al lavoro. Ha costruito con successo codice di test per ricreare l'ambiente in errore e ha diagnosticato il problema sottostante legato all'uguaglianza definizionale. Il modello ha identificato correttamente che, poiché def crea una definizione rigida che richiede un unfolding esplicito, stava di fatto impedendo alla tattica rw di vedere la struttura sottostante necessaria per trovare la corrispondenza.

La correzione proposta era semplice: sostituire def con abbrev. Poiché abbrev crea un alias trasparente che è immediatamente uguale per definizione al tipo originale, la tattica rw poteva di nuovo trovare perfettamente corrispondenza con il pattern (L2 n).length nella dimostrazione. Leanstral completa il compito e spiega perfettamente il razionale all'utente. 

Ragionare sui programmi

Abbiamo copiato definizioni in Rocq da https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html e chiesto a Leanstral di convertirle in Lean. Lo ha fatto con successo, implementando persino una notazione personalizzata. Frammento di esempio:

inductive ceval : com → state → state → Prop where
 | E_Skip (st : state) : ceval .CSkip st st
 | E_Ass (st : state) (a1 : aexp) (n : Nat) (l : ident) (h : aeval a1 st = n) :
     ceval (.CAss l a1) st (update st l n)
 | E_Seq (c1 c2 : com) (st st' st'' : state) (h1 : ceval c1 st st') (h2 : ceval c2 st' st'') :
     ceval (.CSeq c1 c2) st st''
 | E_IfTrue (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = true) (h1 : ceval c1 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_IfFalse (st st' : state) (b1 : bexp) (c1 c2 : com) (h : beval b1 st = false) (h1 : ceval c2 st st') :
     ceval (.CIf b1 c1 c2) st st'
 | E_WhileEnd (b1 : bexp) (st : state) (c1 : com) (h : beval b1 st = false) :
     ceval (.CWhile b1 c1) st st
 | E_WhileLoop (st st' st'' : state) (b1 : bexp) (c1 : com) (h1 : beval b1 st = true) (h2 : ceval c1 st st') (h3 : ceval (.CWhile b1 c1) st' st'') :
     ceval (.CWhile b1 c1) st st''


-- Notation for command evaluation
notation:50 c " / " st " ⇒ " st' => ceval c st st'

È stato anche in grado di tradurre in Lean e poi dimostrare alcune proprietà sui programmi in questo linguaggio partendo dal solo enunciato Rocq (senza dimostrazione):

-- Example command: adds 2 to variable X
def plus2 : com := .CAss "X" (.APlus (.AId "X") (.ANum 2))


-- Theorem: The plus2 command correctly adds 2 to variable X
-- Intuition: If X has value n in the initial state, after executing plus2,
-- X will have value n+2 in the final state
-- This specifies the behavior of the plus2 command
theorem plus2_spec (st : state) (n : Nat) (st' : state) (h1 : st "X" = n) (h2 : plus2 / st ⇒ st') :
 st' "X" = n + 2 := by
 -- plus2 is defined as .CAss "X" (.APlus (.AId "X") (.ANum 2))
 -- Use equation compiler to unfold it
 change ceval (.CAss "X" (.APlus (.AId "X") (.ANum 2))) st st' at h2
 cases h2 with
 | E_Ass _ _ n l h =>
   have : aeval (.APlus (.AId "X") (.ANum 2)) st = n := h
   simp only [aeval] at this
   rw [update]
   simp [← this, h1]

Pretenda la dimostrazione. Provi Leanstral oggi.

Leanstral è disponibile da oggi per tutti.

• Zero setup in Mistral Vibe: abbiamo integrato Leanstral direttamente in Mistral Vibe per attività immediate di vibe coding e dimostrazione, senza setup. Usi /leanstall per attivarlo. Quindi, per usare Leanstral, prema Shift+Tab finché il modello visualizzato non è Leanstral. In alternativa, usi vibe --agent lean.

• Labs API: acceda al modello tramite il nostro endpoint API gratuito/quasi gratuito labs-leanstral-2603. Manteniamo questo endpoint altamente accessibile per un periodo limitato, così da raccogliere feedback realistici e dati di osservabilità utili ad alimentare la prossima generazione di modelli di codice verificato.

• Pesi sotto il proprio controllo: scarichi il modello con licenza Apache 2.0 e lo esegua sul proprio hardware.

Documentazione - Registrarsi a Mistral Vibe