Cogentic: AI가 열린 수학 문제를 풀기까지 — Google Research의 다중 에이전트 증명 하드웨어 해설

한 문장 요약: 이 글을 읽으면 Google Research가 발표한 자동 증명 시스템 Cogentic이 어떤 구성요소로 증명을 만들고 검증하는지, 그리고 실제로 어떤 열린 문제를 무엇으로 개선했는지 이해할 수 있습니다.

개요

  • 주제: 다중 에이전트 오케스트레이션 기반 자동 증명 발견 시스템 Cogentic 해설
  • 핵심 관점: "더 많이 샘플링"이 아니라 증명–검증 루프 + 검증된 원장(ledger) 이 열린 문제 해결의 핵심이다
  • 핵심 키워드: Cogentic, 다중 에이전트, 자동 증명 발견, 적대적 검증, 추론 예산, Gemini 3.1 Pro / Gemini 4 Argon

논문 『Cogentic: Multi-Agent Orchestration for Automated Proof Discovery』(Google Research, 발행일 2026-10-01)는 저자들이 "우리는 자동 증명 발견을 위한 다중 에이전트 하드웨어(harness)를 제시한다"고 서술하며 시작합니다. 저자는 Yang Cai, Vineet Gupta, Yanchen Jiang, Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, Di Wang으로, 원문에 따르면 알파벳순으로 배열되었고 Yang Cai는 Yale University, Vineet Gupta는 Google DeepMind라는 추가 소속을 가집니다 (01_2609.40324v2.pdf, §1·§13. 저작권 및 저자 정보).

핵심 메시지 3가지

1. 단발 생성(single-shot)은 열린 문제에 부족하다

저자는 주장한다 — 프론티어 언어 모델은 한 번의 생성으로 강한 수학적 아이디어를 낼 수 있지만, 여러 경쟁 가설을 탐색하고 미묘한 기술적 장애물을 넘으며 중간 성과를 오랜 호라이즌에 걸쳐 보존해야 하는 열린 문제에는 단발 생성이 흔히 부족하다고. Cogentic은 이 세 가지를 반복적 prove–verify 루프로 해결하려 한다 (01_2609.40324v2.pdf, §1).

2. 검증은 '적대적'이어야 하고, 두 관점에서 동시에 이뤄져야 한다

원문에 따르면 초안은 개별 검증 + 같은 라운드 초안들의 병렬 대조 검증 두 가지를 모두 통과할 때만 accepted된다. 두 검증자는 모두 적대적이다 — "every step is wrong until justified, and every citation is incorrect until checked" (01_2609.40324v2.pdf, §2.2).

3. 검증된 조각은 원장에 축적되어 이후 라운드가 재사용한다

라운드마다 record(시도와 반론의 기록)와 ledger(검증된 중간 결과) 두 산출물이 남는다. 검증자가 증명 전체는 기각하면서 개별 레마를 확인하는 경우가 흔한데, auditor가 그 조각을 추출해 자기완결적 레마로 다시 쓰고 격리 상태로 재검증한다. 살아남은 것만 이후 prover가 재증명 없이 쓸 수 있게 된다. 반대로 반증으로 배제된 상계(bound)는 "excluded"로 기록해 다음 라운드가 재방문하지 않게 한다 (01_2609.40324v2.pdf, §2.3).

왜 기존 접근과 다른가 — 선행 연구의 지형

저자가 제시하는 관련 연구는 세 갈래로 정리된다.

갈래 대표 연구 저자가 지적한 전제 조건
형식 정리 증명 Lean, Isabelle/HOL, Coq; 전제 검색·전술 생성(Yang et al., 2023), 비형식 증명의 형식 스케치 컴파일(Jiang et al., 2022), RL 기반 올림피아드 수준 학습(Hubert et al., 2026) 기계 검증 보장은 주지만, Cogentic은 대비하여 자연어로 도메인 전문가가 검증할 수 있는 수학 산문을 생산
수학 객체 탐색 프로그램 탐색(Romera-Paredes et al., 2024), 진화 코딩 에이전트 AlphaEvolve(Novikov et al., 2025), 뉴로심볼릭 탐색(Trinh et al., 2024) "cheap, faithful, and machine-computable score"가 필요 — 모든 문제가 이 접근에 적합한 것은 아니다
추론 예산 확장 CoT(Wei et al., 2022), self-consistency(Wang et al., 2022), 반복 샘플링+셀렉터(Brown et al., 2024; Snell et al., 2024), 다중 에이전트 토론(Du et al., 2024; Liang et al., 2024) Cogentic은 prover–verifier의 반복 상호작용 위에 구축, 검증자는 증명이 틀렸거나 불완전하다는 가정에서 출발

또한 저자는 연구 수준 하네스 적용작(Feng et al., 2026; Gottweis et al., 2026; Lin et al., 2026; Schmitt et al., 2026; Zheng et al., 2026)을 열거하며 "포괄적 서베이를 시도하지 않는다"고 명시한다. Millennium Prize 문제 해결(OpenAI, 2026b) 등 대형 에이전트 시스템의 이정표를 언급하면서도, 자기 위치를 STOC·FOCS 수준의 열린 질문 + 상대적으로 낮은 추론 예산 O(100)~O(1000) Gemini 호출로 규정한다 (01_2609.40324v2.pdf, §1).

시스템 구성 — 연구 그룹을 그대로 옮긴 구조

저자는 "연구 그룹이 일하는 방식처럼 작업을 나눈다"고 설명한다 (01_2609.40324v2.pdf, §1).

구성요소 역할 핵심 제약
Orchestrator 전역 상태 추적, prover 슬롯을 연구 방향별 분할, summarizer 생성, 검증자 합의 평가, ledger·record 관리 수학적 유도 자체를 수행하지 않음
Literature reviewer 관련 연구·정리·정의 검색, 런 중간 재파견 가능 —
Prover 브리핑 기반으로 후보 증명을 독립·병렬 생성 방향은 배정받되 어떻게 일할지는 스스로 결정
Verifier 보완적 각도·범위에서 후보를 비판 적대적 가정에서 출발
Record / Ledger 시도–반론 기록 / 검증된 중간 레마 축적 에이전트 간 소통의 중심 통로
Advisor 라운드 간 검증 로그에서 패턴 도출, 지침·자원배분 조정 권고 수학적 의견 금지 — 답을 추측하거나 기법을 권고하거나 방향을 유망/폐기로 선언할 수 없음
Consolidation 최종 원고 서식·편집, comparator가 최강 검증 증명 선택, 최종 감사 편집 과정에서 오류가 도입되지 않았는지 승인 증명과 대조

참고: advisor를 별도 에이전트로 둔 이유는, 다수 에이전트를 동시에 거느려야 하는 orchestrator는 로그 추세를 검토·종합할 컨텍스트 윈도우가 거의 없기 때문입니다 (01_2609.40324v2.pdf, §2.4).

한 라운드의 진행 — prove–verify 루프

① 방향 설정 — orchestrator가 실행할 prover 수와 각자가 집중할 'direction'(구체적 주장·반례 탐색·유망 증명의 수리·마무리)을 계획
↓
② 브리핑 생성 — summarizer가 모든 과거 시도와 판정을 읽어 정보량이 큰 것만 골라 prover 개인용 브리핑을 독립적으로 작성 → 같은 라운드 prover들은 같은 역사에 대해 서로 다른 해석을 받는다
↓
③ 병렬 증명 초안 — prover는 긴 문서를 인용하지 않고 경로(path)로 받아 원하는 것만 골라 읽는다
↓
④ 이중 적대적 검증 — 개별 검증 + 라운드 전체 병렬 대조 검증, 둘 다 통과해야 accepted
↓
⑤ 기록·축적 — record와 verified ledger에 기입, process advisor가 지침 조정 권고
↓ ⑥ 종료·출력 — 초안이 검증을 통과하면 comparator가 최강 증명 선택 → formal writer가 완전한 원고로 확장 → 최종 검증 감사

종료 시점에는 "남은 유망 방향이 소진되면" 멈추며, 출력물은 실행 내역을 전혀 모르는 도메인 전문가가 읽고 검증할 수 있는 자기완결 문서입니다 (01_2609.40324v2.pdf, §2.1~§2.5).

비용 측면: 저자에 따르면 대부분 문제는 O(100) 모델 호출, 가장 어려운 문제는 O(1000) 사용. 시스템에는 호출 수 최적화 여지가 남아 있으며 동시에 더 어려운 문제로 자연스럽게 확장되는 것도 허용한다 (01_2609.40324v2.pdf, §1).

실제로 푼 문제 5가지 — 무엇이 얼마나 좋아졌나

각 결과는 동반 논문(companion paper)에서 전개되며, 문제 진술만 주어졌고 사람의 수학적 개입은 없었고, 모든 증명은 이후 도메인 전문가가 검증했습니다 (01_2609.40324v2.pdf, §3, Table 1).

문제 영역 이전 최선 Cogentic 결과
온라인 역선형 최적화 / 저-regret cutting plane 온라인 학습·최적화 효율적 O(d ln T); O(d)는 라운드당 T^Θ(d) 비용의 부적절(improper) 규칙만 T에 대해 일관된 최초의 효율적·최초의 적절(proper) O(d) 한계, 라운드당 O(d²) (Cai et al., 2026a)
양면 Bulow–Klemperer 경쟁 복잡도 경매·시장 설계 O(1) 에이전트로 충분하나 양측 각각 상수 최소 20,000 필요 작은 쪽에 +2명만으로 충분: STR(m, n+2) ≥ OPT(m, n), +1은 어떤 DSIC·IR·약한 예산균형 메커니즘에도 불충분 (Cai et al., 2026e)
n-전문가 anytime regret 온라인 학습 anytime √t ln n vs 고정 horizon √t ln n/2, 인자 √2 미해결 (1 + O(√(ln ln n / ln n)))√(t ln n / 2) — anytime 유효성에 선차수 가격 없음 (Cai et al., 2026b)
단순 vs 최적 수익 (가법 단일 구매자) 메커니즘 설계 5.2·max(SRev, BRev) ≥ OPT (Ma and Simchi-Levi, 2021) 3.52·max(SRev, BRev) ≥ OPT (Cai et al., 2026d)
자동 입찰 경매의 무정부성 가격 경매·autobidding 입찰자 2명 PoA 1.8; 일반 n 입찰자 최적 메커니즘 미해결 2명 최적 PoA 1.5 (익명·단조 메커니즘); n 입찰자 2 − 1/(4n+1) (Cai et al., 2026c)

개별 결과의 성립 조건과 기술 포인트

① 역선형 최적화 (Theorem 1) — 성립 조건: 결정적(proper)·anytime 알고리즘, 라운드당 O(d²) 산술 연산 + 선형 최적화 1회. 한계는 horizon T에 대해 일관(uniform)이며 최적과 O(√d) 인자 차이 — 모든 알고리즘은 Ω(√d)를 감수한다(Sakaue et al., 2025b). 기술 핵심은 log det H_t potential(모든 이전 체적 분석에서 ln T의 원천)을 trace power tr(H_t^{-1/2}) 로 교체한 것 (01_2609.40324v2.pdf, §3.1).

후속 연구 균형: 원문에 따르면 동반 논문 이후 Sakaue (2026b)가 빈틈없는 O(√d) 한계를 얻었으, 그 알고리즘은 비효율적이며 효율적 O(√d) 알고리즘 확보는 여전히 열린 질문이다 (01_2609.40324v2.pdf, §3.1).

② 양면 시장 (Theorem 2) — 성립 조건: 모든 m ≥ n ≥ 1에서 구매자 분포 F_B가 판매자 분포 F_S를 1차 확률적 지배(first-order stochastically dominates) 할 때, 정확히 두 명의 판매자(작은 쪽) 추가로 Seller Trade Reduction이 기대 GFT가 원 시장의 first-best GFT 이상을 달성. 타이트: m = n = 1에서도 판매자 1명 추가는 어떤 사전독립 메커니즘에도 불충분. 상수는 측당 최소 20,000 → 한쪽에 2로 줄고 모집은 단면이다 (01_2609.40324v2.pdf, §3.2). 선행 흐름은 Babaioff et al. (2020a)의 n(m + 4√m) 구매자 추가 → Cai et al. (2024)의 양측 O(1)로 이어집니다.

③ Anytime regret (Theorem 3) — 성립 조건: 손실 벡터가 [0, 1]ⁿ의 모든 수열에 대해 모든 t ≥ 1에서 동시에 성립. 기하 격자 Hᵐ = (1 + ε)ᵐ 위에 multiplicative-weights 인스턴스들을 master MW로 집계하고, 인스턴스 m을 ⌊δHᵐ⌋ 라운드에 깨워 ⌊Hᵐ⌋ 이후 퇴역시켜 동시에 깨어 있는 인스턴스를 O(ε⁻¹ log δ⁻¹)개로 상수 한정한 것이 장애물 해소의 핵심. ε = √(ln ln n / ln n), δ = ε³으로 격자 거칠기·집계 오버헤드·재귀가 합쳐져 1 + O(ε) 인자. 선행 연구의 기여도 균형 있게 보면: Cover(1966)의 고정시각 regret, Luo and Schapire(2014)의 n=2에서 anytime이 엄격히 큼을 증명, Harvey et al. (2023)의 n → ∞에서 선상수가 일치한다는 추측, Harvey et al. (2024)의 독립 브라운 운동 연속시간 근거가 배경이며, Cogentic은 이 추측을 증명했다고 원문은 서술한다 (01_2609.40324v2.pdf, §3.3).

④ 수익 근사 (Theorem 4) — 성립 조건: n개 품목에 대한 값이 독립인 단일 가법 구매자. Cai et al. (2016)의 이중성 프레임워크 OPT ≤ SRev + E[V − M_max]에서 출발해, 기존의 SRev 절단·Core/Tail 분할 대신 공통 척도 M = max{SRev, BRev}에서 절단해 Tail 분석을 완전히 제거. 극단 분포로 E[V_M²]의 2차 모멘트 경계를 유도. 참고로 근사비율 하한은 여전히 2(Rubinstein, 2016)입니다 (01_2609.40324v2.pdf, §3.4).

⑤ 자동 입찰 PoA (Theorem 5) — 메커니즘은 r-비례 선가격 경매 pFPA_r (입찰자 i의 낙찰 확률 x_{i,j} = b_{i,j}^r / Σ_k b_{k,j}^r). 성립 조건 주의: 정리 제2부의 상한은 입찰이 지배적이지 않을(undominated) 때만 성립한다 — "no bidder can raise their bid on any query to win more while satisfying their RoS constraint". 즉 RoS(return-on-spend) 제약을 만족하면서 어떤 쿼리에서든 입찰을 올려 더 많이 이길 수 없는 경우에 한정됩니다 (01_2609.40324v2.pdf, §3.5). 선행 지형은 Aggarwal et al. (2019)의 SPA PoA 2 → Liaw et al. (2023)의 결정적 메커니즘 장벽 2 및 하한 2 − 4/(n+4) → Mehta (2022) 약 1.89 → Liaw et al. (2023) 상한 1.8로 이어집니다.

흥미로운 점을 원문에서 그대로 옮기면: 제1부의 1.5는 저자들이 이미 추측하고 있었으나 증명이 없었고, 제2부는 저자들이 이전에 연구해 본 적이 없으며 시스템에 어떤 힌트도 주지 않았는데, 시스템이 메커니즘과 분석을 독립적으로 도출했다고 서술합니다 (01_2609.40324v2.pdf, §3.5).

저자가 스스로 밝힌 한계와 토론

  • 자연어 증명 + 전문가 검증이 가능했던 것은 문제 선택 방식 때문이다 — 저자들이 실제로 일하는 영역에서 가져왔기 때문이며, 일부 동반 논문에는 해당 문제를 이미 연구 중이던 공저자가 포함된다. 저자들은 주장을 검토하고 설명을 썼으며, 경우에 따라 하드웨어가 한 것보다 further 나아갔다 (01_2609.40324v2.pdf, §4).
  • 초기 논문은 자체적으로 일관되고 읽기 좋았지만, 문헌 내 위치 배치·프레이밍·기법의 정리와 설명은 저자들이 추가했다고 서술합니다.
  • 저자는 시스템이 읽는 속도보다 빠르게 후보 결과를 생산할 수 있고 그 격차는 컴퓨트 예산이 커지며 벌어진다고 지적한다. Lean 등 증명 보조기로 형식화하면 정확성은 기계적으로 확정되지만 인간의 이해는 뒤처질 수 있다 — 이 균형은 여전히 중요한 질문이라고 저자는 주장한다 (01_2609.40324v2.pdf, §4).

관점 포인트 — 실무자가 짚어야 할 5가지

  • 검증 이중화: 개별 검증만으로는 부족하다 — 같은 라운드 초안들을 병렬 대조하는 검증자가 공통 맹점을 잡는다
  • 컨텍스트 윈도우 관리: 모든 이력을 넘기지 않고 summarizer가 프로버별 브리핑을 만들고, 긴 문서는 인용이 아닌 경로 전달
  • 권한 제한이 곧 안전장치: orchestrator와 advisor는 수학적 의견을 낼 수 없다 — 시스템의 방향 결정은 증거(검증 로그)에서만 나온다
  • 부정 결과의 자산화: 배제된 bound·실패한 시도를 record/ledger에 남겨 같은 길을 반복 탐색하지 않게 한다
  • 성립 조건의 확인: PoA 상한의 'undominated' 조건, 양면 시장의 FOSD 조건처럼 결정문만 인용하면 조건이 빠진다

최종 핵심 정리

확인해 볼 핵심 질문:

  • Cogentic은 형식 증명기(Lean 등)를 대체하는가? → 아니라 자연어 산문 + 전문가 검증이라는 다른 축을 택했다
  • 추론 예산은 얼마인가? → 대부분 O(100), 최악 O(1000) Gemini 호출
  • 5개 결과 모두 사람이 개입해 만들었는가? → 문제 진술만으로 자동 생성, 이후 전문가가 검증
  • 가장 눈에 띄는 수치 개선은? → 얈면 시장 상수 최소 20,000(측당) → 한쪽에 2, 수익 근사인자 5.2 → 3.52, autobidding 2인 PoA 1.8 → 1.5
  • 남은 열린 질문은? → 효율적 O(√d) 역선형 최적화, 근사비율 하한 2와의 간극, 그리고 생성 속도와 인간 이해의 균형

한 줄 요약: Cogentic의 본질은 "더 똑똑한 모델"이 아니라, 적대적 이중 검증과 검증된 원장 위에서 실패까지 기록하며 반복하는 연구 그룹의 작업 방식을 코드로 옮긴 것이다.