구글 리서치, 안티그래비티 팀워크 연구 성과 공개

구글 리서치가 11월 13일(미국 시간) 안티그래비티의 다중 에이전트 기능 팀워크(/teamwork)로 수학, 화학, 시스템 소프트웨어, 머신러닝 엔지니어링의 미해결 문제를 풀어낸 연구 성과를 공개했다. 글을 쓴 바합 미로크니 구글 펠로 겸 구글 리서치 부사장은 "이 모든 작업은 인간 전문가와 협업해 이뤄졌다"며 연구에 쓴 에이전트 도구를 외부에도 열겠다고 밝혔다. 성과는 2013년 정보이론 추측의 완전한 증명, 1974년 들리뉴가 증명한 베유 추측의 기계 검증, C++ 운영체제 커널의 러스트 재작성까지 걸쳐 있다. 구글은 학계 연구자 1만 명에게 최상위 사용 등급을 6개월 동안 무료로 주는 신청도 열었다.

팀워크의 설계는 언어 모델의 두 가지 약점에서 출발했다. 첫째는 한 번의 생성이 정답에 닿는다는 보장이 없다는 점이다. 팀워크는 여러 후보를 병렬로 탐색하고, Lean 4 증명 검사기와 손대지 않은 테스트 묶음, 실행 시뮬레이터, 웹 검색, 하드웨어 카운터 같은 반증 장치로 어느 후보가 맞는지 자동으로 가린다. 둘째는 며칠짜리 작업에서 맥락 창이 커지며 세부를 놓친다는 점이다. 팀워크는 에이전트마다 그 단계에 필요한 파일과 도구만 주고, 조정자가 새 후임 에이전트에게 일을 넘기며, 비평가와 감사 에이전트가 원래 작성자의 추론을 모르는 깨끗한 맥락에서 결과를 검증한다.

수학에서 가장 큰 성과는 코타드·쿠마르 추측의 증명이다. 구글과 홍콩중문대, 서던캘리포니아대, 카네기멜런대 연구진은 팀워크의 긴 증명 패턴으로 2013년 제기된 이 추측을 완전한 일반성으로 증명했다. 잡음이 섞인 통신로를 지나는 비트열을 한 비트로 압축할 때 입력 비트 하나를 그대로 베끼는 독재자 함수보다 정보를 더 많이 보존하는 방법은 없다는 내용이다. 제미나이가 먼저 일반화된 추측의 반례를 찾았고, 홍콩중문대 팀이 문제를 14개 변수 최적화로 줄이자 Gemini 4 Argon이 대부분의 새 해석적 경계와 구간 산술 인증서를 만들었다. 연구진은 증명 전체를 Lean 4로 옮겼고, 그 코드는 5,000만 줄에 이른다.

미해결 문제를 그대로 던져 증명을 받아 낸 사례도 이어졌다. 적응형 데이터 분석에서는 2014년부터 열려 있던 표본 수 격차를 닫았고, 양자 계산에서는 같은 해 제기된 질문에 답해 상수 오차에서 n/2번보다 많은 양자 질의가 필요한 n비트 불 함수를 처음 찾았다. 정수 곱셈에서는 2차원 격자 하나에서 도는 새 O(n log n) 알고리즘을 만들었고, 그 C 구현은 10억 비트까지 GNU 다중 정밀도 산술 라이브러리와 비트 단위로 같은 결과를 냈다. 메탈이 확인한 65쪽 분량 논문 원문은 타잔이 1985년 제기한 스플레이 트리 덱 추측에서 모든 유한 반복 역아커만 함수를 넘어서는 새 상한을 증명했고, 저자에는 미로크니 부사장과 데이비드 우드러프, 고란 주지치 등이 이름을 올렸다.

형식 검증의 규모도 커졌다. 구글 클라우드 AI와 함께 만든 다중 에이전트 틀 LEAP은 팀워크와 결합해 베유 추측 전체를 사람 손 없이 기계 검증 코드로 옮겼다. 분량은 Lean 약 180만 줄이고, 하위 에이전트 호출은 2만 8,800번이었다. 일반 정수환 위 힐베르트 열 번째 문제의 최근 증명은 91만 9,000줄이 넘는 Lean으로 처음 형식화했다. 1927년부터 열려 있던 버코프 추측과 50년 넘게 풀리지 않은 3차원 보흐너·리스 추측도 처음 형식화했는데, 후자에서는 최근 공개된 비형식 증명의 빈틈을 찾아 메웠다. 2019년 수학연보에 실린 킬립과 비샨의 57쪽 논문, KdV 물결 방정식이 H⁻¹ 공간에서 잘 정의된다는 정리도 형식화 목록에 들어갔다.

논문 심사 보조 도구 딥 리뷰의 현장 성적도 공개됐다. 2027년 STOC 학회를 앞두고 전체 투고의 3분의 1이 넘는 578편의 저자가 원고 피드백을 신청했다. 진행 중인 저자 설문 응답자 70명 가운데 90%가 피드백이 대부분 또는 거의 모두 사실에 맞다고 답했고, 90%가 다시 쓰겠다고 했다. 30% 넘게는 딥 리뷰가 실질적인 증명 오류나 수학적으로 중요한 오타를 잡았다고 답했고, 14%는 고치는 데 한 시간 넘게 걸린 기술적 빈틈을 찾았다고 했다. 한 저자는 "이런 도구는 더 깨끗하고 정확한 연구를 더 빨리 내도록 도울 수 있다"고 답했다.

실험 과학에서는 생성 에이전트와 검증 에이전트를 짝지었다. 핵자기공명 데이터로 분자 구조를 알아내는 과제에서 30개 에이전트를 물리 기반 스펙트럼 시뮬레이터와 묶은 자기 교정 고리는 복잡한 벤치마크 분자에서 1순위 정확 일치 95%, 상위 3순위 정확도 100%를 기록해 단일 에이전트 성적을 두 배 가까이 끌어올렸다. 인과 추론 벤치마크 제작에서는 사람이 정한 기준 다섯 개를 받은 Argon 에이전트 29개가 11.5시간 동안 공개 표 13개를 과제 50개짜리 벤치마크로 만들었다.

시스템 엔지니어링 수치는 더 직접적이다. 팀워크와 Argon으로 만든 FarArray 위의 연결 요소 계산은 1조 개 간선 그래프까지 확장되며 TCP 키값 저장소보다 처리량 60~90배, 속도 40~180배를 내면서 메모리는 6분의 1만 썼다. 그래프 신경망용 TPU 커널은 고대역폭 메모리 사용을 최대 185분의 1로 줄였다. 9x9 바둑 엔진은 기본 AlphaZero 구현에서 출발해 8일이 안 되는 사이 자기 대국 속도를 2,300배 높이고 Elo를 약 2,600점 올려 1,885점에 닿았다.

코드 이전 작업에서는 러스트 재작성이 눈에 띈다. 팀워크의 새 재작성 패턴은 모듈을 의존 모듈이 컴파일된 뒤에만 배정하고, 원본 테스트 묶음을 고치지 않은 채 연결해 검증한다. 처음 25%만 옮겨져 있던 Zircon 마이크로커널은 2주짜리 Argon 작업으로 나머지 C++ 코드가 약 80만 줄의 안전한 러스트로 바뀌었고, 모든 커널 단위 테스트를 통과해 arm64 하드웨어에서 부팅했다. 구글의 AV1 영상 디코더 libgav1은 약 17만 줄 러스트로 옮겨졌는데, 처음에는 원본보다 4배쯤 느렸지만 프로파일링 도구를 받은 뒤 x86_64와 ARM 모두에서 원래 C++와 손으로 최적화한 어셈블리보다 20~30% 빨라졌다.

구글 내부 인프라에도 적용됐다. 전사 메모리 최적화 작업은 처음 추정한 1PiB 절감을 넘어섰고, 클러스터 관리 시스템 보그의 스케줄링 최적화는 변경 2건을 배포해 일부 하드웨어에서 TPU 작업 선점을 24% 줄였다. TPU 커널 최적화 패턴 DuoDiscover는 7~32분 걸리던 하드웨어 평가 대신 23초짜리 대리 평가기를 만들어, JAXBench 커널 17개에서 기준 구현보다 기하평균 4.09배 빠른 결과를 얻었다.

이번 발표는 팀워크의 두 번째 성적표다. 보도에 따르면 구글은 8월 27일 안티그래비티 블로그에서 Gemini 3.7 Flash와 팀워크로 FOCS·JMLR 등 학술지에 걸린 미해결 문제 7개를 풀고 RISC-V CPU 시뮬레이터를 처음부터 만들었다고 밝혔다. 석 달 만에 바탕 모델이 Gemini 4 세대로 바뀌었고, 대상도 증명 몇 편에서 운영체제 커널과 사내 인프라로 넓어졌다. 메탈은 구글 리서치의 논문 검증 에이전트 딥 리뷰 공개와 구글 딥마인드의 Gemini 4 Argon 공개를 보도한 바 있다.

AI 엔지니어의 눈으로 보면 이 글의 핵심은 수학 난제의 목록보다 검증 장치의 배치에 있다. 모든 성과 옆에는 Lean 4 검사기, 고치지 않은 테스트 묶음, 하드웨어 타이머처럼 모델 바깥의 판정자가 붙어 있다. 에이전트 수를 늘리는 것만으로는 답이 나오지 않고, 각 에이전트가 무엇을 보고 누가 그 결과를 반증하는지를 설계해야 며칠짜리 작업이 무너지지 않는다는 것이 구글이 수십 개 사례로 보여 준 방법론이다. 구글은 앞으로 몇 주 안에 형식 증명 패턴과 추가 전문 작업 흐름을 안티그래비티에 넣고 심층 튜토리얼을 내겠다고 밝혔다.