구글 Cogentic이 다중 에이전트 검증 루프로 미해결 정리 증명을 찾아낸다

무엇인가

이 논문은 미해결 연구 문제, 특히 이론 컴퓨터과학과 수학의 열린 문제에 대해 자연어 증명을 자동으로 찾아내는 다중 에이전트 하네스 Cogentic을 제안한다. 저자들은 최신 언어 모델이 한 번의 생성으로 강한 수학적 아이디어를 낼 수는 있지만, 여러 경쟁 가설을 탐색하고 미묘한 기술적 장애를 넘어서며 장기간에 걸쳐 중간 성과를 유지해야 하는 열린 문제에는 단발 생성이 불충분하다고 본다. 기존 접근과의 차이도 분명히 한다. Lean·Isabelle/HOL·Coq 같은 대화형 정리 증명기는 기계 검증된 보증을 주지만 Cogentic은 자연어 수학 산문을 만들어 도메인 전문가가 직접 읽고 검증하게 한다. 프로그램 탐색이나 신경-기호 탐색 계열은 저렴하고 기계가 계산할 수 있는 점수 함수를 전제하는데, 모든 문제가 그런 오라클에 맞는 것은 아니라는 점도 지적한다.

어떻게 동작하나

시스템은 하나의 문제를 두고 협업하는 에이전트 집단으로 구성된다. 오케스트레이터는 중앙 제어자로서 전역 상태를 추적하고, 연구 방향별로 증명자 슬롯을 배분하며, 요약자를 띄워 이력을 특정 증명자용 브리핑으로 압축하고, 검증자 합의를 평가하고, 지금까지의 발견을 담는 원장(ledger)과 이전 시도 및 그 판정을 기록하는 기록부(record)를 관리한다. 오케스트레이터 자신은 수학적 유도를 하지 않는다. 문헌 조사자는 관련 연구와 정의·정리를 찾아 증명자에게 제공하고, 런 중간에 기술적 장벽을 넘기 위한 표적 검색을 다시 나가기도 한다. 증명자들은 배정된 브리핑을 바탕으로 후보 증명을 독립적·병렬적으로 작성하고, 검증자들은 서로 다른 각도와 범위에서 이를 비판한다. 별도의 조언자는 여러 라운드의 출력을 읽고 오케스트레이터가 다음 라운드의 시도 배분과 지시문을 조정하도록 돕고, 마지막에 통합 단계가 최종 원고를 포맷하고 감사한다.

무엇과 다른가

작업은 라운드 단위로 진행된다. 라운드는 후보 증명 묶음을 만들고 검증을 거쳐 기록부와 검증된 원장에 기록하며, 다음 라운드는 그 지점에서 시작한다. 라운드 시작 시 오케스트레이터는 몇 개의 증명자를 돌릴지, 각자가 어떤 방향을 맡을지 계획한다. 여기서 방향이란 특정 주장(경계, 상수, 구성), 반례 찾기, 또는 진행되면서 유망한 증명을 수리·완성하는 일이다. 증명자는 방향만 배정받고 방법은 스스로 정한다. 이력이 커지면 전체를 입력으로 넣지 않고, 요약자가 각 증명자용으로 독립적으로 작성한 브리핑만 보여준다. 검증은 두 단계다. 각 증명을 읽는 검증자와, 라운드 전체 초안을 나란히 읽어 공통 맹점을 찾고 강도를 비교하는 검증자가 따로 있고, 둘 다 통과해야 채택된다. 두 검증자 모두 적대적이어서 모든 단계는 정당화되기 전까지 틀렸다고 가정하고 모든 인용은 확인되기 전까지 부정확하다고 가정한다. 라운드가 끝나면 감사자가 거부된 증명 안에서도 확인된 보조정리를 추출해 자기완결적 정리로 다시 쓰고 독립적으로 재검증하며, 살아남은 것만 이후 증명자가 재사용할 수 있는 원장에 들어간다. 검증된 반례로 배제된 경계 같은 막다른 길도 기록해 이후 라운드가 재방문하지 않게 한다. 프로세스 조언자는 전체 런의 검증 로그에서 반복되는 실수, 상습적 논증 구멍, 검증 맹점 같은 패턴을 찾아 지시문과 배분을 조정한다. 다만 조언자와 오케스트레이터 모두 수학적 의견은 낼 수 없고, 답이 무엇일지 추측하거나 기법을 추천하거나 방향의 유망함을 선언하지 못한다. 모든 검증을 통과하면 비교자가 가장 강한 증명을 고르고, 작성자가 완전한 원고로 확장하며, 최종 감사가 원고와 채택된 증명을 대조해 전개 과정에서 오류가 들어가지 않았는지 확인한다.

어떻게 쓰나

실험은 Gemini를 기반 모델로 사용해 온라인 학습, 경매 이론, 메커니즘 설계의 열린 문제들에 적용했다. 각 런은 전문가의 수학적 개입 없이 문제 서술만으로 시작했고, 대부분의 문제에서 Gemini 호출 O(100)회, 가장 어려운 문제에서 O(1000)회 수준의 추론 예산을 썼다. 모든 증명은 이후 도메인 전문가가 독립적으로 검증했고 동반 논문으로 전개됐다. 온라인 역선형 최적화에서는 결정론적·proper·anytime 알고리즘이 라운드당 O(d²) 산술 연산과 선형 최적화 1회로 지평 T에 무관한 누적 손실 R_T = O(d)를 달성함을 보였다. 이는 그 차수의 첫 효율적 경계이자 첫 proper 알고리즘이며, 최적 하한 Ω(√d)와 O(√d) 인자 안에서 일치한다. 증명의 핵심은 로그를 만드는 log det H_t 포텐셜을 tr(H_t^{-1/2})로 교체한 것으로, 이 포텐셜은 d에서 시작해 매 라운드 τ/4·s_t²만큼 감소해 Σs_t² ≤ 4d/τ = O(d²)를 지평과 무관하게 준다. 양면 시장 경쟁 복잡도에서는 구매자 분포가 판매자 비용을 1차 확률적으로 지배할 때 작은 쪽인 판매자를 정확히 2명 추가하면 STR(m, n+2) ≥ OPT(m, n)이 성립하고, m=n=1에서도 판매자 1명 추가로는 부족해 이 경계가 tight함을 보였다. 기존 결과가 측당 최소 20,000명의 상수를 요구했던 것에 비해 상수가 2로 줄고 모집도 한쪽으로 끝난다.

전제와 한계

나머지 세 결과도 구체적인 수치를 동반한다. 전문가 예측에서는 지평을 모르는 알고리즘이 모든 t ≥ 1에 대해 R_t ≤ (1 + O(√(ln ln n / ln n)))·√(t ln n / 2)를 동시에 만족함을 보여, n → ∞에서 anytime과 고정 지평의 선행 상수가 일치한다는 것을 증명했다. 증명은 기하 격자 H^m = (1+ε)^m마다 멀티플리커티브 웨이트 인스턴스를 돌리고 마스터로 집계하되, 인스턴스를 ⌊δH^m⌋에 깨우고 ⌊H^m⌋ 후 은퇴시켜 동시 생존 인스턴스를 O(ε^{-1} log δ^{-1})개로 t와 무관하게 묶는 초등적 구성이다. 단일 가산 구매자 판매에서는 3.52·max(SRev, BRev) ≥ OPT를 증명해 기존 6과 5.2를 개선했고(하한은 2), 아이템 가치를 SRev가 아니라 SRev와 BRev를 함께 반영한 결합 스케일 M에서 절단해 Tail 분석을 제거했다. 오토비딩 경매에서는 n=2일 때 표준 비례식 1차 가격 경매(pFPA₁)가 PoA ≤ 1.5를 달성하고 이것이 tight함을, 일반 n에서는 pFPA_{2n}이 PoA ≤ 2 - 1/(4n+1) = 2 - Ω(1/n)을 달성해 하한 2 - 4/(n+4)와 상수 인자까지 맞음을 보였다. 저자들은 1.5를 추측만 하고 증명은 없었으며, 두 번째 부분은 애초에 연구한 적이 없어 시스템에 힌트를 주지 않았는데도 메커니즘과 분석을 독자적으로 찾아냈다고 밝힌다.

개발자 관점에서 이 논문의 값은 특정 정리가 아니라 하네스 설계에 있다. 단발 생성으로 안 되는 작업을 라운드 기반 증명-검증 루프로 바꾸고, 검증자에게 적대적 기본 가정을 주고, 부분적으로 확인된 결과를 영속 원장에 승격시켜 이후 라운드가 재사용하게 하고, 실패 기록을 남겨 같은 막다른 길을 반복하지 않게 하는 패턴은 수학에 국한되지 않는다. 또한 조언자와 오케스트레이터에게 수학적 판단을 금지한 제약, 즉 조정 역할과 판단 역할을 분리한 설계는 자율 에이전트 시스템에서 역할 오염을 막는 실무적 참고점이다. 다만 원문에 데이터셋이나 베이스라인 비교 표는 제시되지 않았고, 성능은 다섯 문제에 대한 전문가 검증 결과와 호출 수 규모로만 보고된다.

저자들이 밝힌 전제와 한계도 분명하다. 문제는 저자들의 전공 영역에서 골랐기 때문에 자연어 증명을 전문가가 직접 검증할 수 있었고, 일부 동반 논문에는 해당 문제를 이미 연구하던 공동저자가 포함됐다. 저자들은 하네스가 낸 초기 논문이 그 자체로 일관되고 읽을 만했지만, 문헌상 위치 설정, 프레이밍, 기법의 정제와 설명은 사람이 덧붙였다고 적는다. 또한 이런 시스템은 결과를 읽어낼 속도보다 빠르게 후보를 양산할 수 있고 컴퓨트 예산이 커질수록 격차가 벌어지는데, Lean 같은 증명 보조기로 형식화하면 정확성은 기계적으로 확정되지만 인간의 이해는 더 뒤처질 수 있다는 점을 중요한 미해결 질문으로 남긴다. 오토비딩 결과의 일반 n 상한은 입찰이 undominated라는 가정 아래에서만 성립한다는 조건도 붙는다.