기술 요약: 형식적 방법과 LLM 의 만남

문제 제기

이 논문은 AI 거버넌스의 중요한 공백을 다룹니다: 개발 수명 주기 전반에 걸쳐 AI 기반 제품 및 서비스를 모니터링, 감사, 개입하기 위한 견고한 메커니즘의 부재입니다. 프런티어 AI 모델의 안전성을 위해 상당한 노력이 기울여지고 있지만 (예: 안전 프레임워크 및 레드팀을 통한), 중소기업 (SME) 과 제 3 자 개발자들은 배포된 블랙박스 AI 시스템 (특히 대규모 언어 모델 또는 LLM) 이 제품별, 산업별, 관할권별 규정을 준수하도록 보장할 도구가 부족한 경우가 많습니다.

핵심적인 과제는 많은 규정 준수 요구사항이 시간적으로 확장된 특성을 가진다는 점입니다. 이는 사건 간의 관계가 시간을 초월하는 행동 제약으로, 예를 들어 "송장이 수신되면 결국 지급되어야 한다"거나 "지불이 확인될 때까지 제품을 배송하지 마라"와 같은 것입니다. 저자들은 현재 감사에 대한 LLM-as-a-Judge 방식의 의존도가 불충분하다고 주장합니다. 왜냐하면 LLM 은 특히 사건 간의 시간 간격이 변하거나 제약의 수가 증가하거나, 각 단계당 명제의 수가 늘어날 때 이러한 시간적 패턴에 대한 추론에 어려움을 겪기 때문입니다.

방법론

저자들은 형식적 방법(구체적으로 선형 시간 논리 또는 LTL) 과 머신러닝을 연결하여 블랙박스 모니터링 및 감사 시스템을 구축하는 프레임워크를 제안합니다. 핵심 접근 방식은 문제를 분해하는 것입니다: LLM 을 사용하여 이벤트에 레이블을 지정하고 (비구조화된 텍스트에서 원자 명제를 추출), 형식 논리를 사용하여 이러한 이벤트의 시퀀스에 대해 추론합니다.

TRAC 프레임워크

저자들은 블랙박스 AI 시스템을 위해 설계된 알고리즘 군인 **TRAC(Temporal Rule Assessment and Compliance)**를 소개합니다:

1. 레이블링 함수 ($L$): LLM(또는 다른 분류기) 은 입력과 출력의 시퀀스를 특정 시간 단계에서 참인 명제 기호 (원자 사실) 집합으로 매핑합니다.
2. LTL 진행 (Progression): 제약 조건을 정적 오토마타로 컴파일하는 대신, 시스템은 LTL 진행을 사용합니다. 이 기술은 현재 진리 할당 $\sigma_t$를 기반으로 LTL 공식 $\psi$를 다시 써서, 트레인의 나머지 부분에 대해 무엇이 성립해야 하는지를 설명하는 잔여 공식 $\psi_{t+1}$을 생성합니다.
   • 이는 시간적 속성의 동적이고 점진적인 평가를 가능하게 합니다.
   • 제약 조건의 기호적 구조를 보존하여, 위반이 발생한 이유를 설명하는 해석 가능한 "증거 (witnesses)"(실행 트레인) 생성을 가능하게 합니다.
3. 알고리즘:
   • TRAC: 실시간 모니터링 및 오프라인 감사를 위한 기본 알고리즘입니다. 판정 (위반, 충족, 아직 결정되지 않음) 과 증거를 출력합니다.
   • TRACR(TRAC with Reset): 지속적인 모니터링을 처리하도록 TRAC 을 확장합니다. 위반 또는 충족이 감지되면 시스템은 공식을 초기 상태로 재설정하여 후속 위반을 감지할 수 있게 합니다 (잡음이 많은 환경이나 반복 작업에 유용함).
   • TRACP+I(TRAC with Predictive and Intervening capabilities):
     • 예측 모니터링: $k$ 시간 범위 내 미래 위반의 확률을 추정하기 위해 샘플링 기반 방법을 사용합니다.
     • 개입: 예측된 위험이 임계값을 초과하면 시스템은 블랙박스 개입을 트리거합니다. 전략에는 다음이 포함됩니다:
       • 거부 샘플링 (Rejection Sampling): 준수하는 출력이 발견될 때까지 모델의 출력을 재샘플링합니다.
       • 제약 조건 기반 프롬프팅: 모델을 유도하기 위해 잔여 LTL 공식을 (자연어로) 프롬프트에 주입합니다.
       • 모델 교체: 출력을 생성하기 위해 더 안전한 대체 모델로 전환합니다.

주요 기여

1. 수학적 프레임워크: 자연어 또는 형식 논리 (LTL) 로 표현된 사용자 지정 행동 요구사항에 대한 블랙박스 AI 시스템을 평가하기 위한 형식적 정의.
2. TRAC 알고리즘: 위반을 감지하고 원인을 파악하며 설명 가능한 증거를 제공하는 LTL 진행을 활용하는 알고리즘 군 (TRAC, TRACR, TRACP+I). 이 논문은 완벽한 레이블링 함수 조건 하에서 LTL 진행 기반 알고리즘의 **정당성 (soundness)**을 증명합니다.
3. LLM 심사관보다 우월함: 시간적으로 확장된 위반을 감지하는 데 있어 TRAC 이 LLM-as-a-Judge 기준선보다 현저히 우수함을 보여주는 실증적 증거. 특히, TRAC 프레임워크 내에서 레이블러로 사용된 소규모 모델이 독립적인 심사관으로 작용하는 프런티어 LLM 의 성능을 맞먹거나 능가합니다.
4. 예측 및 개입 모니터링: 사전 개입을 통해 LLM 기반 에이전트의 위반률을 낮추는 TRACP+I 의 도입으로, 작업 성능을 크게 저하시키지 않으면서도 예방적 거버넌스를 가능하게 합니다.
5. LLM 한계의 규명: 통제된 실험을 통해 LLM 의 시간적 추론 정확도가 다음과 함께 예측 가능하게 저하됨을 밝힘:
   • 관련 사건 간의 거리 증가 (시간적 탄력성).
   • 동시 제약 조건의 수 증가.
   • 시간 단계당 명제의 수 증가.

실험 결과

저자들은 IPC-Trucks(물류 계획), TextWorld(요리 작업), ScienceWorld(과학적 추론) 의 세 가지 환경에서 접근 방식을 평가했습니다.

• 감사 성능: 감사 작업에서 **TRACR + LLM(레이블러로서)**은 모든 환경에서 가장 높은 F1 점수를 달성했습니다. 심지어 Qwen-7B 와 같은 작은 레이블링 모델조차 TRACR 과 결합될 때, 제로샷 또는 퓨샷 심사관으로 사용된 대규모 프런티어 모델 (예: GPT-4.1, Gemini-2.5-Pro) 보다 우수한 성능을 보였습니다.
• 시간적 추론 한계: 합성 트레인을 통한 실험은 LLM 이 시간적 패턴에 어려움을 겪음을 확인시켰습니다. 정확도는 사건 간의 간격이 증가함에 따라 (단순 공식에서 소규모 모델은 약 10 단계에서 프런티어 모델은 약 1000 단계까지) 그리고 공식의 복잡성 (제약 조건/명제의 수) 이 증가함에 따라 현저히 떨어졌습니다.
• 개입 효과성: TRACP+I 프레임워크는 모든 모델과 환경에서 제약 위반률을 성공적으로 감소시켰습니다. 개입 (재샘플링, 프롬프팅, 교체) 은 에이전트를 준수 방향으로 효과적으로 유도하면서도 기준선과 비교 가능한 작업 성능 (누적 보상) 을 유지했습니다.

중요성과 주장

이 논문은 고전적 형식적 방법이 AI 감독에 여전히 가치 있지만, 언어 기반 시스템에 맞게 적응이 필요하다고 주장합니다. 주요 중요성은 제안된 분해 전략에 있습니다: 명제 추출과 같은 의미론적 레이블링에 LLM 의 강점을 활용하는 동시에, 시간적 패턴에 대한 추론에는 형식적 방법 (LTL 진행) 의 강점에 의존하는 것입니다.

저자들은 이 접근 방식이 다음과 같음을 강조합니다:

• 프런티어 모델에 필요한 예산 없이도 규정 준수 감사를 접근 가능하게 합니다.
• 디버깅과 책임 소재 규명에 필수적인 증거를 통한 해석 가능성을 제공합니다.
• 예측 모니터링과 개입을 통한 사전 예방적 거버넌스를 가능하게 하여, 사후 진단을 넘어설 수 있게 합니다.
• 배포 전 평가가 종종 불충분한 영역인 장기간에 걸쳐 행동이 진화하는 에이전트 AI 시스템의 특정 거버넌스 과제를 해결합니다.

이 논문은 한계에 대한 겸손한 인정으로 마무리됩니다: 블랙박스 모니터링은 모든 실패 모드를 감지할 수 없으며, 레이블링 함수는 오류를 도입할 수 있고, 모호한 자연어 요구사항을 정확한 LTL 공식으로 번역하는 것은 여전히 "형식주의 함정 (Formalism Trap)"에 노출된 사회기술적 과제입니다. 궁극적으로 TRAC 은 더 넓은 AI 책임성 생태계 내에서 배포 가능한 도구로 제시됩니다.