Certifying Plans under Model Mismatch: A Trilemma for Reachability from Scarce Data

Sintesi Tecnica: Certificazione di Piani sotto Mismatch del Modello: Un Trilemma per la Raggiungibilità da Dati Scarsi

Enunciato del Problema
Il documento affronta la sfida di certificare sequenze di controllo fissate (ad esempio, chunk di azioni da policy apprese come Diffusion Policy o $\pi_0$) per il dispiegamento su sistemi robotici reali dove la dinamica differisce dal modello di simulazione nominale. La difficoltà principale risiede nel fatto che il sistema target fornisce solo un insieme rado di transizioni isolate a singolo step. In questo contesto, un certificatore deve determinare se una traiettoria pianificata rimarrà sicura (evitando un insieme non sicuro $O$) nonostante l'errore del modello (residuo) tra il modello nominale $f_0$ e la vera dinamica target $f^\star$.

Gli autori identificano un limite fondamentale: lontano dai punti di osservazione dei dati, l'errore del modello può variare arbitrariamente entro un piccolo vicinato senza contraddire le osservazioni. Se l'errore del modello è non ristretto, due sistemi target regolari compatibili con gli stessi dati sparsi possono divergere arbitrariamente una volta che il piano entra in una regione non osservata. Di conseguenza, qualsiasi certificatore deterministico che sia uniformemente corretto (garantendo la sicurezza per tutti i sistemi compatibili) deve o rifiutarsi di certificare o restituire un tubo raggiungibile con una larghezza proiettata arbitrariamente grande, rendendo il certificato non informativo.

Metodologia: ForeReach
Gli autori propongono ForeReach, un certificatore pre-esecuzione che naviga questa limitazione incorporando informazioni collaterali (side information). Il metodo opera secondo il seguente framework:

1. Requisito di Informazioni Collaterali: ForeReach richiede un limite Lipschitz componente per componente ($L$) fornito sul modello di errore su un dominio di certificazione prescritto ($Z_{cert}$). Questo limite deve essere stabilito indipendentemente dai dati sparsi (ad esempio, tramite dinamiche analitiche con parametri limitati o un modello residuo separatamente certificato).
2. Test di Coerenza a Coppie: Prima della propagazione, il metodo verifica se le coppie di residui osservati contraddicono il limite Lipschitz fornito. Se $|e_{r_i, k} - e_{r_j, k}| > \sum L_{k\ell}|z_{i,\ell} - z_{j,\ell}| + 2\sigma_k$, la dichiarazione viene rifiutata e il certificatore si astiene.
3. Involucro di Appartenenza all'Insieme (Set-Membership Envelope): Condizionatamente al rispetto del limite, il metodo costruisce un involucro di appartenenza all'insieme per il residuo in ogni set di stato-input interrogato. Tale involucro è derivato dall'intersezione tra i limiti per singola osservazione estesi tramite la costante di Lipschitz (estensione di McShane) e i limiti del rumore di osservazione.
4. Propagazione Zonotopica: L'incertezza viene propagata in avanti utilizzando il modello nominale $f_0$. L'insieme raggiungibile è rappresentato come un zonotopo, incorporando l'involucro della mappa nominale (utilizzando i limiti dell'Essere di intervallo per i termini residui dell'Esseria Hessiana) e l'involucro del residuo.
5. Logica di Certificazione: Il certificatore emette un certificato di sicurezza solo se:
   • La propagazione rimane all'interno del dominio di certificazione ($Z_{cert}$).
   • Ogni sezione proiettata del tubo raggiungibile evita l'insieme non sicuro ($O$).
   • Il metodo distingue tra tre tipi di astensione: contraddizione a coppie ($\perp_F$), uscita dal dominio ($\perp_D$) e fallimento della sicurezza ($\perp_S$).

Contributi Chiave

1. Il Teorema del Trilemma: Gli autori dimostrano un "trilemma" per i certificatori deterministici utilizzando dati a singolo step finiti. Un certificatore non può essere simultaneamente:
   • Uniformemente corretto su una classe di residui non ristretta.
   • $\bar{\rho}$-informativo (restituendo un tubo con larghezza proiettata finita).
   • Non ristretto oltre le osservazioni.
     Essi derivano inoltre un limite inferiore finito e dipendente dal piano sulla larghezza proiettata per classi di errore del modello con regolarità limitata, mostrando che anche con vincoli di regolarità, un'ampiezza non nulla è forzata dal gap privo di dati.
2. Algoritmo ForeReach: Un metodo pratico che combina i limiti Lipschitz forniti, i controlli di coerenza a coppie e la propagazione zonotopica per fornire il contenimento della traiettoria condizionato alla validità della dichiarazione fornita.
3. Validazione Empirica: Gli esperimenti su due sistemi benchmark (una massa puntiforme affine e una bicicletta dinamica a sei stati) dimostrano che ForeReach si astiene correttamente quando i piani entrano in regioni non supportate (garantendo la correttezza) pur recuperando la certificazione quando sono disponibili dati target rilevanti.

Risultati Sperimentali

• Sistema Massa Puntiforme: I baseline di calibrazione globale hanno certificato piani non supportati ma non sono riusciti a contenere le traiettorie target (0% di copertura), risultando in alti tassi di falsi positivi di sicurezza (false-safe). ForeReach ha ottenuto il 100% di copertura del tubo completo sui piani non supportati tramite l'astensione, e il 99,8% di richiamo certificato sui piani supportati dai corridoi.
• Sistema Bicicletta Dinamica: Sono stati osservati trend simili. La calibrazione globale e altri baseline (processi gaussiani, metodi conformi) hanno prodotto o tubi non informativi o hanno fallito nel contenere le traiettorie nelle regioni non supportate. ForeReach ha mantenuto il 100% di copertura sui piani non supportati (tramite astensione) e ha raggiunto il 98,3% di richiamo certificato nei corridoi supportati con $N=400$ campioni.
• Chunk di Azione Appresi: Quando applicato a piani generati da una policy appresa, il tasso di astensione di ForeReach correla fortemente (Spearman $\rho=0.697$) con la distanza del rollout nominale del piano dal più vicino dato osservato, tracciando efficacementamente il "supporto" dei dati.
• Dichiarazioni Errate: Lo studio ha mostrato che se il limite Lipschitz fornito è troppo piccolo (sottostimando la regolarità), il test a coppie può passare (se non esiste una contraddizione locale), ma il tubo risultante potrebbe essere troppo stretto per contenere la vera traiettoria, portando a certificati falsi. Ciò evidenzia come la correttezza del metodo sia condizionata dalla validità della dichiarazione esterna.

Significatività e Rivendicazioni
Il documento sostiene che il limite primario nella certificazione di piani da dati scarsi non è la quantità di dati, ma la mancanza di vincoli sull'errore del modello nelle regioni non osservate. Gli autori argomentano che un certificato utilizzabile richiede informazioni strutturali (come i limiti Lipschitz) fornite dall'esterno dei dati. Sebbene i dati possano confutare una dichiarazione errata, non possono confermare una dichiarazione corretta nelle regioni non osservate.

La significatività del lavoro risiede nel:

• Formalizzare i limiti teorici (il trilemma) della raggiungibilità guidata dai dati con transizioni sparse e isolate.
• Fornire un metodo che scambia esplicitamente tra correttezza e informatività in base alla validità delle informazioni collaterali, piuttosto che assumere proprietà globali della distribuzione dei dati.
• Dimostrare che l'"astensione" è un esito necessario e informativo quando un piano lascia il supporto dei dati, contrastando con i baseline che possono produrre certificati stretti ma non corretti.

Gli autori sottolineano che la loro garanzia è condizionata: il certificato è valido solo se il limite Lipschitz fornito è valido in tutto il dominio di certificazione. Il metodo non apprende il limite dai dati sparsi, ma lo utilizza per costruire un involucro corretto.