Towards Neuro-symbolic Causal Rule Synthesis, Verification, and Evaluation Grounded in Legal and Safety Principles

1. Enunciato del Problema

Il documento affronta limitazioni critiche nei sistemi basati su regole utilizzati in domini critici per la sicurezza (ad esempio, guida autonoma, controllo industriale):

• Fragilità e Scalabilità: I sistemi basati su regole tradizionali faticano nella manutenzione. Minori cambiamenti nei requisiti spesso innescano revisioni a cascata attraverso regole interdipendenti, creando un "collo di bottiglia nell'acquisizione della conoscenza".
• Specificazione Errata degli Obiettivi: I sistemi di IA spesso ottimizzano per obiettivi ristretti e letterali (hacking della ricompensa) piuttosto che per la vera intenzione dei progettisti umani. Ciò accade perché gli obiettivi umani sono spesso vaghi, dipendenti dal contesto e informali, mentre l'IA richiede specifiche precise e formali.
• Mancanza di Tracciabilità: I metodi esistenti spesso mancano di un collegamento chiaro e tracciabile tra principi umani di alto livello (legali/sicurezza) e le regole logiche di basso livello che governano il comportamento del sistema.

La sfida centrale è creare un sistema in grado di sintetizzare, verificare e valutare in modo incrementale regole formali derivate da obiettivi e principi in linguaggio naturale, assicurando che siano minimali, necessarie, sufficienti e sicure.

2. Metodologia

Gli autori propongono un'estensione di un precedente Framework Causale Neuro-Simbolico (NeSy). La nuova architettura introduce un Livello di Sintesi e Verifica Meta-Livello che si colloca sopra il ciclo di feedback standard MAPE-K (Monitor-Analyze-Plan-Execute).

A. L'Architettura Core

Il sistema integra tre spazi di rappresentazione:

1. Alberi di Abduzione Simbolica (SAT): Logica del primo ordine (FOL) per codificare la conoscenza del dominio e spiegare le violazioni.
2. Modelli Causali Strutturali (SCM): Per rappresentare le dipendenze e supportare il ragionamento controfattuale.
3. Apprendimento per Rinforzo Profondo (DRL): Per il processo decisionale operativo.

Il nuovo Livello di Sintesi e Verifica agisce come un meta-ciclo chiuso, aggiornando la teoria FOL governante del sistema in base all'input umano e al rilevamento di anomalie.

B. La Pipeline di Sintesi (Sintetizzatore di Obiettivi/Regole)

Questa pipeline utilizza Modelli Linguistici di Grande Formato (LLM) per trasformare obiettivi in linguaggio naturale in regole formali attraverso quattro passaggi:

1. Decomposizione in Cause: L'LLM scompone un obiettivo di alto livello (effetto) in cause candidate (condizioni/comportamenti) richieste per raggiungerlo, vincolato da principi di sicurezza e legali.
2. Consolidamento Semantico: L'LLM identifica e fonde cause sovrapposte o ridondanti per creare un insieme unico di condizioni, riducendo l'ambiguità.
3. Traduzione Simbolica: Le cause in linguaggio naturale consolidate vengono tradotte in predicati e regole di Logica del Primo Ordine (FOL). L'LLM fornisce spiegazioni per queste traduzioni per garantire l'allineamento semantico.
4. Valutazione di Necessità e Sufficienza: Il sistema analizza le combinazioni di cause per determinare:
   • Necessità Individuale: Una causa specifica è essenziale da sola?
   • Insiemi Necessari Minimi: Qual è il più piccolo insieme di cause richiesto per rendere l'effetto impossibile se rimosso?
   • Insiemi Sufficianti Minimi: Quali combinazioni di cause garantiscono che l'effetto si verifichi?

C. La Pipeline di Verifica (Motore di Verifica delle Regole)

Prima di essere integrate nella base di conoscenza, le regole subiscono una verifica automatizzata in tre fasi:

1. Validazione Sintattica e dello Schema: Assicura che le regole conformino al linguaggio logico e alle ontologie del dominio.
2. Analisi di Coerenza Logica: Controlla le contraddizioni rispetto alla base di conoscenza FOL esistente.
3. Verifica di Sicurezza e Invarianti: Verifica formalmente (utilizzando solver come Z3) che le regole preservino proprietà critiche del sistema (ad esempio, evitare collisioni).

Solo le regole che superano tutte le fasi vengono confermate nella base di conoscenza, guidando l'adattamento futuro.

3. Contributi Chiave

• Ciclo di Sintesi a Meta-Livello: Un'architettura innovativa che tratta la manutenzione delle regole come un processo incrementale e tracciabile, spostandosi da basi di regole monolitiche verso insiemi di regole modulari e collegati agli obiettivi.
• Abduzione Causale Guidata da LLM: Dimostrazione di come gli LLM possano essere vincolati per eseguire ragionamento abduttivo strutturato (generazione di cause da effetti) e ragionamento deduttivo (valutazione di necessità/sufficienza) fondato su specifici domini legali e di sicurezza.
• Formalizzazione degli Insiemi "Necessari e Sufficienti": Un metodo sistematico per derivare insiemi di regole minimi che garantiscono gli obiettivi di sicurezza, affrontando il problema della sovra-specificazione o sotto-specificazione negli obiettivi dell'IA.
• Tracciabilità: Ogni regola sintetizzata è esplicitamente collegata al suo obiettivo umano originario e al principio legale, migliorando l'auditabilità e la spiegabilità.

4. Risultati (Dimostrazione di Concetto)

Gli autori hanno valutato l'approccio utilizzando un'implementazione di dimostrazione di concetto in due scenari di guida autonoma, impiegando GPT-4o Mini di OpenAI e un set curato di regolamenti stradali tedeschi e principi di sicurezza fisica.

• Scenario 1: Immissione nel Traffico Pesante
  • Il sistema ha scomposto con successo l'obiettivo in 4 cause consolidate uniche.
  • Ha identificato che, sebbene alcune cause non fossero individualmente necessarie, erano essenziali all'interno di specifici insiemi necessari minimi.
  • Ha derivato un singolo Insieme Sufficiante Minimo contenente tutte e quattro le cause, garantendo un'immissione sicura.
• Scenario 2: Mantenimento di Velocità Costante in Autostrada
  • Il sistema ha identificato 6 cause uniche, restringendole a 3 condizioni individualmente necessarie (controllo, limiti di velocità, attrito).
  • Ha generato due distinti Insiemi Sufficianti Minimi, mostrando che diverse combinazioni di condizioni (ad esempio, presenza di ostacoli vs cambiamenti nel traffico) potevano soddisfare l'obiettivo.
• Traduzione Simbolica: L'LLM ha mappato con successo condizioni complesse in linguaggio naturale (ad esempio, "distanza sufficiente") in regole FOL precise (ad esempio, ∀x(sd_front(x) ∧ sd_rear(x) ← ¬dense(x))).

Esito: La pipeline ha derivato con successo insiemi di regole minimi, necessari e sufficienti da obiettivi di alto livello, formalizzandoli come vincoli logici senza allucinare comportamenti insicuri.

5. Significato e Lavori Futuri

• Colmare il Divario: Il lavoro colma il divario tra l'intento umano vago e la verifica formale rigorosa, offrendo un percorso per mitigare l'hacking della ricompensa e la specificazione errata degli obiettivi nell'IA.
• Scalabilità: Localizzando i cambiamenti delle regole in moduli specifici collegati agli obiettivi, l'approccio riduce l'onere di manutenzione e il rischio di guasti a cascata in grandi insiemi di regole.
• Assicurazione di Sicurezza: L'integrazione di un motore di verifica garantisce che solo regole logicamente coerenti e che preservano la sicurezza vengano distribuite, cruciale per sistemi critici per la sicurezza.

Limitazioni e Direzioni Future:

• L'approccio attuale si basa su un set predefinito di regolamenti; i lavori futuri mirano ad espandere la copertura del dominio.
• L'LLM agisce come una "scatola nera" e la sensibilità ai prompt rimane una sfida.
• I piani futuri includono l'integrazione di solver automatizzati per rilevare conflitti tra regole nuove ed esistenti e l'incorporazione di ragionamento probabilistico per gestire l'incertezza in modo più robusto.

In conclusione, questo documento presenta un framework robusto per la Sintesi di Regole Causali Neuro-Simboliche, dimostrando che combinare LLM con logica formale e ragionamento causale può creare sistemi di IA adattivi, spiegabili e sicuri fondati su principi legali e di sicurezza umani.