Can LLMs Write Correct TLA+ Specifications? Evaluating Natural-Language-to-TLA+ Generation

Immagina di cercare di insegnare a un robot molto intelligente e colto come scrivere una ricetta matematica rigorosa per una macchina complessa. Questa macchina è un "sistema distribuito" (come i server cloud che fanno funzionare Amazon o Microsoft), e la ricetta è scritta in un linguaggio speciale chiamato TLA+.

Questo linguaggio è come un puzzle ad alta posta in gioco. Se dimentichi un singolo simbolo o sbagli leggermente la logica, la macchina potrebbe funzionare nella ricetta ma crashare nella realtà. Il problema è che scrivere queste ricette a mano è difficile e lento. Così, i ricercatori si sono chiesti: possiamo semplicemente chiedere a un'IA moderna (un Large Language Model, o LLM) di scrivere queste ricette per noi?

Questo articolo è il primo grande rapporto di valutazione su questa domanda. Ecco cosa hanno scoperto, spiegato in modo semplice:

1. Il divario tra "Grammatica e Significato"

I ricercatori hanno chiesto a 30 diverse IA di scrivere queste ricette TLA+ basandosi su descrizioni in linguaggio naturale.

• La buona notizia (Grammatica): Circa il 26% delle volte l'IA ha scritto una ricetta che appariva corretta in superficie. Il "correttore ortografico" (chiamato SANY) ha detto: "Ok, le parole e i simboli sono nell'ordine giusto".
• La cattiva notizia (Significato): Tuttavia, quando hanno effettivamente eseguito la ricetta attraverso un "tester logico" (chiamato TLC) per vedere se funzionasse davvero, solo l'8,6% delle volte ha superato la prova.

L'analogia: Immagina di chiedere a uno studente di scrivere un contratto legale. Lo studente usa un'ortografia e una grammatica perfette (26% di successo), ma il contratto che ha scritto dice in realtà l'opposto di ciò che era inteso, o omette una clausola cruciale, rendendolo legalmente inutile (solo l'8,6% di successo). L'IA è brava a imitare l'aspetto del linguaggio, ma spesso fallisce nel comprendere la logica che ci sta dietro.

2. Più grande non significa sempre meglio

Di solito, assumiamo che un'IA più grande e potente faccia un lavoro migliore. Ma in questo studio, non è stato così.

• La sorpresa: Un modello di IA più piccolo (DeepSeek r1:8b) ha fatto un lavoro molto migliore rispetto al suo "fratello maggiore" enorme (DeepSeek r1:70b).
• Perché? Il modello più piccolo è stato addestrato specificamente per "pensare passo dopo passo" (come uno studente di matematica che mostra i passaggi), mentre il modello più grande è stato addestrato su una quantità enorme di dati generici da internet e si è confuso con le regole rigide di TLA+. È come uno chef specializzato che sa esattamente come preparare un soufflé, rispetto a un generalista che sa cucinare tutto ma potrebbe complicarsi la vita con una ricetta specifica.

3. Gli "Esperti di Codice" sono falliti

I ricercatori hanno testato IA famose per scrivere codice informatico (come Python o Java). Sorprendentemente, questi "esperti di codice" hanno fatto peggio delle IA generiche.

• Il motivo: Questi modelli sono così abituati a scrivere codice con punti e virgola (;) o parentesi graffe ({}) che continuavano ad aggiungerli accidentalmente nella ricetta TLA+. Poiché TLA+ non usa questi simboli, la ricetta si rompeva immediatamente. È come un carpentiere che cerca di riparare un orologio ma prova accidentalmente a usare un martello perché è quello che usa per tutto il resto.

4. Il trucco del "Passo dopo Passo" ha funzionato meglio

I ricercatori hanno provato quattro modi diversi per chiedere aiuto all'IA. Il metodo più efficace è stato chiamato "Prompting Progressivo".

• Come funzionava: Inveve di chiedere all'IA di scrivere l'intera ricetta in una volta sola, le hanno chiesto di costruirla pezzo per pezzo: "Per prima cosa, scrivi il titolo. Ora, scrivi le variabili. Ora, scrivi le regole".
• Il risultato: Questo è stato l'unico metodo che ha prodotto ricette completamente funzionanti (il tasso di successo dell'8,6%). È come costruire una casa: se provi a costruire il tetto, le pareti e le fondamenta in un unico salto gigante, probabilmente fallirai. Ma se costruisci una stanza alla volta, hai una possibilità di successo in più.

5. Le "Allucinazioni" dell'IA

L'articolo ha trovato cinque modi specifici in cui l'IA continuava a commettere gli stessi errori, che chiamano "allucinazioni":

1. Simboli errati: Usare simboli matematici elaborati (come ∧) invece dei simboli di testo semplice richiesti da TLA+ (come /\).
2. Mescolanza di linguaggi: Aggiungere accidentalmente punti e virgola o backtick provenienti da altri linguaggi di programmazione.
3. Pensare ad alta voce: L'IA a volte incollava il proprio "processo di pensiero" (come ...) direttamente nella ricetta finale, il che la rompeva.
4. Lunghezza errata: A volte l'IA scriveva una ricetta 9 volte troppo lunga, o a volte non scriveva quasi nulla.
5. Struttura interrotta: Mancanza dei marcatori di "fine" della ricetta, lasciando il documento incompleto.

Il succo del discorso

L'articolo conclude che le attuali IA non possono ancora scrivere specifiche TLA+ affidabili da sole. Sebbene possano imitare l'aspetto del linguaggio, commettono ancora troppi errori logici per essere affidabili senza che un esperto umano controlli ogni singola riga.

I ricercatori suggeriscono che per risolvere questo problema, dobbiamo:

• Usare il metodo di prompting "passo dopo passo".
• Usare modelli più piccoli e focalizzati sul ragionamento piuttosto che modelli enormi e generici.
• Costruire strumenti che corregano automaticamente gli errori comuni (come la rimozione dei simboli errati) prima ancora che l'IA provi a eseguire la ricetta.

Fino ad allora, scrivere queste critiche ricette di sistema rimane un lavoro per esperti umani, con l'IA che funge da assistente utile ma propenso all'errore.