Cogentic: Multi-Agent Orchestration for Automated Proof Discovery

Paper: Yang Cai; Vineet Gupta; Yanchen Jiang; Christopher Liaw; Aranyak Mehta; Grigoris Velegkas; Di Wang (2026). Cogentic: Multi-Agent Orchestration for Automated Proof Discovery. arXiv:2609.40324v1 · PDF · 프로젝트 페이지. 부록의 실제 문제 프롬프트까지 포함한 17쪽을 기준으로 읽는다.

이 글은 논문이 제안한 연구팀형 하네스와 다섯 결과의 의미를 쉽게 설명한다. 정리별 가정·수치·인간 개입·재현성의 상세 감사는 상세 읽기에 정리했다. 결과는 저자 보고이며, 시스템 실행이나 수학 정리의 독립 재증명은 하지 않았다.

새로운 정리를 찾을 때는 후보를 많이 만드는 것만으로 충분하지 않다. 잘못된 논증을 걸러내고, 실패한 시도에서도 맞는 보조정리를 건져 다음 시도에 넘겨야 한다. Cogentic은 이 과정을 여러 AI 역할과 반복 라운드로 나눈다. 핵심 기여는 새 모델 구조나 학습 알고리즘이라기보다 연구 탐색을 조직하는 다중 에이전트 하네스다.

1. 제안하고, 서로 비판하고, 남은 부분을 넘긴다

한 라운드에서 오케스트레이터는 증명할 방향이나 반례 찾기 같은 탐색 과제를 나눈다. 문헌 검토자는 정의와 관련 연구를 찾고, 각 summarizer는 이전 시도 중 필요한 내용만 prover별 briefing으로 추린다. prover들은 병렬로 초안을 쓰고, process advisor는 반복 오류나 검토 누락을 로그에서 찾아 다음 지시·자원 배분을 조언한다. advisor에게 수학적 의견이나 풀이 방향 추천은 금지되어 있다. 초안은 먼저 혼자서, 이어서 같은 라운드의 다른 초안들과 나란히 놓고 비판적으로 검토한다. 두 검토를 통과한 뒤에도 다음 라운드에서 더 나은 결과를 찾을 수 있다.

Figure 1. 한 라운드에서 방향 배정·briefing·병렬 증명·개별 및 교차 검토를 거쳐 기록을 갱신한다. 탐색이 끝나면 comparator가 결과를 고르고, writer가 원고를 정리하며, paper verifier가 원고와 승인된 증명을 대조한다. 이 마지막 단계도 Lean 같은 형식 증명 검증기를 뜻하지 않는다. 출처: Cai et al. (2026), arXiv v1, p. 3, Figure 1.

라운드 사이에는 세 가지를 남긴다. Record는 시도한 주장과 실패한 반론을 적고, Verified ledger는 별도로 다시 확인한 보조정리나 배제된 경계를 모으며, 상시 지침은 다음 탐색의 절차를 조정한다. 전체 초안이 거부돼도 그 안의 보조정리가 독립 검토를 통과하면 재사용할 수 있다는 구상이다.

다만 여기서 “verified”는 운영상의 검토 상태다. 에이전트 역할 간 자연어 비평과 후속 전문가 확인이지, 증명 커널이 논리적 soundness를 보증했다는 뜻은 아니다. Figure 1의 “Formal writer”도 완전한 수학 원고를 작성하는 단계이지 Lean/Coq 형식화가 아니다.

2. 다섯 결과는 서로 다른 정리의 사례다

논문은 온라인 최적화, 시장 설계, 전문가 조언, 가격 책정, 경매 자동입찰에서 다섯 결과를 보고한다. 이는 다섯 개 정리를 제안된 하네스가 찾는 데 관여했다는 사례이며, 같은 시험에서 측정한 다섯 성능 점수는 아니다.

분야	저자 보고 결과	읽을 때의 조건
온라인 역최적화	문제 차원 d에서 누적 후회 O(d)인 결정론적 알고리즘	매 행동 전에 목적 방향을 제시하는 proper 조건과, 종료 시점을 몰라도 보장하는 anytime 조건이다. 라운드당 O(d²) 산술 외에 선형 최적화 1회가 들며 전체 증명은 동반 논문에 있다.
양면시장	더 작은 쪽인 판매자를 두 명 추가하면 원래 시장의 최대 기대 거래이득 이상을 보장	구매자 가치 분포가 판매자 비용 분포를 확률적으로 우위해야 한다. 모든 개별 거래가 이익이라는 말은 아니다.
전문가 조언	전문가 수 n이 커질 때 anytime regret의 앞 상수가 고정시간 최선에 점근적으로 접근	유한한 모든 n에서 정확히 같은 보장이라는 뜻은 아니다.
개별판매 대 묶음판매	독립 품목 가치를 가진 단일 구매자의 최적 수익이 개별판매·전체묶음 판매 중 높은 수익의 3.52배 이내	프롬프트 목표는 factor 3이었지만 결과는 3.52다. 알려진 하한 2와 간극도 남는다.
자동입찰 경매	두 입찰자 r=1 조건에서 Price of Anarchy 1.5, 일반 n에서는 2−1/(4n+1) 이하	일반 n 보장에는 undominated bids 조건이 붙는다. PoA는 낮을수록 좋다.

최대 3.52배 같은 값은 최악의 경우 이론적 근사 보장이지 실제 경매에서 수익이 3.52배 올랐다는 실험 결과가 아니다. 일반 n의 undominated bids는 입찰자가 RoS 조건을 지키면서 입찰을 올려 더 자주 이길 수 없는 상태를 뜻한다. 마찬가지로 다른 네 항목도 조건이 붙은 이론 정리다. 상세 리뷰는 각 정리의 정의와 가정을 따로 설명한다.

3. 어디까지 자동이고, 증거는 무엇인가

저자들은 실행 중 수학자의 개입 없이 결과를 찾았다고 설명하지만, 부록 프롬프트는 단순한 주제 한 줄만 주지 않는다. 기존 논문이나 참고문헌, 구체적 목표 정리, 일부 가정이 주어졌다. 예를 들어 개별판매·묶음판매 과제는 factor 3을 목표로 하고, 달성하지 못하면 factor 4부터 강화하라고 안내했다. 따라서 시스템이 증명을 제안한 것과 인간이 문제·목표·관련 지식을 제공한 것은 함께 보아야 한다. 실행 이후 저자들은 논증을 확인하고 원고를 보강했으며, 자동 산출물과 최종 논문의 기여도 동일시할 수 없다.

논문은 다섯 성과를 제시하지만 전체 시도한 문제 수나 실패 수가 없어 성공률을 계산할 수 없다. 단일 Gemini, 단순 반복 샘플링, 구성요소별 제거 실험과 같은 하네스 통제군도 없다. 따라서 다섯 정리가 흥미롭다는 것과 오케스트레이터·ledger·교차 검토 중 어느 요소가 성과를 만들었는지는 서로 다른 주장이다.

또한 공개 논문은 Gemini의 정확한 실행 버전, 역할별 설정, 호출·토큰 로그와 원시 기록을 제공하지 않는다. 대부분 문제에서 O(100), 가장 어려운 문제에서 O(1000) 호출이라는 규모를 보고하지만, 비용이나 재현 가능한 자원 측정은 아니다. 저자들의 도메인 전문가 검토를 보고했지만, 검토자와 절차의 독립성을 외부에서 재현할 자료도 없다.

4. 핵심 가치는 증명 보증이 아니라 탐색 구조다

Cogentic의 장점은 병렬 prover, 서로 다른 범위의 비평, 실패 기록, 다시 확인한 보조정리의 재사용을 하나의 라운드에 묶은 점이다. 특히 실패에서 검토 가능한 부분 결과를 추출해 다음 탐색의 입력으로 만드는 방식은 유용한 설계다.

반면 모델 검토는 형식 검증이 아니며, ledger의 오류 철회·가정 추적, 판정자 간 오류 상관, 하네스 통제 실험과 전체 실패 분모는 공개 근거만으로 알 수 없다. 그러므로 이 논문은 전문가가 후속 확인하는 자연어 증명 탐색을 조직하는 사례로 읽는 것이 적절하다. 다섯 결과만으로 모든 열린 문제를 자율적으로 해결하거나 증명의 soundness를 보장한다고 결론 내릴 수는 없다.

같이 읽기: GraphCert · Context Language Models

상세 읽기

References

Cai, Y., Gupta, V., Jiang, Y., Liaw, C., Mehta, A., Velegkas, G., & Wang, D. (2026). Cogentic: Multi-Agent Orchestration for Automated Proof Discovery [Preprint]. arXiv. https://arxiv.org/abs/2609.40324v1