LeanGuard는 Lean4 증명으로 도구 호출을 막고 수리한다

무엇인가

도구를 쓰는 언어모델 에이전트는 도메인 정책이 금지한 동작을 실제로 실행한다. 저자들이 문제를 규정하는 방식이 실무적이다. 호출이 '잘 형성되었는가'와 '허용되는가'는 다른 질문이며, 후자는 백엔드 상태, 이전 행동의 이력, 사용자에게 무엇을 보여줬는지, 사전 승인이 있었는지, 이미 시도된 작업인지에 달려 있다. 그래서 이 논문은 가드레일을 상태 전이에 대한 통제로 다룬다. 모델이 행동을 제안하고, 별도의 정책 런타임이 그 전이가 형식 명세 아래 허용 가능한지 결정한다. 메시지 발송, 예약 변경, 결제 개시처럼 외부 상태를 바꾸는 호출은 성공하더라도 정책이 금지한 전이일 수 있기 때문에 문제가 크다.

어떻게 동작하나

LeanGuard는 Lean4로 구현된 런타임으로, 모델과 도구 사이에 놓인다. 모델은 평소의 도구 스키마를 그대로 보고 평범한 구조화 호출을 내며, 호스트가 이를 도구에 도달하기 전에 가로채 신뢰할 수 없는 데이터로 취급한다. 에이전트는 Lean 코드도, 증명도, 정책 규칙도, 승인 기록도 쓰지 못한다. 도메인 어댑터가 권위 있는 백엔드의 스냅샷을 뜨고 인자를 검증해 정책이 필요로 하는 사실을 도출하며, 스냅샷에는 승인이 의존하는 상태의 리비전이 붙고 과거 결과는 디스패치 시점에 기록된 사실을 유지한다. 따라서 모델이 '고객이 이미 승인했다'고 주장해도 정책을 만족시킬 수 없다. 허용된 호출은 도구 실행 전에 디스패치 예약으로 기록되어, 결과를 모르는 동안 단일 사용 작업이 반복되지 않는다. 사용자 확인도 정확한 제안과 상태 리비전에 묶여 한 번만 쓸 수 있는 신뢰 증거로 취급된다.

무엇과 다른가

정책은 상태 술어와 실행 이력 위의 범위 지정 과거시제 연산자로 구성된다. 연산자는 previous(직전 관련 이벤트에서 성질이 성립), once(이전에 일치하는 이벤트가 있었음), since(특정 목격 이벤트 이후 조건이 계속 성립) 세 가지이며, 각각 시간 창으로 제한할 수 있고 주체·대화·자원을 공유하는 이벤트 위에서 평가된다. 규칙은 permits, requirements, forbids 세 종류로 도구 행동에 붙는다. 허가 없이는 기본 거부이고, 넓은 허가는 충족되지 않은 요구사항이나 적용되는 금지를 덮어쓸 수 없다. 평가는 fail-closed다. 술어가 읽는 데이터가 없거나 형식이 깨지면 false가 아니라 오류로 처리하고, 관련 구성요소가 모두 오류 없이 평가될 때만 허용한다. 실행 평가기와 별개로 LeanLTL 라이브러리에 이력 트레이스를 임베딩한 독립 의미론을 두고, 모든 이력에 대해 평가기가 그 해석과 정확히 일치한다는 것을 단일 시간 공식, 권한 부여, fail-closed 오류 조건을 포함한 전체 입장 결정 순서로 증명한다. 증명은 정책을 빌드할 때 검사되며, sorry나 비표준 공리에 의존하는 정리는 검증 스크립트가 거부한다.

어떻게 쓰나

거부된 호출을 고치는 경로는 두 가지다. 피드백 경로에서는 실패한 규칙 식별자, 적용된 금지, 평가 오류, 근거 증거를 담은 결정 기록과 "고객에게 거래 확인을 요청하라" 같은 자연어 힌트를 돌려준다. 형식 부분은 Lean 정책이 정하고 힌트는 검증되지 않는 렌더링일 뿐이며, 수정은 모델이 한다. 증명 유도 수리 경로에서는 Lean 메타프로그래밍으로 쓴 guard_repair? 택틱이 유한한 후보 편집 집합을 순서대로 시도하고, 사용자 의도를 보존하는 편집인지(EditOK)와 편집된 호출을 정책이 허용하는지를 함께 증명한다. 예를 들어 100단위 예산에서 60을 쓴 계정에 70 지출을 제안했다면, 작업이 더 작은 금액을 허용할 때 40으로 수리된다. 해소는 Lean의 grind 엔진을 조합한 guard_solve가 맡고, 수리는 커널 검증된 증명과 함께만 반환된다. 정책 작성자는 guard_rule 속성으로 증명된 사실을 솔버 정리 데이터베이스에 등록하거나 자체 해소 택틱을 공급할 수 있다. 다만 수리 증명은 발견된 문맥에서만 성립하므로 수리된 호출도 평범한 입장 심사를 다시 통과하며, 후보 집합에서 수리를 찾지 못했다고 해서 수리가 존재하지 않는 것은 아니다. 그리고 런타임은 아직 이 탐색을 호출하지 않는다.

전제와 한계

실험은 τ²-bench의 retail·airline·telecom 도메인과 프롬프트 인젝션 레드팀 벤치마크 DTap에서 이뤄졌다. τ²-bench 정책의 도구 강제 가능 부분집합을 43개 도구에 걸친 45개 규칙, 583줄의 Lean으로 형식화했고, DTap은 7개 도메인에 199개 도구 계약을 두었다. 모델은 Qwen3.5 0.8B·2B·4B·9B와 Qwen3.8-27B다. 가드 없는 에이전트는 Lean 정책이 금지한 호출을 최소 33건, 28개 에피소드에서 실행해 상태를 바꿨고, LeanGuard 아래에서는 그런 호출이 하나도 실행되지 않았으며 차단된 1,702건 중 실행된 것은 없었다. 과제 성공률은 가드 없음 72.7%, LeanGuard+피드백 70.9%(p=0.21)로 유의한 변화가 없었고, 피드백 없는 단순 거부는 68.9%(p=0.007)였다. LLM 판정관이 정책 위반으로 표시한 에피소드는 가드 없음 9.7%에서 LeanGuard 5.6%, 피드백 포함 6.5%로 줄었다(p=0.002). 차단된 호출을 유형별로 보면 권한 부여 실패가 572건으로 가장 많았고(그중 338건이 고객 확인 없는 쓰기, 268건이 고객 소유가 아닌 자원에 대한 행동), 잘못된 호출 551건, 시간적 비호환 411건, 금지 위반 313건 순이었다. DTap에서는 직접 프롬프트 인젝션 성공률이 57.9%에서 5.9%로, 간접 인젝션은 22.3%에서 3.8%로 떨어졌다. 쓰기가 거의 필요 없는 telecom에서는 정상 과제 성공률이 75.1% 대 75.3%로 유지되면서 직접 공격 성공률이 55.1%에서 2.4%로 하락했다. 반면 읽기 전용으로 배포한 다른 도메인에서는 정상 쓰기까지 막혀 전체 정상 성공률이 53.1%에서 12.5%로 떨어졌다.

거부 이후 동작에 대한 측정도 있다. 피드백이 없으면 에이전트는 같은 호출을 반복한다. Qwen3.5-2B는 141개 고유 거부 행동에 대해 271건의 차단 호출을 냈고(행동당 약 1.9회), 피드백을 받으면 104개 행동에 144건(1.4회)으로 줄었다. 전체 모델에서 차단 호출은 983건에서 719건으로 감소했고, 요구사항을 충족한 뒤 재호출하는 복구는 34건에서 48건(거부 행동의 5.5%에서 9.1%, p=0.02)으로 늘었다. 단순 거부 대비 피드백은 5개 모델 중 4개에서 과제 성공률을 2.2~5.8pp 올렸고(전체 68.9%에서 70.9%), Qwen3.8-27B만 75.9%에서 71.2%로 내려갔다. 수리는 τ²-bench 라이브 실행의 입장 결정 7,720건을 전부 재현한 오프라인 리플레이에서 평가됐다. 인자 값 때문에 발생한 252건의 거부 중 88건(34.9%)에서 허용 가능한 편집이 증명되었고, 중앙값 2ms(최대 70ms)가 걸렸다. 대부분 원 결제 수단으로의 환불(64건)과 항공편 변경을 여행 증서 대신 카드로 결제하는 수리(18건)였다. 에이전트가 나중에 스스로 그 수리된 호출을 낸 경우 과제 성공이 22건 중 16건으로, 그렇지 않은 66건 중 7건보다 높았다.

실무에서 이 논문이 주는 신호는 명확하다. 프롬프트로 "하지 마"라고 부탁하는 대신 도구 경계에 결정 절차를 두고, 그 절차가 형식 의미론에 대해 옳다는 것을 빌드 시점에 증명한다는 발상이다. 다만 도입 전에 확인할 것이 많다. 보증은 검토된 형식 명세와 신뢰된 입력에 상대적이며, 자연어 정책의 도구 강제 가능 부분집합만 형식화했고 그 형식화는 LLM 작성 보조로 초안을 만든 뒤 손으로 고친 것이라 이 단계의 오류나 누락은 증명이 잡아주지 않는다. 도메인 어댑터가 환경을 충실히 보고한다는 가정, 모든 중요 도구 호출이 모니터를 통과한다는 가정도 필요하고, 자유 형식 대화를 동의 기록으로 바꾸는 변환은 보증 범위 밖이다. 도구 호출만 통제하므로 응답 텍스트가 해를 나르는 공격은 막지 못한다. 가드가 켜진 고객서비스·여행 에피소드에서도 그런 공격이 30.2% 성공했고(가드 없음 41.0%), 의료의 5개 공격 범주는 직접 공격에서 21.4~37.0% 성공률을 유지했다. 읽기 전용 DTap 배포는 정상 쓰기를 허용하는 정책에 비해 보호 효과를 과대평가한다. 증명 유도 수리는 오프라인 리플레이로만 평가되어 런타임이 아직 호출하지 않으므로, 수리를 에이전트에 전달했을 때의 효과는 측정되지 않았다. τ²-bench 규칙 두 개는 벤치마크 정책보다 엄격하고, DTap은 14개 도메인 중 7개만 다룬다. 판정은 평가 대상 모델 중 하나인 LLM 판정관에 의존하며, 실험은 모두 단일 모델 계열(Qwen), 영어 과제, 시뮬레이션 사용자로 이뤄졌다.