Verso l'Autoformalizzazione degli Output Generati da LLM per la Verifica dei Requisiti

Informazioni Fondamentali

• ID Articolo: 2511.11829
• Titolo: Towards Autoformalization of LLM-generated Outputs for Requirement Verification
• Autori: Mihir Gupte, Ramesh S. (General Motors)
• Classificazione: cs.CL, cs.AI, cs.FL, cs.LO
• Data di Pubblicazione: 18 novembre 2025 (preprint arXiv)
• Link Articolo: https://arxiv.org/abs/2511.11829

Riassunto

Questo articolo esplora la fattibilità dell'utilizzo di tecniche di autoformalizzazione per verificare l'accuratezza degli output generati da modelli di linguaggio di grandi dimensioni (LLM). Poiché gli LLM hanno dimostrato potenziale nel convertire requisiti in linguaggio naturale in output strutturati (come scenari Gherkin), la verifica formale dell'accuratezza di questi output diventa una questione critica. Il team di ricerca ha condotto due serie di esperimenti: la prima ha identificato con successo l'equivalenza logica tra due requisiti in linguaggio naturale con formulazioni diverse; la seconda ha identificato incoerenze logiche tra gli output generati da LLM e i requisiti originali. Sebbene l'ambito della ricerca sia limitato, i risultati indicano che l'autoformalizzazione ha un potenziale significativo nel garantire la fedeltà e la coerenza logica degli output generati da LLM.

Contesto e Motivazione della Ricerca

1. Problema Centrale

Con la diffusione delle applicazioni LLM, in particolare nella generazione automatica di scenari di test e altri compiti ingegneristici, esiste una sfida critica: la mancanza di metodi formali per verificare se gli output generati da LLM riflettono accuratamente i requisiti originali in linguaggio naturale. Ad esempio, dopo aver generato uno scenario Gherkin da un requisito come "Quando la velocità del veicolo ≥ 10 e la cintura di sicurezza non è allacciata, attivare il promemoria della cintura di sicurezza", non è possibile garantire la correttezza logica del contenuto generato.

2. Importanza del Problema

Nei settori critici per la sicurezza come l'ingegneria automobilistica, la verifica dei requisiti è fondamentale. Una conversione errata dei requisiti può portare a:

• Casi di test incompleti o errati
• Comportamento del sistema non conforme alle aspettative
• Potenziali rischi per la sicurezza

3. Limitazioni dei Metodi Esistenti

• Metodi di formalizzazione tradizionali: principalmente applicati alla dimostrazione di teoremi matematici, con scarsa applicazione alla verifica dei requisiti ingegneristici
• Metodi di valutazione degli LLM: dipendono da controlli manuali o metodi euristici, mancano di verifica logica rigorosa
• Ricerca sull'autoformalizzazione: principalmente focalizzata sulla costruzione di dataset e l'addestramento di modelli, con scarsa attenzione alle applicazioni ingegneristiche pratiche

4. Motivazione della Ricerca

Questo articolo propone l'applicazione di tecniche di autoformalizzazione a un nuovo scenario: la verifica degli output generati da LLM. Convertendo sia i requisiti in linguaggio naturale che gli output generati da LLM in rappresentazioni di logica formale (Lean 4), si utilizza un dimostratore di teoremi per verificare l'equivalenza logica.

Contributi Fondamentali

1. Propone la prima pipeline di autoformalizzazione specificamente progettata per la verifica degli output generati da LLM: converte i requisiti in linguaggio naturale e gli output degli LLM in rappresentazioni formalizzate in Lean 4, verificando la coerenza logica attraverso la dimostrazione di equivalenza bicondizioanale
2. Valida due scenari di applicazione concreti:
   • Identifica l'equivalenza logica di requisiti in linguaggio naturale con formulazioni diverse
   • Rileva incoerenze logiche tra gli output generati da LLM e i requisiti originali
3. Identifica sfide tecniche critiche:
   • La necessità e la difficoltà di automazione del grounding delle variabili
   • L'impatto della non-determinismo degli LLM sulla formalizzazione
   • La gestione dell'ambiguità del linguaggio naturale
4. Propone direzioni di ricerca future: pone le basi per la costruzione di un framework affidabile per la verifica degli output degli LLM

Spiegazione Dettagliata del Metodo

Definizione del Compito

Input:

• Una coppia di affermazioni la cui relazione logica deve essere verificata (S₁, S₂), che possono essere:
  • Due requisiti in linguaggio naturale
  • Un requisito in linguaggio naturale e uno scenario Gherkin generato da LLM

Output:

• Giudizio di equivalenza logica: equivalente (è possibile provare S₁ ↔ S₂) o non equivalente (la prova fallisce)

Vincoli:

• Le affermazioni devono essere formalizzabili come logica proposizionale
• Sono necessarie informazioni sul contesto del sistema per il grounding delle variabili

Architettura del Modello

La pipeline complessiva comprende quattro passaggi chiave (come mostrato nella Figura 9):

Passaggio 1: Autoformalizzazione

Utilizza DeepSeek-Prover-v2 (modello 7B) per convertire affermazioni in linguaggio naturale in proposizioni Lean 4:

-- Esempio: formalizzazione del requisito R1
variable (vehicle_speed_avg : ℝ)
variable (calibratable_speed : ℝ)
variable (seatbelt_active : Bool)
variable (initiate_chime : Bool)

def seatbelt_chime_condition : Prop :=
  (vehicle_speed_avg ≥ calibratable_speed ∨ ¬seatbelt_active) → initiate_chime

Modello di Prompt (vedi Appendice A.1):

• Richiede esplicitamente la generazione di istruzioni def in Lean 4
• Specifica l'uso della logica proposizionale (tipo Prop)
• Richiede la rappresentazione delle condizioni come implicazioni (A ∧ B → C)

Passaggio 2: Grounding delle Variabili

Implementazione Attuale: Identificazione manuale e unificazione di variabili che si riferiscono allo stesso concetto in diverse formalizzazioni

Esempio di Problema:

• vehicle_speed_avg in R1 e mean_vehicle_speed in R2 si riferiscono alla stessa grandezza fisica
• È necessario comunicare esplicitamente al compilatore Lean questa equivalenza

-- Esempio di grounding manuale
(h_speed : vehicle_speed_avg = mean_vehicle_speed)
(h_belt : seatbelt_active = seatbelt_plugged_in)

Passaggio 3: Costruzione del Teorema di Equivalenza Bicondizioanale

Costruisce un teorema formalizzato per verificare l'equivalenza logica:

theorem req1_eq_req2 
  (h_grounding : <ipotesi di grounding delle variabili>) :
  (Proposition_A) ↔ (Proposition_B) := by
  <processo di dimostrazione>

Passaggio 4: Dimostrazione Automatica di Teoremi

Utilizza nuovamente DeepSeek-Prover-v2 per generare il codice di prova in Lean:

• Dimostrazione Riuscita → Le due affermazioni sono logicamente equivalenti
• Dimostrazione Fallita → Esiste un'incoerenza logica

Punti di Innovazione Tecnica

1. Innovazione nell'Applicazione Interdisciplinare: Prima applicazione di tecniche di autoformalizzazione dal campo della dimostrazione di teoremi matematici alla verifica dei requisiti dell'ingegneria del software
2. Utilizzo Doppio di LLM:
   • Primo livello: traduzione di formalizzazione (NL → Lean)
   • Secondo livello: dimostrazione di teoremi (verifica di equivalenza)
3. Meccanismo di Verifica Basato sul Fallimento: Utilizza il fallimento del dimostratore di teoremi come indicatore di incoerenza logica, un metodo di verifica negativa innovativo
4. Identificazione del Grounding delle Variabili: Identifica esplicitamente il grounding delle variabili come passaggio indispensabile nella pipeline di autoformalizzazione, aspetto non sufficientemente enfatizzato nella ricerca precedente

Configurazione Sperimentale

Dataset

Esperimento 1: Verifica dell'Equivalenza dei Requisiti

• R1: "If Vehicle Speed Average Driven ≥ CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is inactive then initiate SeatBelt Chime"
• R2: "If mean vehicle speed is greater than CALIBRATABLE Seatbelt Reminder Speed OR Seatbelt is not plugged in then initiate chime for seatbelt"

Esperimento 2: Verifica dell'Output di LLM

• R3: "When Front Passenger Seat Belt Status changes to 'Fastened' then the Front Passenger Seat Belt Reminder Indication On shall be set to FALSE."
• G3: Scenario Gherkin generato da LLM (contiene 4 righe di esempio, introduce variabili aggiuntive come seat_occupancy)

Metriche di Valutazione

Metriche Qualitative:

• Successo/Fallimento della compilazione in Lean 4
• Successo/Fallimento della dimostrazione del teorema

Standard di Verifica:

• Equivalenza Logica: Il teorema PA ↔ PB è dimostrabile
• Incoerenza Logica: La dimostrazione del teorema fallisce o il codice Lean non può essere compilato

Dettagli di Implementazione

Scelta del Modello:

• DeepSeek-Prover-v2 (7B)
• Motivi della scelta:
  1. Addestrato su Lean 4
  2. Possiede capacità di comprensione del linguaggio naturale
  3. Impiega una strategia di decomposizione dei sotto-obiettivi

Linguaggio di Formalizzazione: Lean 4

• Potente capacità di dimostrazione di teoremi
• Espressione logica precisa
• Compatibilità con DeepSeek-Prover-v2

Intervento Manuale:

• Il passaggio di grounding delle variabili è completamente manuale
• La verifica dell'output di formalizzazione dipende dal compilatore Lean

Risultati Sperimentali

Risultati Principali

Esperimento 1: Verifica dell'Equivalenza dei Requisiti (Caso di Successo)

Output di Formalizzazione:

• R1 e R2 sono stati convertiti con successo in proposizioni Lean (Figure 3, 4)
• La mappatura delle variabili è stata stabilita manualmente:
  • vehicle_speed_avg ≡ mean_vehicle_speed
  • seatbelt_active ≡ seatbelt_plugged_in

Risultati di Verifica (Figura 5):

• ✅ Compilazione Lean riuscita
• ✅ Dimostrazione del teorema req1_eq_req2 riuscita
• Conclusione: R1 e R2 sono logicamente equivalenti

Significato: Dimostra che la pipeline può identificare requisiti semanticamente identici ma con formulazioni diverse, utile per il controllo della coerenza dei requisiti.

Esperimento 2: Verifica dell'Output di LLM (Caso di Fallimento)

Output di Formalizzazione:

• R3: Proposizione semplice, contiene solo la condizione di cambio dello stato della cintura di sicurezza (Figura 6)
• G3: Proposizione complessa, contiene variabili aggiuntive (seat_occupancy, initial_seatbelt_status) (Figura 7)

Scoperte Chiave:

• G3 introduce variabili non menzionate in R3
• La struttura logica è più complessa (contiene 4 scenari di esempio)

Risultati di Verifica (Figura 8):

• ❌ Compilazione del codice Lean fallita o dimostrazione fallita
• Conclusione: G3 è logicamente incoerente con R3

Significato: Rileva con successo il problema della "sovra-generazione" negli output degli LLM — l'aggiunta di condizioni vincolanti non presenti nei requisiti originali.

Analisi dei Casi

Caso: Problema di Ambiguità (R4)

Requisito:

"When the seatbelt is Unfastened and the vehicle is in motion then the Front Passenger Seat Belt Reminder Indication On shall be set to TRUE."

Problema: L'ambiguità nella formalizzazione di "vehicle in motion"

Due Possibili Formalizzazioni (Figura 10):

1. pass@1: Variabile booleana vehicle_in_motion : Bool
2. pass@2: Variabile numerica vehicle_speed > 0

Analisi:

• Entrambe le formalizzazioni possono essere semanticamente corrette nel sistema
• Ma sono non equivalenti nella logica formale (tipi diversi)
• Evidenzia l'impatto dell'ambiguità del linguaggio naturale sulla formalizzazione

Scoperte Sperimentali

1. La Formalizzazione Dipende dall'Interpretabilità: La non-determinismo degli LLM porta a possibili diverse formalizzazioni dello stesso requisito, tutte potenzialmente "ragionevoli"
2. Il Grounding delle Variabili è un Collo di Bottiglia:
   • Passaggio più dispendioso in termini di tempo
   • Richiede conoscenza del dominio del sistema
   • Attualmente realizzabile solo manualmente
3. Il Contesto del Sistema è Critico: L'assenza di definizioni esplicite del sistema (come dizionari di dati) porta a incoerenze nella formalizzazione
4. La Verifica Negativa è Efficace: Il fallimento della dimostrazione può indicare efficacemente l'incoerenza logica

Lavori Correlati

Costruzione di Dataset per l'Autoformalizzazione

• ProofNet: Autoformalizzazione matematica a livello universitario
• MiniF2F: Benchmark matematico a livello olimpico
• Dataset Multilingue: Addestramento combinato su Lean, Isabelle, Coq migliora le prestazioni

Strategie di Addestramento degli LLM

• Metodo "Bozza-Schizzo-Prova" (Jiang et al.): Genera contorni di prova per guidare la formalizzazione
• Decomposizione dei Sotto-obiettivi: Strategia di ricerca ricorsiva adottata da DeepSeek-Prover
• Apprendimento per Rinforzo: Migliora il tasso di successo della dimostrazione di teoremi

Affrontare la Non-Determinismo

• Framework di Equivalenza Simbolica: Gestisce le differenze tra pass@1 e pass@k
• Metodo RAG: Recupera definizioni formali precise per fornire contesto

Estensione dei Campi di Applicazione

• Risoluzione di Problemi Matematici: Matematica da scuola superiore a università
• Verifica del Codice: Verifica della correttezza dei programmi
• Biomedica: Verifica dei fatti

Contributo di questo Articolo: Prima applicazione dell'autoformalizzazione alla verifica dei requisiti ingegneristici e alla verifica degli output degli LLM, aprendo una nuova direzione di ricerca.

Conclusioni e Discussione

Conclusioni Principali

1. Verifica della Fattibilità: La pipeline di autoformalizzazione può verificare efficacemente la coerenza logica tra gli output generati da LLM e i requisiti originali
2. Valore Doppio dell'Applicazione:
   • Controllo della coerenza dei requisiti (identificazione di requisiti equivalenti)
   • Controllo della qualità degli output degli LLM (rilevamento di errori logici)
3. Prova di Concetto: Sebbene il campione sia limitato, dimostra con successo il potenziale dell'applicazione di tecniche di dimostrazione di teoremi all'ingegneria del software

Limitazioni

1. Limitazioni di Scala:
   • Testati solo 3 coppie di requisiti
   • Mancanza di valutazione su larga scala
   • Nessuna analisi di significatività statistica
2. Dipendenza Manuale:
   • Grounding delle variabili completamente manuale
   • Dispendioso in termini di tempo e soggetto a errori
   • Limita la scalabilità
3. Limitazioni del Modello:
   • Utilizzo di modello 7B (risorse limitate)
   • Modelli più grandi (671B) potrebbero avere prestazioni migliori
   • La qualità della formalizzazione dipende dalle capacità del modello
4. Ambiguità Non Risolta:
   • Ambiguità intrinseca del linguaggio naturale
   • Mancanza di supporto di ontologie di sistema
   • Possibilità di produrre multiple formalizzazioni "corrette" ma non equivalenti
5. Specificità del Dominio:
   • Gli esperimenti sono limitati ai requisiti di sicurezza automobilistica
   • La capacità di generalizzazione è sconosciuta

Direzioni Future

L'articolo propone tre questioni di ricerca chiave (RQ):

RQ1: Metodo di Formalizzazione Ottimale

• Esplorare strategie k-pass (generare multiple formalizzazioni, selezionare la più probabile)
• Confrontare l'accuratezza della conversione singola rispetto al campionamento multiplo

RQ2: Automazione del Grounding delle Variabili

• Metodo 1: Formalizzazione contestuale singola (elaborare tutte le affermazioni in una singola chiamata)
• Metodo 2: Grounding basato sulla similarità (utilizzare embedding per abbinare l'ontologia del sistema)
• Sfida: Come verificare la correttezza stessa delle ipotesi di grounding dell'LLM

RQ3: Verifica degli LLM in Sistemi Vincolati

• Costruire grafi di conoscenza delle azioni del sistema
• Sviluppare meccanismi di attraversamento degli LLM
• Utilizzare l'autoformalizzazione per garantire la coerenza logica degli output
• Scenari di Applicazione: Case intelligenti, assistenti in auto e altri sistemi con spazio di azioni limitato

Altre Direzioni:

• Sviluppare tecniche automatizzate di normalizzazione delle variabili
• Integrare ontologie specifiche del dominio (come dizionari di dati dei sistemi automobilistici)
• Estendere a rappresentazioni logiche più complesse (come logica temporale)

Valutazione Approfondita

Punti di Forza

1. Definizione del Problema Innovativa:
   • Prima applicazione sistematica dell'autoformalizzazione alla verifica degli output degli LLM
   • Risolve un vero dolore nella pratica ingegneristicamente
   • Apre una nuova direzione di ricerca
2. Metodologia Chiara:
   • Design della pipeline semplice e comprensibile
   • Utilizza strumenti consolidati (Lean 4, DeepSeek-Prover)
   • Forte riproducibilità
3. Identificazione Profonda dei Problemi:
   • Evidenzia chiaramente la criticità del grounding delle variabili
   • Analizza profondamente il problema dell'ambiguità
   • Discute onestamente l'impatto della non-determinismo degli LLM
4. Valore Pratico Elevato:
   • Mirato ai settori critici per la sicurezza (ingegneria automobilistica)
   • Applicabile direttamente ai processi di ingegneria dei requisiti
   • Contribuisce ad aumentare l'affidabilità delle applicazioni degli LLM
5. Qualità Eccellente della Scrittura:
   • Struttura chiara, logica rigorosa
   • Fornisce modelli di prompt dettagliati (Appendice)
   • Figure ricche, facili da comprendere

Carenze

1. Scala Sperimentale Gravemente Insufficiente:
   • Solo 3 campioni: impossibile trarre conclusioni statistiche
   • Mancanza di test su requisiti di diversi domini e complessità
   • Nessuna valutazione delle prestazioni su dataset più grandi
   • Raccomandazione: Necessari almeno 50-100 coppie di requisiti per una valutazione adeguata
2. Mancanza di Valutazione Quantitativa:
   • Nessuna metrica di precisione, richiamo, ecc.
   • Nessun rapporto sul tasso di successo della formalizzazione
   • Mancanza di confronto con la verifica manuale
   • Raccomandazione: Costruire dataset annotati, calcolare metriche di precisione
3. Troppo Intervento Manuale:
   • Grounding delle variabili completamente manuale, indebolisce la dichiarazione di automazione
   • Nessuna implementazione concreta di soluzioni automatizzate
   • Scalabilità discutibile
   • Raccomandazione: Implementare almeno un prototipo di sistema di grounding automatizzato
4. Scelta del Modello Limitata:
   • Solo modello 7B utilizzato a causa di limitazioni di risorse
   • Nessuna esplorazione di modelli 671B o alternative
   • Mancanza di analisi dell'impatto della dimensione del modello sui risultati
   • Raccomandazione: Confrontare almeno diversi modelli su un piccolo campione
5. Mancanza di Analisi dei Casi di Fallimento:
   • Nessuna analisi dettagliata delle cause del fallimento della dimostrazione di teoremi
   • Nessuna distinzione tra errori di formalizzazione vs. vera incoerenza logica
   • Mancanza di analisi di falsi positivi/falsi negativi
   • Raccomandazione: Stabilire un sistema di classificazione degli errori
6. Criteri di Valutazione Singoli:
   • Dipende solo dal successo/fallimento della compilazione Lean
   • Non considera i casi parzialmente corretti
   • Mancanza di analisi fine-grained dei tipi di errore
7. Capacità di Generalizzazione Sconosciuta:
   • Testato solo su requisiti di sicurezza automobilistica
   • Nessuna verifica dell'applicabilità in altri domini (medicina, finanza, ecc.)
   • La specificità degli scenari Gherkin potrebbe limitare l'universalità del metodo

Impatto

Contributo al Campo:

• ⭐⭐⭐⭐ Contributo Concettuale Elevato: Propone una nuova direzione di ricerca e scenario di applicazione
• ⭐⭐ Contributo Tecnico Moderato: Principalmente combinazione di tecniche esistenti
• ⭐⭐⭐ Valore Pratico Relativamente Elevato: Risolve problemi reali nella pratica ingegneristicamente

Valore Pratico:

• Breve Termine: Fornisce ai tecnici dei requisiti idee per la verifica
• Medio Termine: Potrebbe catalizzare lo sviluppo di strumenti specializzati di verifica dei requisiti
• Lungo Termine: Potrebbe diventare un processo standard di garanzia della qualità per le applicazioni degli LLM

Riproducibilità:

• ✅ Utilizza strumenti open source (Lean 4, DeepSeek-Prover)
• ✅ Fornisce modelli di prompt dettagliati
• ❌ Nessun rilascio di codice o dati
• ❌ I passaggi manuali sono difficili da riprodurre
• Valutazione: ⭐⭐⭐ (Moderata)

Impatto Previsto:

• Potrebbe stimolare più ricerca sulla verifica formale degli output degli LLM
• Potrebbe promuovere l'integrazione tra ingegneria dei requisiti e metodi formali
• Il problema del grounding delle variabili potrebbe diventare un nuovo punto focale della ricerca

Scenari di Applicabilità

Altamente Applicabile:

• ✅ Verifica dei requisiti di sistemi critici per la sicurezza (automotive, aerospaziale, medico)
• ✅ Controllo della coerenza e deduplicazione dei requisiti
• ✅ Controllo della qualità dei casi di test generati da LLM

Moderatamente Applicabile:

• ⚠️ Verifica di logica aziendale complessa (richiede capacità di formalizzazione estesa)
• ⚠️ Requisiti multimodali (come requisiti contenenti diagrammi)
• ⚠️ Sistemi in tempo reale (richiede estensione a logica temporale)

Non Applicabile:

• ❌ Testo in linguaggio naturale altamente ambiguo
• ❌ Scenari senza definizioni di sistema chiare
• ❌ Scenari che richiedono risposte in tempo reale (i passaggi manuali attuali sono troppo lenti)

Suggerimenti per il Miglioramento

1. Immediatamente Realizzabile:
   • Estendere ad almeno 50 coppie di requisiti
   • Implementare un prototipo di base di grounding automatizzato delle variabili
   • Stabilire un sistema di classificazione degli errori
2. Miglioramenti a Breve Termine:
   • Confrontare modelli di diverse dimensioni
   • Introdurre metriche di valutazione quantitativa
   • Testare su più domini
3. Obiettivi a Lungo Termine:
   • Pipeline completamente automatizzata
   • Integrazione di grafi di conoscenza specifici del dominio
   • Supporto per logica temporale e vincoli complessi

Bibliografia (Letteratura Chiave)

1. Weng et al. (2025): Autoformalization in the era of large language models: A survey - Letteratura di rassegna
2. Wu et al. (2022): Autoformalization with large language models - Lavoro fondamentale sull'autoformalizzazione
3. Ren et al. (2025): DeepSeek-Prover-v2 - Modello principale utilizzato in questo articolo
4. Jiang et al. (2022): Draft, sketch, and prove - Metodo di decomposizione dei sotto-obiettivi
5. de Moura & Ullrich (2021): The Lean 4 theorem prover - Linguaggio di formalizzazione

Valutazione Complessiva: Questo è un articolo di verifica di concetto di natura esplorativa che propone una nuova direzione di ricerca di valore, ma con verifica sperimentale gravemente insufficiente. Come preprint e ricerca preliminare, identifica con successo problemi chiave e fornisce un percorso tecnico fattibile, ma rimane a grande distanza da una soluzione matura. Il valore principale dell'articolo risiede nella definizione del problema e nella guida direzionale, piuttosto che nel breakthrough tecnico. Si raccomanda che i lavori successivi si concentrino sulla risoluzione dell'automazione del grounding delle variabili e sulla valutazione su larga scala.