허기홍

8 minute read

꼼수

∀x, y. (Us(x) ∧ Perform(x, y)) → ((Fail(y) → Rebellion(x)) ∧ (Succeed(y) → Revolution(x)))

퀴즈: 위 문장은 2023년 개봉한 한국 영화의 명대사를 다른 언어로 적은 것이다. 어떤 영화의 무슨 대사일까?

정답은 <서울의 봄> 에 나오는 “실패하면 반역, 성공하면 혁명 아입니까?”이다. 일반인들에게는 다소 낯설 수 있는 언어이다. 이 언어는 일차논리(first-order logic)라고 하고, 위에 적힌 것 같은 문장은 일차논리식(first-order logic formula)이라고 부른다. 생긴게 조금 얄궂긴 하지만, 한국어나 영어와 마찬가지로 문법에 맞게 문장을 기술할 수 있고, 문장마다 의미가 있는 또 다른 언어일 뿐이다. 다만 한국어, 영어 같이 자연스럽게 만들어진 “자연어”와 달리, 인간이 만들어낸 “인공어”이다. 그런 까닭에 자연어와 달리, 문법과 의미가 명확하고 모호함이 없다는 장점이 있다. 따라서 철학, 논리학, 수학, 전산학에서 무언가 맞는지 따져볼 때 쓰기 좋다. 특히, 내 연구 분야에서는 프로그램이 올바르게 동작하는지 증명할 때 쓰인다.

위 퀴즈의 반대 방향, 즉, “실패하면 반역, 성공하면 혁명 아입니까?”라는 문장을 일차논리식으로 번역하는 것은 내가 가르치는 과목의 기말고사 문제였다. 2022년부터 프로그램논증이라는 과목을 매년 가르치고 있다. 이 과목의 목표는 프로그램이 올바르게 동작하는지 따져보는 기술을 배우는 것이다. 그러다 보니 저러한 논리식을 배우고, 프로그램이 논리식에서 말하는 바와 같이 동작하는지 증명하는 방법을 배운다. 개설 첫해 기말고사에 논리식과 관련된 문제로 무엇을 낼까 고민하던 차에, 저러한 번역 문제를 재미로 시도해 보았다. 일차논리로 표현할 수 있는 것이 무궁무진하며 우리 일상 생활과도 동떨어진 것이 아니라는 느낌을 학생들에게 전해 주고 싶었기 때문이다. 그 이후로 문제 선정하는 것도 재미있고, 가사, 속담, 대사 등 무궁무진하게 새로운 문제를 만들 수 있는 점도 편해서 매년 등장시키고 있다.

묘수

시험 문제를 편하게 만들려는 얕은 꼼수가, 놀랍게도 깊은 묘수였음은 몇 년 지나서 알게 되었다. 두 해에 걸쳐 같은 형태로 문제를 내면서 재미를 보고, 세 번째 해 기말고사를 앞둔 2024년 10월 말이었다. KAIST 서울 도곡 캠퍼스에 강의가 있어서 올라갔다가 복도에서 우연히 우리 학부의 신인식 교수님을 만났다. 오랜만에 만나서 인사를 드리고 강의 준비를 하러 가려던 차에, 신 교수님이 갑자기 물으셨다. “허 교수님 프로그램 검증 연구하시죠? AI 에이전트도 검증할 수 있을까요?” 사연은 이랬다. 신 교수님은 모바일 시스템을 구동하는 AI시스템을 연구중이셨다. 사람이 말로 명령을 내리면 그에 맞게 AI가 스마트폰을 제어해 주는 자율 에이전트 시스템이다. 가령, “8월에 뉴욕으로 가는 가장 싼 항공권을 예매해줘”라고 지시를 하면, AI가 항공권 구매 앱을 켜고, 8월에 뉴욕으로 가는 항공권을 검색한 다음, 가격 비교후 가장 싼 항공권을 예매하고 결제까지 해주는 것이다. 그런데, 당연히도 AI가 사용자의 지시사항을 제대로 수행했는지 검증할 수 있는 방법이 필요했다. 출발일이 8월이 맞는지, 도착지가 뉴욕이 맞는지, 가격이 가장 싸긴 한지, 결제까지 제대로 되었는지 등을 따져보아야 한다. 하지만 마땅히 검증할 방법이 없어서 검사하는 역할을 하는 AI로 다시 한 번 검토하는 것이 당시 최고 수준이라고 했다. AI의 동작이 못미더워 검증을 해야 하는데, 그 검증을 AI가 하는 상황이라니. 우스꽝스럽다.

문제 상황을 듣고 자연스럽게 든 생각은 이랬다. “자연어 지시사항을 논리식으로 번역하면 엄밀하게 검증할 수 있지 않을까요?” 여러모로 더 생각해야 할 것들이 많긴 하지만, 어찌 되었건 논리식으로 번역하는 것은 반드시 필요한 조건이라 생각했다. 그리고 몇 년간 시험 문제로 학생들을 통해 실험해 본 결과, 해 볼 만하다는 확신도 있었다. 간단히 서로 문제와 아이디어를 설명한 뒤, 다음에 더 자세히 이야기하기로 하며 헤어졌다.

익숙함과 새로움이 공존하는 재미난 주제였다. 대전으로 돌아와서, 당시 석사과정(현 박사과정)이었던 동재에게 이야기를 꺼냈다. 당시 동재도 AI의 행동을 검증하는 방법을 연구하고 있었다. 우리의 대상은 프로그램을 짜는 AI였고, 신 교수님의 대상은 모바일 앱 제어 AI였지만 큰 틀에서는 같았다. 그동안 연구하면서 알게 된 내용과 아이디어도 쉽게 적용할 수 있을 것 같았다. 그렇게 2024년 12월부터 신 교수님 연구진과 함께 본격적으로 뛰어들었다.

일은 일사천리로 진행되었다. 신 교수님 연구실에서는 이미 돌아가는 모바일 AI 에이전트가 있었고 이를 위한 충분한 실험 환경이 마련되어 있었기에 가능했다. 동재와 나는 그 AI가 수행할 지시사항을 논리식으로 번역하고 행동을 제어할 방법을 연구했다. 우리는 모바일 에이전트 행동 검증을 위한 언어를 정의하고, AI를 활용하여 자연어를 그 언어로 번역하기로 했다. 현대 AI가 기반하고 있는 LLM에게 태초에 주어진 사명이었던 자연어 처리 능력을 활용하자는 것이다. 논리식으로 번역되면, AI가 행동할 때마다 그 행동이 어떠한 논리적 함의를 갖는지 추출하고, 행동이 논리식에서 말하는 바와 일치하는지 논리 검증기로 엄밀하게 검증할 수 있다. 또한, AI의 행동이 틀렸을 때 어떤 이유로 틀렸는지 명확히 분석할 수 있으므로, AI를 멈춰 세운 뒤 틀린 이유를 설명하고 다시 지시를 내릴 수 있다. 이러한 과정은 요구사항이 자연어로 기술되어 있다면 결코 제대로 할 수 없는 일이다. AI의 행동을 관찰하고 논리식으로 추출하는 것은 신 교수님 연구진이, 논리식으로 번역하고 행동과 일치하는지 판단하는 검증기는 동재가 만들었다.

핵심은 사용자 의도를 논리적으로 엄밀하게 기술할 언어를 정의하는 것이었다. 논리를 표현하는 언어는 여러 가지가 있다. 다만 각 언어마다 간결성, 표현력에 차이가 있다. 위에 언급한 일차논리는 표현력이 강해서 다양한 논리적 사실과 조건을 표현할 수 있지만, 보시다시피 간명하지 않아서 읽고 쓰기가 어렵다. 사람에게 읽고 쓰기 어려운 언어는 AI에게도 마찬가지이다. 언어가 어려우면, AI가 번역을 잘못할 가능성이 크고, 의도가 제대로 번역되지 못하면 검증 자체가 무의미해진다. 모바일 앱 제어를 충분히 표현할 수 있으면서도 최대한 간결한 언어를 정의하는 것이 중요했다.

우리가 스마트폰을 사용할 때 어떤 생각으로 조작을 하는지 되짚어 보니 답이 보였다. 사람들은 스마트폰으로 아주 복잡한 일을 하지는 않는다. 대부분 단순한 조건을 상정하고, 그 조건이 맞으면 특정 동작을 수행하는 식이다. 예컨대,

“8월에 뉴욕으로 가는 가장 싼 항공권을 예매해줘”

라는 지시사항은, 조건 1) 출발일이 8월, 조건 2) 도착지가 뉴욕, 조건 3) 가격이 가장 싼 항공권이라는 세 가지 조건을 검사하고, 모두가 만족되면 항공권을 예매하라는 의미이다. 간소화된 형태로 쓰면

(Depart = “August” ∧ Destination = “NewYork” ∧ Cheapest = True) → Book

와 같이 쓸 수 있다. 여기서 ∧ 는 “그리고”, → 는 “그러면”이라는 의미이다. 보시다시피, 자연어의 구조와 흡사하다. 이와 같은 조건-결론 구조를 갖는 논리식을 특별히 혼 절(Horn Clause)라고 부른다1. 이런 구조로 요구사항이 기술되어 있으면, 읽기도, 쓰기도, 결론을 계산하기에도 편한 까닭에, 이를 기반으로 한 여러 프로그래밍 언어도 존재한다. 이른바 논리형 프로그래밍 언어라고 부르는데, 대표적으로 Prolog라는 언어가 있다. 한 가지 재미있는 점은, 이 Prolog 언어가 1972년에 개발되던 당시 주요 목적이 인공지능 개발이었다는 것이다. 당시에는 이러한 규칙 기반 시스템을 잘 만들고, 여러 규칙을 넣어주면 인공지능을 만들 수 있다고 생각했다. 최근에는 AI기술의 주류가 인공신경망으로 바뀌면서, 예전만큼 많이 쓰이고 있지는 않다. 하지만, 우리가 더 안전한 AI 시스템을 개발하려다 보니, 자연스레 70년대 선배들과 비슷한 결론에 도달하게 되었다는 점이 흥미롭다. 잊고 있던 고대 기술 문명의 유적을 다시 발견한 기분이랄까.

연구를 본격적으로 시작한 지 3개월 만인 2025년 3월, 만족스러운 기술이 완성되어 MobiCom 2025에 논문을 제출했다. 서로 다른 분야의 연구진이 모여서 3개월 만에 논문까지 완성할 수 있으리라고는 생각지 못했다. 석사 과정동안 AI 모델의 바닥까지 들여다 보고, 프로그램 합성기, 검증기를 만들어본 동재의 능력과, 모바일 시스템을 설계와 구현에 오랜 경험이 있는 신 교수님 연구진의 협업이 눈부셨다. 배경이 다른 공저자들과 함께 타 분야의 사람들이 쉽게 이해할 수 있도록 여러 번 글을 고쳐 썼던 나날도 빛났다. 논문23은 예상대로 좋은 평을 받고 채택되었고, 11월 홍콩에서 열린 MobiCom 2025에서 동재가 발표했다.

동시에 신 교수님 연구진의 주도로 과기부에서 주최하는 <인공지능 챔피언 대회>에도 모바일 에이전트 기술을 출품했고, 홍콩에서 MobiCom이 벌어지고 있던 날에 우승을 차지했다. 실용에 가까운 모바일 기술로 인정받은 셈이다. 최종 결선에서 신 교수님의 발표 이후, 한 심사위원이 물었다.

“AI 에이전트에 물건 주문을 시킬 경우, 환각이 발생해서 주문을 잘못하는 경우도 발생할 수 있을 텐데, 해결책이 있나요?”

반가웠다. 신 교수님은 우리가 연구한 논리 기반 검증 기술을 소개했고, 우리는 대상인 과기부 장관상을 받았다. 신 교수님과 우연히 복도에서 만나 이야기를 나눈 지 1년 만이었다.

Expecto Patronum

즐거웠던 동행을 일단락하고, 동재와 나는 원래 우리가 연구하던 프로그램 검증 문제로 돌아왔다. 모바일 에이전트 행동 검증을 연구하면서 배운 것들로 밑천이 두둑해진 채로. 우리의 문제도 비슷하다. 사용자의 요구사항이 자연어로 기술되어 있을 때, AI 코딩 에이전트가 만드는 프로그램이 사용자가 원하는 것과 일치하는지 검증하는 문제이다. 마찬가지로 자연어로 기술된 요구사항은 모호하고 장황하여 맞는지 엄밀히 따져 보기가 어렵다. 이를 위해서는 역시, 사용자의 요구사항을 엄밀한 논리 명세로 번역하는 것이 필요하다. 다만 코딩은 모바일 앱 제어보다 훨씬 복잡한 문제이므로, 고품질 번역을 위한 기술이 필요했다.

이번에도 일은 순조로웠다. 또 한 번 “온고지신”의 묘미를 만끽하며. 코딩을 위한 복잡한 요구사항을 처리할 방법으로 동재는 하향식 명세 합성(top-down spec synthesis)을 제안했다. 기존 프로그램 합성 분야에서 널리 쓰이던 하향식 프로그램 합성에서 착안한 방법이다. 만들고자 하는 대상을 큰 틀에서 먼저 얼개를 잡고, 점점 세부적인 사항을 채워 나가는 방식이다. 복잡한 문제일수록 이런 식으로 문제를 쪼개어 푸는 것이 효과적일 수밖에 없다. 다만 쪼개는 과정이 체계적이어야 하고, 쪼개어 풀고 합치는 중간 과정에서 계속 올바른지 검사해야 한다. 이 과정도 그간 프로그래밍 언어 분야에서 축적된 논리 검증 기술을 접목하면 가능할 것이라 보았다. 원리와 직관, 그리고 기본에 충실하면 흔들리지 않는다는 변치 않는 진리를 재확인하며 나아갔다.

우리의 아이디어는 적중했다. 성능은 기존 순수 LLM 기반 번역 기술보다 훨씬 뛰어났다. 천방지축 AI 코딩 에이전트를 올바른 방향으로 이끌 주문이었으면 해서 “Expecto”라고 이름을 붙였다. 모바일 에이전트 연구가 끝난 3월부터 8개월간 갈고 다듬어 11월 PLDI에 제출하니, 역시나 좋은 평가를 받고 단숨에 채택되었다. 문제도 시의적절하고, 아이디어도 직관적인데다가, 더욱이 모바일 에이전트 검증 연구를 통해 동재가 크게 성장한 덕택이었다. 심사평 중 일부는 다음과 같다.

“I found the idea of using a top-down approach to be very interesting and natural. […] This is a clever and neat idea, the authors are going to rack up the citations for it for sure, well done!”

역시 우리의 직관에 다들 공명하고 있었다. 연구 결과는 2026년 6월, 미국에서 열린 PLDI에서 동재가 발표를 했다. 거기서도 많은 사람들의 관심을 받았고, 학회 기간 내내 여러 사람들에게 우리의 비전을 소개했다. 기술에 관한 자세한 내용은 논문3, 위키4, 웹페이지5를 통해 확인할 수 있다.

자연어의 모호함과 싸우는 사람들

요즘 AI가 이토록 많은 사람들의 관심을 받는 이유는 단연코 자연어 구사 능력 때문일 것이다. 인간 이외의 존재 중 인간의 언어를 제대로 이해하는 첫 번째 존재이기에 여타 기계나 동물에게는 느낄 수 없는 친근함이 있다. 허나 인간들 사이의 소통에서도 자연어의 모호함 때문에 숱한 오해와 갈등이 생기지 않던가. 엄밀함을 추구해야 할 과학기술 분야도 마찬가지이다. 중요한 요구사항, 기술문서가 자연어로 모호하게 적혀 있는 탓에, 인간이 문서를 해석하는 과정에서 오해가 생기고, 그로 인해 여러 결함이 생겼다는 소식은 AI바람 이전에도 심심치 않게 들려왔다. 다만, 그동안은 그런 모호함이 큰 문제가 될 정도로 인간이 빠르게 실행에 옮기지 못했을 뿐이며, 따라서 뒷처리를 감당할 시간이 비교적 충분했기 때문이라 추측한다. 하지만, 인간과 비교할 수 없을 정도로 빠르고, 인간보다 훨씬 더 많이 일하는 존재가 모호한 지시사항을 실행에 옮길 미래에는, 가차없지 않을까?

세계 인구보다 더 많은 새로운 존재가 갑자기 자연어를 구사하게 된 세상. 그동안 못 본 체하고 있던 진짜 문제가 수면 위로 올라오고 있다. AI와 함께 살 미래가 안전할까 걱정하지만, 문제는 예전부터 우리 안에 있었는지도 모른다. 오히려 AI 덕분에 문제를 직시하게 되어 다행이다. 그러므로 이제 본격적으로 자연어의 모호함과 싸워야 한다. 이미 힘겹게 싸우고 있는 이가 있다면, 엄밀한 응원과 격려를 보낸다.

뒷 이야기

본 글의 제목은 최근 본 드라마 <모두가 자신의 무가치함과 싸우고 있다>의 제목을 패러디한 것이다. 그림 잘 그리는 AI도 있겠다, 재미삼아 패러디한 제목에 맞게 드라마 포스터도 패러디해 보았다. 허나, AI에게 수정 지시를 내리면서 또 한 번 자연어의 모호함과 고되게 싸워야 했다. 몇 글자 바꾸는 것을 지시하는데 어찌 그리 손이 많이 가는지.
잘 보면 보일 것이다. 싸우다 포기한 인간의 흔적.

참고

[1] 논리학자 Alfred Horn이 소개한 개념이다. 위키백과 참고.
[2] Jungjae Lee, Dongjae Lee, Chihun Choi, Youngmin Im, Jaeyoung Wi, Kihong Heo, Sangeun Oh, Sunjae Lee, and Insik Shin, Safeguarding Mobile GUI Agent via Logic-based Action Verification, MobiCom 2025
[3] VeriSafe Agent, PL Wiki
[4] Dongjae Lee and Kihong Heo, Expecto: Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles, PLDI 2026
[5] Expecto, PL Wiki
[6] Expecto Webpage

You May Also Enjoy