대규모 파운데이션 모델(Large Foundation Models, LFMs)은 인간-컴퓨터 상호작용 분야에서 새로운 가능성을 열어 주었으며, 특히 모바일 GUI(그래픽 사용자 인터페이스)를 대상으로 상호작용할 수 있는 모바일 GUI 에이전트의 등장과 함께 그 가능성이 두드러지고 있다. 이러한 에이전트는 사용자가 간단한 자연어 지시를 통해 복잡한 모바일 작업을 자동화할 수 있게 해준다. 그러나 LFMs의 본질적인 확률적 특성과 모바일 작업의 모호함 및 맥락 의존성이 결합되면서, LFM 기반 자동화는 신뢰성이 낮고 오류가 발생하기 쉽다. 이 중대한 문제를 해결하기 위해, 우리는 VeriSafe Agent(VSA)1를 도입한다. VSA는 모바일 GUI 에이전트를 위한 논리적 기반의 안전장치로서 기능하는 형식 검증(formal verification) 시스템이다. VSA는 에이전트가 행동을 실행하기 전에, 그 행동이 사용자의 의도와 엄밀히 일치하도록 하는 것을 결정론적으로 보장한다. 핵심적으로 VSA는 자연어 기반 사용자 지시를 형식적으로 검증 가능한 명세로 변환하는 새로운 자동 형식화(autoformalization) 기법을 제안한다. 이를 통해 에이전트의 행동에 대해 실행 시(runtime) 규칙 기반 검증을 수행할 수 있으며, 실제로 실행되기 전부터 오류가 있는 행동을 탐지할 수 있다. 우리가 아는 한, VSA는 GUI 에이전트에 형식 검증의 엄밀함을 도입하려는 최초의 시도이며, LFM 기반 행동과 형식 소프트웨어 검증 사이의 간극을 연결한다. 우리는 시판되는 LFM 서비스(GPT-4o)를 사용하여 VSA를 구현하고, 널리 사용되는 18개 모바일 앱에 걸쳐 300개의 사용자 지시에 대해 성능을 평가한다. 그 결과, VSA는 에이전트 행동을 검증하는 데 94.33%–98.33%의 정확도를 달성하며, 기존의 LFM 기반 검증 방법보다 30.00%–16.33% 더 우수한 성능을 보였다. 또한 GUI 에이전트의 작업 완료율(task completion rate)을 90%–130%까지 증가시켰다.

*본 초록은 AI를 통해 원문을 번역한 내용입니다. 정확한 내용은 하기 원문에서 확인해주세요.