LeanGuard, Lean4로 도구 사용 에이전트의 실행을 검증하다

들어가며

언어 모델 에이전트가 검색, 데이터 수정, 외부 시스템 조작까지 수행하게 되면 안전성은 생성된 문장만으로 판단할 수 없습니다. 모델이 제안한 행동이 실제 환경에서 실행되는지가 더 중요해집니다. 프롬프트 인젝션이나 잘못된 인자로 인해 에이전트가 도메인 정책에 어긋나는 도구 호출을 할 수 있기 때문입니다. LeanGuard는 이 실행 경로에 검증 단계를 추가해, 모든 도구 호출을 환경에 전달하기 전에 검사합니다.

핵심 내용

• 현재 상태와 실행 이력을 함께 본다. 정책은 Lean4로 작성되며 상태 술어와 범위가 지정된 과거 시점 시간 연산자를 결합합니다. 따라서 현재 호출의 인자뿐 아니라 이전에 특정 행동이 발생했는지도 조건으로 표현할 수 있습니다.
• 증명되지 않으면 차단한다. LeanGuard는 페일 클로즈 방식으로 동작합니다. 호출이 정책을 만족한다고 확인할 수 없으면 허용하지 않습니다. 의사결정 절차가 LeanLTL 의미론과 동등하다는 점도 형식적으로 증명됐습니다.
• 거부 이후의 수정도 지원한다. 피드백 방식에서는 위반된 규칙과 힌트를 에이전트에 전달합니다. 증명 유도 복구 방식에서는 Lean 메타프로그래밍이 사용자의 의도를 유지하는 가까운 대체 호출을 찾고, 해당 호출이 정책을 만족한다는 사실을 증명합니다.
• 금지된 실행을 차단한다. Tau-Bench에서 0.8B부터 27B까지 다섯 개 Qwen 모델을 평가한 결과, 보호되지 않은 에이전트는 Lean 정책이 금지한 호출을 최소 33회 실행했습니다. LeanGuard는 이런 호출을 허용하지 않았습니다. 피드백을 추가해도 전체 작업 성공률은 크게 달라지지 않았고, 차단된 호출의 반복은 줄었습니다.
• 프롬프트 인젝션에도 효과가 있었다. DTap에서 직접 프롬프트 인젝션 성공률은 57.9%에서 5.9%로 낮아졌습니다. 정상 작업에 쓰기 동작이 필요하지 않은 통신 시나리오에서는 정상 작업 성공률이 유지됐습니다. 인자 값 때문에 거부된 호출을 재생한 사례에서는 252건 중 88건에 대해 허용 가능한 수정안을 증명했으며, 처리 시간 중앙값은 2밀리초였습니다.

의미와 한계

LeanGuard의 핵심은 모델을 항상 올바르게 만드는 데 있지 않습니다. 대신 모델의 계획과 실제 실행 권한을 분리합니다. 모델은 사용자의 의도를 이해하고 호출을 제안하지만, Lean4 정책은 현재 상태와 실행 이력에 따라 해당 행동을 허용할지 결정합니다. 계정 변경이나 데이터 쓰기처럼 실수의 비용이 큰 작업에서 특히 유용한 구조입니다.

그러나 형식 검증이 정책 자체의 완전성을 보장하는 것은 아닙니다. 정책이 조직의 의도를 제대로 담았는지, 도구 스키마가 바뀌었을 때 정책이 여전히 적절한지, 검증 지연과 거부 후 재시도 비용이 감당 가능한지는 별도로 관리해야 합니다. 이번 결과는 실행 전 검사가 효과적임을 보여주지만, 운영 환경에서 지속적인 정책 검토가 필요하다는 사실까지 없애지는 않습니다.

그럼에도 프롬프트 지시나 사후 감사에만 의존하는 방식과 비교하면, 실행 경계에서 보수적이고 감사 가능한 판정을 내리는 설계는 에이전트를 실제 시스템에 연결하기 위한 현실적인 안전 방향을 제시합니다.

출처: Hugging Face Daily Papers