Cogentic: 여러 AI가 증명과 검증을 나누어 미해결 수학 문제를 푸는 방법

배경과 문제

수학과 이론 컴퓨터 과학의 개방형 연구 문제는 단일 추론만으로 해결하기 어렵다. 최신 대규모 언어 모델(LLM)은 한 번의 생성으로 강력한 수학적 아이디어를 제시할 수 있지만, 개방형 문제는 여러 경쟁하는 추측을 탐색하고, 미묘한 기술적 장애를 극복하며, 장기간에 걸쳐 중간 진전을 유지해야 한다. 예를 들어, 어떤 접근이 실패했는지 기억하지 못하면 같은 실수를 반복할 수 있고, 하나의 증명 방향에만 매달리면 더 유망한 다른 길을 놓칠 수 있다.

Lean, Isabelle/HOL, Coq 같은 정리 증명 도구는 형식화된 증명을 기계로 검사할 수 있다. 논문은 이런 접근의 가치를 인정하면서, 저자들이 직접 읽고 수학적 논증을 확인할 수 있는 자연어 증명을 이번 연구의 목표로 삼았다. 자연어 증명은 읽을 수 있는 설명을 제공하지만, 에이전트끼리 검토를 통과했다는 사실만으로 기계 검증과 같은 보증을 얻지는 못한다. Cogentic은 여러 에이전트의 상호 검토와 이후 전문가의 확인을 함께 사용한다.

기존 접근의 한계

LLM을 활용한 수학적 발견에는 크게 두 갈래가 있다. 첫째는 '수학적 객체 탐색'이다. 예를 들어, 프로그램 탐색으로 극단 조합론의 새로운 구성을 찾거나, 진화적 코딩 에이전트로 알고리즘과 경계를 개선하는 방식이다. 이 접근은 값싸고 충실하며 기계로 계산 가능한 점수 함수가 필요하다. 그러나 모든 정리가 그러한 객체 탐색으로 환원되는 것은 아니다. 증명 자체가 복잡한 논증을 요구하는 문제에는 적용하기 어렵다.

다른 갈래는 여러 답을 샘플링하거나 모델을 여러 번 호출하고 에이전트끼리 상호작용하도록 해 추론 예산을 늘리는 접근이다. Cogentic도 이 계열에 속하지만, 연구 방향 배분과 이전 실패 기록, 검증한 중간 결과의 재사용을 하나의 반복 과정으로 묶는 데 초점을 맞춘다. 이 논문은 관련 시스템들을 포괄적으로 조사하거나 같은 조건에서 성능을 비교하는 연구는 아니라고 밝힌다. 따라서 기존 방법 모두가 기록이나 장기 탐색 구조를 갖추지 못했다고 일반화하기보다는, 이번 시스템이 어떤 구조를 조합했는지 살펴보는 것이 정확하다.

연구방법을 단계별로

Cogentic의 핵심은 '라운드(round)' 단위의 반복 작업이다. 각 라운드는 오케스트레이터(orchestrator)가 문제를 여러 연구 방향으로 나누고, 각 방향에 증명 에이전트(prover)를 배정하는 것으로 시작한다. 방향은 특정 경계값 증명, 반례 찾기, 유망한 증명 수정 등 구체적인 주장이다. 증명 에이전트는 해당 방향에 대한 이전 시도와 검증 의견, 문헌 조사, 검증된 보조정리 원장(ledger)을 요약한 브리핑을 받고 독립적으로 증명 초안을 작성한다.

각 증명 초안은 두 종류의 검증 에이전트(verifier)를 통과해야 한다. 하나는 개별 초안을 검토하고, 다른 하나는 같은 라운드의 모든 초안을 나란히 읽어 공통된 맹점이나 상대적 강점을 찾는다. 두 검증자 모두 적대적(adversarial)으로 작동하여, 모든 단계가 정당화될 때까지 틀렸다고 가정하고 모든 인용이 확인될 때까지 부정확하다고 가정한다. 초안이 두 검증을 모두 통과해야만 채택된다.

라운드가 끝나면 두 가지 산출물이 남는다. '기록(record)'은 시도된 증명과 실패한 이유를 저장하고, '원장(ledger)'은 검증된 중간 보조정리를 축적한다. 검증자는 종종 전체 증명은 거부하지만 개별 보조정리는 옳다고 확인한다. 감사자(auditor)가 그러한 조각을 추출하여 독립적인 보조정리로 다시 작성하고 격리된 상태에서 재검증한다. 살아남은 보조정리는 이후 모든 증명 에이전트가 재증명 없이 재사용할 수 있다. 원장은 또한 검증된 반례로 배제된 경계값과 같은 '막다른 길'도 기록하여 이후 라운드에서 재방문하지 않도록 한다.

각 라운드 말미에 프로세스 어드바이저(advisor)가 전체 실행의 검증 로그를 검토하여 반복되는 실수, 논증의 공통된 공백, 검증 맹점 등을 파악하고 다음 라운드의 지침을 조정한다. 예를 들어, 여러 증명 에이전트가 계속 저지르는 실수에 대한 경고를 추가하거나, 이전 초안에서 논증을 건너뛴 단계에 대해 더 엄격한 정당화 기준을 요구할 수 있다. 중요한 점은 어드바이저와 오케스트레이터 모두 수학적 의견을 가질 수 없다는 것이다. 그들은 답이 무엇일지 추측하거나, 기법을 추천하거나, 방향이 유망하다고 선언할 수 없다.

후보 증명이 모든 검증을 통과하면 오케스트레이터는 더 나은 결과를 얻을 수 있는 남은 유망한 방향을 계속 탐색할 수 있다. 종료 시 비교기(comparator)가 가장 강력한 검증된 증명을 선택하고, 형식 작성기(formal writer)가 완전한 논문 원고로 확장하며, 최종 검증 감사가 원고와 채택된 증명을 대조하여 설명 과정에서 오류가 도입되지 않았는지 확인한다. 출력은 문제의 배경, 표기법, 의존하는 보조정리를 모두 포함한 자기 완결적 문서로, 실행 과정을 모르는 도메인 전문가도 읽고 검증할 수 있다.

결과와 숫자의 의미

Cogentic은 Gemini를 바탕으로 온라인 학습, 경매 이론, 메커니즘 설계의 다섯 개 개방형 문제에서 얻은 새로운 결과를 제시한다. 실행은 문제 설명에서 시작해 별도의 전문가 힌트 없이 초안을 만들었고, 이후 해당 분야 전문가들이 논증을 검증하고 동반 논문의 설명과 일부 결과를 보강했다. 다섯 개는 이 논문이 보고한 결과의 수이며, 전체 시도한 문제 수를 분모로 한 성공률이나 모든 수학 분야의 성능 점수는 아니다. 저자는 대부분의 문제에 O(100), 가장 어려운 문제에 O(1000) 규모의 Gemini 호출을 사용했다고 보고한다. 이는 호출 규모 설명이며, 모든 방법과 같은 조건에서 비교한 비용 벤치마크는 아니다.

다섯 결과는 서로 다른 가정 아래의 수학적 정리다. 첫째, 온라인 역선형 최적화에서는 효율적이며 목적함수 추정치를 먼저 정하는 proper 알고리즘으로 시간 지평에 무관한 O(d) 리그렛 상한을 얻었다. 둘째, 구매자가 판매자보다 적지 않고 구매자 가치 분포가 판매자 가치 분포를 일차 확률 지배하는 양면 시장에서는 판매자 두 명 추가가 충분함을 보였다. 셋째, 손실이 [0,1] 범위인 전문가 조언 문제에서는 전문가 수 n이 커질 때 anytime 리그렛의 선도 상수가 고정 시간의 최적 상수에 접근한다. 넷째, 상품별 가치가 서로 독립인 단일 가산 구매자 설정에서 단순 판매의 근사 계수를 5.2에서 3.52로 낮췄다. 다섯째, 지출 대비 수익 제약이 있는 자동 입찰 시장에서 두 입찰자용 메커니즘의 최적 PoA 1.5를 얻었으며, 일반 n명에 대한 2 - 1/(4n+1) 상한은 입찰이 비지배적이라는 추가 가정 아래 성립한다.

이 숫자들은 서로 다른 의미를 가진다. O(d)는 실제 리그렛이 언제나 d에 정확히 비례한다는 말이 아니라, 시간 T가 늘어도 차원 d에 선형인 차수의 상한으로 제한된다는 뜻이다. 이전의 효율적인 O(d ln T) 보장에는 T가 커질수록 늘어나는 항이 있었다. 양면 시장의 비교는 이전 보장의 양쪽 각각 최소 20,000명 추가에서 새 정리의 한쪽 판매자 두 명 추가로 바뀐 것이다. 전문가 조언 문제의 선도 상수 일치는 n이 무한히 커지는 점근적 결론이며, 모든 유한한 n에서 두 경계가 정확히 같다는 뜻은 아니다. 3.52는 독립적인 상품 가치라는 가정 아래 최적 수익이 개별 판매와 일괄 판매 중 더 나은 수익의 3.52배를 넘지 않는다는 보장이다. 일반 n명 경매의 상한과 하한이 상수 배 수준에서 맞는다는 설명도 PoA 전체 비율이 아니라 2에서 떨어지는 1/n 항에 관한 것이다.

구체적인 예시

온라인 역선형 최적화 문제를 예로 들어보자. 학습자는 전문가의 선택을 관찰하고 동일한 선택을 하려고 하지만, 전문가가 무엇을 최적화하는지 알려주지 않는다. 숨겨진 벡터 w*가 있고, 매 라운드마다 행동 집합 X_t가 주어지면 학습자는 추천 x̂_t를 제시하고 전문가의 선택 x_t를 관찰한다. 학습자는 누적 손실 R_T = Σ⟨w*, x_t - x̂_t⟩를 최소화하려 한다. 이 문제는 절단 평면 게임으로 환원되는데, 학습자가 점 p_t를 질의하면 적대자가 ⟨w* - p_t, v_t⟩ ≥ 0을 만족하는 단위 벡터 v_t를 반환한다.

Cogentic이 찾은 증명은 Sakaue et al.의 변수 메트릭 프레임워크를 기반으로 한다. 두 가지 변경이 로그 항을 제거한다. 첫째, 랭크-1 메트릭 업데이트 g_t g_t^T를 관찰된 방향의 쌍대 메트릭 길이 s_t = ||g_t||_{H_t^{-1}}로 나누어 자기 정규화한다. 둘째, 기존의 log det H_t 포텐셜(이는 d log T로 증가하여 ln T의 원천)을 trace power tr(H_t^{-1/2})로 대체한다. 이 포텐셜은 d에서 시작하여 매 라운드 최소 τ/4 * s_t^2만큼 감소하므로, Σ s_t^2 ≤ 4d/τ = O(d^2)가 되어 시간에 독립적이다. 결과적으로 R_T = O(d)가 된다.

또 다른 예로, n명의 전문가에 대한 anytime 리그렛 문제를 보자. 고정 시간 T를 알면 multiplicative weights 알고리즘을 T에 맞게 조정하여 √(T ln n / 2)의 리그렛을 얻을 수 있다. 그러나 anytime 알고리즘은 시간을 모르고 모든 t에서 동시에 경계를 만족해야 한다. Cogentic의 증명은 기하 격자 H_m = (1+ε)^m에 대해 각 시간 구간마다 하나의 multiplicative weights 인스턴스를 실행하고, 마스터 multiplicative weights로 집계한다. 문제는 인스턴스 풀이 t와 함께 증가하여 마스터의 리그렛이 시간 의존적 오버헤드를 남긴다는 것이다. 이 구성은 인스턴스 m을 라운드 ⌊δH_m⌋에서만 깨우고 ⌊H_m⌋ 이후에 은퇴시켜 풀을 유계로 유지한다. ε = √(ln ln n / ln n), δ = ε^3으로 설정하면 격자 조잡성, 집계 오버헤드, 재귀가 함께 1 + O(ε)의 비용을 초래한다.

한계와 오해하기 쉬운 점

Cogentic이 생성한 증명은 자연어로 작성되어 기계 검증이 아니라 도메인 전문가의 검증에 의존한다. 논문은 '우리는 논증을 확인하고, 그 주변에 설명을 작성했으며, 어떤 경우에는 하네스가 한 것보다 더 발전시켰다'고 밝히고 있다. 즉, 최종 결과물에는 인간 저자의 추가적인 설명과 문헌 배치, 기법 설명이 포함되어 있다. 따라서 자율적으로 생성한 초기 논문 초안과, 사람이 검증하고 설명·결과를 보강한 최종 동반 논문을 구분해야 한다.

문제 선택은 저자들이 전문성을 가진 분야를 중심으로 이루어졌다. 이는 결과를 직접 확인할 수 있게 했지만, 생소한 분야에서도 같은 성과를 낸다는 증거는 아니다. 일부 동반 논문에는 이미 해당 문제를 연구하던 공동 저자도 참여했다. 이 사실은 최종 논문에서 사람과 시스템의 역할을 구분해 읽어야 한다는 뜻이며, 그것만으로 실행 중에 인간의 힌트가 들어갔다고 추정해서는 안 된다.

추론 예산도 제한된 방식으로 해석해야 한다. O(100)과 O(1000)은 보고된 실행의 호출 규모를 나타내며, 정확히 100회·1000회라는 횟수나 최대 1000회라는 보장으로 읽으면 안 된다. 제공된 본문은 Gemini의 구체적인 모델 버전, 각 호출의 토큰 길이, 총 실행 시간, 금액을 함께 제시하지 않는다. 호출 수만으로 누구나 저렴한 비용에 재현할 수 있다고 결론내릴 수 없으며, 다른 모델과 문제에서 같은 성과가 날지도 별도 평가가 필요하다.

마지막으로, Cogentic은 증명을 '발견'하지만 그 증명이 왜 옳은지에 대한 인간의 이해를 보장하지 않는다. 논문의 토론 섹션은 '이와 같은 시스템은 읽을 수 있는 속도보다 더 빨리 후보 결과를 생성할 수 있으며, 계산 예산이 커질수록 그 격차가 벌어진다'고 경고한다. Lean과 같은 증명 보조 도구로 형식화하면 정확성은 기계적으로 해결되지만, 인간의 이해는 뒤처질 수 있다. 과거에는 해의 이해가 새로운 방향과 문제로 이어졌기 때문에, 생성 처리량과 인간 이해의 균형을 맞추는 것이 중요한 과제로 남는다.

실제로 어떻게 활용할까

Cogentic은 연구자가 특정 분야의 개방형 문제를 해결하려 할 때 초기 탐색 도구로 활용할 수 있다. 문제 설명만 제공하면 시스템이 자율적으로 여러 증명 방향을 탐색하고, 검증된 중간 결과를 축적하며, 최종적으로 전문가가 검토할 수 있는 자연어 증명을 생성한다. 연구자는 생성된 증명을 읽고, 논리적 비약이나 숨은 가정을 확인한 후, 필요한 경우 추가 설명을 덧붙여 논문으로 발전시킬 수 있다.

이 설계를 참고할 때 가장 중요한 것은 검증 책임을 남기는 것이다. 생성된 자연어 증명은 해당 분야 전문가가 독립적으로 확인해야 하며, 전문가가 익숙한 문제를 고른 이유도 이 확인을 가능하게 하려는 것이었다. 전문 분야와 가깝다는 이유만으로 시스템 출력 자체의 정확도가 더 높아진다는 실험 결과는 제시되지 않았다. 또한 중간 보조정리와 실패 기록을 검토하면 탐색 과정을 이해하는 데 도움이 될 수 있지만, 논문에 적힌 호출 규모만으로 필요한 총 컴퓨팅 자원이나 비용을 판단할 수는 없다.

다음은 원문이 실험한 결과가 아니라 응용 가능성을 생각해 보는 예시다. Cogentic의 설계 원리를 다른 분야에 옮긴다면, 예를 들어, 실험 과학에서 가설 생성과 검증을 분리하고, 검증된 중간 결과를 공유 원장에 축적하는 방식은 문헌 검토와 실험 설계의 자동화에 응용될 수 있다. 다만, 각 도메인에 맞는 검증 기준과 '적대적 검증자'의 역할을 신중하게 정의해야 한다. 수학에서는 논리적 정당성이 핵심이지만, 실험 과학에서는 재현성과 통계적 유의성이 더 중요할 수 있다.