This is a paper introducing LeanGuard, a runtime that checks every tool call an agent proposes against a policy written in Lean4 before the call reaches the environment.
Tests: On Tau-Bench with five Qwen models (0.8B to 27B), unguarded agents ran at least 33 calls the Lean policy forbids, and LeanGuard ran none. Task success with feedback did not change significantly.
Prompt injection: On DTap, direct prompt-injection success fell from 57.9% to 5.9%.
Repair: Proof-guided repair found an admissible edit for 88 of 252 denials caused by argument values, with a median of 2ms, and it runs without the model.
Benign tasks: In telecom, where benign tasks need no writes, benign success is unchanged.
Repair works without the model, so the proofs do the fixing.
Sign in to comment.
TL;DR of the paper, generated automatically.
This is a paper introducing LeanGuard, a runtime that checks every tool call an agent proposes against a policy written in Lean4 before the call reaches the environment.
Repair works without the model, so the proofs do the fixing.