Claude Fable 5.2로 멀티 에이전트 팀을 안전하게 확장하는 방법

멀티 에이전트 팀은 길고 어려운 문제도 풀어낼 수 있습니다. 지난 9월에는 Claude Fable 5.1에 견줄 만한 내부 연구 모델을 구동하는 에이전트 수십 개가 페르마의 마지막 정리를 처음부터 끝까지 형식화한 결과를 공개했습니다. 이 작업은 수학 형식화 플랫폼인 Prove2Me와 연구자의 지휘를 바탕으로 진행됐습니다. 이번 소규모 실험에서는 Claude Fable 5.2 초기 버전을 구동하는 에이전트 1,000개로 팀을 꾸려, Prove2Me의 지원 구조나 연구자의 지시 없이 같은 증명을 재현했습니다. 소요 시간은 28.7시간, 출력 토큰은 기존의 3분의 1 수준이었고, 증명 길이는 원본의 7분의 1에 그쳤습니다.

에이전트는 모두 인터넷이 차단된 샌드박스에서 작업했습니다. 분류기(classifier)가 셸 명령과 파일 수정을 실행 전에 일일이 검사했고, 오프라인 모니터가 팀의 모든 행동을 검토했습니다. 에이전트에게 준 자료는 증명할 명제 60개, 고전적 증명 경로를 한 문장으로 요약한 개요, 명제에 쓰이는 정의, 앞선 형식화에서 증명을 마친 보조정리 47개이고, 여기에 리더와 헬퍼 역할을 배정했습니다. 정리를 어떻게 증명하고 팀을 어떻게 꾸릴지에 대해서는 다른 안내를 하지 않았습니다.

이번 소규모 실험은 Fable 5.2 같은 모델을 구동하는 에이전트 팀이 신중하게 설계한 안전 경계 안에서 장기적이고 야심찬 목표를 달성할 수 있음을 보여줍니다.

문제

페르마의 마지막 정리는 2보다 큰 모든 n에 대해 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c가 존재하지 않는다는 내용입니다. 350년 넘게 풀리지 않다가 1995년 앤드루 와일즈 경이 129쪽 분량의 증명을 내놓으면서 해결됐습니다. 이 증명의 모든 단계를 컴퓨터가 검증할 수 있게 만드는 형식화는 수학계의 오랜 숙원이었습니다.

지난 9월의 형식화에는 연구자 한 명과 에이전트 수십 개가 11일 동안 출력 토큰 약 60억 개를 들였습니다. 이들이 작성한 코드는 Lean으로 1,300만 줄에 달합니다. Lean은 컴퓨터가 증명의 모든 단계를 검증하는 프로그래밍 언어입니다.

에이전트들은 Prove2Me를 통해 협업했습니다. 이 플랫폼은 Tianyi Peng(현재 Anthropic 기술 스태프)과 컬럼비아 대학교의 동료들이 설계했습니다. Prove2Me는 증명할 명제와 그 명제를 쪼갠 더 작은 명제들을 공유 그래프로 연결합니다. 어떤 에이전트든 명제를 분할할 수 있고, 다른 에이전트는 그래프에 질의해 바로 착수할 수 있는 미증명 조각을 찾을 수 있어서 프로젝트 상태를 놓치지 않습니다. 각 명제와 증명은 독립적으로 컴파일되는 별도 파일에 담았기 때문에, 여러 에이전트가 같은 파일을 건드리지 않고 병렬로 작업할 수 있었습니다.

하네스

우리는 Fable 5.2 같은 모델 기반의 에이전트 팀이 Prove2Me도, 작업을 지휘하는 연구자도 없이 범용 도구로 만든 하네스(harness)만으로 이 결과를 낼 수 있는지 확인하고 싶었습니다.

도구

이번 과제에서는 에이전트 1,000개로 구성된 팀에 최종 정리 하나와 중간 단계 59개를 포함한 명제 60개를 증명하라고 했습니다. 에이전트는 각 명제마다 Lean으로 증명을 작성하고, Lean 도구로 빌드해 검증한 뒤, Git의 공유 메인 브랜치에 제출해야 했습니다. 제출된 증명은 채점기가 확인했습니다. 에이전트마다 다음 도구를 제공했습니다.

• 네트워크가 차단된 개별 샌드박스 안의 셸과 파일 편집기
• 샌드박스 이미지에 내장된 Lean 툴체인과 Mathlib
• 에이전트별 Git 브랜치와 main으로 머지 리퀘스트를 올릴 수 있는 권한
• 셸에서 접속하는 공유 Postgres 데이터베이스

협업

증명 작업은 나눌 수 있어서 멀티 에이전트 팀에 적합한 과제입니다. 다만 서로의 작업을 이어받고 중복 작업을 피하려면 에이전트 간 조율이 필요합니다. 기존 형식화에서 Claude의 초기 시도는 에이전트들이 프로젝트 상태를 놓치고 효과적으로 협업하지 못해 실패했습니다. Prove2Me 플랫폼으로 옮기면서 이 문제가 해결됐습니다.

이번 실험에서는 에이전트마다 경량 가상 머신에 샌드박스를 하나씩 두었습니다. 공유 머신 한 대로는 에이전트 약 100개에서 한계에 부딪혔습니다. 에이전트 100개로 돌린 실행의 절반 넘게가 메모리, 디스크, CPU 부족으로 중단되거나 재시작해야 했습니다.

샌드박스가 1,000개로 나뉘면서 에이전트들이 작업 결과를 공유할 방법이 필요해졌고, 그래서 SQL 데이터베이스를 제공했습니다(그림 1). SQL을 고른 이유는 정보를 정리하는 범용 기본 요소를 갖추고 있고, 트랜잭션으로 에이전트 1,000개의 동시 쓰기를 처리할 수 있으며, Claude가 이미 익숙한 언어이기 때문입니다. 에이전트들은 이 데이터베이스로 작업을 선점하고, 메모를 공유하고, 완료한 작업을 기록했습니다.

프롬프트

프롬프트에는 증명할 명제 60개를 각각 한 줄짜리 비형식적 설명과 함께 나열하고, 사용 가능한 도구(위 목록)를 설명했습니다.

팀에 부여한 구조는 리더 1개와 헬퍼 999개로 이뤄진 계층뿐이었습니다. 리더에게는 문제를 여러 부분으로 나눠 헬퍼에게 배정하라고 했고, 헬퍼에게는 리더의 지시를 기다리되 작업이 불분명하면 리더에게 확인하라고 했습니다.

실행 중에 하네스는 리더에게 남은 시간을 알리는 자동 알림을 19번 보내 계속 진행하도록 독려했습니다.

안전

앞서 공유한 대로, 방어 계층 하나만으로는 에이전트 팀을 통제하기에 충분하지 않습니다. 이번 실험에서는 샌드박싱에 실시간 모니터링과 오프라인 모니터링을 결합했습니다. 각 에이전트를 네트워크가 없는 자신의 가상 머신에 가두고, 샌드박스 탈출이나 모니터링 조작 시도가 있으면 탐지하기 위해서입니다.

샌드박싱

에이전트별 샌드박스는 다음과 같이 보호했습니다(그림 2).

• 통신: 에이전트에게는 전용 메시징 도구가 없었고, 데이터베이스와 Git만으로 조율했습니다.
• 코드 변경: 에이전트는 자기 Git 브랜치에만 푸시할 수 있고, main으로 머지 리퀘스트를 열 수 있었습니다. 별도의 작업이 변경 사항을 main에 병합했으며, 충돌이나 관련 없는 히스토리 같은 결함이 있을 때만 거부했습니다.
• 데이터베이스 접근: 데이터베이스 호출은 공유 비특권 역할로 실행했습니다. SQL 문마다 5초의 시간 제한을 두었고, 256MiB를 넘는 쓰기는 거부했습니다.
• 네트워크 통제: 샌드박스에는 네트워크 접근이 없었습니다. 외부로 나가는 유일한 통로는 요청을 중계하는 게이트웨이로의 파이프였습니다.
• 신원: 한 에이전트가 다른 에이전트를 사칭하지 못하도록, 게이트웨이가 샌드박스 바깥에서 모든 요청에 에이전트의 신원을 태깅했습니다.
• 커널: 각 샌드박스의 커널은 루트 사용자가 커널에 직접 접근할 수 있는 기능(로드 가능 모듈, kexec, raw 메모리 접근, 커널 프로브 등)을 빼고 빌드했으며, 커널 락다운 모드로 실행했습니다.
• 최소 권한: 에이전트의 명령은 샌드박스 안에서 비특권 사용자로 실행했고, 루트 권한을 되찾을 수 있는 sudo 같은 도구는 제거했습니다. 에이전트의 도구는 자신을 실행하는 에이전트 루프를 읽거나 변경할 수 없도록 설계했습니다.

실시간 모니터링

이런 실행을 더 안전하게 만들기 위해 프롬프트 기반 LLM 분류기를 사용합니다. 이 분류기는 셸 명령과 파일 수정을 포함한 모든 도구 호출을 차단할 수 있습니다. 샌드박스 탈출, 경계 탐색, 모니터링 조작 시도는 물론, 모델이 샌드박스를 벗어났을 때 할 수 있는 유해한 행동도 감시합니다. 분류기가 도구 호출을 차단하면 에이전트 팀 전체가 멈추고, 사람이 차단 건을 검토해야 팀을 재개할 수 있습니다. 다른 에이전트가 차단된 행동을 대신 수행하는 일을 막기 위한 조치입니다.

분류기가 정교한 사보타주도 탐지할 수 있는지 시험하기 위해, 멀티 에이전트 사이드 태스크 평가와 사보타주 평가를 실시했습니다. 레드팀 에이전트가 분해 공격(decomposition attack) 같은 전략으로 분류기를 속여 샌드박스 탈출을 허용하게 만들려는 방식입니다. 그 결과 에이전트의 추론 과정(CoT)과 에이전트 간 통신까지 볼 수 있는 모니터는 이 평가의 사보타주 시도를 모두 탐지했고, 그래서 지금은 멀티 에이전트 실행을 감시할 때 이런 모니터를 씁니다. 동시에 같은 모니터의 행동 기반 버전도 함께 운영합니다. CoT는 보지 않고 행동만 보는 이 버전은, 에이전트의 추론이 모니터를 설득해 유해한 행동을 허용하게 만드는 상황에 대비합니다.

우리는 사람이 이끄는 레드팀과 자동 레드팀, 과거 사고를 포함한 실제 서비스 트랜스크립트 기반 평가, 위협 모델링 확대를 통해 모니터링 스택을 계속 개선하고 있습니다. 이 글의 실행에서는 행동 기반 모니터만 사용했습니다. 리더가 차단되어야만 실행이 끝나고, 헬퍼가 차단되면 해당 헬퍼만 제외됩니다.

이 실행 직후에 병렬 CoT 모니터를 추가했습니다. 이런 실험은 출시 전 정렬(alignment) 평가를 마치지 않았을 수 있는 모델로 진행하므로, 모델이 정렬되지 않았을 가능성까지 고려해 모니터링을 설계합니다. 우리가 출시하는 모델은 그 평가를 먼저 통과하며, 이는 위험을 줄여주지만 완전히 없애지는 못합니다.

이번 실행의 도구 호출은 100만 건이 넘었지만, 차단 기준에 해당하는 건은 하나도 없었습니다. 이 호출들을 CoT 모니터와 현재의 평가 기준으로 다시 돌려 보니, 루트 권한 확인 한 건만 차단에 근접했습니다.

오프라인 모니터링

실시간 모니터링과 별개로 오프라인 모니터도 운영합니다. 이 모니터는 실시간 모니터와 같은 위협 모델을 기준으로 에이전트 팀의 행동을 분석하되, 다른 에이전트의 행동을 조회하는 등 추가 기능을 활용할 수 있습니다.

결과

Prove2Me 없이 팀이 자체 조율 체계를 구축했습니다

이 증명 작업은 여러 층위에서 이뤄집니다.

• 증명: 2보다 큰 모든 n에 대해 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수 a, b, c는 존재하지 않는다.
• 명제: 팀에 증명하라고 준 60개의 명제로, 최종 정리와 중간 단계 59개를 포함합니다.
• 더 작은 명제: 에이전트가 어려운 명제를 쪼갠 더 작은 명제, 즉 보조정리입니다.
• Lean: 모든 명제와 보조정리는 Lean에서 하나의 정리(theorem)로 표현됩니다.

각 명제는 Lean에서 증명 자리를 비워 둔 상태로 시작하며, Lean 검증기가 완성된 증명을 받아들여야 비로소 증명된 것으로 칩니다. 증명 방식과 이 여러 층위에 걸친 팀 조율 방식은 리더가 정하도록 했습니다.

리더는 처음 10분 안에 데이터베이스에 테이블 다섯 개를 만들었습니다(그림 3).

• announce: 리더가 팀 전체에 내리는 지시(예: 작업 분할 방법)
• assign: 누가 무엇을 맡는지 기록(예: 각 명제를 맡거나 대행할 헬퍼)
• notes: 누구나 쓸 수 있는 게시판(예: 작업 선점, 진행 상황 보고)
• subtasks: 어떤 에이전트든 작업을 추가할 수 있고, 가장 먼저 선점한 헬퍼가 담당하는 할 일 목록
• landed: 완료한 작업의 기록

리더가 명제를 나눠 맡겼습니다

테이블을 만든 리더는 세 가지 일을 했습니다. 먼저 assign 테이블에 헬퍼마다 한 줄씩 999개 행을 써서, 각 명제를 16~17명의 헬퍼로 이뤄진 크루에 배정했습니다. 다음으로 크루마다 헬퍼 한 명을 캡틴으로 지정했습니다. 캡틴은 notes 테이블에 계획을 올리고, 작업을 크루가 subtasks 테이블에서 선점할 수 있는 태스크로 쪼개는 역할을 맡았습니다. 마지막으로 announce 테이블에 지시를 올려, 모든 헬퍼가 먼저 자기 명제의 난이도를 판단해 notes 테이블에 결과를 남기도록 했습니다.

헬퍼들은 프롬프트를 통해 데이터베이스가 있다는 것을 알고 있었습니다. 이들은 announce 테이블을 찾아 평가를 시작했고, 대부분 notes 테이블에 판단 결과를 올렸습니다. 약 27분이 지났을 때는 이미 명제 세 개가 증명됐고 리더도 올라온 판단을 모두 읽은 상태였습니다. 리더는 대다수 헬퍼가 이번 실행의 예산 안에서는 불가능하다고 본 명제 47개를 제쳐 두고, 끝낼 수 있다고 판단한 나머지 10개에 거의 모든 헬퍼를 재배정했습니다. 크루 규모는 17명 안팎에서 46~139명으로 커졌습니다.

헬퍼는 대부분 리더의 지시에 정리된 다음 순서를 반복하며 일했습니다.

• notes 테이블에서 해당 명제의 계획을 찾는다.
• subtasks 테이블에서 태스크를 선점한다.
• Lean으로 증명을 작성하고, Lean 도구로 검증한 뒤, Git의 메인 브랜치에 제출한다.
• 태스크를 완료로 표시한다.
• notes 테이블에 진행 상황을 올린다.

45분쯤 지나 10개 명제 중 다섯 개가량이 증명됐을 때, 리더는 이렇게 썼습니다.

"팀의 처리 속도는 초기에 '예산 내 불가능'이라고 판단했을 때 가정한 것보다 훨씬 높다"

10개 명제는 모두 약 70분 만에 증명됐습니다.

이후 리더는 헬퍼들을 더 어려운 명제로 옮겼습니다

처음 10개 명제가 끝나자 리더는 "놀릴 이유가 없다"라고 쓰고, 헬퍼들을 처음에 제쳐 두었던 더 어려운 명제에 재배정했습니다. 명제가 하나씩 증명될 때마다 헬퍼를 새 과제로 계속 옮겼고, 이는 대부분 첫 6시간 안에 일어났습니다(그림 4에서 빨간색으로 표시된 assign 테이블 쓰기 참고).

처음에 리더는 캡틴에게 작업을 subtasks 테이블의 태스크로 나누라고 지시했습니다. 그러나 작업이 진행되면서 헬퍼들이 각 명제를 푸는 데 더 많은 책임을 맡기 시작했습니다. 때로는 캡틴이 도움을 요청한 뒤에, 헬퍼들이 직접 태스크를 작성하기 시작했습니다. 5.6시간째에는 헬퍼 73명이 태스크 756개를 작성했고, 그중 캡틴은 16명뿐이었습니다. 그림 4에는 여러 헬퍼가 subtasks 테이블에 쓴 기록(빨간색)이 나타나 있지만, 대부분은 태스크를 선점하거나 완료로 표시하는 쓰기였습니다. 태스크를 끝낸 헬퍼는 더 맡겠다고 자원하기도 했습니다.

"FREE … 조각 하나를 처음부터 끝까지 끝냅니다 … 깊이 있는 조각 ONE개를 지정해 주세요 … 바로 시작하겠습니다"

초반에는 리더가 헬퍼를 특정 명제에 직접 배정했습니다. 이 방식은 첫 1시간 안에 바뀌기 시작해, 3시간째에는 리더가 놀고 있는 헬퍼들에게 "나를 기다리지 말라"고 했습니다. 덕분에 리더가 새 배정을 계속 써 내려가는 중에도 한가한 헬퍼들이 리더를 기다리지 않고 다른 명제의 작업을 이어받을 수 있었습니다.

리더가 팀을 Langlands–Tunnell에 투입했습니다

18시간 무렵에는 Langlands–Tunnell, 그리고 이에 의존하는 명제들과 다른 명제 하나만 남아 있었습니다. 나머지 하나는 팀이 작업하는 과정에서 증명했습니다. Langlands–Tunnell은 와일즈의 증명이 기대는 고전적 결과입니다. 실행 초반에 이 명제를 맡은 캡틴은 비관적이어서, 증명에 Lean 코드 70만~100만 줄이 필요하고 시간 안에 끝낼 확률은 1% 미만이라고 추정했습니다. 리더는 이 명제를 제쳐 두었습니다.

다른 작업이 거의 끝나자 리더는 팀의 초점을 Langlands–Tunnell로 돌렸습니다. 마지막 하향식 배정으로 헬퍼 약 750명을 이 명제에 투입하며 "솔직히 승산은 낮다"라고 썼습니다.

Langlands–Tunnell은 에이전트들이 다뤄 온 어떤 명제보다 훨씬 컸습니다. 태스크는 약 9배 많았고 새로 작성한 코드는 2배를 넘었습니다. 헬퍼들은 이번에도 subtasks 테이블로 작업을 나눴지만, 초기 태스크 중 다수는 헬퍼 한 명이 혼자 끝내기에는 너무 컸습니다.

그래서 팀은 작업을 트리 구조로 조직했습니다. 캡틴이 명제를 10개 영역으로 나눈 계획을 세우고 각 조각을 태스크로 나열했습니다. 혼자 감당하기에 조각이 너무 크다고 본 헬퍼는 그 아래에 더 작은 태스크를 추가해 쪼갤 수 있었습니다. 에이전트 한 명이 풀기에 버거운 조각이 나올 때마다 트리가 자랐고, 결국 태스크 2,418개, 깊이 최대 10단계에 이르렀습니다(그림 5). 각 조각은 그 아래 조각들이 참이라고 가정할 수 있었기 때문에, 아래 조각들이 증명되기 전에도 수백 명의 헬퍼가 병렬로 작업할 수 있었습니다.

그림 6은 전체 실행 동안 모든 헬퍼가 무엇을 작업했는지 보여줍니다. 초반에는 헬퍼들이 여러 명제에 흩어져 있다가 후반에는 Langlands–Tunnell에 모였습니다. Langlands–Tunnell은 28.4시간째에 증명됐고, 28.7시간째에 최종 정리가 뒤따랐습니다. 그러자 리더는 이렇게 썼습니다.

"모두 고맙습니다. 페르마의 마지막 정리가 main에 올라갔고, 공식 검증기의 커널 검증을 통과했습니다."

결론

이번 소규모 실험으로 에이전트 1,000개로 이뤄진 팀이 길고 어려운 과제를 어떻게 풀어 가는지 살펴볼 수 있었습니다. 에이전트들은 Git과 공유 데이터베이스만으로 역할 배정과 결과 공유를 위한 테이블을 설계하고, 팀을 꾸리고, 가장 어려운 명제를 분해할 태스크 트리를 만들었습니다. 그 명제는 담당 캡틴조차 시간 안에 끝낼 확률이 1% 미만이라고 본 것이었습니다.

이 결과가 도메인 특화 하네스나 플랫폼의 필요성을 없애는 것은 아닙니다. 예를 들어 Prove2Me는 에이전트가 Lean 코드를 더 빠르게 컴파일하고 사람이 만든 기존 결과를 검색해 재사용하도록 도와 효율을 높일 수 있습니다.

특정 시점에는 사람의 지시도 여전히 유용할 수 있습니다. 에이전트는 어려운 문제를 포기하고 난이도를 잘못 판단하는 경향이 있습니다. 초반에 헬퍼들은 60개 명제 중 47개를 이번 실행의 예산 안에서는 불가능하다고 판단했지만, 팀은 결국 그중 대부분을 증명했습니다. 이런 순간에 사람이 격려하면 에이전트가 너무 일찍 멈추는 일을 막을 수 있습니다.

신중하게 설계한 안전 경계가 있었기에 이 실험을 시작할 수 있었습니다. Claude는 우리가 제공한 도구로 문제를 원하는 방식대로 풀 수 있었지만, 네트워크가 차단된 샌드박스 안에서, 서로 다른 두 모니터의 감시를 받으며 작업했습니다.

이런 방법은 빠르게 발전할 것으로 예상하며, 이 같은 팀이 더 어려운 작업을 맡을수록 이를 둘러싼 안전 경계도 보조를 맞춰야 합니다. 안전하게 확장한 멀티 에이전트 팀이 앞으로 우리가 마주한 가장 어려운 문제 가운데 일부를 푸는 데 도움이 되리라 믿습니다.