Choir: An Open Protocol for Distributed Multi-Agent Autoformalization

3줄 요약

1. 하버드대의 Yidi Qi와 Melanie Weber가 2026년 9월 25일 arXiv에 공개한 논문이다. 두 연구자는 수학 형식화 프로젝트를 여러 기여자가 분담하는 개방형 프로토콜 콰이어(Choir)를 제안했다. 기여자는 자기 컴퓨터에서 자기 LLM 구독으로 에이전트를 실행하고, 모든 조정은 프로젝트의 GitHub 저장소에서 이뤄진다.
2. 사람인 감독자가 오케스트레이터 에이전트를 실행하면, 오케스트레이터가 정리의 진술을 작성해 GitHub 이슈로 과제를 게시한다. 워커는 댓글로 과제를 선점하고 증명을 완성해 풀 리퀘스트로 제출한다. 결정론적 검증 게이트는 제출물을 다시 빌드하고, 새 공리의 도입 여부와 임시 증명 표시의 잔존 여부, 진술 변경 여부를 검사한다. 모든 검사를 통과한 제출물만 오케스트레이터가 검토해 병합한다. Lean 4, Isabelle, Rocq를 지원하며 코드는 Apache-2.0 라이선스로 공개됐다.
3. 저자들은 Yufei Zhao의 MIT 강의 노트 『조합론의 확률적 방법(Probabilistic Methods in Combinatorics)』을 Lean 4로 형식화해 Choir를 시험했다. 공개 저장소에 따르면 11개 장에서 정리 285개를 형식화했고, 남은 미완성 증명 하나는 수학계의 미해결 문제에 해당한다. 논문에는 한계도 적혀 있다. 교과서보다 큰 프로젝트에는 Choir를 써 보지 않았고, Isabelle과 Rocq에서는 텍스트를 그대로 둔 채 진술의 의미만 바꾼 제출을 게이트가 검출하지 못한다.

형식화 비용을 한 팀이 모두 부담하는 구조

Lean 4, Isabelle, Rocq 같은 증명 보조기는 증명의 모든 단계를 작은 신뢰 커널로 검사한다. 그래서 한 번 형식화된 결과는 증명을 다시 읽지 않고도 믿을 수 있다. 수학 공동체는 이런 증명 보조기를 기반으로 공용 라이브러리를 관리해 왔다. Lean에는 수학의 Mathlib, 물리학의 Physlib, 컴퓨터과학의 CSLib가 있고, 새 형식화 작업은 이 라이브러리를 활용한다. 최근까지 이 작업은 거의 전부 사람이 손으로 했으며, 라이브러리를 만드는 데 많은 기여자가 여러 해를 들였다.

논문은 지난 1년 사이 AI 에이전트가 이 속도를 크게 바꿨다고 정리했다.

논문에 따르면 이 시스템 대부분은 한 팀이 자기 예산으로 모든 에이전트를 실행하는 방식으로 만들어졌고, 일부는 일반적인 학계 연구 그룹이 감당할 수 없는 규모로 운영된다. 반면 개방된 수학 공동체에는 전문 지식이 있다. 개인 LLM 구독료에 이미 포함된 에이전트 사용량도 상당하다. 저자들은 여러 기여자가 각자의 사용량을 공동 프로젝트에 활용하면, 대규모 형식화가 자금이 넉넉한 한 팀에 의존하지 않게 된다고 보았다. Choir는 이 구상을 구현한 프로토콜이다.

논문은 기술적 기여로 세 가지를 제시했다.

1. 프로젝트의 형식화 작업을 GitHub 저장소를 통해 여러 기여자의 에이전트에 배분하고, 기여자가 제출한 분해 결과로 증명 트리를 확장하는 과제 배분 관리 시스템.
2. 모든 풀 리퀘스트를 소스에서 기계적으로 다시 검사하는 결정론적 검증 게이트.
3. git 로그, 이슈, 풀 리퀘스트만으로 증명 트리의 확장 과정을 재현하고, 각 노드를 증명하거나 분해한 기여자를 확인하는 이력 시각화 도구.

네 주체의 역할 분담

Choir에서는 사람인 감독자, 두 종류의 LLM 에이전트, 그리고 저장소 자체가 역할을 분담한다.

Choir는 여러 에이전트의 파일 수정과 버전 관리를 GitHub에 맡긴다. 저자들은 조정 플랫폼에 필요한 신원 확인, 이벤트 트리거, 접근 제어, 공개 감사 기록을 GitHub가 이미 갖추고 있다는 점을 그 근거로 들었다. 에이전트가 실행할 수 있는 동작은 GitHub gh CLI의 Python 래퍼로 구현한 명령으로 제한된다. 오케스트레이터의 절차는 플레이북 문서에 적혀 있으므로, 플레이북을 읽고 이 명령을 실행할 수 있는 에이전트라면 어느 것이든 오케스트레이터를 맡을 수 있다. 자주 쓰는 명령은 다음과 같다.

과제 하나가 병합되기까지

논문은 오케스트레이터가 계획을 세운 뒤 풀 리퀘스트 하나가 병합될 때까지의 과정을 단계별로 설명했다.

계획

오케스트레이터는 프로젝트를 시작할 때 저장소에 로드맵을 작성한다. 로드맵에는 목표, 증명 방침, 오케스트레이터 자신의 추론 기록, JSON 형식의 의존성 그래프가 포함된다. 어떤 노드의 진술과 그 노드가 명시한 모든 의존 노드의 진술이 형식화되면, 그 노드를 과제로 게시할 수 있다.

이 단계에서 오케스트레이터는 부담을 줄이려고 정리 분해를 일부러 몇 단계만 한다. 오케스트레이터는 수학적 구조를 결정하는 주요 정리만 진술하고, 더 세밀한 분해는 워커에게 맡긴다. 계획 모듈은 교체할 수 있다. 감독자는 로드맵 형식만 지키면 자체 계획 도구를 쓰거나 사람이 작성한 파일을 활용할 수 있고, 이 경우 Choir는 과제 관리에만 쓰인다.

게시

choir orch create-task는 게시 가능한 노드를 GitHub 이슈로 만든다. 이슈 본문은 YAML 기록으로 시작한다. 과제 하나는 증명 대신 임시 표시를 넣은 진술 하나이며, 오케스트레이터가 난이도와 우선순위를 라벨로 지정한다. 감독자는 워커가 쓰는 모델에 따라 그 워커가 맡을 수 있는 최대 난이도를 제한할 수 있다. 저자들은 이 제한이 비용을 줄이고, 약한 모델이 끝내기 어려운 과제를 맡지 않게 한다고 설명했다.

선점

다른 계정으로 작업하는 기여자에게는 프로젝트 저장소 쓰기 권한이 없다. 그래서 워커는 사람끼리 협업할 때처럼 과제 이슈에 댓글을 달아 과제를 선점한다. 여러 워커가 같은 과제를 요청하면 가장 먼저 댓글을 단 워커가 과제를 맡는다. 선점한 뒤 하루 동안 아무 갱신이 없으면 점유가 만료되고, 그 과제는 다른 워커가 다시 선점할 수 있게 된다. 선점에 성공하면 같은 명령이 작업 공간을 구성한다. 작업 공간은 과제가 고정한 커밋의 프로젝트를 과제 전용 브랜치로 체크아웃한 것이다.

증명과 제출

증명은 기여자의 컴퓨터에서 기여자 계정으로 진행된다. Choir에는 증명 에이전트가 포함되어 있지 않다. 기여자는 Choir의 과제 형식과 제출 규칙만 지키면 어떤 에이전트나 작업 방식이든 쓸 수 있다. 작업이 길어지면 choir worker heartbeat가 워커 자신의 댓글을 수정해 점유를 유지한다. 증명이 끝나면 choir worker submit이 브랜치를 푸시하고 풀 리퀘스트를 생성한다. 과제를 깔끔하게 반납할 때는 choir worker release를 쓰고, 오랫동안 응답이 없는 점유는 정기 점검 작업이 해제한다.

분해

게시된 과제가 너무 어려울 때도 있다. 수학적 내용이 풀 리퀘스트 하나로 해결되지 않는다고 판단한 워커는 과제를 더 분해할 수 있다. 워커는 목표 정리와 같은 파일에 중간 보조정리를 진술하고, 보조정리의 증명에는 임시 표시를 넣는다. 그런 다음 이 보조정리들을 사용해 목표 정리를 증명한다. 그리고 풀 리퀘스트 본문의 choir-reduction 블록에 부모 노드와 자식 노드 목록을 적어 무엇에 의존했는지 선언한다.

증명 트리의 깊이는 이 장치로 늘어난다. 오케스트레이터는 주요 정리만 게시하고, 트리의 세부 구조는 그 수학을 실제로 시도한 워커가 제안한다. 따라서 오케스트레이터는 트리의 전체 구조를 알아야 하지만 모든 증명 경로를 직접 구상할 필요는 없다. 분해가 승인되면 오케스트레이터는 로드맵과 의존성 그래프를 갱신하고, 자식 노드마다 새 과제를 게시한다. 이 과제도 다시 분해될 수 있으므로 증명 트리는 계속 확장될 수 있다.

검토와 병합

워커가 제출한 풀 리퀘스트는 먼저 게이트의 기계적 검사를 받고, 이어서 오케스트레이터의 검토를 받는다. 오케스트레이터는 수학이 타당한지, 분해가 합리적인지 등을 확인한다. 풀 리퀘스트는 게이트와 검토를 모두 통과해야 병합된다. 게이트 검사나 오케스트레이터 검토에서 거부되면, 오케스트레이터는 과제를 다시 게시할 수 있다. 이때 거부된 풀 리퀘스트의 부분 결과를 새 과제에 포함할지도 오케스트레이터가 정한다.

Fig. 2. 풀 리퀘스트의 처리 경로. 게이트 검사를 통과한 풀 리퀘스트만 오케스트레이터의 검토를 받는다. 어느 단계에서든 거부되면 오케스트레이터가 과제를 다시 게시한다. 타당하지 않은 작업은 처음부터 다시 하게 하고, 거의 완성됐지만 실패한 작업은 부분 결과를 재사용하게 한다. 출처: Qi & Weber, arXiv:2609.31903 (2026), CC BY 4.0

골프

골프는 오케스트레이터가 게시할 수 있는 또 다른 과제 유형이다. 이미 증명된 선언 하나를 지정하고, 진술은 그대로 둔 채 더 짧은 증명을 요청한다. 워커는 두 가지 방식으로 답할 수 있다. 더 짧은 증명만 제출하는 방식은 게이트가 가장 확실하게 검증할 수 있는 경우다. 다른 방식은 증명을 보조정리 몇 개로 분해하는 것이다. 이때 워커는 보조정리를 같은 파일에 진술하고, 보조정리의 이름을 풀 리퀘스트 본문에 적는다.

결정론적 검증 게이트

기여자의 신원과 그 기여자가 사용하는 모델을 모두 알 수 없는 경우도 있다. 게이트는 이런 제출의 품질을 관리하려고, 오케스트레이터가 검토하기 전에 모든 풀 리퀘스트에 기본 검사를 실행한다. 검사는 풀 리퀘스트가 생성되거나 갱신될 때 GitHub Actions에서 자동으로 실행된다. 모든 검사는 병합 기준 커밋(merge base)에서 확정한 정책에 따라 저장소에서 소스부터 다시 계산한다. 게이트의 강제력은 choir orch merge 명령에 구현되어 있다. 이 명령은 풀 리퀘스트의 검사 결과 집계를 읽고, 필수 검사가 하나라도 없거나 차단 검사가 하나라도 실패했으면 병합을 거부한다.

진술 불변성 검사의 목적은 워커가 증명만 제공하고, 주장하는 수학 내용은 하나도 바꾸지 않게 하는 것이다. Lean 4에서는 Lean FRO의 comparator로 이 조건을 커널 수준에서 판정할 수 있다. comparator는 진술이 의존하는 모든 것을 추적해 각 정의의 본문까지 비교한다. Isabelle과 Rocq에는 아직 이런 도구가 없어서, 소스 텍스트만으로 이 조건을 확인한다.

저자들은 소스 텍스트 비교가 생각보다 약한 보장이라고 설명했다. 워커는 게시된 진술을 한 바이트도 바꾸지 않으면서 그 진술의 의미를 바꿀 수 있다. 예를 들어 가정을 몰래 추가하는 방법이 있다. 모순된 가설을 사용할 수 있는 상태라면, 폭발 원리에 따라 거짓인 진술까지 증명할 수 있다.¹ 현재 이런 제출을 검출하는 일은 오케스트레이터와 사람 감독자의 검토에 의존한다.

증명 트리의 이력 시각화

GitHub를 기반으로 삼은 덕분에, 프로젝트의 git 로그와 이슈, 풀 리퀘스트에는 증명 트리가 만들어진 과정이 이미 기록되어 있다. choir orch viz는 이 세 가지 기록에서 시간순 이력을 추출하고, 그 이력을 재생하는 HTML 페이지 하나를 생성한다.

페이지는 증명 트리를 그리고, 슬라이더나 재생 버튼으로 프로젝트의 날짜별 사건을 차례로 보여 준다. 사건에는 노드의 진술 작성과 증명 완료, 과제의 게시와 선점과 반납, 풀 리퀘스트의 병합과 종료, 분해 승인이 포함된다. 노드는 미게시, 게시, 선점, 부분 증명, 증명 완료 상태에 따라 색이 다르다. 선점에는 워커마다 고유한 색이 지정되어 있어서, 각 증명과 분해를 어느 워커가 수행했는지 알 수 있다. 감독자는 이 페이지로 프로젝트 진행을 추적할 수 있다.

Fig. 3. Zhao 강의 노트 형식화 도중의 증명 트리 일부. 파란색으로 채워진 노드는 증명된 노드, 파란 테두리 노드는 게시된 과제, 그 밖의 색은 워커 한 명의 선점을 뜻한다. 모서리가 둥근 상자는 정의다. 이 시점에는 서로 다른 워커 넷이 과제 네 개를 동시에 선점하고 있었다. 출처: Qi & Weber, arXiv:2609.31903 (2026), CC BY 4.0

시연: 『조합론의 확률적 방법』 형식화

저자들은 Yufei Zhao의 MIT 18.226 강의 노트 『조합론의 확률적 방법』을 Lean 4로 형식화해 Choir를 시험했다. 이 강의 노트는 Meta FAIR의 Atlas가 형식화한 교과서 목록에도 포함되어 있어서, 논문은 두 결과를 직접 비교할 수 있다고 소개했다.² 형식화 결과와 Choir 코드는 모두 GitHub에 공개되어 있다.

시연 저장소의 README에 정리된 현황은 다음과 같다.

• 11개 장 전체에서 정리 285개를 형식화했고, lake build가 성공한다. 남은 sorry는 하나다.
• 남은 sorry는 11.3절 컨테이너 정리의 한 사례다. README는 이 sorry를 형식화 미완료와 구분해, 수학계의 미해결 문제라고 설명했다.
• 이 미해결 문제를 가정으로 삼아 증명한 정리 네 개는 공리 검사에서 조건부 결과로 표시된다. 정리 11.3.1과 Erdős-Kleitman-Rothschild 정리가 여기에 포함된다.
• 원문이 증명 없이 인용만 한 정리에 의존하는 세 절은 완성하지 못했다. 2.6절의 교차수는 오일러 공식과 쿠라토프스키 정리에 의존한다. 9.4절의 등주 부등식에는 브룬-민코프스키 부등식과 하퍼 정리, 존슨-린덴슈트라우스 보조정리가 필요하다. 9.5절과 9.6절은 탈라그랑 부등식에 의존한다. 이 정리들은 Mathlib에 없고, 탈라그랑 부등식은 원문도 증명을 생략한다고 밝혔다.
• 작은 사례를 직접 계산하는 과정에서 원문에 빠진 가정 다섯 개와 오타 하나를 찾았다. 2.4.4절에는 n ≥ 5라는 가정이 필요하다. 9.3.1절에는 n ≥ 2, 2.5.2절에는 n > 0이라는 가정이 필요하다. 6.3절의 부등식은 엄격한 부등식이어야 한다. 6.5.6절의 ℙ(Aᵢ) = 1 − 1/n은 1/n을 잘못 적은 것이다.
• 6.4절에서는 원문의 가정을 더 강하게 바꿨다. 원문은 k(1 + log(1 + dD)) ≤ d를 조건으로 제시했는데, 논증이 실제로 확보하는 의존 차수에 비해 이 조건이 약했다. README는 이 조건으로는 논증이 성립하지 않는 반례로 k = 5, d = 21, D = 1을 들었다.

저장소는 2026년 9월 12일에 만들어졌다. 풀 리퀘스트는 9월 13일부터 25일까지(UTC) 200건이 생성되어 197건이 병합됐고, 제목 기준으로 증명 과제가 172건, 골프 과제가 27건이었다.³ 논문은 Claude Opus 5와 GPT-5.6 같은 상용 모델을 쓰는 워커 몇 개로 시험했다고 밝혔다.

골프 과제의 결과도 저장소에 기록되어 있다. Lopsided.lean의 보조정리 하나를 골프한 풀 리퀘스트 #401에서는 heartbeat가 31,400에서 2,430으로 92.3% 감소했고, 증명 본문은 137줄에서 117줄이 됐다.⁴ 풀 리퀘스트 본문을 보면, 워커는 같은 꼴의 다른 보조정리를 골프하면서 얻은 진단을 이 보조정리에 그대로 적용했다. tauto 호출 세 개를 or_assoc, or_left_comm으로 교체한 것만으로 heartbeat가 85.1% 줄었다고 한다.

관련 연구와의 차이

최근의 자동 형식화 시스템 대부분은 Choir와 같은 다중 에이전트 구조를 쓴다. Meta FAIR의 RepoProver와 AutoformBot에서는 계획자가 증명할 진술 목록을 작성하고, 워커가 병렬로 증명하며, 검토자가 결과를 확인한 뒤 병합한다. LeanMarathon, FormalFlow, Archon은 연구 수준의 긴 증명에 비슷한 방식을 적용했다. Choir도 오케스트레이터와 워커 구조를 쓴다. 차이는 워커를 실행하는 주체에 있다. 다른 시스템에서는 한 팀이 자기 연산 자원과 예산으로 모든 에이전트를 실행하고, Choir에서는 다른 사람들의 에이전트가 각자의 컴퓨터와 계정에서 실행된다.

기여자의 자원을 공동으로 활용하는 발상은 자원 컴퓨팅(volunteer computing)에서 유래했다. BOINC 참여자는 자기 컴퓨터의 계산 시간을 기부하고, 프로젝트는 참여자를 통제할 수 없으므로 참여자가 반환한 결과를 직접 검사한다. Choir와 가장 비슷한 시스템들은 같은 발상을 형식화에 적용해, 기여자가 각자 자기 에이전트를 실행하게 한다.

저자들이 강조한 차이는 Choir가 인프라라는 점이다. 단일 라이브러리나 플랫폼과 달리, 어느 프로젝트든 자기 저장소에 자기 오케스트레이터를 두고 Choir를 구성할 수 있다.

한계와 다음 단계

저자들은 한계 세 가지를 밝혔다.

1. Choir는 오케스트레이터 하나와 워커 여럿을 두는 고전적인 다중 에이전트 설계를 따른다. Mathlib 규모의 프로젝트에서는 오케스트레이터가 수학 내용 전체를 추적하지 못하게 될 수 있다. 저자들은 이를 완화하려고 오케스트레이터가 주요 정리만 진술하고 세부 분해를 워커에게 맡기게 했으며, 로드맵을 관련 결과 묶음으로 분할해 오케스트레이터가 결정에 필요한 부분만 읽게 했다. 이 방식은 교과서 규모까지만 시험했고, 효과가 없으면 오케스트레이터를 계층 구조로 두는 방안이 도움이 될 수 있다고 적었다.
2. Isabelle과 Rocq의 진술 불변성 검사는 소스 텍스트를 비교하므로, 텍스트를 바꾸지 않고 의미를 바꾼 제출은 검토 단계에서만 검출된다. 저자들은 다음 버전에서 이 문제를 기계적으로 해결할 계획이다.
3. 지금까지의 시험은 주로 Lean 4 교과서 수준의 형식화였고, Claude Opus 5와 GPT-5.6 같은 상용 모델을 쓰는 워커 몇 개만 참여했다. 저자들은 오픈소스 모델과 하네스를 쓰는 실험을 포함해, 더 큰 규모의 실험에 참여할 협력자를 모집하고 있다.

저자들은 학계 연구 그룹은 물론 취미로 수학을 하는 사람들도 구독과 오픈소스 모델을 활용해 적은 예산으로 함께 대규모 형식화를 할 수 있게 될 것이라고 전망했다. 이 연구는 미국 방위고등연구계획국(DARPA)의 지원을 받았다.⁵

참여 방법

Choir 저장소는 Claude Code와 Codex용 플러그인을 제공하며, 저장소의 상태 표시는 프리알파다. Claude Code 세션에서는 다음 두 명령으로 설치한다.

/plugin marketplace add Weber-GeoML/Choir
/plugin install choir@choir

설치한 뒤 “Formalize ‹정리, 논문, 장› with Choir”라고 요청하면 감독자로서 프로젝트를 시작하고, “Join ‹owner/repo› as a Choir contributor”라고 요청하면 그 컴퓨터를 워커로 설정한다. 플러그인은 설정 스크립트를 실행하고 플레이북을 따르게 할 뿐 자체 동작을 정의하지 않는다. 따라서 다른 에이전트도 저장소의 docs/agents/ORCHESTRATOR.md나 docs/agents/CONTRIBUTOR.md를 읽게 하면 같은 역할을 맡을 수 있다.

시연 저장소를 읽고 나서

나는 논문을 다 읽은 뒤 시연 저장소의 풀 리퀘스트 목록을 확인했는데, 작성자 정보가 예상과 달랐다. 200건 모두 저자 Yidi Qi의 계정 하나가 만든 것이었고, 출처도 포크가 아닌 시연 저장소 자체의 브랜치였다. 논문이 설계한 워커는 저장소 쓰기 권한이 없는 낯선 기여자이고, 그 워커는 댓글로 선점하고 자기 포크에서 제출하도록 되어 있다. 공개된 시연은 그런 기여자가 한 명도 참여하지 않은 상태에서, 게이트와 분해 반복을 저자들이 실행한 워커로 시험한 기록이다. 논문 역시 워커 몇 개로 시험했다고 밝혔다.

게이트가 상정한 상대도 바로 그 낯선 기여자다. 진술을 바이트 단위로 그대로 두면서 모순된 가정을 추가하는 제출은 선의의 워커가 일부러 만들 일이 드물다. 이런 제출은 기여자가 성과를 과장하려 하거나, 증명을 끝내지 못한 모델이 편법을 쓸 때 나올 법하다. Lean에서는 comparator가 이 경우를 검출하고, Isabelle과 Rocq에서는 오케스트레이터와 사람의 검토에 의존한다. 개인 구독을 공동 프로젝트에 활용한다는 구상은 아직 검증을 기다리고 있다. 낯선 기여자들의 에이전트가 실제로 제출을 보내고 게이트가 그 제출을 검사한 기록이 생겨야 판단할 수 있을 것이다.

형식화 과정에서 원문의 빠진 가정 다섯 개와 오타 하나가 드러났다는 점도 인상 깊었다. 증명 보조기는 증명을 검사하는 도구로 소개되지만, 이 시연에서는 워커가 작은 사례를 계산하다가 강의 노트의 오류를 찾아냈다. MIT 강의 노트는 여러 해 동안 수강생들이 읽어 온 문서다. 그런 문서에서도 빠진 가정과 오타가 여섯 건 나왔으니, 교과서 26권을 형식화한 Atlas는 원문의 오류를 몇 건이나 찾았는지 알고 싶어진다.

출처

Yidi Qi, Melanie Weber (Harvard University), “Choir: An Open Protocol for Distributed Multi-Agent Autoformalization”, arXiv:2609.31903, 2026년 9월 25일. CC BY 4.0.

원문: https://arxiv.org/abs/2609.31903

코드: https://github.com/Weber-GeoML/Choir

시연 저장소: https://github.com/yidiq7/ProbMethodCombinatorics

증명 트리 이력 페이지: https://yidiq7.github.io/ProbMethodCombinatorics/choir-proof-tree.html