Sintesi Tecnica: VASO – Skill Auto-evolutive Formalmente Verificabili per Agenti di IA Fisica

Problema

Le skill riutilizzabili per robot fungono da interfaccia tra i modelli di fondazione e il controllo fisico, permettendo agli agenti incorporati (embodied agents) di eseguire compiti a lungo termine sotto vincoli di sicurezza. Sebbene i modelli di fondazione abbiano ridotto il costo di generazione di queste skill tramite il linguaggio naturale, non hanno risolto il problema dell'assurance delle skill (garanzia di correttezza). Le metodologie di auto-evoluzione esistenti si affidano a segnali di feedback "morbidi" — come gli esiti dell'esecuzione, i test unitari, le ricompense dell'ambiente o l'autocritica degli LLM — che forniscono solo una prova a livello di traccia, dimostrando che una skill ha funzionato su esecuzioni campionate, ma senza garantire che i piani indotti dalla skill soddisfino contratti di sicurezza temporale in condizioni non testate. Nella robotica, una singola violazione di sicurezza rara ma grave (ad esempio, un robot a terra che si muove dopo aver rilevato una persona) è inaccettabile, eppure il feedback morbido spesso non riesce a rilevare questi casi limite (edge cases).

La sfida centrale consiste nel chiudere il ciclo tra la verifica formale e l'evoluzione delle skill senza limitarsi a filtrare i piani non sicuri o a perfezionare i pesi del modello. È necessaria una rappresentazione in cui i controesempi formali possano aggiornare direttamente i contratti delle skill riutilizzabili, garantendo che i miglioramenti siano ispezionabili, riutilizzabili e verificabili.

Metodologia: Framework VASO

Gli autori propongono VASO (Verification-Guided Automated Skill Optimization), un framework a ciclo chiuso per l'auto-evoluzione dei contratti di skill per robot generati da LLM. VASO opera trattando le skill come contratti semantici che accoppiano un'interfaccia formale con un'interfaccia rivolta al pianificatore (planner).

1. Rappresentazione della Skill Verificabile

Una skill $sk$ è definita come una tupla $(G, \psi_{sk}, C_{sk})$:

• $G$ (Specifiche Globali): Un insieme di formule LTL che rappresentano i vincoli di sicurezza che devono sempre essere rispettati.
• $\psi_{sk}$ (Regola Locale): Una formula LTL che definisce l'intento specifico o l'obiettivo della skill.
• $C_{sk}$ (Contratto Semantico): Il componente centrale composto da:
  • $L_{sk}$ (Funzione di Etichettatura Allineata alle Proposizioni): Una funzione che mappa gli stati del robot a basso livello, le osservazioni e i comandi di controllo in proposizioni logiche atomiche. Questo colma il divario tra l'esecuzione fisica e il model checking simbolico.
  • $C^p_{sk}$ (Template di Piano Basato sul Testo): Un prior comportamentale che guida il pianificatore nella generazione di comandi eseguibili (ad esempio, chiamate API o traiettorie).

2. Ciclo di Verifica a Due Livelli

VASO impiega un processo di verifica gerarchico per raffinare le skill:

• Verifica a Livello di Skill (Controllo di Fattibilità): Prima di campionare i piani, il framework controlla se la regola locale $\psi_{sk}$ è logicamente coerente con le specifiche globali $G$. Viene costruito un sistema di transizione universale per verificare la soddisfacibilità. Se la regola locale contraddice la sicurezza globale (ad esempio, una regola che ordina il movimento quando viene rilevata una persona), la skill viene rifiutata e il modello di fondazione viene interrogato per raffinare la regola locale.
• Verifica a Livello di Piano (Controllo Comportamentale): Una volta ottenuta una skill fattibile, un pianificatore genera un piano eseguibile $\pi$. Questo piano viene compilato in un sistema di transizione simbolica (automa) utilizzando la funzione di etichettatura $L_{sk}$. Un model checker (NuSMV) verifica il piano rispetto a $G \land \psi_{sk}$.

3. Ottimizzazione tramite Gradienti Testuali

Quando la verifica fallisce, il model checker restituisce un traccia di controesempio. VASO converte questa traccia in un gradiente testuale (ad esempio, "viola la specifica: $G(\text{persona\_rilevata} \to X \text{ fermati})$"). Questo feedback testuale viene fornito al modello di fondazione per aggiornare il contratto semantico $C_{sk}$ e la regola locale $\psi_{sk}$.

• Vincolo Chiave: I pesi del modello di fondazione rimangono congelati. L'ottimizzazione avviene interamente a livello di prompt/contratto, raffinando l'artefatto della skill riutilizzabile piuttosto che il tuning dei parametri del modello o di un singolo prompt di task.
• Processo: Il ciclo alterna la generazione in avanti (Contratto $\to$ Piano $\to$ Automa) e il raffinamento all'indietro (Automa $\to$ Gradiente Testuale $\to$ Contratto Aggiornato).

Contributi Chiave

1. Rappresentazione delle Skill Auto-evolutive Verificabili: Il documento introduce una struttura di skill che collega esplicitamente le specifiche di logica temporale, la semantica del robot allineata alle proposizioni e i template rivolti al pianificatore. Ciò consente alle skill generate da LLM di essere utilizzate per la pianificazione pur rimanendo esposte alla verifica formale.
2. Controesempi Formali come Feedback di Ottimizzazione: Gli autori sviluppano un ciclo di verifica a due livelli in cui le tracce di controesempio vengono convertite in gradienti testuali. Ciò consente il raffinamento del contratto della skill riutilizzabile stessa, invece di limitarsi a rifiutare un piano specifico o a fare il tuning di un prompt.
3. Validazione su Agenti Fisici: Il framework è validato su piattaforme robotiche reali (Clearpath Jackal e quadricottero PX4), dimostrando che le skill ottimizzate possono raggiungere un'elevata conformità alle specifiche formali senza il fine-tuning del modello di fondazione sottostante.

Risultati Empirici

Il framework è stato valutato su 11 specifiche di logica temporale attraverso 400 piani generati su due piattaforme robotiche.

• Conformità: VASO ha raggiunto una conformità alle specifiche formali del 97,2% utilizzando meno di 100 campioni di ottimizzazione (meno di 20 minuti per skill).
• Confronto: Ha superato i baseline zero-shot, i metodi di ottimizzazione del prompt (come LAD-VF) e gli approcci basati sul fine-tuning (come RLVF). Notevolmente, VASO ha raggiunto punteggi di sicurezza più elevati rispetto ai metodi di fine-tuning pur richiedendo solo una frazione del costo e del tempo di addestramento.
• Generalizzazione: Le skill ottimizzate hanno dimostrato una forte capacità di generalizzazione a prompt di task non visti all'interno della stessa famiglia di task, mantenendo alti tassi di sicurezza e completamento del compito senza ulteriore raffinamento.
• Allineamento Automatico: Lo studio ha mostrato che le funzioni di etichettatura allineate alle proposizioni generate automaticamente hanno performato allo stesso livello delle mappature create manualmente, eliminando la necessità di competenza tecnica manuale nella definizione delle astrazioni simboliche.

Significato e Rivendicazioni

Il documento sostiene di essere il primo framework capace di chiudere il ciclo tra la verifica formale e l'auto-evoluzione delle skill generate da LLM per agenti di IA fisica.

• Cambio di Paradigma: A differenza dei normali pipeline di pianificazione verificata che utilizzano la verifica meramente come filtro pass/fail per piani singoli, VASO utilizza la ragione del rifiuto (il controesempio) per migliorare la fonte del piano (la skill riutilizzabile).
• Efficienza e Sicurezza: Ottimizzando il contratto della skill anziché i pesi del modello, VASO fornisce un meccanismo per generare comportamenti più sicuri e affidabili che sono ispezionabili e riutilizzabili in diversi task, affrontando il collo di bottiglia critico dell'assurance delle skill nella IA fisica.
• Limitazioni: Gli autori riconoscono che le garanzie formali sono condizionate sulla correttezza della funzione di etichettatura allineata alle proposizioni generata dall'IA. Gli errori nella mappatura della dinamica a basso livello verso le proposizioni simboliche potrebbero portare a risultati di verifica spurii, sebbene i dati empirici suggeriscano che ciò accada raramente (degradazione della sicurezza <1%). L'attuale framework assume inoltre l'esecuzione sequenziale, non concorrente.