AI VIDEO BRIEFING

형식 기법과 로봇 학습의 접점 — 시간 논리로 로봇 행동을 명세하고 실패를 미리 경고하는 법

코넬대 하다스 크레스가지트 교수가 CMU 로보틱스 세미나에서 데이터 기반 로봇 학습과 형식 기법의 강점이 정확히 엇갈린다고 짚었다. 시간 논리로 로봇 행동을 명세하고, 강건성 수치로 실패를 미리 경고하는 방법을 정리했다.

로봇이 데이터로 배우는 시대, 수학적 검증은 무엇을 할 수 있나 영상 대표 이미지

핵심 메시지

  • 데이터 기반 학습은 손재주와 변형물 조작처럼 모델 기반 기법으로 하기 어려운 일을 해내지만, 의미 연결·안전·실패 예측·복구가 약하다.
  • 형식 기법은 그 반대다. 무엇을 하고 무엇을 하지 말아야 하는지 수학적으로 적을 수 있지만 추상화를 사람이 만들어야 하고 확장성이 떨어진다.
  • 로봇에서는 ‘언제나 옳다’는 검증을 고집하는 대신 반증, 실패 예측, 복구로 목표를 옮겨야 한다. 검증 대상이 로봇만이 아니라 환경과 사람까지 포함하기 때문이다.
  • 신호 시간 논리는 만족 여부뿐 아니라 얼마나 만족했는지를 수치로 주고, 그 강건성 값이 희귀한 실패를 찾고 학습된 정책을 비교하는 도구가 된다.
  • 성공률 한 숫자는 실패 양상을 감춘다. 강건성 분포를 보면 어떤 정책이 아예 대상을 건드리지 못하고 지나가는지까지 구분된다.

쉽게 이해하기

코넬대 기계항공공학과 하다스 크레스가지트 교수가 카네기멜런대 로보틱스 인스티튜트 세미나에서 ‘빅데이터 시대의 로봇 형식 기법’을 주제로 발표했다. 그는 로봇 학습 데모 영상을 먼저 틀며 약속과 과장을 함께 짚는다. 두 대의 로봇이 처음 보는 정리 작업을 자율로 해내는 장면은 인상적이지만, 몇 번을 다시 찍었는지 어떻게 실패했는지는 공개되지 않으며 영상 속 부엌은 실제 가정의 부엌과 거리가 멀다는 것이다.

형식 기법은 명세, 개발, 검증을 위한 수학 기반 기법으로 정의된다. 문제는 로봇이 물리적 실체라는 점이다. 2015년 다르파 로보틱스 챌린지 결선 첫날의 실패 모음 영상에서 로봇은 균형을 잃고, 밸브를 잡았다고 판단한 채 엉뚱한 곳에 힘을 준다. 같은 해 인간-로봇 상호작용 학회에서 소개된 일본 쇼핑몰 실험에서는 아이들이 로봇의 길을 막고 발로 차기도 했다. 검증 대상이 로봇 하나가 아니라 로봇과 환경과 사람의 조합이라는 뜻이다.

그래서 발표자는 정의를 조금 바꾼다. 명세는 계속 쓰되 추상화가 따라와야 하고, 모든 픽셀과 모든 위치를 추론할 수는 없으니 문제를 추론 가능한 블록으로 나눠야 한다. 명세와 추상화에서 제어기를 자동으로 만들어내는 합성이 그다음이고, ‘언제나 옳다’는 검증 대신 언제 실패할 것 같은지를 판단하는 반증, 실패가 다가온다는 피드백, 그리고 복구가 목표가 된다.

선형 시간 논리 사례들이 이어진다. 각자 자기 임무만 아는 두 로봇이 서로에 대한 가정이 깨졌을 때 명세 조각을 주고받아 충돌을 자율로 푼다. 군집에서는 추상화를 ‘로봇이 어디 있나’가 아니라 ‘어느 구역에 로봇이 있나’로 바꿔 로봇 수와 무관한 명세를 쓴다. 모듈러 로봇은 계단을 보면 오르고 분홍색을 보면 물건을 놓으라는 높은 수준 명세에 따라 스스로 뱀 형태로 재구성하고 보행 방식을 바꾼다.

신호 시간 논리는 참·거짓 기호 대신 연속 신호 위에 술어와 시간 구간을 쓴다. 테이블에서 팔 길이만큼 떨어져 있으라는 조건을 5분 안이라는 시간과 함께 적을 수 있고, 무엇보다 얼마나 만족했는지를 강건성 값으로 준다. 발표에서는 명세 몇 줄만 고쳐 로봇의 행동을 즉시 바꾸는 데모, 그리고 60초 안에 반대편에 도달하면서 사람이 조종하는 로봇 곁을 지켜야 하는 과제에서 아직 실패하지 않았지만 곧 실패한다는 사전 경고를 띄우는 데모가 이어졌다.

주요 인사이트

  • 확률적 검증은 시뮬레이션을 많이 돌려 실패 횟수를 세는 방식이라 실패가 드물면 무너진다. 아무 실패도 못 찾고 성공률 100퍼센트라고 보고하게 되기 때문이다. 강건성 값과 그 변화를 보며 표본을 실패 쪽으로 몰아주면 몬테카를로보다 정확하게 실패 영역을 찾아낼 수 있었다.
  • 학습된 정책 평가에도 같은 도구가 쓰인다. 접촉 센서 값과 그리퍼 높이를 신호로 두고 ‘접촉 중이면 높이가 일정 값보다 커야 한다’는 명세를 쓰면, 성공률 한 숫자로는 구분되지 않던 여섯 정책의 차이가 드러난다. 강건성이 특정 값에 몰린 정책은 대상을 아예 건드리지 않고 허공을 지나간 것이다.
  • 시뮬레이션 성공률의 임계값 자체가 틀렸을 수 있다는 지적도 나온다. 강건성이 아주 조금 모자라 실패로 집계됐는데 영상으로 보면 멀쩡한 경우가 있고, 그때는 임계값이 지나치게 빡빡한 것이다. 시행 횟수가 적을수록 두어 건 차이가 백분율을 크게 흔든다는 점도 함께 짚었다.
  • 형식 기법의 병목은 추상화다. 기호가 물리 세계의 무엇을 뜻하는지 붙이는 일만 수동이고 그 뒤는 자동이지만, 추상화가 세밀할수록 다룰 수 있는 규모가 줄어드는 맞교환이 존재한다. 그래서 추상화를 학습으로 얻는 방향이 시너지 후보로 제시된다.
  • 자연어 명세에 대한 답은 단호했다. 사람이 쓰기 쉽다는 장점은 분명하지만 언어는 모호하고, 로봇을 제어할 때는 결국 모호하지 않은 것이 필요하다. 자연어에서 형식 표현으로 옮긴 뒤 그 뜻을 여러 설명으로 되돌려 확인하는 왕복이 필요하며, 가정용 로봇처럼 언어가 중요한 영역과 도메인이 좁아 언어를 제한해야 하는 영역이 다르다고 봤다.
  • 안전 모니터를 학습으로 만들면 검증기 자체를 검증해야 하는 순환 문제가 생기지 않느냐는 질문에는, 하나로 모든 것을 푸는 반지는 없다는 답이 돌아왔다. 학습 기반과 명세 기반 각각의 실패 양상이 다르므로 여러 기법의 앙상블로 신뢰를 쌓아야 한다는 것이다.

자주 묻는 질문

형식 기법이란 무엇인가요?

소프트웨어와 하드웨어의 명세, 개발, 그리고 수동 또는 자동 검증을 위한 수학 기반 기법을 가리키는 컴퓨터과학의 한 분야입니다. 시스템이 무엇을 해야 하고 무엇을 하지 말아야 하는지를 수학적 언어로 적고, 실제로 그렇게 동작하는지 증명하려 합니다.

선형 시간 논리와 신호 시간 논리는 어떻게 다른가요?

선형 시간 논리는 참 또는 거짓인 기호를 시간에 따라 연결해 ‘항상’이나 ‘언젠가’ 같은 조건을 씁니다. 신호 시간 논리는 연속 신호 위에 술어를 쓰고 5초 이내 같은 시간 구간과 거리 값을 넣을 수 있으며, 만족 여부뿐 아니라 얼마나 만족했는지를 강건성 값으로 알려줍니다.

로봇을 완전히 검증하는 일이 가능한가요?

발표자는 로봇과 사람과 환경이 함께 있는 상황에서 로봇이 항상 옳게 행동한다는 검증은 믿지 않는다고 말합니다. 대신 언제 실패할 것 같은지를 판단하는 반증, 실패가 임박했다는 사전 경고, 그리고 이미 벌어진 실패를 고치는 복구로 목표를 옮깁니다.

형식 기법이 데이터 기반 학습을 대체하나요?

아닙니다. 발표의 결론은 두 접근의 강점과 약점이 서로 엇갈린다는 것입니다. 안전 필터와 안전 실드, 학습 과정의 제약, 실패 예측과 모니터링, 명세로부터의 데이터 생성처럼 양쪽이 서로를 돕는 자리가 있고 모든 문제를 푸는 단일 해법은 없다고 봅니다.

원문과 출처

이 글은 원본 영상의 자막을 바탕으로 한국어 독자를 위해 요약했습니다. 전체 맥락과 최신 정보는 원문에서 확인하세요.

YouTube 원본 영상 보기 ↗

관련 AI 소식