LEANGUARD: guardrail verificati con Lean per agenti che usano strumenti

Abstract degli autori

Gli agenti basati su modelli linguistici che usano strumenti eseguono spesso azioni vietate dalle policy del loro dominio. Presentiamo LeanGuard, un runtime che verifica ogni chiamata a uno strumento proposta rispetto a una policy scritta in Lean4, prima che la chiamata raggiunga l’ambiente. Le policy combinano predicati di stato con operatori temporali sul passato, con ambito definito, applicati alla cronologia dell’esecuzione; la valutazione adotta un comportamento fail-closed e la procedura decisionale è dimostrata equivalente a una semantica LeanLTL. Una chiamata negata può essere corretta in due modi. Con il feedback, l’agente riceve la regola violata e un suggerimento; con la correzione guidata da prove, la metaprogrammazione Lean cerca una chiamata simile che mantenga l’intento dell’utente e dimostra che la policy la ammette, senza ricorrere al modello. Su Tau-Bench, con cinque modelli Qwen (da 0,8B a 27B), gli agenti senza protezioni eseguono almeno 33 chiamate vietate dalla policy Lean, mentre LeanGuard non ne esegue nessuna; con il feedback, il successo nelle attività non cambia in misura significativa. Su DTap, LeanGuard riduce dal 57,9% al 5,9% il successo degli attacchi diretti tramite prompt injection e, nel settore delle telecomunicazioni, dove le attività lecite non richiedono scritture, il successo delle attività lecite resta invariato. Il feedback riduce le chiamate bloccate ripetute e aumenta il successo nelle attività per quattro modelli su cinque rispetto al semplice rifiuto. Sui dinieghi riprodotti, la correzione dimostra che una modifica ammissibile è possibile per 88 dei 252 dinieghi causati dai valori degli argomenti, con un tempo mediano di 2 ms.