기술 요약: MANTRA – SMT 검증 준수 벤치마크 합성

문제 정의

도구를 사용하는 대규모 언어 모델 (LLM) 에이전트가 기업 운영, 의료, 여행 예약 등 중요한 분야에서 점점 더 많이 배포되고 있으며, 이러한 에이전트의 행동은 엄격한 절차 매뉴얼을 준수해야 합니다. 이러한 에이전트를 평가하는 데 있어 근본적인 과제는 입력과 출력 간의 '불일치'입니다. 절차 규칙은 인간의 해석을 위해 비구조화된 자연어로 작성되는 반면, 에이전트의 행동은 도구 호출 시퀀스 (실행 추적) 로 나타납니다.

기존 평가 방법은 다음과 같은 중대한 한계를 겪고 있습니다:

• 수동 구축: 수동으로 벤치마크를 생성하는 것은 고품질이지만, 대규모 복잡한 매뉴얼이나 새로운 도메인으로 확장되지 못합니다.
• LLM 기반 심사자: 배포는 쉽지만, 이러한 심사자는 긴 실행 추적에 걸쳐 엄격한 시간적 제약, 전제 조건, 금지 행위를 신뢰성 있게 강제하는 데 어려움을 겪어 신뢰할 수 없는 평가로 이어집니다.
• 결과만 평가하는 방식: 많은 벤치마크는 최종 상태만 확인하여 에이전트가 비준수 절차 경로를 통해 올바른 결과에 도달했는지 감지하지 못합니다.

자연어 매뉴얼에서 결정론적이고 기계가 검증 가능한 채점을 제공하는 추적 수준 준수 벤치마크를 자동으로 생성할 수 있는 확장 가능하고 재현 가능한 방법이 부족합니다.

방법론: MANTRA 프레임워크

MANTRA(Manual-to-Test-Translation) 는 자연어 절차 문서와 도구 스키마에서 준수 벤치마크를 자동으로 합성하도록 설계된 프레임워크입니다. 이는 LLM 생성과 형식 검증을 결합하는 3 단계 파이프라인을 통해 작동합니다:

1. 문서 수집 및 시나리오 생성

• 의존성 그래프 구축: 시스템이 절차 매뉴얼 ($D$) 을 수집하고, 노드가 콘텐츠 청크 (예: 단락) 를 나타내고 엣지가 계층적 및 참조 관계를 나타내는 의존성 그래프 ($G_D$) 를 구축합니다.
• 커버리지 주도 샘플링: 작업 복잡성을 제어하고 광범위한 커버리지를 보장하기 위해 MANTRA 는 $G_D$ 에서 부분 그래프 ($G_{DS}$) 를 샘플링합니다. 작고 밀집된 부분 그래프는 간단한 시나리오를 생성하고, 크거나 느슨하게 연결된 부분 그래프는 여러 규칙이 관련된 복잡한 시나리오를 유도합니다.
• 도구 관련성 및 시나리오 합성: 각 샘플에 대해 LLM 이 관련 도구 ($T_S$) 를 식별하고 구체적인 시나리오 ($\lambda$) 를 생성합니다. 각 시나리오에는 자연어 프롬프트 ($p_\lambda$) 와 변수의 할당값이 포함되며, 여기에는 에이전트를 안내하기 위해 프롬프트에 명시된 내부 상태 변수 (예: "요청이 대기 중임") 가 포함됩니다.

2. 체크 생성 및 세계 모델 생성

준수를 결정론적으로 평가하기 위해 MANTRA 는 각 시나리오에 대해 두 가지 독립적인 산출물을 생성합니다:

• 추적 수준 체크 ($C_\lambda$): LLM 이 필요한 도구 호출, 금지된 호출 및 시간적 순서를 지정하는 부울 체크 집합을 생성합니다 (예: check_inventory 는 assign_warehouse_picker 보다 앞서야 함). 이러한 체크는 구체적인 인수 값으로 근거를 둡니다.
• 기호 세계 모델 ($W_S$): 독립적으로 LLM 이 절차 규칙을 상태 전이 시스템으로 표현하는 세계 모델을 생성합니다. 이 모델은 상태 변수, 도구 전제 조건 및 사후 조건을 정의하는 타입 지정 도메인 특화 언어 (DSL) 로 표현됩니다. 이 추상화는 복잡한 절차 논리의 컴팩트한 표현을 가능하게 합니다.

3. SMT 솔버를 통한 교차 검증

MANTRA 의 핵심 혁신은 생성된 체크와 세계 모델을 교차 검증하기 위해 만족도 이론 (SMT) 솔버 (특히 Z3) 를 사용하는 것입니다.

• 경계 모델 검증: $C_\lambda$ 와 $W_S$ 모두 추적 지평선 $h$ 에 대해 경계 SMT 인코딩 ($b\Phi_h$) 으로 컴파일됩니다.
• 충돌 검색: 시스템은 두 가지 유형의 불일치를 검색합니다:
  1. 전방 충돌: 체크는 만족하지만 세계 모델을 위반하는 추적 (체크가 너무 약하거나 모델이 너무 제한적임을 나타냄).
  2. 후방 충돌: 세계 모델은 만족하지만 특정 체크를 위반하는 추적 (체크가 너무 제한적임을 나타냄).
• 구조화된 수정 루프: 충돌이 발견되면 MANTRA 는 수정 루프를 사용합니다:
  • 세계 모델 해결: 동일한 샘플의 여러 시나리오가 공통 충돌을 공유하는 경우, LLM 이 세계 모델에 대한 공유 수정 (예: 누락된 전제 조건 추가) 을 제안합니다.
  • 체크 해결: 충돌이 지속되면 시스템이 개별 시나리오에 대한 특정 체크를 식별하고 수정합니다.
  • 결정론적 편집: 수정은 잘 형성됨을 보장하기 위해 타입 지정 편집 언어를 통해 적용된 후 재컴파일 및 재검증을 거칩니다.
• 인간 개입 루프: 자동 수정이 설정된 반복 횟수 후 실패하면, 시스템은 구조화된 인간 검토를 위해 해당 시나리오를 플래그로 표시하며, 검토자가 모호함을 수동으로 해결할 수 있습니다.

주요 기여

1. 자동화 파이프라인: 자연어 매뉴얼과 도구 스키마를 제어 가능한 작업 난이도와 결정론적 채점을 갖춘 기계 검증 가능 벤치마크로 변환하는 완전 자동화 파이프라인.
2. 이중 산출물 구성: SMT 솔빙을 통해 교차 검증되는 추적 수준 체크와 기호 세계 모델의 분리. 이는 벤치마크가 수용되기 전에 불일치를 자동으로 식별하고 수정하여 인간 개입을 최소화합니다.
3. 벤치마크 스위트: 6 개 도메인 (운영, Sneaky Sasquatch, 캐빈 안전, 소매, 항공사, 통신) 에 걸쳐 285 개의 다양한 작업을 포함하는 새로운 벤치마크 스위트 생성. 이러한 작업은 최소한의 인간 노력으로 최대 약 16,000 단어의 절차 매뉴얼과 148 개의 도구에 확장됩니다.
4. 세분화된 실패 분석: 프레임워크는 에이전트 실패 모드의 세부적인 디버깅을 가능하게 하는 추적 수준 체크를 제공하여 누락된 호출, 순서 위반 및 금지 행위를 구분합니다.

결과 및 평가

저자들은 MANTRA 프레임워크와 결과 벤치마크를 6 가지 다른 LLM 에이전트를 사용하여 평가했습니다.

• 검증 효율성: SMT 기반 교차 검증은 생성된 테스트 케이스의 상당 부분을 자동으로 성공적으로 검증했습니다. 예를 들어, "운영" 도메인에서는 전방 및 후방 정제 라운드 후 66 개 생성된 사례 중 63 개가 검증되었습니다.
• 에이전트 성능: 평가 결과, 현재 LLM 에이전트는 절차 준수에 어려움을 겪는 것으로 나타났습니다. 성공률은 도메인에 따라 크게 달라졌으며, "소매" 및 "항공사" (τ-Bench 에서) 는 문서 길이보다 복잡한 도구 사용으로 인해 특히 어려웠습니다.
• 실패 모드 분석: 10,895 개의 실패한 체크에 대한 분석 결과, **실패의 76%**가 "필수 호출 누락"(명시된 도구 건너뛰기) 또는 "앵커 누락"(순서 조항의 전제 조건 실행 실패) 으로 인한 것이었습니다.
  • 지배적인 실패 패턴은 "조기 작성"으로, 에이전트가 필요한 읽기 스타일 조회를 수행하기 전에 쓰기 스타일 도구를 호출하는 경우였습니다.
  • Qwen3.6:36B 모델은 "읽기 후 쓰기" 습관을 엄격히 유지함으로써 항공사 및 소매 도메인에서 우수한 성능을 보였으며, 이러한 도메인에서 0% 의 조기 작성률을 달성했습니다.
• 기존 벤치마크와의 비교: 수동 구축이나 LLM 심사자에 의존하는 기존 벤치마크와 달리, MANTRA 는 최소한의 인간 노력으로 대규모 비구조화 문서와 새로운 도메인으로 확장 가능한 결정론적 추적 수준 평가를 제공합니다.

중요성 및 주장

이 논문은 MANTRA 가 자동화된 벤치마크 생성과 형식적으로 근거된 검증 방법을 결합하여 도구 사용 에이전트를 위한 확장 가능하고 신뢰할 수 있는 벤치마크를 만드는 타당성을 입증한다고 주장합니다.

• 신뢰성: SMT 솔버를 사용하여 세계 모델에 대한 체크를 교차 검증함으로써, MANTRA 는 LLM 환각으로 인해 발생할 수 있는 논리적 불일치가 없는 벤치마크를 보장하여 LLM-as-a-judge 접근 방식보다 평가 결과에 대한 더 높은 수준의 신뢰를 제공합니다.
• 확장성: 이 프레임워크는 수동 벤치마크 생성의 확장성 병목 현상을 해결하여 임의의 도메인에서 복잡하고 현실적인 절차 매뉴얼 (최대 50 페이지 이상) 에 대한 에이전트 평가를 가능하게 합니다.
• 디버깅 기능: 추적 수준 체크의 세분성은 연구자들이 단순한 통과/실패 지표를 넘어 에이전트 추론의 특정 구조적 실패 (예: 전제 조건 조회를 건너뛰는 경향) 를 이해할 수 있게 합니다.

저자들은 MANTRA 를 안전한 행동에 대한 독립적인 보장으로 위치시키기보다는, 준수 중요 환경에서 더 신뢰할 수 있는 AI 시스템을 개발하기 위한 핵심 구성 요소로, 기계 학습과 형식 검증 간의 간극을 메우는 것으로 위치시킵니다.