Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Riepilogo Tecnico: Logica del Passato Causale per la Verifica a Runtime di Flussi di Lavoro di Agenti LLM Distribuiti

Enunciato del Problema
I flussi di lavoro distribuiti di agenti basati su Modelli Linguistici su Grande Scala (LLM), in cui più agenti interagiscono in modo asincrono senza memoria condivisa, non possono essere monitorati efficacemente come se producessero un singolo log sequenziale. Nelle esecuzioni asincrone, una decisione presa da un agente (una "linea di vita") dipende solo dagli eventi che sono causalmente visibili ad esso. Un evento che appare prima in un log sequenziale globale potrebbe non essere ancora noto localmente, mentre un evento localmente recente potrebbe non riflettere lo stato più recente di un agente remoto.

Gli approcci esistenti di verifica a runtime fanno spesso affidamento su tracce sequenziali o analisi di log a posteriori. Tuttavia, per i flussi di lavoro degli agenti, ciò è insufficiente perché il monitoraggio dovrebbe influenzare l'esecuzione al momento della decisione. Se un decisore (ad esempio, un Committer) non ha causalmente visto un risultato di test pulito, il sistema non dovrebbe unire e segnalare una violazione in un secondo momento; dovrebbe bloccare l'unione o richiedere un riesecuzione immediatamente. Inoltre, i meccanismi di guardia standard nelle applicazioni LLM spesso trattano l'esecuzione come un log sequenziale, ignorando la struttura causale necessaria per un corretto processo decisionale distribuito.

Metodologia
Gli autori estendono il framework ZipperGen, un sistema di programmazione coreografica per agenti LLM distribuiti, introducendo la Logica del Passato Causale (CPL).

1. Modello Formale (MSC): Le esecuzioni sono modellate come Diagrammi di Sequenza di Messaggi (MSC), dove gli eventi sono distribuiti sulle linee di vita. L'ordine causale è definito dalla chiusura transitiva riflessiva della successione locale e della consegna dei messaggi. Ogni evento porta una valutazione delle variabili locali.
2. Logica del Passato Causale (CPL): La CPL è una piccola logica temporale passata progettata come linguaggio di guardia a livello sorgente.
   • Sintassi: Le formule includono modali temporali passati standard (Precedente $Y$, Da $S$) interpretati lungo una singola linea di vita, e una modalità causale $@A(\phi)$ che valuta $\phi$ all'ultimo evento della linea di vita $A$ che è causalmente visibile all'evento corrente.
   • Accesso alle Variabili: La logica supporta termini come $@A.x$, che leggono il valore della variabile $x$ all'ultimo evento causalmente visibile della linea di vita $A$.
   • Semantica: Una guardia $\phi@A$ è valutata localmente dal proprietario della linea di vita $A$ in un punto di decisione (ramo o ciclo). Il valore di verità determina il flusso di controllo. La logica non è rigorosa: se nessun evento di $A$ è visibile, la formula valuta a falso.
3. Algoritmo di Monitoraggio Online:
   • Gli autori propongono un algoritmo di monitoraggio distribuito in cui ogni linea di vita mantiene un orologio vettoriale e viste dei valori più recenti.
   • Stato: Ogni agente mantiene un orologio vettoriale per tracciare il numero di eventi visti da ogni altra linea di vita. Mantiene anche una mappa parziale di "viste dei valori più recenti" per formule booleane e valori di variabili provenienti da altre linee di vita.
   • Propagazione: Quando un agente invia un messaggio, allega il proprio orologio vettoriale corrente e le viste dei valori più recenti. Ricevendo un messaggio, l'agente unisce queste viste al proprio stato locale, aggiorna il proprio orologio vettoriale e rivaluta tutte le guardie dal basso verso l'alto.
   • Correttezza: L'algoritmo garantisce che il valore del monitor calcolato localmente coincida con la semantica denotazionale della guardia sull'MSC.

Contributi Chiave

• Logica del Passato Causale (CPL): Una logica innovativa per i flussi di lavoro di agenti distribuiti che combina operatori temporali passati standard con l'accesso causale allo stato più recente visibile di altri agenti. Permette alle guardie di esprimere condizioni come "i test richiesti sono passati e nessun fallimento è stato visto da allora, nel passato causale".
• Guardie a Livello Sorgente: A differenza di monitor esterni che controllano i log a posteriori, le formule CPL sono integrate nel codice sorgente del flusso di lavoro. Sono valutate online dal decisore per influenzare direttamente il flusso di controllo.
• Monitoraggio Distribuito con Orologi Vettoriali: Un algoritmo di monitoraggio online efficiente che utilizza orologi vettoriali e viste dei valori più recenti per tracciare la visibilità causale senza richiedere un osservatore centrale o un log sequenziale globale.
• Verifica Formale: Le definizioni di MSC, soddisfacimento CPL, valutatore locale e il teorema di correttezza del monitor sono meccanizzati e verificati in Lean 4. Il documento dimostra che la valutazione a runtime locale di una guardia corrisponde alla sua semantica denotazionale all'evento corrente.
• Implementazione Prototipale: Un'implementazione prototipale nel framework ZipperGen (Python) dimostra la fattibilità dell'approccio, mostrando come le guardie possano confrontare variabili tra linee di vita (ad esempio, assicurando che un risultato di test corrisponda al candidato di unione corrente).

Risultati

• Teorici: Il documento dimostra il Lemma 1 (Correttezza della valutazione locale) e il Lemma 2 (Invarianti dello stato del monitor), culminando nel Teorema 1 (Correttezza del monitor). Queste prove stabiliscono che l'algoritmo distribuito calcola correttamente il valore di verità di qualsiasi formula CPL basandosi sul passato causale visibile alla linea di vita proprietaria.
• Pratici: L'implementazione prototipale in ZipperGen gestisce con successo l'esempio di una revisione del codice distribuita, in cui un Committer decide di unire una patch solo se causalmente vede test e scansioni di sicurezza superati per il candidato specifico, bloccando l'unione se un fallimento è visibile nel passato causale.

Significato
Il documento sostiene che la verifica a runtime per i flussi di lavoro di agenti LLM distribuiti deve andare oltre l'analisi dei log sequenziali. Trattando il monitoraggio come parte integrante del linguaggio di coordinamento (tramite guardie a livello sorgente), il sistema può prendere decisioni corrette basate sulle informazioni causalmente visibili disponibili al punto di decisione, piuttosto che attendere un log globale o un osservatore centrale. Questo approccio affronta la difficoltà fondamentale della programmazione distribuita in cui le decisioni locali dipendono da viste causali parziali. Il lavoro colma il divario tra programmazione coreografica (specifiche globali proiettate su agenti locali) e applicazione di vincoli a runtime, garantendo che le proprietà di sicurezza e coordinamento siano applicate dinamicamente e causalmente correttamente.