Framework Neurosimbiotico Traduce il Linguaggio Naturale in Logica Temporale

I ricercatori hanno introdotto NeuroNL2LTL, un'architettura neurosimbiotica che combina traduzione appresa con verifica formale per convertire il linguaggio naturale in Logica Temporale Lineare (LTL). Il sistema instrada la traduzione attraverso una rappresentazione intermedia che preserva la struttura durante la mappatura in LTL. Le specifiche generate vengono sottoposte a controlli di soddisfacibilità e non trivialità, con un meccanismo di riparazione a modifiche minime che corregge output quasi corretti. L'innovazione chiave è l'addestramento con verificatore nel ciclo, dove i risultati della verifica fungono da segnali di ricompensa per l'apprendimento per rinforzo, consentendo ai componenti neurali di ottimizzare per la correttezza formale. Questo approccio affronta la sfida di tradurre il linguaggio naturale in logiche formali, che tipicamente richiede competenze specialistiche e limita la portata della verifica formale nello sviluppo critico per la sicurezza. I metodi basati su template sacrificano l'espressività per l'affidabilità, mentre i metodi neurali mancano di garanzie di correttezza. NeuroNL2LTL mira a colmare questo divario garantendo sia fluidità che correttezza formale.