Formal Methods Meet LLMs: Auditing, Monitoring, and Intervention for Compliance of Advanced AI Systems

Who Should Read

LLM 기반 에이전트나 챗봇을 프로덕션에 배포하면서 규정 준수, 안전 제약, 행동 모니터링이 필요한 백엔드/AI 엔지니어. 특히 금융, 의료, 물류 등 규제 산업에서 LLM 제품을 개발하는 팀.

Core Mechanics

• LLM-as-a-Judge(LLM이 다른 LLM을 심판하는 방식)는 시간적으로 확장된 행동 패턴(예: '결제 후에만 배송') 감지에 취약함. 이벤트 간 거리가 멀어지거나 제약 조건 수가 늘면 정확도가 랜덤 수준으로 떨어짐.
• TRAC(Temporal Rule Assessment and Compliance) 알고리즘은 LTL(Linear Temporal Logic, 시간 흐름에 따른 논리 규칙 언어) 기반으로 LLM의 입출력을 실시간 모니터링하며, 위반 발생 시 어떤 규칙이 언제 깨졌는지 설명하는 witness(증거 추적)도 제공.
• 핵심 아이디어는 역할 분리: LLM은 '이벤트 라벨링'(지금 무슨 일이 일어났나 판단)만 하고, 시간 패턴 추론은 LTL progression(공식 기반 점진적 평가)이 담당.
• Qwen-7B 같은 소형 모델을 라벨러로 쓴 TRAC이 GPT-4.1, Gemini-2.5-Pro 같은 프론티어 LLM을 단독 심판으로 쓰는 것보다 F1 점수가 높음. 즉 비용을 줄이면서 정확도를 높일 수 있음.
• TRACP+I는 예측 모니터링(위반이 일어나기 전에 예측)과 개입(intervention)을 추가한 확장 버전. 위반이 예상되면 ①프롬프트 수정, ②여러 출력 중 선택(best-of-n), ③더 안전한 모델로 교체 등 3가지 방식으로 자동 개입.
• LLM의 시간 추론 한계를 실험으로 정량화: 이벤트 간 거리(gap)가 늘수록, 동시에 모니터링할 제약 수가 늘수록, 스텝당 명제(proposition) 수가 늘수록 정확도가 체계적으로 떨어짐.

Evidence

• TRACR + 소형 LLM 라벨러(Qwen-7B)가 IPC-Trucks, TextWorld, ScienceWorld 3개 환경 모두에서 GPT-4.1, Gemini-2.5-Pro를 단독 LLM-as-a-Judge로 쓸 때보다 F1 점수가 일관되게 높음 (Figure 2).
• LLM 라벨러 정확도는 환경별로 Qwen-7B 기준 IPC-Trucks 0.77, TextWorld 0.87, ScienceWorld 0.98로 개별 명제 라벨링 자체는 소형 모델도 매우 잘 수행 (Table 1).
• TRACP+I 개입 전략(Inject/Resample/Switch) 적용 시 모든 모델-환경 조합에서 위반율(violation rate)이 베이스라인 대비 감소하며, 태스크 성능(cumulative reward)은 유의미한 저하 없이 유지됨 (Figure 4, Figure 7).
• 시간 간격 실험에서 소형 모델은 gap ~10 스텝부터, 프론티어 모델은 복잡한 공식에서 gap이 커질수록 정확도가 랜덤(~50%) 수준으로 수렴 (Figure 3a, 3d).

How to Apply

• LLM 에이전트에 규칙을 심을 때, 규칙을 자연어로만 프롬프트에 넣지 말고 LTL 공식으로 변환한 뒤 TRAC 모니터를 래퍼로 씌워라. 자연어→LTL 변환은 NL2LTL 같은 autoformalization 도구로 반자동화 가능.
• 비용이 걱정되면 고가 프론티어 모델(GPT-4.1, Gemini-2.5-Pro)을 심판으로 쓰는 대신, 소형 LLM(Qwen-7B 수준)을 라벨러로만 쓰고 시간 패턴 추론은 LTL progression 엔진에 맡겨라. 성능은 올라가고 비용은 낮아짐.
• 프로덕션 LLM 에이전트에서 위반이 자주 생기는 규칙이 있다면 TRACP+I의 constraint-guided prompting(잔여 LTL 공식을 자연어로 프롬프트에 주입) 전략을 써라. 같은 모델을 재사용하면서 위반율을 낮출 수 있고, 모델 교체가 필요한 경우에는 model substitution 전략으로 더 안전한 모델로 자동 전환.

Code Example

# TRAC 모니터링 핵심 로직 (Python 의사코드)
# 자연어 규칙: '결제가 확인되기 전에 제품을 배송하지 마라'
# LTL 공식: G(ship -> (payment_confirmed U ship))
# 즉, 배송이 일어나면 항상 그 전에 결제 확인이 되어 있어야 함

from ltl_monitor import LTLMonitor, LLMLabeler

# 1. 규칙을 LTL 공식으로 정의
formula = "G(ship -> (payment_confirmed U ship))"

# 2. LLM을 라벨러로 사용 (소형 모델도 OK)
labeler = LLMLabeler(
    model="qwen-7b",
    propositions=["ship", "payment_confirmed", "invoice_received"]
)

# 3. TRAC 모니터 초기화
monitor = LTLMonitor(formula=formula, labeler=labeler)

# 4. 에이전트 실행 중 매 스텝 모니터링
for step in agent_execution_loop():
    input_text = step.user_input
    output_text = agent.generate(input_text)
    
    # 라벨러가 현재 스텝에서 참인 명제 추출
    labels = labeler.extract(input_text, output_text)
    
    # LTL progression으로 공식 업데이트 및 판정
    verdict, witness = monitor.step(labels)
    
    if verdict == "VIOLATED":
        print(f"규칙 위반 감지! 증거: {witness}")
        # 개입 로직 실행 (TRACP+I)
        output_text = intervene(output_text, monitor.residual_formula)
    
    yield output_text

# 오프라인 감사 (로그 데이터에 적용)
audit_results = monitor.audit_log(historical_logs)
for violation in audit_results.violations:
    print(f"스텝 {violation.step}: {violation.rule} 위반 - {violation.witness}")

Terminology

Related Papers

• MemTrace: Tracing and Attributing Errors in Large Language Model Memory Systems

  RAG, Mem0 같은 LLM 메모리 시스템이 왜 틀린 답을 내는지 자동으로 찾아주는 디버깅 프레임워크

• DeepSWE: A contamination-free benchmark for long-horizon coding agents

  기존 SWE-bench의 데이터 오염 및 검증 오류 문제를 해결하기 위해 처음부터 새로 만든 코딩 에이전트 벤치마크로, GPT-5.5가 70%로 1위를 차지하고 모델 간 성능 격차가 훨씬 뚜렷하게 드러난다.

• Constraint Decay: The Fragility of LLM Agents in Back End Code Generation

  LLM 코딩 에이전트는 구조적 제약(아키텍처 패턴, ORM, DB 설계)이 쌓일수록 성능이 급격히 떨어지는 'constraint decay' 현상을 보인다는 연구 결과로, AI 코딩 도구를 프로덕션에 쓰려는 개발자라면 반드시 알아야 할 한계다.

• AMEL: Accumulated Message Effects on LLM Judgments

  LLM을 자동 평가자로 쓸 때 이전 대화 기록의 긍정/부정 분위기가 이후 판단을 오염시킨다는 걸 75,898개 API 호출로 증명한 연구.

• Language-Switching Triggers Take a Latent Detour Through Language Models

  8B LLM에 심어진 백도어 트리거가 중간 레이어에서 언어 탐지기를 완전히 속이는 직교 부분공간(orthogonal subspace)으로 숨어 이동한다는 걸 회로 분석으로 밝혀냈다.

• Bun Rust rewrite: "codebase fails basic miri checks, allows for UB in safe rust"

  Anthropic이 인수한 Bun 런타임이 Zig 코드베이스를 AI로 Rust에 재작성했는데, 가장 기본적인 메모리 안전성 검사(miri)조차 통과하지 못하는 UB(Undefined Behavior)가 발견됐다는 이슈가 제기됐다.

Related Resources

• TRAC GitHub 코드
• NL2LTL: 자연어→LTL 변환 Python 패키지