💻 computer science

VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents

VASO는 파운데이션 모델의 가중치를 수정하지 않고도 반례를 사용하여 시간적 안전 사양에 대해 재사용 가능한 기술을 반복적으로 정제함으로써, 최소한의 최적화 샘플만으로 물리적 에이전트에 대해 높은 준수성을 달현하며, 형식 검증을 통해 LLM이 생성한 로봇 기술 계약의 자기 진화를 가능하게 하는 새로운 프레임워크이다.

원저자: Yunhao Yang, Neel P. Bhatt, Kevin Wang, Samuel Tetteh, Zhangyang Wang, Ufuk Topcu

게시일 2026-06-05

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Yunhao Yang, Neel P. Bhatt, Kevin Wang, Samuel Tetteh, Zhangyang Wang, Ufuk Topcu

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

VASO에 대한 설명: 쉬운 언어와 창의적인 비유를 활용하여

거대한 문제: 신뢰할 수 없는 "똑똑한" 로봇

당신이 매우 유능하고 창의적인 요리사(AI)를 고용하여 로봇 주방을 위한 레시피(기술)를 작성하게 한다고 상상해 보세요. 이 요리사는 몇 초 만에 "샌드위치 만들기"나 "고양이 피하기"와 같은 레시피를 써낼 수 있습니다.

하지만 함정이 있습니다: 레시피가 영어로 읽기에 그럴듯하다고 해서, 로봇이 집을 태워 먹지 않을 것이라는 보장은 없습니다.

기존 방식들은 로봇이 레시피를 직접 실행해 보게 하고, 실패하면 요리사에게 다시 써달라고 요청하는 방식으로 이를 해결하려 합니다. 이는 마치 국 맛을 보고 "너무 짜니까 다시 만들어 봐"라고 말하는 것과 같습니다. 하지만 이 방식은 국이 '이번 한 번' 짰다는 사실만 알려줄 뿐입니다. (예를 들어 가스레인지가 너무 뜨거워지거나, 조리대 위로 고양이가 뛰어오르는 등의) 모든 가능한 상황에서도 레시피가 안전할 것이라는 점은 증명하지 못합니다.

해결책: VASO (수학적 편집자)

저자들은 로봇 레시피를 위한 엄격한 수학적 편집자 역할을 하는 시스템인 VASO를 소개합니다. 단순히 국 맛을 보는 대신, VASO는 깨뜨릴 수 없는 안전 법칙(예: "불에 손대지 마라" 또는 "사람이 근처에 있으면 항상 멈춰라")에 따라 레시피를 검토합니다.

VASO의 작동 단계는 다음과 같습니다.

1. "번역기" (가교 역할)

로봇은 "코드"(왼쪽으로 이동, 정지, 속도 높임)로 말하지만, 안전 규칙은 "논리"(사람이 보이면, 그러면 정지)로 작성됩니다.

비유: 로봇은 "로봇어"만 할 줄 아는 외국인이고, 안전 검사관은 "논리어"만 할 줄 아는 상황을 상상해 보세요.
VASO의 역할: VASO는 로봇의 움직임을 논리적 문장으로 즉시 변환하는 **번생기(labeling function)**라는 번역기를 만듭니다. 이를 통해 안전 검사관이 로봇이 정확히 무엇을 하고 있는지 이해할 수 있게 합니다.

2. "수학적 검증" (형식 검증)

로봇이 레시피를 실행하기도 전에, VASO는 수학적 시뮬레이션을 실행합니다.

비유: 이것은 조종사를 위한 비행 시뮬레이터와 같습니다. 비행기가 이륙하기 전, 시뮬레이터는 비행 계획이 산에 충돌하는지 확인하기 위해 수백만 개의 시나리오를 실행합니다.
VASO의 역할: VASO는 레시피가 안전 규칙을 어길 가능성이 있는지 확인합니다. 만약 수학적으로 "예, 이 레시피는 충돌할 수도 있습니다"라는 결과가 나오면, 단순히 "실패"라고만 하지 않습니다. 대신 정확히 어느 순간에 충돌이 발생하는지(반례, counterexample)를 찾아냅니다.

3. "텍스트 그래디언트" (피드백 루프)

이것이 핵심적인 마법 같은 부분입니다. 보통 수학적 검증이 실패하면 코드 전체를 다시 써야 합니다. 하지만 VASO는 더 똑똑합니다.

비유: 수학적 검증 결과가 요리사에게 다음과 같은 쪽지를 보내는 것과 같습니다: "당신의 레시피는 사람이 있을 때도 '앞으로 걷기'라고 되어 있습니다. 이 부분을 '멈추기'로 수정하세요."
VASO의 역할: VASO는 수학적 실패를 텍스트 지시 사항(텍스트 그래디언트)으로 변환합니다. 이는 AI 요리사에게 오류를 수정하기 위해 레시피 자체를 어떻게 다시 써야 하는지 정확히 알려줍니다.
중요한 세부 사항: AI 요리사의 두뇌(기저 모델)는 그대로 유지됩니다. 우리는 요리사를 재학습시키는 것이 아니라, 그들이 작성한 특정 레시피 카드를 편집하는 것뿐입니다.

이것이 왜 중요한가

이 논문은 두 가지 실제 로봇, 즉 지상 로봇(강력한 성능의 로보락 같은 형태)과 드론을 대상으로 테스트했습니다.

결과: VASO는 100번 미만의 시도로 로봇이 안전 규칙을 97.2%의 확률로 준수하도록 만들었습니다.
비교: 단순히 AI에게 다시 시도하라고 요청하거나, AI의 두뇌를 재학습시키는 다른 방식들은 안전성이 떨어지거나 훨씬 더 많은 시간과 컴퓨팅 자원을 소모했습니다.

"자기 진화(Self-Evolving)" 부분

논문에서는 이를 "자기 진화하는 기술(Self-Evolving Skills)"이라고 부릅니다.

과거 방식: 로봇에게 백만 개의 사례를 학습시켜 일반적인 "감"을 익히게 합니다.
VASO 방식: 로봇에게 특정 기술(예: "운전하기")을 주고, 수학적으로 검증한 뒤, 결함을 찾아내어 기술의 정의를 업데이트합니다. 이제, 그 동일한 기술은 미래의 모든 작업에서 더 안전하게 작동합니다. 이는 마치 자동차 한 대를 고치는 것이 아니라, 자동차 엔진의 설계도를 업그레이드하여 그 설계도로 만들어지는 모든 자동차가 더 안전하게 만드는 것과 같습니다.

한 문장 요약

VASO는 수학적 증명을 사용하여 로봇 지침의 결함을 찾아내고, 그 결함을 간단한 텍스트 피드백으로 변환하며, AI의 두뇌를 재학습시키지 않고도 로봇의 "기술 레시피"를 자동으로 수정하여 완벽하게 안전하게 만드는 시스템입니다.

이 논문이 주장하지 않는 것 (한계점)

이 시스템이 의료 수술이나 생사가 걸린 결정에 작동한다고 주장하지 않습니다 (테스트는 내비게이션과 드론을 대상으로 진행되었습니다).
로봇이 안전을 "의식"하거나 "이해"한다고 주장하지 않습니다. 로봇은 단지 수학적으로 검증된 규칙을 따를 뿐입니다.
이 시스템이 모든 가능한 로봇 시나리오에 즉각적으로 작동한다고 주장하지 않습니다. 이는 "번역기(labeling function)"가 올바르게 작성되어 있다는 것에 의존합니다. 만약 번역기가 실수를 한다면, 수학적 검증은 잘못된 안전 신호를 줄 수 있습니다.

기술 요약: VASO – 물리적 AI 에이전트를 위한 형식적으로 검증 가능한 자기 진화형 스킬

문제 정의

재사용 가능한 로봇 스킬은 파운데이션 모델과 물리적 제어 사이의 인터페이스 역할을 하며, 임바디드 에이전트(embodied agents)가 안전 제약 조건 하에서 장기적인 과업을 수행할 수 있도록 합니다. 파운데이션 모델은 자연어를 통해 이러한 스킬을 생성하는 비용을 낮추었지만, 스킬 보증(skill assurance) 문제는 해결하지 못했습니다. 기존의 자기 진화 방식은 실행 결과, 단위 테스트, 환경 보상 또는 LLM의 자기 비판과 같은 "소프트(soft)" 피드백 신호에 의존합니다. 이러한 신호는 샘플링된 실행 사례에서는 스킬이 작동했음을 보여주는 **트레이스 수준의 증거(trace-level evidence)**만을 제공할 뿐, 테스트되지 않은 조건에서도 스킬에 의해 유도된 계획이 시간적 안전 계약(temporal safety contracts)을 준수한다는 것을 보장하지 못합니다. 로보틱스에서 단 한 번의 드문이지만 심각한 안전 위반(예: 사람을 감지한 후 지상 로봇이 움직이는 경우)은 용납될 수 없으나, 소프트 피드백은 이러한 엣지 케이스를 탐지하는 데 실패하는 경우가 많습니다.

핵심 과제는 단순히 안전하지 않은 계획을 필터링하거나 모델 가중치를 미세 조정하는 것을 넘어, 형식적 검증(formal verification)과 스킬 진화 사이의 루프를 닫는 것입니다. 즉, 형식적 반례(counterexamples)가 직접적으로 재사용 가능한 스킬 계약을 업데이트하여, 개선 사항이 검사 가능하고 재사용 가능하며 검증 가능하도록 보장하는 표현 방식이 필요합니다.

방법론: VASO 프레임워크

저자들은 LLM이 생성한 로봇 스킬 계약의 자기 진화를 위한 폐쇄 루프 프레임워크인 **VASO(Verification-Guided Automated Skill Optimization)**를 제안합니다. VASO는 스킬을 형식적 인터페이스와 플래너 지향 인터페이스를 결와한 시맨틱 계약(semantic contracts)으로 취급하여 작동합니다.

1. 검증 가능한 스킬 표현

스킬 $sk $는 튜플$ (G, \psi_{sk}, C_{sk})$로 정의됩니다:

$G$ (Global Specifications): 항상 준수되어야 하는 안전 제약 조건을 나타내는 LTL 공식들의 집합.
$\psi_{sk}$ (Local Rule): 스킬의 구체적인 의도나 목표를 정의하는 LTL 공식.
$C_{sk}$ (Semantic Contract): 다음 요소들로 구성된 핵심 구성 요소:
- $L_{sk}$ (Proposition-Aligned Labeling Function): 저수준 로봇 상태, 관측값 및 제어 명령을 원자적 논리 명제(atomic logical propositions)로 매핑하는 함수. 이는 물리적 실행과 기호적 모델 체킹 사이의 간극을 메웁니다.
- $C^p_{sk}$ (Text-Based Plan Template): 플래너가 실행 가능한 명령(예: API 호출 또는 궤적)을 생성하도록 유도하는 행동 사전 지식(behavioral prior).

2. 2단계 검증 루프

VASO는 스킬을 정교화하기 위해 계층적 검증 프로세스를 채택합니다:

스킬 수준 검증 (Feasibility Check): 계획을 샘플링하기 전에, 프레임워크는 로컬 룰 $\psi_{sk}$ 가 글로벌 사양 $G$ 와 논리적으로 일치하는지 확인합니다. 이를 위해 유니버설 전이 시스템(universal transition system)이 구축됩니다. 만약 로컬 룰이 글로벌 안전성을 위반한다면(예: 사람이 관찰되었을 때 움직임을 명령하는 규칙), 해당 스킬은 거부되며 파운데이션 모델에 로컬 룰을 정교화하도록 질의합니다.
계획 수준 검증 (Behavioral Check): 실행 가능한 스킬을 얻으면, 플래너가 실행 가능한 계획 $\pi$ 를 생성합니다. 이 계획은 라벨링 함수 $L_{sk}$ 를 사용하여 기호적 전이 시스템(automaton)으로 컴파일됩니다. 모델 체커(NuSMV)는 $G \land \psi_{sk}$ 에 대해 계획을 검증합니다.

3. 텍스트 그래디언트를 통한 최적화

검증에 실패하면, 모델 체커는 **반례 트레이스(counterexample trace)**를 반환합니다. VASO는 이 트레이스를 텍스트 그래디언트(예: "명세 위반: $G(\text{person\_observed} \to X \text{ stop})$ ")로 변환합니다. 이 텍스트 피드백은 시맨틱 계약 $C_{sk}$ 와 로컬 룰 $\psi_{sk}$ 를 업데이트하기 위해 파운데이션 모델에 입력됩니다.

핵심 제약: 파운데이션 모델의 가중치는 **동결(frozen)**된 상태를 유지합니다. 최적화는 모델 파라미터나 단일 태스크 프롬프트를 튜닝하는 것이 아니라, 오직 프롬프트/계약 수준에서 이루어지며, 재사용 가능한 스킬 아티팩트를 정교화합니다.
프로세스: 루프는 순방향 생성(Contract $\to$ Plan $\to$ Automaton)과 역방향 정교화(Automaton $\to$ Textual Gradient $\to$ Updated Contract)를 교대로 수행합니다.

주요 기여

검증 가능한 자기 진화형 스킬 표현: 본 논문은 시간 논리 사양, 명제 정렬 로봇 시맨틱스, 그리고 플래너 지향 템플릿을 명시적으로 연결하는 스킬 구조를 도입합니다. 이를 통해 LLM이 생성한 스킬이 계획에 사용되면서도 동시에 형식적 검증에 노출될 수 있도록 합니다.
최적화 피드백으로서의 형식적 반례: 저자들은 반례 트레이스가 텍스트 그래디언트로 변환되는 2단계 검증 루프를 개발했습니다. 이를 통해 특정 계획을 단순히 거부하거나 프롬프트를 튜닝하는 것이 아니라, 재사용 가능한 스킬 계약 자체를 정교화할 수 있습니다.
물리적 에이전트 검증: 본 프레임워크는 실제 로봇 플랫폼(Clearpath Jackal 및 PX4 quadcopter)에서 검증되었으며, 최적화된 스킬이 파운데이션 모델을 미세 조정하지 않고도 높은 형식적 사양 준수율을 달성함을 입증했습니다.

실험 결과

프레임워크는 두 가지 로봇 플랫폼에서 400개의 생성된 계획에 대해 11개의 시간 논리 사양을 대상으로 평가되었습니다.

준수율: VASO는 100개 미만의 최적화 샘플(스킬당 20분 미만)을 사용하여 97.2%의 형식 사양 준수율을 달성했습니다.
비교: VASO는 제로샷 베이스라인, 프롬프트 최적화 방법(LAD-VF 등), 그리고 미세 조정 기반 접근 방식(RLVF 등)보다 우수한 성능을 보였습니다. 특히, VASO는 미세 조정 방식보다 더 높은 안전 점수에 도달하면서도 훨씬 적은 비용과 시간만을 소요했습니다.
일반화: 최적화된 스킬은 동일한 태스크 패밀리 내의 미학습 태스크 프롬프트에 대해 강력한 일반화 능력을 보여주었으며, 추가적인 정교화 없이도 높은 안전성과 태스크 완료율을 유지했습니다.
자동 정렬: 연구 결과, 자동으로 생성된 명제 정렬 라벨링 함수가 수작업으로 제작된 매핑과 대등한 성능을 보였음을 확인하였으며, 이를 통해 기호적 추상화를 정의하는 데 필요한 수동 도메인 전문 지식의 필요성을 제거했습니다.

의의 및 주장

본 논문은 물리적 AI 에이전트를 위한 형식적 검증과 자기 진화형 LLM 생성 스킬 사이의 루프를 닫은 최초의 프레임워크라고 주장합니다.

패러다임의 전환: 검증된 계획을 일회성 계획을 위한 통과/실패 필터로만 사용하는 표준 검증 계획 파이프라인과 달리, VASO는 거절의 이유(반례)를 사용하여 계획의 근원(재사용 가능한 스킬)을 개선합니다.
효율성 및 안전성: 모델 가중치가 아닌 스킬 계약을 최적화함으로써, VASO는 검사 가능하고 다양한 태스크에 재사용 가능한 더 안전하고 신뢰할 수 있는 행동을 생성하는 메커니즘을 제공하며, 이는 물리적 AI의 핵심 병목 현상인 스킬 보증 문제를 해결합니다.
한계점: 저자들은서 형식적 보증이 AI가 생성한 명제 정렬 라벨링 함수의 정확성에 조건부임을 인정합니다. 저수준 역학을 기호적 명제로 매핑하는 과정에서 오류가 발생하면 잘못된 검증 결과가 나올 수 있으나, 실험 데이터에 따르면 이러한 현상은 매우 드물게 발생하며(안전 점수 저하 <1%), 현재 프레임워크는 순차적, 비동시적 실행을 가정합니다.