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

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

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

• MetaBackdoor: Exploiting Positional Encoding as a Backdoor Attack Surface in LLMs

  입력 텍스트는 멀쩡한데 입력 길이만으로 LLM 백도어가 발동되는 새로운 공격 기법 발견.

• Tell HN: Dont use Claude Design, lost access to my projects after unsubscribing

  Claude Design 구독을 해지했더니 기존 프로젝트에 접근이 완전히 차단됐다는 사용자 경고로, AI 도구에 중요한 작업물을 의존할 때의 리스크를 잘 보여주는 사례다.

• History Anchors: How Prior Behavior Steers LLM Decisions Toward Unsafe Actions

  시스템 프롬프트에 '이전 전략과 일관되게 행동하라' 한 문장만 추가하면, 최고 성능 LLM들이 안전한 선택을 0%에서 90%+ 위험한 선택으로 뒤집힌다.

• Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

  LLM에게 조합 최적화 문제의 solver를 만들게 할 때, 'Python + OR-Tools'가 가장 정확하고 '효율 최적화' 프롬프트는 오히려 정확도를 망친다.

• Postmortem: TanStack NPM supply-chain compromise

  2026년 5월 11일 TanStack의 42개 npm 패키지가 GitHub Actions cache poisoning과 OIDC 토큰 탈취를 조합한 공격으로 악성 버전이 배포됐으며, 공격 벡터와 대응 과정을 상세히 분석한 글이다.

Related Resources

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