Skip to content

VeriSafe Agent

Jump to bottom
duncan020313 edited this page Nov 25, 2025 · 2 revisions

VeriSafe Agent: 안전한 모바일 GUI 에이전트를 위한 논리 기반 에이전트 행동 검증

1. 개요

AI 에이전트는 사용자 지시를 이해하고 자동 수행하는 지능형 소프트웨어로, 현실 세계에 직접적인 영향을 미칠 수 있어 안전성 보장이 필수적이다. 그러나, 현재 에이전트의 안전을 보장하기 위한 방법은 또 다른 언어 모델에 의존하거나, 단순히 샌드박스 환경에서 에이전트를 실행하는 것에 그치고 있다. 이러한 한계를 극복하기 위해 최초의 논리식 기반의 에이전트 행동 검증 시스템 VeriSafe Agent1을 제안한다. VeriSafe Agent는 기존 방법 대비 검증 정확도 38.2% 향상, 비용 효율은 25.8배 향상되었다.

2. AI 에이전트의 위험성

AI 에이전트는 사용자의 지시사항을 입력으로 받아 의도를 이해하고 이를 자동으로 수행하는 지능형 소프트웨어다. 사용자의 지시사항을 수행하는 과정에서 단순히 텍스트 응답을 반환하는 것을 넘어 스스로 기존 인프라, 소프트웨어를 활용하면서 목표를 달성해나간다. 이러한 외부 도구 사용을 통해 에이전트는 현실 세계에 직접적으로 영향을 미칠 수 있다. 에이전트가 현실 세계에 일으킨 변화는 단순히 프로그램을 실행하는 것과 달리 돌이킬 수 없는 피해를 남길 수 있다 (금융 거래, 물품 구매, 데이터 유출 등). 아직 에이전트가 활발히 도입되지 않은 초기 단계임에도 다음과 같은 피해 사례들이 지속적으로 보고되고 있다.

  1. 맥도날드 드라이브스루에 도입된 에이전트가 주문을 잘못 이해한 사례 2
    • 잘못된 품목을 추가하거나, 개수를 잘못 설정하는 등의 문제가 발생
  2. Claude 기반 Agent가 부트로더 (GRUB) 설정을 손상시킨 사례 3
    • 부팅 시스템이 망가져 컴퓨터가 켜지지 않음
  3. Cursor 상담 봇이 존재하지 않는 회사의 정책을 고객에게 알린 사례 4
    • Cursor가 기기 1대에서만 로그인 가능하다는 메일을 보냈으나, 그런 정책은 존재하지 않았음

앞으로 에이전트 소프트웨어가 급속도로 보급될 것을 생각하면, 에이전트 안전성 보장 기술이 절실한 상황이다. VeriSafe Agent는 모바일 환경에서 동작하는 모바일 GUI (Graphical User Interface) 에이전트의 안전성을 보장하기 위한 시스템으로, 최초의 논리식 기반 에이전트 행동 검증 시스템이다.

3. 논리식 기반 에이전트 행동 검증 시스템

VeriSafe Agent는 사용자 지시사항을 논리식으로 변환하고, 이를 활용하여 에이전트의 행동이 올바른지 검증한다. 에이전트의 행동이 논리식을 위반하지 않는지 확인하는 방식이다. 만약 위반한다면 에이전트의 행동을 막고 왜 이 행동이 논리식을 위반하는지 에이전트에게 알려준다. 이러한 추론 과정은 모두 논리식 기반으로 이루어지기 때문에 수학적으로 올바름이 보장된다. 즉, 사용자 지시사항만 논리식으로 잘 변환되면 그 이후의 과정은 전부 신뢰할 수 있다는 의미이다.

언어 모델을 기반으로 에이전트의 행동을 검증하는 기존 검증 방법인 자가 검사 (Self-Reflection)와 비교하면 5가지 장점이 있다.

# 언어 모델 자가 검사 VeriSafe Agent
1 검증 자체에서도 환각 (Hallucination) 문제 발생 검증에서는 환각 없음
2 일관되지 않은 검증 결과 일관된 검증 결과
3 틀린 이유 설명을 언어 모델에 의존 틀린 이유도 수학적으로 추론 가능
4 작업 길이가 길어지면 정확도 저하 작업 길이가 길어져도 정확도 유지
5 잦은 모델 호출로 높은 비용 발생 검증 과정에서는 모델 호출 없음

다음 예제를 통해 구체적인 동작 방식을 이해해보자.

예제: 에이전트에게 비행기표 구매를 요청하는 상황

먼저, 사용자의 지시사항을 논리식으로 번역한다.

사용자: "3월 7일에 출발해서 3월 9일에 돌아오는 일본 비행기 예약해 줘. 가격은 30만 원 이하로!

번역 결과: $Ticket(depart = 03.07, return = 03.09, dest = \text{Japan}, price \le 300,000₩) \Rightarrow Book$

이제 논리식을 활용하여 에이전트의 행동을 검증해 보자. 우선, 에이전트가 올바른 행동을 한 경우를 살펴보자.

에이전트: 달력에서 출발 날짜를 3월 7일로 선택

에이전트 행동 논리식: $Ticket(depart = 03.07)$

검증기: $Ticket(depart = 03.07) \Rightarrow Ticket(depart = 03.07, \ldots)$

검증기: 검증 성공

에이전트가 잘못된 행동을 한 상황에서 검증기가 어떻게 동작하는지 살펴보자.

에이전트: 달력에서 돌아오는 날짜를 3월 11일로 선택

에이전트 행동 논리식: $Ticket(return = 03.11)$

검증기: $Ticket(return = 03.11) \Rightarrow Ticket(return = 03.09, \ldots)$

검증기: 검증 실패...

원인: $Ticket(return = 03.11) \not\Rightarrow Ticket(return = 03.09)$

이처럼 검증기는 에이전트의 행동이 논리식을 위반하는지 확인하고, 위반한다면 원인을 알려준다.

VeriSafe Agent를 실제 상황에 적용하기 위해서는 다음 3가지 문제에 대한 답을 제시해야 한다.

  1. 어떻게 번역된 논리식의 올바름을 보장할 것인가? (#3.1)
  2. 어떤 언어로 논리식을 작성할 것인가? (#3.2)
  3. 어떻게 논리식을 활용하여 에이전트의 행동을 검증할 것인가? (#3.3)

3가지 문제에 대한 VeriSafe Agent의 답을 하나씩 살펴보자.

3.1. 어떻게 번역된 논리식의 올바름을 보장할 것인가?

사용자 지시사항을 논리식으로 정확히 번역하는 것은 전체 시스템의 정확성 보장을 위해 가장 중요한 부분이다. 번역된 논리식이 올바르지 않은 경우 이후에 논리식을 기반으로 이루어지는 검증들이 모두 잘못되기 때문이다. VeriSafe Agent는 다음 4가지 전략을 체계적으로 사용하여 번역 오류를 최소화한다.

  1. 구문 분석 (Parsing): 번역 모델이 생성한 논리식이 사전에 정의된 문법 규칙을 올바르게 따르는지 확인한다. 만약 잘못된 문법이 발견되면, 피드백을 통해 수정을 요구하여 일관된 형태의 논리식만 생성되도록 유도한다.
  2. 유형 검사 (Type Checking): 논리식에 포함된 값들이 올바른 유형(Type)을 갖는지 검사한다. 예를 들어, '사과 5개' 주문 시 수량(quantity) 값은 정수형인 5가 되어야 하며, 문자열인 "5개"가 값으로 들어가면 유형 오류로 판단하고 수정을 요구한다.
  3. 일관성 검사 (Self-Consistency): 번역된 논리식을 다시 자연어로 복원한 뒤, 원래 사용자의 지시사항과 의미상 일치하는지 비교하는 과정을 거친다. 이 양방향 번역 및 비교를 통해 번역 과정에서 정보가 누락되거나 왜곡되는 것을 방지할 수 있다.
  4. 메모리 시스템 (Memory System): 과거에 성공적으로 번역했던 자연어-논리식 쌍 데이터를 참고 자료로 활용한다. 새로운 지시사항이 들어오면 과거의 유사한 번역 사례를 프롬프트에 포함하여 언어 모델에 제공하여 번역의 정확도를 높인다.

3.2. 어떤 언어로 논리식을 작성할 것인가?

모바일 에이전트의 행동을 효과적으로 검증하기 위해서는 사용자의 지시사항과 앱의 상태를 잘 표현할 수 있는 적절한 언어를 선택해야 한다. 일반적인 일차 논리(First-order logic)는 필요한 모든 것을 표현할 수 있지만, 특정 앱 환경에 최적화되어 있지 않아 자연어를 논리식으로 번역하는 난이도를 높이는 단점이 있다. 이 문제를 해결하기 위해 VeriSafe Agent는 모바일 에이전트 검증을 위한 도메인 특화 언어(Domain-Specific Language, DSL)를 자체적으로 정의하여 사용한다. 이 DSL의 특징은 다음과 같다.

  • Horn Clause5 기반: Datalog나 Prolog와 같은 논리 프로그래밍 언어와 유사하게 Horn Clause를 기반으로 설계되었다.
  • 직관적인 규칙 구조: $\text{조건1} \land \text{조건2} \land \ldots \Rightarrow \text{행동}$ 과 같이 '어떤 조건들이 충족되면 특정 행동을 해라'는 직관적인 형태로 규칙을 작성한다. 이를 통해 사용자의 복잡한 요구사항이나 앱의 상태를 간결하게 표현할 수 있다.
  • 높은 표현력: 사용자의 지시사항이나 앱의 상태 대부분을 표현할 수 있도록 설계되었다.

예를 들어, "레스토랑 ‘R’을 오후 7시 전으로 예약하고, 만약 예약할 수 없으면 아무것도 하지 마시오" 라는 지시사항은 다음과 같은 규칙들로 표현될 수 있다.

  • 규칙 1: $\text{RestaurantInfo}(\text{name} = \text{``R"}) \land \text{ReserveInfo}(\text{date} = \text{Today}, \text{time} < \text{19:00}, \text{available} = \text{True}) \Rightarrow \text{Reserve}$
  • 규칙 2: $\text{Reserve} \land \text{ReserveResult}(\text{success} = \text{True}) \Rightarrow \text{Done}$
  • 규칙 3: $\text{RestaurantInfo}(\text{name} = \text{``R"}) \land \text{ReserveInfo}(\text{date} = \text{Today}, \text{time} < \text{19:00}, \text{available} \neq \text{True}) \Rightarrow \text{Reserve}$

3.3. 어떻게 논리식을 활용하여 에이전트의 행동을 검증할 것인가?

논리식으로 표현된 요구사항과 에이전트의 실제 행동을 연결하고, 실시간으로 변화하는 앱의 상태를 검증에 반영하기 위해 VeriSafe Agent는 앱 상태 관측(Instrumentation) 방식을 사용한다.

핵심은 앱 개발자가 상태 변화가 일어나는 시점을 직접 명시하도록 하는 것이다. 이를 위해 VeriSafe Agent는 개발자가 쉽게 자신의 앱 상태를 관측할 수 있는 라이브러리를 제공하며, 개발자는 앱의 기존 이벤트 처리기(Event Handler) 코드에 간단한 상태 업데이트 규칙을 추가하기만 하면 된다.

예를 들어, 앱에서 검색 버튼이 눌렸을 때 현재 검색창에 있는 텍스트를 RestaurantInfo라는 상태로 업데이트하도록 하려면, 개발자는 기존 onClickListener에 다음과 같은 코드를 추가할 수 있다.

searchButton.VSAOnClickListener (() -> {
    VSA.updateState ("RestaurantInfo", {
        "name": searchTextField.getText(),
        });
    /* existing code for onClickListener */
});

앱의 각 부분에서 상태 정보가 실시간으로 업데이트되면, 검증기는 이 정보를 바탕으로 에이전트의 다음 행동이 사용자의 요구사항(논리식)을 만족시키는지 논리적으로 추론하고 검증한다. 만약 행동이 요구사항을 위반하면 즉시 에이전트에게 피드백을 보내 잘못된 행동을 막고 올바른 방향으로 유도한다.

4. 평가

VeriSafe Agent의 효용성을 검증하기 위해, 언어 모델을 활용한 자가 점검 방식과 성능을 비교했다. 평가는 모바일 환경에서의 GUI 기반 작업 수행을 다루는 LlamaTouch6 벤치마크의 일부와 자체 제작한 복잡한 지시사항(Complex Instructions) 벤치마크를 사용했으며, 에이전트와 검증 모델로는 GPT-4o가 사용되었다.

에이전트 행동 검증에서는 잘못된 행동을 올바르다고 판단하는 False Negative를 최소화하는 것이 매우 중요하다. 이는 잘못된 계좌로 송금하거나 다른 날짜로 항공권을 예매하는 등 치명적인 오류로 이어질 수 있기 때문이다.

VeriSafe Agent는 주요 평가 지표에서 기존 방식 대비 월등한 성능을 보였다.

  • 검증 정확도: 기존 언어 모델 기반 검증 방식과 비교했을 때, VeriSafe Agent는 38.2% 향상된 검증 정확도를 달성했다. 이는 논리 기반 검증 과정에서 환각(Hallucination)이 원천적으로 배제되기 때문이다.
  • 복잡한 작업 성공률: VeriSafe Agent는 에이전트의 행동이 틀렸을 때, 그 이유를 논리적으로 추론하여 정밀한 피드백을 제공한다. 이러한 피드백을 통해 에이전트가 스스로 오류를 수정하고 작업을 완수할 수 있도록 유도한 결과, 복잡한 작업의 성공률이 130% 향상되었다.
  • 지연 시간 및 비용 효율: 언어 모델 기반 검증은 행동을 검증할 때마다 비용이 높은 언어 모델을 호출해야 한다. 반면, VeriSafe Agent는 검증 과정에서 언어 모델 호출이 필요 없어 지연 시간은 12.5배, 호출 비용은 25.8배 절감하는 압도적인 효율성을 보였다. 작업 단계 수가 늘어날수록 이 격차는 더욱 커진다.

5. 결론

VeriSafe Agent는 스스로 외부 도구를 사용하며 현실 세계에 영향을 미치는 AI 에이전트의 안전성을 확보하기 위해, 세계 최초로 제안된 논리 기반 에이전트 행동 검증 시스템이다. 본 시스템은 언어 모델에 의존하는 기존 검증 방식의 한계를 극복하고, 신뢰성과 비용 효율 측면에서 모두 크게 앞서는 결과를 보였다.

6. 관련 자료

7. 참고 문헌

  • [1]: Jungjae et al., 2025, "Safeguarding Mobile GUI Agent via Logic-based Action Verification", Annual International Conference On Mobile Computing And Networking
  • [2]: Nick Robins-Early, 2024.06.17 "McDonald’s ends AI drive-thru trial as fast-food industry tests automation"
  • [3]: Buck Shlegeris, 2024.09.30, https://x.com/bshlgrs/status/1840577720465645960
  • [4]: Benj Adwards, 2025.04.18, "Company apologizes after AI support agent invents policy that causes user uproar"
  • [5]: Wikipedia, 2024.12.03, https://simple.wikipedia.org/wiki/Horn_clause, retrived 2025.07.25
  • [6]: Zhang et al., 2024, "LlamaTouch: A faithful and scalable testbed for mobile UI task automation", ACM Symposium on User Interface Software and Technology

Clone this wiki locally