MAGS, 에이전트가 짠 코드에 증명서를 붙이는 방법

arXiv에 공개된 논문 MAGS: Multi-agent Auto-formalization Guarantees Safety for Agentic Outputs는 에이전트가 만들어내는 실행 가능한 프로그램에 형식적인 안전 보장을 붙이겠다고 제안합니다. 원문 링크는 제목 아래에 걸어 두었습니다.

이 논문이 내세우는 주장은 한 문장으로 정리할 수 있는데, 사람이 검토한 API와 안전 요구사항을 먼저 형식화해서 얼려 두면 여러 에이전트가 협업해서 그 조건을 기계적으로 검증할 수 있는 코드를 만들 수 있다는 것입니다. 오늘 글에서는 이 발상이 왜 나왔는지, 어떤 순서로 동작하는지, 그리고 220개 사례에서의 결과를 어디까지 믿어야 하는지를 차례로 짚어보겠습니다.

안녕하세요, 패트릭입니다. 요즘 저는 에이전트가 짜주는 코드를 보면서 예전과는 다른 불안함을 느낍니다. 예전에는 코드가 짧아서 의심스러운 부분을 직접 읽을 수 있었는데, 이제는 한 번에 수백 줄이 뚝딱 나오니까 어디부터 읽어야 할지 막막해지더라고요. 그렇다면 사람이 다 읽을 수 없는 코드를 우리는 어떻게 믿어야 할까요. MAGS는 이 질문에 테스트를 더하는 방식이 아니라 증명을 붙이는 방식으로 답하려는 시도라서 끝까지 읽어보게 됐습니다.

에이전트가 짠 코드를 사람이 다 읽을 수 있을까

여러 사람이 함께 일하다 보면 누군가 써놓은 문서를 처음부터 끝까지 읽기 어려울 때가 있습니다. 양이 많아서이기도 하고, 그 문서가 전제하는 맥락을 다 알기 어려워서이기도 하죠. 그렇다면 에이전트가 대규모로 만들어내는 코드는 어떨까요. 논문이 출발점으로 삼는 진단은 바로 이 지점인데, LLM 코딩 에이전트가 이제 사람이 꼼꼼히 검토하기 어려울 만큼 복잡한 프로그램을 빠른 속도로 만들어낸다는 것입니다.

이 진단은 생각보다 중요합니다. 코드가 짧을 때는 사람이 눈으로 읽으면서 이상한 부분을 잡을 수 있는데, 코드가 길어지고 호출 관계가 얽히면 그런 방식은 금방 한계에 부딪히기 때문입니다. 특히 에이전트는 지치지 않고 계속 코드를 뱉어내니까 검토해야 할 양만 한쪽으로 늘어나는 구조가 되죠. 그래서 저는 이 논문의 문제의식을 규모와 신뢰 사이의 간극이라고 읽었습니다.

여기서 재미있는 질문이 생깁니다. 검토 속도를 코드 생성 속도에 맞추는 것이 가능할까요. 사람을 더 붙이는 방식은 비용이 금방 늘어나고, 대충 읽는 방식은 놓치는 부분이 생깁니다. 일종의 숙제 검사처럼요. 숙제가 몇 장일 때는 선생님이 다 읽을 수 있지만, 숙제가 트럭으로 오면 채점 방식을 바꿔야 합니다. MAGS는 채점을 더 빨리하는 대신 채점의 성격을 바꾸자고 제안하는데, 그 차이가 다음 이야기와 이어집니다.

테스트를 더 해도 왜 구멍이 남을까

테스트를 열심히 하면 안전해질 것 같지만, 실제로는 그렇지 않은 경우가 많습니다. 퍼즈 테스트는 무작위 입력을 넣어서 터지는 경우를 찾고, 정적 분석은 코드 구조에서 의심스러운 패턴을 잡아내며, LLM을 검증자로 쓰는 방식은 모델이 직접 코드를 읽고 문제를 지적합니다. 그런데 이 논문이 지적하는 대로 이런 방법들은 많은 실패를 찾아낼 수는 있어도 모든 가능한 모서리 경우를 다 덮기는 어렵습니다.

왜 그럴까요. 이유는 입력 공간이 너무 넓기 때문입니다. 터미널 스크립트 하나를 생각해보면 경로 이름, 권한, 환경 변수, 네트워크 상태가 계속 바뀌는데, 테스트는 그중 일부 조합만 건드릴 수밖에 없죠. 그래서 테스트를 통과했다는 말은 시험해본 범위에서는 괜찮았다는 뜻에 가깝고, 시험해보지 않은 곳에서는 아무 말도 해주지 않습니다. 저는 이 대목을 읽으면서 성적표와 건강검진을 떠올렸습니다. 성적표가 좋다고 해서 몸에 아무 문제가 없다는 보장은 아니니까요.

문제는 그다음입니다. 에이전트가 만드는 코드가 CUDA 커널처럼 병렬 실행이 얽히거나, 파일을 지우고 권한을 바꾸는 터미널 명령을 포함하거나, 물리적인 팔을 움직이는 로봇 제어에 닿으면 테스트가 놓친 하나의 구멍이 그대로 사고로 이어질 수 있습니다. 그래서 논문은 더 많은 테스트가 아니라 다른 종류의 보장, 즉 형식 검증으로 눈을 돌립니다. 이 선택이 타당한지는 뒤에서 다시 따져보겠습니다.

증명 가능한 코드를 만들겠다는 발상은 어디서 왔을까

처음 MAGS를 보면 거대한 검증기를 에이전트 뒤에 붙인 것 아닌가 하는 생각이 들 수 있습니다. 그런데 논문을 조금 더 들여다보면 진짜로 눈여겨볼 부분은 검증기 자체가 아니라, 검증을 염두에 둔 중간 표현을 파이프라인 한가운데에 놓았다는 데 있습니다. 그 중간 표현이 바로 Dafny인데, 안전 속성을 기계적으로 검사할 수 있는 검증 친화적인 언어로 쓰입니다.

이 발상이 흥미로운 이유는 순서가 바뀌었기 때문입니다. 보통은 에이전트가 코드를 먼저 만들고 나중에 검사하는 흐름을 떠올리죠. 반면 MAGS는 처음부터 증명할 수 있는 형태로 코드를 바라보고, 그 형태를 유지하면서 실행 가능한 결과물을 뽑아냅니다. 생각해보면 사람도 비슷하게 배웁니다. 수학 문제를 풀 때 답만 맞히면 되는 시험도 있지만, 풀이 과정을 함께 보는 시험에서는 과정이 맞아야 점수를 주거든요. MAGS는 후자에 가깝습니다.

제가 이 논문에서 가장 흥미롭게 본 부분은 단일 모델의 똑똑함이 아니라 일을 나누는 방식입니다. 하나의 거대 에이전트가 모든 것을 잘하기를 기대하는 대신, 형식화하고 생성하고 검증하고 고치는 역할을 여러 에이전트가 나눠 맡는 구조를 택했기 때문입니다. 여러 사람이 함께 일할 때 검토자와 작성자를 분리하는 것처럼요. 역할이 나뉘면 각 단계에서 무엇을 보장하는지가 분명해지고, 나중에 실패했을 때 어디서 어긋났는지도 추적하기 쉬워집니다.

안전 조건을 먼저 얼려 두는 이유는 무엇일까

MAGS 파이프라인에서 제가 눈을 오래 둔 대목은 생성보다 먼저 오는 단계입니다. 사람이 검토한 API와 안전 요구사항을 형식화한 뒤에는 그 내용을 얼려 둡니다. 얼린다는 말은 이후 생성과 검증 과정에서 그 조건을 마음대로 바꾸지 않는다는 뜻인데, 이 장치는 생각보다 큰 역할을 합니다.

이유는 에이전트의 유연함이 때로는 독이 되기 때문입니다. 에이전트는 주어진 목표를 이루기 위해 표현을 바꾸고 우회로를 찾는 데 능숙한데, 안전 조건까지 함께 움직이면 검증이 무색해집니다. 시험 문제를 푸는 학생이 채점 기준까지 같이 고치는 셈이죠. 그래서 기준을 먼저 고정하고, 그 뒤에는 기준에 맞는 답만 찾도록 만드는 것입니다. 기준이 고정돼 있으니 나중에 나온 코드가 조건을 만족하는지를 기계적으로 따질 수 있게 됩니다.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 누가 그 조건을 쓰고 누가 검토할까요. 논문 흐름상 사람은 API와 안전 요구사항을 감사하는 자리에 있습니다. 다시 말해 사람은 모든 코드를 한 줄씩 읽는 대신, 무엇을 허용하고 무엇을 금지할지를 정하는 쪽으로 이동합니다. 저희가 새로운 AI 아키텍처를 볼 때도 benchmark 숫자만 보지는 않습니다. 실제로 무엇이 바뀌었고, 그 변화가 시스템에서 어떤 비용 구조를 만드는지를 함께 봅니다. 같은 관점에서 보면 이 얼리기 단계는 자동화와 사람 검토 사이의 경계를 다시 긋는 일이라서 인상 깊었습니다.

Dafny라는 중간 언어를 고른 셈이 되는 것일까

Dafny라는 이름을 처음 들으면 또 하나의 프로그래밍 언어가 나온 건가 싶을 수 있습니다. 그런데 여기서는 언어를 새로 배우자는 이야기가 아니라, 안전 속성을 기계적으로 검사할 수 있는 중간 표현을 두자는 이야기입니다. 에이전트가 만드는 실행 코드는 그대로 두되, 그 코드의 의미를 Dafny 쪽으로 옮겨서 검사한다는 구상이죠.

이 선택은 일종의 번역 과정처럼 읽힙니다. 사람이 쓴 기획서를 개발용 명세서로 옮기면 모호한 표현이 드러나듯이, 실행 코드를 검증 가능한 형태로 옮기는 과정에서 숨은 가정이 드러나기 때문입니다. 예를 들어 배열에 접근할 때 인덱스가 항상 범위 안에 있는지, 동시에 도는 스레드들이 같은 메모리를 어지럽히지 않는지 같은 조건은 평소에는 눈에 잘 띄지 않는데, 증명을 시도하면 바로 질문으로 바뀝니다. 그래서 저는 이 숫자보다 그 뒤의 구조가 더 중요하다고 봅니다. Dafny를 썼다는 사실 자체보다, 증명을 시도하면서 빠진 조건을 드러내는 과정이 중요하다는 뜻입니다.

물론 여기서 조심해서 읽을 필요가 있습니다. 중간 언어가 있다고 해서 모든 안전이 자동으로 증명되는 것은 아닙니다. 어떤 속성은 쉽게 형식화되지만, 어떤 속성은 말로 적기조차 어렵기 때문입니다. 특히 로봇 팔처럼 물리 세계와 만나는 부분에서는 허용 가능한 힘과 속도, 충돌 회피 같은 조건을 어디까지 수식으로 옮길 수 있는지가 관건이 됩니다. 논문이 말하는 형식 보장이 바로 이 형식화된 조건에 대한 보장이라는 점을 기억해야 뒤의 100퍼센트라는 숫자를 오해하지 않습니다.

만들고 고치고 다시 묶는 파이프라인은 어떻게 돌까

이제 전체 흐름을 머릿속으로 따라가 보겠습니다. 사실은 이렇게 이어집니다. 먼저 감사된 API와 안전 요구사항이 고정되고, 에이전트들이 그 틀 안에서 실행 코드를 만듭니다. 그다음 그 코드는 Dafny로 번역되고, 검증자가 조건을 만족하는지를 기계적으로 확인합니다. 만약 어긋난 부분이 있으면 검증 피드백을 받아 코드를 고치고, 다시 검증하는 과정을 반복합니다. 조건을 통과한 결과는 다시 실행 가능한 코드로 컴파일돼 돌아옵니다.

이 흐름에서 눈에 띄는 점은 고치는 과정이 감이 아니라 피드백에 묶여 있다는 것입니다. 사람이 코드를 고칠 때도 컴파일러 오류를 보고 고치면 방향이 분명해지죠. MAGS의 검증자도 비슷한 역할을 하는데, 어디가 어긋났는지를 알려주니까 에이전트가 막연히 다시 쓰는 대신 그 지점을 targeted하게 고칠 수 있습니다. (참고로 여기서 말하는 검증 피드백은 모델이 느낌으로 주는 점수가 아니라, 검증기가 규칙에 따라 내보내는 실패 위치와 조건에 가깝다고 이해하면 됩니다.)

그런데 이런 순환이 매번 매끄럽게 돌까요. 저는 여기서 조금 의심했습니다. 번역 과정에서 의미가 조금씩 어긋나면 검증자는 엉뚱한 것을 증명할 수 있기 때문입니다. 그래서 파이프라인의 신뢰도는 각 단계의 정확도보다 단계 사이를 잇는 번역의 정확도에 달려 있습니다. 이 이야기는 뒤에서 실패 사례와 함께 다시 다루겠습니다. 그 전에 이 파이프라인이 실제로 무엇을 만들어냈는지를 먼저 보겠습니다.

CUDA 커널과 터미널 명령과 로봇 팔에서 무엇을 봤을까

논문이 고른 평가 무대는 220개 사례인데, 100개의 CUDA 커널과 100개의 터미널 스크립트, 20개의 로봇 팔 과제로 나뉩니다. 숫자를 풀어보면 일반 파일에만 둔 것이 아니라 성격이 다른 세 영역을 일부러 고른 셈인데, 이 구성은 이해가 됩니다. 병렬 계산과 시스템 명령과 물리 제어가 각각 다른 종류의 위험을 품고 있기 때문입니다.

각 영역의 위험을 일상적인 장면으로 바꿔보면 감이 옵니다. CUDA 커널에서는 수백 개의 스레드가 동시에 메모리에 손을 뻗는데, 하나라도 범위를 벗어나면 전체 계산이 조용히 망가질 수 있습니다. 터미널 스크립트에서는 한 줄의 삭제 명령이 중요한 디렉터리를 날려버릴 수 있고, 권한 변경 하나가 이후 모든 접근을 막을 수도 있죠. 로봇 팔에서는 목표 지점까지의 경로가 짧아 보여도 중간에 장애물이 있으면 그대로 부딪힙니다. 밤사이 공시가 늦게 도착해도 예측 라인은 멈추면 안 되듯이, 이런 작업들은 한 번의 실수가 바로 비용으로 이어진다는 공통점이 있습니다.

논문이 보고하는 결과는 이 220개 사례 모두에 대해 얼려 둔 명세에 비춰 자명하지 않은 안전 보장을 담은 프로그램을 만들어냈다는 것입니다. 자명하지 않다는 표현이 재미있는데, 항상 참인 빈말이 아니라 실제로 검사할 가치가 있는 조건을 증명했다는 뜻으로 읽힙니다. 같은 모델에 같은 질문을 던져도 결과가 크게 달라질 수 있다는 것을 경험으로 알고 있죠. 그래서 여러 에이전트가 검증 피드백을 반복하면서 끝까지 통과한 결과물을 냈다는 점은 분명히 눈여겨볼 만합니다. 다만 이 숫자는 그대로 믿기 전에 조건을 봐야 합니다. 다음 대목에서 그 조건을 풀어보겠습니다.

100퍼센트라는 숫자를 조심해서 읽어야 하는 이유

100퍼센트라는 숫자는 사람을 멈칫하게 만듭니다. 220개 모두 성공했다니 대단해 보이죠. 그런데 이 숫자는 얼려 둔 명세에 대한 성공률이라는 점을 함께 읽어야 합니다. 다시 말해 에이전트가 정한 것도, 검증 도중에 바꾼 것도 아닌, 처음에 고정해둔 조건을 기준으로 삼았을 때의 결과라는 뜻입니다.

이 차이는 생각보다 중요합니다. 시험에 비유하면 문제와 채점 기준을 미리 고정해두고, 그 기준으로는 모두 통과했다는 이야기입니다. 기준 자체가 현실을 충분히 담고 있는지는 별개의 질문이죠. 표면적으로 보면 단순합니다. 실제로는 그렇지 않습니다. 기준이 허술하면 통과율이 높아도 현실에서는 구멍이 남기 때문입니다.

그렇다면 이 숫자를 어떻게 받아들여야 할까요. 저는 이 결과를 에이전트가 아무것도 못 한다는 증거도, 모든 안전 문제를 풀었다는 증거도 아니라고 봅니다. 오히려 이렇게 읽는 편이 정확합니다. 조건을 분명히 적을 수만 있다면, 에이전트들은 그 조건을 만족하는 코드를 검증 가능한 형태로 꾸준히 만들어낼 수 있다는 것입니다. 조건을 적는 일의 어려움은 여전히 사람 쪽에 남아 있고, 그 어려움이 다음 실패 이야기와 연결됩니다. 숫자는 구조를 보여주지만, 구조의 한계까지 보여주지는 않으니까요.

의미가 어긋나면 증명도 빗나간다

앞에서 미뤄뒀던 질문으로 돌아올 차례입니다. 번역이 정확하지 않으면 어떻게 될까요. 논문도 이 점을 숨기지 않는데, 별도의 독립적인 평가에서는 자동 형식화된 의미가 목표 동작을 온전히 담지 못할 때 실패가 드러났다고 보고합니다. 증명은 통과했지만 현실에서는 어긋난 경우죠.

이 대목은 곱씹을수록 의미가 큽니다. 형식 검증이 틀렸다는 뜻이 아니라, 증명한 대상과 실제로 돌릴 대상 사이에 간극이 있었다는 뜻이기 때문입니다. 계약서를 비유로 들면 조항 자체는 완벽히 지켰는데, 계약서가 현실의 거래를 잘못 옮긴 경우와 같습니다. 도장은 멀쩡하지만 내용은 빗나간 셈이죠. 그래서 검증기의 초록불만 보고 안심하면 안 되고, 명세가 현실을 제대로 옮겼는지를 따로 물어야 합니다.

여기서는 조금 조심해서 읽을 필요가 있습니다. 이 실패를 두고 형식화 자체가 무용하다고 말하는 것은 성급합니다. 반대로 증명이 통과했으니 현실도 안전하다고 말하는 것도 성급하죠. 제가 앞으로 보고 싶은 것은 바로 이 간극을 좁히는 장치입니다. 자동 형식화가 어디까지 믿을 만한지, 사람이 어디에서 다시 개입해야 하는지, 그리고 의미가 어긋났을 때 그것을 먼저 잡아내는 독립 평가를 파이프라인 안에 어떻게 넣을지가 다음 연구의 관건이라고 봅니다.

증명서를 들고 나오는 에이전트와 남는 질문

여기까지 읽고 나면 MAGS의 윤곽이 비교적 또렷해집니다. 에이전트가 코드를 만들고 사람이 조건을 정해주면, 그 사이를 Dafny라는 검증 가능한 형태로 이어서 기계가 확인할 수 있는 보장을 붙인다는 그림이죠. 테스트가 해본 범위 안에서는 괜찮다고 말하는 방식이라면, 형식 검증은 적어둔 조건 안에서는 항상 괜찮다고 말하는 방식입니다. 표현을 바꾸면 보장의 모양이 달라지는 셈입니다.

실제 시스템 관점에서 보면 다음 질문이 바로 생깁니다. 이 방식을 어디에 먼저 쓸 수 있을까요. 저는 모든 코드에 일괄 적용하는 그림보다는 위험이 분명하고 조건을 적기 쉬운 곳부터 들어갈 것이라고 봅니다. 파일을 지우거나 권한을 바꾸는 관리 스크립트, 범위를 벗어나면 조용히 망가지는 병렬 커널, 사람 곁에서 움직이는 로봇 동작처럼 실패 비용이 분명한 작업이 먼저 떠오릅니다. 좋은 건 알겠는데, 이걸 실제로 어떻게 서빙할까요. 검증에 드는 시간과 컴퓨팅 비용, 명세를 쓰고 감사하는 사람의 시간까지 함께 따져야 답이 나오기 때문입니다.

그렇다면 사람의 역할은 무엇일까요. MAGS가 그리는 미래에서는 사람이 코드를 한 줄씩 읽는 검수자에서 무엇을 금지하고 무엇을 허용할지를 정하는 설계자로 이동합니다. 저는 그 이동이 꽤 설득력 있다고 봅니다. 사람이 잘하는 일은 모든 경우를 다 외우는 것이 아니라 중요한 경계를 정하는 일이니까요. 다만 경계를 정하는 일이 쉬워지는 것은 아닙니다. 오히려 책임이 더 분명해지는 셈이라서, 명세를 잘못 적으면 그 실수가 그대로 시스템에 박히게 됩니다. 앞으로 에이전트가 더 오래 일하고 더 많은 코드를 만들수록, 개별 출력 하나가 맞았는지를 넘어 어떤 조건을 고정했고 그 조건이 현실을 얼마나 담고 있는지를 함께 살펴봐야 할 것 같습니다.