기술 요약: SENTINEL

문제 정의

기초 모델(Foundation Models, FMs)을 체화된 에이전트(embodied agents)에 통합하는 것은 계획 수립 및 인간-로봇 상호작용 능력을 확장시켰으나, 동시에 안전 위험을 증폭시켰다. 기존의 FM 기반 에이전트 평가 벤치마크는 주로 작업 완료 지표(예: 성공률)에 집중하며, 물리적 위험을 단순한 작업 실패가 아닌 별도의 안전 위반 사항으로 취급하지 않는 경우가 많다. 현재의 안전 평가 방식은 휴리스틱 규칙이나 주관적인 FM 기반 판단(LLM-as-Judge)에 크게 의존하고 있으며, 이는 엄격한 정의가 부족하고 에이전트 파이프라인의 서로 다른 단계(의미론적 오해, 안전하지 않은 계획 생성, 또는 안전하지 않은 물리적 실행)에서 발생하는 실패를 구분하지 못한다. 또한, 이러한 방식은 특정 수준에서 안전 위반이 어디서 기원했는지 국지화(localize)하는 데 어려움을 겪는다.

방법론

저자들은 SENTINEL(Safety EvaluatioN framework with Temporal logics for INterpretable Embodied foundation modeL-based agents)을 제안한다. 이는 물리적 안전을 시계열 논리(temporal logic) 명세에 접지(grounding)시킨 다층적 형식 프레임워크이다. 이 프레임워크는 시뮬레이션 환경(VirtualHome 및 AI2-THOR) 내에서 작동하며, 세 가지 점진적인 수준에 걸쳐 에이전트를 평가한다:

1. 형식적 안전 명세 (Formal Safety Specification)

SENTINEL은 자연어 안전 제약 조건을 시계열 논리(Temporal Logic) 공식, 구체적으로 선형 시계열 논리(LTL)와 계산 트리 논리(CTL)로 인코딩한다.

• 상태 불변성(State Invariants): 모든 시간 동안 안전하지 않은 상태를 금지하는 제약 조건 (예: 충돌 방지를 위한 $G(\neg p)$).
• 순서 제약(Ordering Constraints): 적절한 행동 순서를 강제하는 제약 조건 (예: "결국 꺼야 함"을 위한 $G(p \to F q)$).
• 분류: 안전 규칙은 상태 불변성과 순서 제약으로 분류되며, 시뮬레이션 내 객체의 속성에서 유도된 원자 명제(atomic propositions)에 매핑된다.

2. 다층 평가 파이프라인 (Multi-Level Evaluation Pipeline)

이 프레임워크는 실패를 점진적으로 필터링하고 위반 사항을 국지화하기 위해 3단계 파이프라인을 채택한다:

• 의미론적 수준 평가 (Semantic-Level Evaluation):

  • 목표: 자연어 안전 요구사항을 형식적인 LTL 공식으로 번역하는 FM의 능력을 평가한다.
  • 방법: 에이전트에게 안전 제약 조건을 프롬프트로 제공하고 후보 LTL 공식을 생성하게 한다. 생성된 공식은 구문 검사와 뷔키 오토마타(Büchi automata) 및 언어 포함 관계 검증을 통해 정답(ground-truth) LTL 명세와 비교된다.
  • 출력: 구문 오류, 의미론적 비동등성, 그리고 성공적인 해석에 대한 지표.

• 계획 수준 평가 (Plan-Level Evaluation):

  • 목표: 실행 전 고수준 행동 계획과 하위 목표를 LTL 제약 조건에 대해 검증한다.
  • 방법: 에이전트는 고수준 계획(마일스톤 하위 목표들)을 생성한다. 이 계획은 안전하지 않은 기호적 순서나 누락된 전제 조건을 탐지하기 위해 LTL 공식과 대조된다. 행동 공간 내에서 계획의 실행 가능성을 검증하기 위해 너비 우선 탐색(BFS)이 사용된다.
  • 출력: 작업 목표는 만족하지만 안전 제약 조건은 위반하는 안전하지 않은 계획의 식별.

• 궤적 수준 평가 (Trajectory-Level Evaluation):

  • 목표: 분기되는 결과와 환경 역학을 고려하여 계획의 물리적 실행을 평가한다.
  • 방법: 고수준 계획을 바탕으로 시뮬레이터로부터 여러 실행 궤적을 샘플링한다. 이 궤적들은 하나의 **계산 트리(Computation Tree, $T$)**로 병합된다. 안전 요구사항은 분기 시간 속성을 평가하기 위해 L مدل LTL에서 CTL로 격상된다.
  • 검증: CTL 모델 체커가 트리($T$)에 대해 속성(예: "모든 경로가 항상 $\phi$를 만족함"을 의미하는 $AG \phi$)을 검증한다.
  • 출력: 실행 의존적 위반 탐지 및 반례 경로(실패를 유발하는 특정 상태 또는 시퀀스) 생성.

3. 피드백 기반 정교화 (Feedback-Driven Refinement)

SENTINEL은 궤적 수준 검사 중에 생성된 반례를 활용하여 에이전트에게 검증 가능한 피드백을 제공한다. 이 피드백 루프를 통해 에이전트는 근본적인 에이전트 구조를 수정하지 않고도 안전성을 개선하기 위해 계획을 반복적으로 정교화할 수 있다.

주요 기여

1. 형식적이고 해석 가능한 안전 명세: 본 연구는 직관적인 안전 요구사항을 LTL 및 CTL에 접지함으로써, 휴리스틱한 판단 대신 명시적인 분류(상태 불변성, 시간적 의존성)와 형식적 검증을 가능하게 한다.
2. 통합된 다층 형식 안전 평가: SENTINEL은 의미론적 해석, 계획 생성, 물리적 실행에 걸쳐 안전성을 점진적으로 평가하는 최초의 프레임워크이다. 이 설계는 실패를 특정 단계(이해 vs 추론 vs 실행)로 국지화할 수 있게 한다.
3. 교차 수준 경험적 분석: 저자들은 VirtualHome과 AI2-THOR에 SENTINEL을 적용하여 안전 중심 요구사항을 포함하도록 과업을 확장했다. 이를 통해 안전 위반이 서로 다른 수준(예: 의미론적 오해 vs 저수준 컨트롤러 오류)에서 기인할 수 있음을 입증했으며, 형식적 평가가 작업 성공률만을 보는 벤치마크에서는 보이지 않는 실패 모드를 드러낸다는 것을 보여주었다.

실험 결과

저자들은 여러 폐쇄형 모델(GPT-5, Claude-Opus, Gemini)과 오픈 소스 모델(DeepSeek, Qwen, Mistral, Llama), 그리고 시각-언어 모델(VLM)을 평가하였다.

• 의미론적 수준: 규모가 큰 모델들이 작은 오픈 소스 모델들에 비해 자연어를 LTL로 번역하는 데 있어 현저히 높은 성능을 보였다. 그러나 강력한 모델들조차 전역적 금지(global prohibitions)에 비해 조건부 금지(conditional prohibitions)를 처리하는 데 어려움을 겪었다.
• 계획 수준: 의미론적 동등성 비율이 높은 모델들이 계획 수준에서 더 높은 안전율을 유지했다. 그러나 명시적인 안전 가이드(LTL 프롬프트)를 추가하는 것이 안전 지표를 개선하기는 했으나, 모든 위반을 제거하지는 못했다.
• 궤적 수준:
  • LLM vs VLM: VLM 기반 에이전트는 시각적 접지(visual grounding)가 물리적 위험 감지를 도와주기 때문에 텍스트 전용 LLM보다 일반적으로 더 높은 안전율을 달acia 달성했다. 그러나 VLM은 종종 더 낮은 작업 성공률을 보였는데, 이는 안전 능력과 작업 수행 능력 사이의 트레이드오프를 나타낸다.
  • 실행 실패: "성공 및 안전(Success & Safety)" 지표가 계획 수준에서 궤적 수준으로 넘어갈 때 상당한 하락이 관찰되었으며, 이는 많은 실패가 저수준 행동 인자(action arguments)와 컨트롤러의 안전 메커니즘 부재에서 기인함을 시사한다.
• 안전성 개선: 정교화 루프 실험에서, SENTINEL의 검증 가능한 반례 피드백은 LLM-as-Judge 베이스라인보다 훨씬 더 큰 안전 지표 개선(약 2배)을 이끌어내는 동시에, 작업 성공률은 유사한 수준으로 유지했다. 분석 결과, LLM-as-Judge 베이스라인은 실제 안전하지 않은 궤적을 놓치는 경우가 많았으나(한 연구에서 83%의 미탐지율), SENTINEL의 형식적 검사는 더 신뢰할 수 있었다.
• 효율성: 병합된 계산 트리 상에서의 CTL 기반 검증이 독립적인 LTL 검증보다 더 효율적이며, 궤적 수가 증가함에 따라 속도 향상이 커지는 것으로 나타났다.

의의 및 주장

본 논문은 SENTINEL이 FM 기반 체화된 에이전트의 안전성을 체계적으로 평가하기 위한 엄격한 토대를 제공한다고 주장한다. 휴리스틱하거나 주관적인 판단을 넘어, 이 프레임워크는 다음을 제공한다:

• 국지화(Localization): 안전 실패가 명령 오해, 안전하지 않은 계획 생성, 또는 안전하지 않은 행동 실행 중 어디에서 발생하는지 정확히 짚어낼 수 있는 능력.
• 실행 가능한 피드백(Actionable Feedback): 정교화 루프를 통해 의미 있는 안전 개선을 이끌어낼 수 있는 검증 가능한 반례 생성.
• 확장성(Scalability): 샘플링된 궤적으로부터 구성된 계산 트리 상에서의 CTL 사용은, 복잡한 물리적 환경에서 전체 상태 모델 검사(full-state model checking)의 불가능함을 피하면서도 실용적인 트레이드오프를 제공하는, 샘플링 기반의 실증적 위반 탐지 방식을 제시한다.

저자들은 SENTINEL이 완전한 검증(certified verification)보다는 **경험적 탐지(empirical detection)**를 제공한다는 점을 명시하며, 이는 샘플링된 궤적으로 구성된 유한한 계산 트리 상에서 작동하기 때문이다. 샘플 수가 충분하지 않을 경우 위반을 놓칠 가능성이 있음을 인정하지만, 이 접근 방식이 통계적 모델 검사(statistical model checking)에 더 가까우며, FM의 블랙박스 특성과 물리적 환경의 복잡성을 고려할 때 필수적이라고 주장한다. 이 프레임워크는 검증 가능한 안전 벤치마크와 안전 인지 강화 학습 보상(safety-aware RL rewards)을 향한 단계로 제시된다.