Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science

Paper: Honghao Lin; David P. Woodruff; Yuan Deng; Jieming Mao; Song Zuo; Vahab Mirrokni (2026). Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science. Google Research. Lin과 Woodruff는 공동 제1저자입니다. arXiv:2609.15983v1 · PDF. 2026년 9월 14일 공개된 v1을 기준으로 합니다.

이 글은 여러 에이전트가 긴 수학 연구를 이어 가도록 구성한 하네스와 주요 결과를 설명합니다. 증명 전략·다섯 연구 성과·TCS 채점 절차·Codeforces 비교 조건의 상세 분석은 상세 읽기에 있습니다. 아래의 성과는 논문 보고 수치이며, 하네스나 증명을 다시 실행해 확인한 결과가 아닙니다.

긴 증명은 글을 길게 생성하는 것만으로 완성되지 않습니다. 어느 접근을 계속할지 정하고, 증명을 작은 일로 나누고, 서로 의존하는 가정을 맞추고, 문제가 생기면 어느 부분을 고칠지 알아야 합니다. Stellar Colosseum은 이 작업을 여러 단계와 역할로 나눕니다. 핵심은 새로운 기반 모델이라기보다 연구 진행 상태와 검토를 관리하는 다중 에이전트 하네스입니다.

1. 증명 계획이 준비됐는지 먼저 묻는다

먼저 탐색 역할이 가능한 전략과 그 전략을 무너뜨릴 반례를 찾습니다. 그다음 readiness gate가 증명이 완성됐는지를 묻는 대신, 남은 문제를 안정된 증명 계획의 각 단계에 맡길 수 있는지 판단합니다. 해결되지 않은 보조정리가 남아 있어도 어디서 어떻게 풀지 명시할 수 있으면 나아갈 수 있지만, 중심 아이디어가 바뀌어야 하는 공백이라면 탐색으로 돌아갑니다.

준비가 되면 증명 골격을 절별 작업과 의존성 그래프로 나눕니다. 독립적인 부분은 병렬로 풀고, 선행 결과가 필요한 절은 그 결과가 준비된 뒤 시작합니다. 부분 검토 후에는 전체 원고를 다시 읽어 가정·표기·절 사이 연결과 결론이 맞는지 확인합니다. 문제가 국소적이면 해당 절을 고치고, 중심 전략이 실패하면 탐색 단계로 돌아갑니다.

Figure 1. 위쪽은 전략 탐색부터 readiness gate, 증명 분해, 부분 풀이와 전역 검토까지의 흐름입니다. 아래쪽은 후보와 그에 대한 반론을 함께 여러 그룹에 전달해 합성하는 방식입니다. 출처: Lin et al. (2026), arXiv v1, p. 2, Figure 1.

여기서 “준비”나 “검증”은 자동으로 증명이 참임을 보장한다는 뜻이 아닙니다. 에이전트가 자연어 논증을 검토하는 절차이지 Lean 같은 증명 커널로 형식 검증하는 시스템은 아닙니다. 어려운 공백을 미해결 상태로 표시하고 다음 작업을 정리하는 구조에 가깝습니다.

2. 후보와 반론을 함께 넘기고, 단순 투표는 피한다

각 단계에서 여러 증명 후보를 만들고 반증 역할이 각 후보의 허점이나 빠진 조건을 찾습니다. 합성 단계는 후보와 비평을 묶어서 다음 단계에 넘깁니다. 각 묶음 안에서는 중복 없이 몇 후보를 뽑지만, 서로 다른 묶음은 일부 후보를 공유할 수 있습니다. 다음 합성기는 서로 맞는 증명 조각을 합치고, 충돌이나 반론은 수정하거나 미해결 사항으로 남깁니다.

따라서 이 방식은 다수결로 가장 인기 있는 답을 선택하는 절차가 아닙니다. 논문은 이전 증명 초안과 검토 의견을 이어 주고, 실패·문헌·계산 관찰을 별도의 지식 디렉터리에 보존한다고 설명합니다. 하지만 이 지식 공간 자체가 오류 없는 정리만 저장하는 형식적 데이터베이스는 아닙니다.

3. 논문은 다섯 수학 결과와 긴 증명 사례를 보고한다

논문은 하네스가 여러 연구 성과에 기여했다고 보고합니다. 아래는 각 결과의 방향을 쉽게 요약한 것이며, 완전한 정리·가정·증명은 논문이 연결하는 별도 연구를 보아야 합니다.

• Strong coreset: 모든 저차원 부분공간의 비용을 근사하는 표본 크기에서, p>2 조건으로 오차 ε에 대한 의존성을 개선했다고 보고합니다.
• 희소 최소제곱: 특정 무작위 Small-Set Expansion 가설 아래에서, 특정 정확도와 성공확률을 유지하며 해를 더 희소하게 만드는 데 한계가 있음을 보입니다. 무조건적인 불가능 정리는 아닙니다.
• 단일 벡터 임베딩: 최대 내적 검색을 위한 표현 차원의 하한을 높여 기존 상한과의 간격을 줄입니다. 어려운 경우가 존재한다는 결과이지 모든 데이터에서 벡터 검색이 실패한다는 뜻은 아닙니다.
• Hadamard 양자화: 특정 단위 입력·고정 질의·점근 조건에서 양자화 상한의 선도상수를 줄이고 잔여 단계가 필요 없는 구성을 보고합니다. 5.93은 실측 검색 속도 향상 배수가 아닙니다.
• Prefix 행렬 분해: 행렬 분해의 하한을 기존 상한과 로그로그 인자만큼 차이가 남는 수준까지 끌어올렸다고 보고합니다.

긴 초안 사례도 같은 수준으로 해석해야 합니다. Knuth cycles의 46쪽·75쪽 증명 초안은 긴 논증을 처리한 사례이지 새 문제를 최초 해결했다는 증거는 아닙니다. Erdős unit-distance 문제의 22쪽 초안도 주요 전략을 재발견한 사례로 보고하지만, 공개 README에는 공식 오류와 증명 공백이 적혀 있습니다. 인터넷을 막은 실행이라는 사실만으로 학습 데이터에 그 아이디어가 없었다고 입증되지는 않습니다.

4. TCS-Bench 71%는 두 실행을 고른 결과다

TCS-Bench의 300개 수학·이론 컴퓨터과학 과제에서 Colosseum 실행 하나의 채점 결과는 Gemini 3.1 Pro 54%, Gemini 3.7 Flash 55%였습니다. 저자들은 두 실행을 따로 만든 뒤 별도의 Flash 비평으로 어느 증명을 제출할지 고르는 절차에서 71.0%를 보고합니다. 두 실행 중 사후에 더 잘한 쪽을 고르는 oracle은 77.3%였습니다.

Table 2. 인쇄된 benchmark 정확도입니다. 71.0%는 두 Colosseum 실행의 cross-model selection 결과이고, 77.3%는 결과를 알고 난 뒤 더 나은 실행을 고르는 oracle입니다. 출처: Lin et al. (2026), arXiv v1, p. 13, Table 2.

선택 규칙은 Pro 실행을 Flash가 여덟 번 비평하게 한 다음 최소 다섯 번 맞다고 판단하면 Pro 증명을, 아니면 Flash 증명을 제출하는 방식입니다. 그러므로 71%는 한 번의 모델 실행 결과나 단순 투표 점수가 아닙니다. 반면 77.3% oracle은 어느 실행이 맞았는지 미리 아는 사후 상한이므로 실제 배포 가능한 선택기와 같지 않습니다.

채점기는 기준 증명을 참고하는 자동 평가기입니다. 별도 전문가 라벨 100개로 채점 프롬프트를 다듬었다고 보고하지만, 이는 새로운 테스트 집합에서 검증한 정확도나 형식 증명 검증과 같지 않습니다. 또한 71%가 여러 호출을 포함한 두 실행의 결과이므로, 동일 계산 예산에서 단일 모델보다 나았다고 단정하기 어렵습니다.

5. Codeforces에서는 다섯 문제 더 통과했지만 조건이 다르다

222개 Codeforces 문제에서 실행 probe를 쓴 설정은 218개를 통과했고, probe가 없는 설정은 213개를 통과했습니다. probe는 공개 예제뿐 아니라 모델이 만든 스트레스 입력을 실행해 시간·메모리·checker 결과를 수정 과정에 되돌려 줍니다. 숨은 테스트는 개발 과정에서 읽지 않고 최종 제출 채점에만 사용합니다.

Table 5. 222문제 중 accepted 수와 논문이 계산한 corpus 성능 rating입니다. 두 설정은 revision 예산도 달라 probe 하나의 효과를 분리하지 못합니다. 출처: Lin et al. (2026), arXiv v1, p. 15, Table 5.

218 대 213은 관측된 결과 차이입니다. 저자들은 두 설정의 수정 예산이 다르고, probe를 제외한 모든 조건을 고정한 인과 절제 실험은 아니라고 밝힙니다. 따라서 다섯 문제 차이를 실행 피드백만의 효과라고 말할 수 없습니다. 표의 4263과 3918도 이 문제 묶음의 논문 산출 rating이지 공식 대회 참가자 rating은 아닙니다. 숨은 테스트 통과는 강한 실행 증거지만 가능한 모든 입력에 대한 수학적 증명은 아닙니다.

6. 설계의 장점과 남은 검증 질문

Colosseum의 실용적 아이디어는 탐색과 증명 작성 사이에 준비도 판단을 두고, 후보에서 반론을 떼지 않은 채 절별 작업과 전체 논증을 각각 검토하는 것입니다. 작업 상태와 실패 기록을 보존해 무엇을 수정할지 좁히는 구조도 긴 추론에서 유용할 수 있습니다.

다만 총 호출·토큰·시간·비용과 같은 계산 예산이 모든 기준선과 맞춰진 비교는 없습니다. readiness gate, 중첩 표집, 기억 디렉터리 같은 구성요소의 효과를 각각 분리한 절제 실험도 부족합니다. 반례를 찾지 못했다는 사실이나 자연어 검토 통과만으로 증명이 참이 되지는 않습니다. 저자들이 제시한 수학 성과와 벤치마크 결과는 유망한 사례이지만, 어떤 모듈이 얼마만큼 기여했는지 또는 모든 결과가 독립 검증됐는지는 별도 질문입니다.

따라서 이 논문은 “AI가 긴 수학 연구를 오류 없이 자율 수행했다”기보다, 연구 과정을 단계·의존성·반론·수정 이력으로 조직하는 하네스와 그 활용 사례로 읽는 것이 적절합니다. 71%는 2회 실행의 선택 성과이고, 218/222는 probe와 수정 예산이 함께 달라진 구성의 비교라는 점을 기억해야 합니다.

같이 읽기: Cogentic · Context Language Models

상세 읽기

References

Lin, H., Woodruff, D. P., Deng, Y., Mao, J., Zuo, S., & Mirrokni, V. (2026). Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science [Preprint]. arXiv. https://arxiv.org/abs/2609.15983v1