LLM 기반 사이버-물리 시스템 반례 탐색 기술 개발
Large Language Models as Falsifiers for Cyber-Physical Systems
arXiv사이버-물리 시스템(CPS)의 안전성 검증을 위해 대규모 언어 모델(LLM)을 활용하여 반례를 탐색하는 새로운 기법이 개발되었습니다.
- 연구진은 LLM에게 단순히 최적화 명령만 내리는 것이 아니라, 자연어 이름이나 궤적 같은 의미론적 정보를 제공해 효율성을 극대화했습니다.
- 이는 복잡하고 신뢰성이 중요한 CPS의 안전성 검증 과정을 혁신적으로 개선하며 관련 산업에 큰 기술적 진전을 가져올 것으로 기대됩니다.
- 실제 벤치마크 테스트에서 기존의 다양한 최적화 기법들을 능가하는 성능을 입증하며, LLM 기반 검증 도구의 높은 가능성을 보여줍니다.
사이버-물리 시스템(CPS)에서 안전성 검증을 위해 형식 명세(formal specifications)의 반례를 찾는 '반례 탐색(Falsification)' 기법이 연구되었습니다. Signal Temporal Logic (STL)으로 작성된 명세를 활용하는 이 과정은 전통적으로 블랙박스 검색 알고리즘을 통해 견고성 최적화 문제로 다루어져 왔습니다. 본 연구에서는 (LLM)의 최근 효과적인 최적화 능력을 결합하여, STL 견고도 정도를 최소화함으로써 명세를 반례 탐색하는 LLM-Falsifier라는 새로운 접근 방식을 제시했습니다.
기존의 일반적인 기반 최적화를 넘어, 이 연구의 핵심 아이디어는 LLM에게 자연어 모델에 적합하지만 표준 수치 최적화 도구에는 부재했던 의미론적 정보를 노출하는 것입니다. 구체적으로 자연어 입력 및 출력 이름, 출력 궤적(trajectories), 그리고 최소 견고도 값을 위한 임계 시간 증인(critical-time witnesses) 등의 정보가 추가되었습니다. 이러한 요소들은 LLM 기반의 견고성 탐색을 더욱 지능적이고 샘플 효율적으로 만듭니다.
실제 ARCH-COMP 반례 탐색 에서, LLM-Falsifier는 기존의 다양한 최적화 패러다임(대리 모델 기반 및 베이즈 최적화 등)과 비교했을 때 우수한 성능을 보였습니다. 평균 시뮬레이션 횟수로 측정했을 때, 총 21개의 명세 중 14개에서 반례를 찾는 데 기존 도구들을 능가하는 결과를 입증했습니다.
용어 풀이
- 대규모 언어 모델
- 방대한 글을 학습해 문장을 이해하고 만들어 내는 AI 모델. ChatGPT, Claude, Gemini가 여기에 속해요.
- 프롬프트
- AI에게 주는 지시나 질문 글.
- 벤치마크
- 모델 성능을 같은 조건에서 비교하려고 만든 시험 문제 모음.