LeanGuard — 도구 실행 전에 정책 검사하기

TL;DR

LeanGuard는 실행 전에 제안된 도구 호출을 Lean4 정책과 대조해 검사한다. 저자들은 시험한 환경에서 금지된 행동과 직접적인 프롬프트 주입의 성공률이 줄었다고 보고한다. 이는 정책이 모든 안전 요구사항을 담고 있음을 증명하지 않는다. (source)

저자와 소속

저자는 Sreehari Sankar, Debargha Ganguly, Vikash Singh, Mohsen Hariri, Weicong Chen, Yanyan Zhang, Shouren Wang, Wang Yang, Chaoda Song, Alexander Nemecek, Osama Zafar, Idan Davidovich, Yuting Shao, Kai Ye, Biyao Zhang, Xinpeng Li, Joe Stubbs, Erman Ayday, Jing Ma, Vipin Chaudhary이다. 수집한 초록 기록만으로 소속은 확인되지 않는다. 최초 제출일은 2026-11-02이다. (source)

방법

정책은 상태 술어와 실행 이력에 적용되는 범위가 한정된 과거 시제 시간 연산자를 결합한다. 평가가 실패하면 실행을 차단하며, 결정 절차가 LeanLTL 의미론과 동등함을 증명한다. (source)

호출을 거부한 뒤 피드백은 위반한 규칙과 힌트를 제공한다. 다른 방식인 증명 기반 수정은 언어 모델 없이 Lean 메타프로그래밍으로 사용자 의도를 보존하는 유사한 호출을 탐색하고 정책이 이를 허용함을 증명한다. (source)

결과

Qwen 모델 다섯 개(0.8B–27B)를 사용한 Tau-Bench에서 보호되지 않은 에이전트는 정책상 금지된 호출을 최소 33회 실행하지만, LeanGuard는 한 번도 실행하지 않는다. 피드백을 제공할 때 과제 성공률은 유의하게 변하지 않는다. 이 횟수는 코드로 표현한 정책이 금지하는 호출을 가리킨다. (source)

DTap에서 직접적인 프롬프트 주입 성공률은 57.9%에서 5.9%로 낮아진다. 정상 과제에 쓰기 작업이 필요 없는 통신 분야에서는 정상 과제 성공률이 변하지 않는다. 피드백은 단순 거부에 비해 다섯 모델 중 네 모델의 과제 성공률을 높이고 차단된 호출의 반복을 줄인다. (source)

인수 값 때문에 거부된 호출을 재생했을 때 수정 절차는 252건 중 88건에 대해 허용되는 수정안을 증명한다. 초록은 수정 시간 중앙값을 2,ms로 표기한다. 이 잘못된 단위 문자열은 임의로 해석하지 않고 그대로 보존한다. (source)

의의

Agent Runtime Containment와 Agents (LLM Agents) 관점에서 이는 제안된 행동과 실행 사이에 명시적인 집행 지점을 둔다. 해석: 정책 평가에 관한 증명과 과제 성공에 관한 증거는 서로 다른 질문에 답하며, 실용적인 보호 장치를 평가하려면 둘 다 필요하다. (source)

열린 질문

초록만으로 정책의 완전성, 침해된 도구에 대한 견고성, 평가 영역 밖에서의 안전성은 확인되지 않는다. 수정이 가능한 범위는 재생한 거부 사례의 일부로 제한되며 전체 운영 오버헤드는 여기서 확인되지 않았다. 논문 전문과 코드는 검토하지 않았다. (source)

인용

• arXiv:2611.02332.
• 수집한 초록.