UPPAAi, LLM과 형식 검증 도구 결합

ai.euno.news 자동 뉴스 요약

UPPAAi 연구진이 대규모 언어 모델(LLM)을 활용해 실시간·사이버물리 시스템의 모델링부터 검증, 분석, 합성까지 지원하는 통합 접근법을 제안했다. 핵심 원칙은 역할 분담이다. 사용자가 작업을 요청하면 LLM이 해법을 제안하고 설명하며 도구 사용을 조율하고, 형식 검증 도구 UPPAAL이 결과의 타당성을 확인한다.¹

UPPAAL은 30년 넘게 실시간·사이버물리 시스템을 모델링하고 분석하는 데 쓰였다. 그러나 적절한 모델을 만들고, 검증할 속성을 형식화하며, 분석 기법을 고르고, 반례를 해석하는 과정에는 상당한 전문성이 필요하다. 이 작업들은 한 번에 끝나지 않고 모델과 명세를 거듭 고치는 방식으로 진행된다. UPPAAi는 이 반복 과정에 대화형 인터페이스를 결합해 사용자가 LLM과 함께 모델을 작성·설명·디버깅하고 명세하도록 설계됐다.¹

이를 위해 연구진은 UPPAAL의 편집기와 질의 기능, 검증기를 도구 API(Tools API)로 공개했다. LLM은 자연어 답변만 내놓는 데 그치지 않고 이 기능들을 호출해 작업 흐름을 구성한다. 다만 최종 판정까지 LLM에 맡기지는 않는다. LLM이 그럴듯하지만 틀린 설명이나 해법을 만들 수 있다는 한계를 전제로, 검증 가능한 부분은 UPPAAL이 담당하게 했다. 생성 능력과 형식 검증을 결합한 구조가 UPPAAi의 중심이다.¹

논문은 초보자에게 모델을 설명하는 사례부터 제어기 학습까지 모두 7개 사례 연구를 제시했다. 대상에는 시간 오토마타(timed automata), 확률적 하이브리드 오토마타(stochastic hybrid automata), 전략 학습이 포함됐다. 연구진은 LLM이 해법 생성뿐 아니라 사용자가 요청하지 않은 관련 UPPAAL 기능을 먼저 제안하는 데도 큰 도움이 됐다고 보고했다.¹

다만 공개된 초록에는 사례별 정확도나 기존 방식과의 정량 비교가 제시되지 않았다. 따라서 UPPAAi가 전문가의 작업량을 얼마나 줄이는지, 서로 다른 LLM에서도 같은 수준의 지원을 제공하는지는 이 자료만으로 판단하기 어렵다. 논문 역시 완성된 자동화 체계라기보다 LLM 보조 형식공학을 향한 접근법으로 UPPAAi를 제시한다.

읽기 목록은 이 브라우저에 저장됩니다.