Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents

이 논문은 대규모 LLM 에이전트들이 정적 계획 대신 보너스 기반 시장 메커니즘을 활용하여 상호작용적 정리 증명 (ITP) 환경에서 대수적 위상수학의 자동 형식화와 증명 탐색을 분산 협력적으로 수행하는 실험을 다룹니다.

핵심

이 논문은 **"수학이라는 거대한 퍼즐을 해결하기 위해, 인공지능 에이전트들이 서로 경쟁하고 협력하는 시장 **(시장 경제)에 대한 실험 보고서입니다.

이 복잡한 내용을 일상적인 비유로 쉽게 설명해 드릴게요.

1. 배경: 왜 이런 실험을 했나요?

기존에 인공지능 (LLM) 이 수학 교재를 컴퓨터가 이해할 수 있는 형식으로 번역하는 '자동 형식화' 작업을 해왔지만, 한 명의 에이전트가 모든 일을 하려다 보니 속도가 너무 느렸습니다. 마치 한 명의 요리사가 거대한 뷔페 식당의 모든 요리를 혼자 만들려고 하다가 지쳐버리는 상황과 비슷합니다.

그래서 연구진은 **"여러 명의 요리사 **(에이전트)를 도입하기로 했습니다.

2. 핵심 아이디어: "상금 (Bounty) 시장"

이 실험의 핵심은 **'상금 시스템'**입니다.

• 작업장: '메갈로돈 (Megalodon)'이라는 수학 증명 검증 프로그램이 있는 가상의 도시입니다.
• 작업: 알기 어려운 위상수학 (Topology) 교재의 내용을 증명하는 것.
• 시스템:
  1. 임무 공고: 먼저 수학자들이 (또는 AI 가) 증명해야 할 문제들을 나열하고, 각 문제마다 **'상금 **(보상)을 붙입니다. (예: "이 정리를 증명하면 100 달러를 드립니다.")
  2. 경쟁과 협력: 4 명의 AI 에이전트 (앨리스, 밥, 찰리, 데이브) 가 이 상금을 노리고 뛰어듭니다.
     • 경쟁: 누구보다 빨리 증명해서 상금을 가져가려 합니다.
     • 협력: 너무 어려운 문제는 "이건 내가 못하겠으니, 이 부분을 증명해 주는 사람에게 10 달러를 줄게"라고 **하위 상금 **(서브 상금)을 걸고 다른 에이전트에게 도움을 요청합니다.
  3. **보증금 **(Lock) 에이전트는 특정 문제를 "내가 증명할게!"라고 선언하며 상금의 10% 를 보증금으로 맡깁니다. 만약 다른 사람이 그 문제를 먼저 증명해 버리면, 보증금은 돌려받지만 상금은 못 받습니다.

3. 실험 결과: 얼마나 빨랐나요?

이 "AI 시장"은 놀라운 속도를 보여줬습니다.

• 속도: 한 명의 에이전트가 하루에 약 7,000 줄의 코드를 작성하는 반면, 4 명의 에이전트가 협력하자 하루에 약 39,000 줄을 작성했습니다. 약 5 배 이상 빨라진 것입니다.
• 상금 흐름: 에이전트들은 서로의 작업을 가로채기도 했지만 (경쟁), 서로의 부족한 부분을 채워주기도 했습니다 (협력). 마치 건설 현장에서 한 팀이 기초 공사를 하고, 다른 팀이 벽을 쌓으며, 또 다른 팀이 배관을 설치하는 것과 비슷했습니다.

4. 재미있는 에피소드와 문제점

• 실수 교정: 처음에는 "연습문제"에도 상금을 붙여줬는데, 에이전트들이 연습문제를 증명하느라 시간을 낭비하는 바람에 연구진이 "연습문제에는 상금 주지 마!"라고 규칙을 수정했습니다.
• AI 의 한계: 에이전트들이 '브라우어 고정점 정리' 같은 어려운 문제를 증명해냈지만, **'사인 **(sin) 함수의 정의가 컴퓨터에게는 너무 모호해서 막혔습니다. 마치 "원주율을 3.14 로 정의해라"라고 했을 때, AI 가 "어떤 3.14?"라고 혼란을 겪는 것과 비슷합니다. AI 는 스스로 더 정확한 정의를 만들어내야 했지만, 아직 그 수준에는 미치지 못했습니다.

5. 결론: 이 실험이 의미하는 바는?

이 논문은 **"중앙에서 모든 일을 지시하는 것보다, 에이전트들에게 상금을 걸고 자유롭게 경쟁하게 하는 것이 훨씬 빠르고 유연하다"**는 것을 증명했습니다.

마치 **크라우드소싱 **(대중 참여형 작업)이나 경매 시장처럼, AI 들이 스스로 일을 찾아서 하고, 서로 도와가며 거대한 수학의 산을 빠르게 정복해 나가는 새로운 방식을 제시한 것입니다.

한 줄 요약:

"한 명의 천재가 모든 문제를 푸는 대신, 여러 명의 AI 에게 '상금'을 걸고 서로 경쟁하게 했더니, 수학 증명 속도가 5 배나 빨라졌다!"

기술 요약

논문 요약: Agent Hunt - LLM 에이전트를 활용한 보상 기반 협업 자동 형식화

이 논문은 대화형 정리 증명 (Interactive Theorem Proving, ITP) 환경에서 대규모 수학 텍스트 (대수적 위상수학) 를 자동 형식화하는 실험을 다룹니다. 단일 에이전트에 의존하는 기존 방식의 한계를 극복하기 위해, 다수의 LLM 에이전트가 보상 (Bounty) 시장 메커니즘을 통해 경쟁하고 협력하는 분산형 접근법을 제안하고 검증했습니다.

1. 문제 제기 (Problem)

• 대규모 형식화의 비효율성: 기존 연구 [6] 에서 대규모 수학 텍스트 (일반 위상수학) 의 자동 형식화는 유망한 결과를 보였으나, 단일 에이전트만으로는 진행 속도가 느리고 프로젝트 완료까지 장기간이 소요되었습니다 (예: 35 만 줄 이상의 코드가 2 개월 이상 진행 중).
• 중앙 집중식 계획의 한계: 대규모 형식화 작업은 증명 내의 간극 (gaps), 선행 참조 (forward references) 등 예측 불가능한 요소가 많아, 사전에 모든 작업을 중앙에서 세밀하게 계획하고 분배하는 것이 어렵습니다.
• 해결 필요성: 여러 에이전트가 병렬적으로 작업을 수행하고, 동적으로 작업을 분배하며, 효율적으로 협업하여 대규모 프로젝트를 가속화할 수 있는 메커니즘이 필요합니다.

2. 방법론 (Methodology)

연구팀은 Megalodon (고차 집합론 증명 검사기) 환경에서 4 개의 LLM 에이전트 (Alice, Bob, Charlie, Dave) 를 활용하여 보상 기반 시장 (Bounty-based Marketplace) 시스템을 구축했습니다.

• 시스템 아키텍처:
  • 에이전트 구성: 4 개의 LLM 에이전트 (ChatGPT Pro Codex, Claude Code 등) 가 참여하며, 서로 경쟁하되 조기에 프로젝트를 완료하기 위해 협력하도록 인센티브를 부여받습니다.
  • 보상 (Bounty) 시스템:
    • 각 정리 (Theorem) 에는 초기에 노력과 난이도에 기반한 가상의 보상 (USD 토큰) 이 책정됩니다.
    • 에이전트는 정리를 증명하여 보상을 획득하거나, 새로운 보조 정리 (Lemma) 를 제안하고 보상을 걸 수 있습니다.
    • 잠금 (Locking) 메커니즘: 에이전트는 정리의 보상의 10% 를 지불하여 24 시간 동안 해당 정리를 '잠금'할 수 있으며, 이 기간 중 다른 에이전트가 증명하더라도 보상은 잠금한 에이전트에게 지급됩니다.
  • 협업 및 경쟁: 에이전트는 타인의 보상을 해결하거나, 하위 보조 정리 (Sub-lemmas) 에 보상을 걸어 다른 에이전트의 도움을 받을 수 있습니다.
• 초기 설정 및 품질 관리:
  • 블루프린트: 초기에 한 명의 LLM 에이전트 (Claude Opus 4.6) 가 Munkres 교재의 대수적 위상수학 부분 (약 200 페이지) 을 형식화하고 보상을 책정했습니다. 이 과정에서 정의와 정리의 오류를 방지하기 위해 엄격한 검증과 수정이 이루어졌습니다.
  • 가드 스크립트 (Guard Scripts): 에이전트가 규칙 (잔액 음수 방지, 잠금 횟수 제한, 정의 불변성 등) 을 위반하지 않도록 로컬에서 실행되는 검증 스크립트를 도입했습니다.
  • Megalodon 개선: LLM 생성 파일의 효율적 처리를 위해 증명 의존성 검사 강화, 오류 메시지 개선, 불투명한 해시 대신 가독성 있는 이름 사용 등 시스템을 수정했습니다.

3. 주요 기여 (Key Contributions)

1. 분산형 협업 증명 검색: 중앙 집중식 계획 없이, 시장 메커니즘 (보상, 경쟁, 협력) 을 통해 다수 에이전트가 자율적으로 대규모 형식화 작업을 수행하는 새로운 패러다임을 제시했습니다.
2. 동적 작업 분배: 에이전트가 자신의 강점에 맞춰 주제 (예: 호모토피, 덮개 공간, 대수적 구조 등) 를 자연스럽게 분담하고, 인터페이스에서 발생하는 중복을 최소화하며 협업했습니다.
3. 대규모 형식화 속도 향상: 단일 에이전트 대비 월등히 빠른 형식화 속도를 달성하여, 대규모 수학 프로젝트의 자동화 가능성을 입증했습니다.
4. 시스템 및 도구 개선: LLM 에이전트와의 상호작용을 최적화하기 위해 ITP 환경 (Megalodon) 과 검증 도구를 대폭 개선했습니다.

4. 실험 결과 (Results)

• 성능 지표:
  • 진행 속도: 4 개의 에이전트가 2 일 15 시간 만에 약 12 만 줄의 형식화 코드를 생성했습니다. 이는 하루 평균 약 39,000 줄에 해당하며, 기존 단일 에이전트 프로젝트 (하루 평균 7,000 줄) 보다 약 5.5 배 빠른 속도였습니다.
  • 비용 효율성: 실험 비용은 약 150 달러 (LLM 구독료) 로 추정되며, 이는 정규화된 코드 1,000 줄당 약 1 달러 미만입니다.
• 협업 및 경쟁 패턴:
  • 총 709 개의 보상이 생성되었으며, 그중 279 개는 생성자가 직접 증명했고, 114 개는 다른 에이전트가 증명하여 성공적인 교차 협력이 이루어졌습니다.
  • 에이전트 간 명확한 역할 분담이 관찰되었습니다 (예: Bob 은 호모토피와 기본군, Charlie 는 기하학적 위상수학, Alice 는 경로 연결 및 군 법칙, Dave 는 추상 군론 지원 등).
• 주요 증명 성과:
  • 기본군 (Fundamental Group): 기본군이 실제로 군 (Group) 임을 증명하는 등 핵심 정리들을 증명했습니다.
  • 브라우어 고정점 정리 (Brouwer Fixed Point Theorem): 원의 기본군이 정수와 동형이라는 전제하에 증명되었으나, 이 전제 자체의 증명 (cos/sin 정의의 문제) 은 아직 미해결 상태로 남았습니다.
  • 장문의 증명: 400 줄 이상의 정규화된 증명을 가진 20 개 이상의 주요 정리를 성공적으로 증명했습니다 (예: cyclic_infinite_order_iff_Z - 1,999 줄).

5. 의의 및 시사점 (Significance)

• 확장 가능한 자동 형식화: 이 연구는 LLM 에이전트 기반의 자동 형식화가 단일 에이전트의 한계를 넘어, 분산형 시장 메커니즘을 통해 대규모 수학 프로젝트에 확장 가능함을 보여줍니다.
• 실제 수학 프로젝트 적용 가능성: 예측 불가능한 요소가 많은 실제 수학 텍스트 (교재 등) 를 형식화할 때, 사전 계획보다 유연한 동적 분배가 더 효과적임을 입증했습니다.
• 도구 및 방법론의 발전: ITP 환경과 LLM 에이전트 간의 원활한 상호작용을 위한 새로운 검증 도구 (Guard Scripts) 와 증명 환경 (Megalodon) 개선 방안을 제시하여, 향후 자동화 연구의 기초를 마련했습니다.
• 한계와 향후 과제: 현재까지도 일부 정의 (예: 삼각함수) 의 부정확성으로 인해 특정 정리의 완결이 어려운 경우가 있으며, 이는 에이전트가 새로운 올바른 정의를 생성하고 검증해야 하는 과제로 남았습니다.

결론적으로, Agent Hunt는 LLM 에이전트들이 보상 시스템을 통해 경쟁하고 협력함으로써, 인간 전문가의 개입을 최소화하면서도 대규모 수학적 지식을 효율적으로 형식화할 수 있는 강력한 가능성을 제시한 획기적인 연구입니다.