구글 연구진이 수학과 이론 컴퓨터과학 연구에 추론 자원을 배분하는 다중 에이전트 하니스 Stellar Colosseum을 공개했다. FOCS·STOC·SODA 논문에서 뽑아낸 연구급 정리 증명 과제 벤치마크에서 정확도 71.0%를 기록했다고 밝혔다. Honghao Lin, David P. Woodruff, Vahab Mirrokni 등이 참여한 이 논문은 설계 단계부터 모델에 종속되지 않도록 만든 시스템을 설명하며, 해당 기술은 이미 Google Antigravity에 통합됐다.
출발점은 익숙한 실패 양상이다. 언어 모델은 짧은 증명은 그럴듯하게 써내지만, 불확실하고 서로 얽힌 판단이 사슬처럼 이어지는 장기 과제에서는 성능이 무너진다. 초반에 한 번 잘못 확정하면 그 뒤 전부가 오염된다. Colosseum의 대답은 증명을 하나의 궤적으로 다루기를 그만두는 것이다.
핵심 요약
- Stellar Colosseum은 Gemini 3.1 Pro와 Gemini 3.7 Flash를 함께 써서, FOCS·STOC·SODA 논문에서 가져온 연구급 정리 증명 과제 모음 TCS-Bench에서 71.0%를 기록했다.
- Gemini 3.1 Pro로 진행한 별도 Codeforces 평가에서는 실행 피드백을 붙인 증명 지향 파이프라인이 222문제 중 218문제를 풀었다.
- 이 작업 흐름은 현재 Google Antigravity의 Teamwork 프레임워크에 Long Proof 패턴으로 들어가 있으며, 유료 요금제에서 프리뷰 명령으로 쓸 수 있다.
하니스는 연산을 어디에 쓰나
Colosseum은 증명을 쓰기로 확정하기 전에 여러 단계를 거친다. 먼저 그럴듯해 보이는 첫 경로로 곧장 파고들지 않고 대안 전략들을 탐색한다. 이어 준비도 게이트를 적용해 해당 경로가 분해할 만큼 무르익었는지 판단한다. 그 뒤에야 증명 계획을 서로 의존하는 섹션 단위 하위 문제 집합으로 표현한다.
검증은 이 구조에 도로 연결된다. 검증기가 문제를 짚어내면, 처음부터 다시 시작하는 대신 그 지적이 영향을 주는 논증 부분으로 결과가 전달된다. 모든 단계에서 하니스는 후보를 병렬로 생성하고, 표적화된 반증으로 이를 공격하며, 후보와 그에 대한 비판을 하나의 연구 산출물로 합친다. 저자들은 이 방식을 중첩 무작위 표본 트리 집계라고 부른다.
단일 에이전트의 컨텍스트를 키우고 더 오래 생각하게 하는 접근과는 베팅의 방향이 다르다. 오히려 작은 적대적 연구 그룹을 굴리는 쪽에 가깝다. 다만 여기서 스케줄링되는 값비싼 자원은 연구자의 시간이 아니라 추론이다.
벤치마크 수치가 말하는 것
TCS-Bench는 모델 발표에 단골로 등장하는 경시대회 수학 문제 모음보다 난도가 높다. 과제 자체가 이 분야 최상위 이론 학회 세 곳에 채택된 논문에서 나왔기 때문이다. 71.0%라는 수치는 혼합 구성에서 나왔다. Gemini 3.1 Pro에 더 저렴한 Gemini 3.7 Flash를 붙인 조합이다. 하니스가 모든 호출을 최대 모델로 몰아서가 아니라 조율을 통해 품질을 회복한다는 뜻으로 읽힌다.
Codeforces 결과는 범위가 좁지만 눈에 띈다. 실행 피드백을 루프에 넣어 222문제 중 218문제를 풀었다. 두 수치 모두 저자들이 직접 수행한 평가에서 나왔고, 아직 독립적으로 재현되지 않았다. 모든 에이전트 스캐폴드 논문에 붙는 벤치마크 단서가 여기에도 그대로 붙는다. 하니스 성적은 재구현 과정에서 좀처럼 살아남지 못하는 프롬프트와 도구 설정의 세부에 악명 높을 만큼 민감하다.
논문에서 제품으로
대부분의 연구용 스캐폴드와 달리 이쪽은 이미 제품 접점이 있다. 구글은 Colosseum 작업 흐름을 Antigravity의 Teamwork 프레임워크에 Long Proof 패턴으로 통합했다고 밝혔다. 시스템이 골라 쓰는 다섯 개 패턴 중 하나다. 구글은 Teamwork가 미해결 문제에서 일곱 건의 결과를 냈으며, 여기에는 JMLR 논문의 희소 볼록 최적화 문제와 Lean으로 검증한 커누스의 사이클 추측이 포함된다고 설명했다.
논문은 FOCS와 JMLR 논문의 미해결 문제를 다룬 새로운 결과를 얻었다고 주장한다. 이는 벤치마크 정확도와는 성격이 전혀 다른 주장이고, 학계가 가장 날카롭게 들여다볼 대목이기도 하다. OpenAI가 에이전트 1만 개로 시도한 나비에-스토크스 증명 때도 헤드라인보다 단서 조항이 더 중요했다. 다만 Lean 형식 검증 덕분에 구글은 그 주장의 적어도 일부에서 더 단단한 발판을 확보했다.
자주 묻는 질문
TCS-Bench란 무엇인가?
TCS-Bench는 이론 컴퓨터과학 분야 대표 학회인 FOCS, STOC, SODA에 실린 논문에서 뽑아낸 연구급 정리 증명 과제 벤치마크다. 경시대회식 연습 문제가 아니라 열린 연구 문제를 겨냥한다. Stellar Colosseum은 Gemini 3.1 Pro와 Gemini 3.7 Flash 조합으로 여기서 71.0% 정확도를 기록했다고 보고했다.
Stellar Colosseum은 Gemini에 묶여 있나?
그렇지 않다. 저자들은 이 하니스를 모델에 종속되지 않는 구조로 설명한다. 어떤 모델이 호출을 처리하든 그 위에 얹히는 스케줄링·집계 계층이라는 것이다. 다만 공개된 평가가 Gemini 3.1 Pro와 Gemini 3.7 Flash로 이뤄진 만큼, 보고된 수치는 아키텍처 자체가 아니라 해당 모델에 한정된 결과다.
지금 개발자가 쓸 수 있나?
간접적으로 가능하다. Colosseum 작업 흐름은 Google Antigravity의 Teamwork 프레임워크에서 Long Proof 패턴으로 제공되며, 유료 요금제의 프리뷰 명령 형태다. 논문 자체는 arXiv 프리프린트이며 동료 심사를 거치지 않았다.
