[논문리뷰] LEANGUARD: Lean-Verified Guardrails for Tool-Using Agents

링크: 논문 PDF로 바로 열기

메타데이터

저자: Sreehari Sankar, Debargha Ganguly, Vikash Singh, et al.

---

1. Key Terms & Definitions (핵심 용어 및 정의)

• LeanGuard: Lean 4를 기반으로 구현된 런타임 가드레일로, 에이전트의 tool call이 환경에 실행되기 전 정책 준수 여부를 검증합니다.
• LeanLTL: Linear Temporal Logic을 지원하는 Lean 4 라이브러리로, 정책의 실행 의미론(semantics)을 정의하고 검증하는 데 사용됩니다.
• Proof-guided repair: Lean의 메타프로그래밍 프레임워크를 활용하여, 에이전트가 제안한 거부된 tool call을 사용자 의도를 유지하면서 허용 가능한 형태로 자동 수정하고 이를 입증하는 기술입니다.
• Fail-closed evaluation: 정책 검증 중 데이터 누락이나 오류가 발생할 경우, 해당 동작을 명시적으로 차단하여 안전성을 보장하는 평가 방식입니다.

2. Motivation & Problem Statement (연구 배경 및 문제 정의)

본 논문은 tool을 사용하는 LLM 기반 에이전트가 도메인 정책을 위반하거나 안전하지 않은 환경 변화를 초래하는 문제를 해결하기 위해 LeanGuard를 제안합니다. 기존 에이전트들은 복잡한 상태 의존성을 제대로 처리하지 못하거나, 외부로부터 주입된 부적절한 명령에 휘둘려 정책에 반하는 동작을 실행하는 경우가 빈번합니다 [Figure 1]. 또한, 기존의 가드레일은 모델의 reasoning에 의존하거나 검증의 엄밀성이 부족하다는 한계가 있습니다. 이를 해결하기 위해 저자들은 Lean 4를 이용한 형식 검증 기반의 엄격한 런타임 제어 메커니즘이 필요하다고 판단하였습니다 [Figure 2].

3. Method & Key Results (제안 방법론 및 핵심 결과)

저자들은 에이전트의 모든 tool call을 Lean 4 정책과 대조하여 검증하는 LeanGuard 런타임 프레임워크를 설계하였습니다. 이 프레임워크는 과거 상태를 고려한 temporal operator와 상태 술어(state predicates)를 활용하며, 모든 승인 결정은 LeanLTL 의미론과 동등하도록 수학적으로 증명되었습니다 [Figure 2]. 실험 결과, τ2-bench 환경에서 기존 에이전트가 최소 33건의 정책 위반 호출을 수행한 반면, LeanGuard는 이를 0건으로 완벽히 차단했습니다. DTap 벤치마크에서는 직접적인 prompt-injection 성공률을 기존 57.9%에서 5.9%로 획기적으로 낮추었습니다 [Table 1]. 또한, Proof-guided repair를 통해 거부된 호출의 34.9%를 평균 2ms 이내에 자동 수정하여 작업 성공률을 높이는 성과를 거두었습니다 [Table 2].

4. Conclusion & Impact (결론 및 시사점)

본 연구는 에이전트의 자율적 행동과 시스템의 형식적 안전성을 결합하는 새로운 접근 방식을 제시합니다. LeanGuard는 모델의 판단을 보완하는 엄격한 보호막을 제공하며, 특히 수정 가능한 호출에 대한 증명된 교정 기능을 통해 에이전트의 복구 능력을 크게 향상시킵니다. 이는 향후 금융, 의료, 통신 등 높은 신뢰성이 요구되는 도메인에서 LLM 에이전트를 안정적으로 도입하기 위한 핵심적인 기술적 기반이 될 것으로 기대됩니다.

⚠️ 알림: 이 리뷰는 AI로 작성되었습니다.