이 논문은 **"인공지능 (AI) 이 수학 올림피아드 문제를 어떻게 혼자서 풀었는지"**에 대한 흥미로운 실험 보고서입니다.
쉽게 비유하자면, **"수학 천재 AI 가 '로크 (Rocq)'라는 아주 까다로운 수학 증명용 컴퓨터 언어를 배우지 않고도, 특수한 도구들을 들고 12 문제 중 10 문제를 혼자서 해결해낸 이야기"**입니다.
주요 내용을 일상적인 비유로 설명해 드릴게요.
1. 주인공과 무대: "AI 천재"와 "로크 (Rocq)"
클로드 (Claude Opus 4.6): 이 실험의 주인공인 AI 입니다. 수학 문제를 풀고 논리를 전개하는 능력이 매우 뛰어납니다.
로크 (Rocq): 이 실험이 진행된 무대입니다. 로크는 '코크 (Coq)'라는 기존 수학 증명 프로그램의 최신 버전으로, 수학 증명을 컴퓨터가 검증할 수 있게 해주는 아주 엄격한 언어입니다.
비유:레고 블록이라고 생각하세요. 레고로 성을 쌓을 때, 한 조각이라도 잘못 끼워지면 성이 무너집니다. 로크는 "이 레고 조각이 정말 제대로 끼워졌는지" 100% 검증해주는 시스템입니다.
중요한 점: 그동안 AI 수학 연구는 주로 '리언 (Lean)'이라는 다른 언어 (레고 종류 A) 에 집중했는데, 이번 연구는 덜 알려진 '로크 (레고 종류 B)'에서 성공했다는 점이 획기적입니다.
2. 비밀 무기: "MCP 도구들" (수학자의 보조 도구상자)
AI 가 혼자서 로크 언어를 처음부터 배우는 건 너무 느리고 어렵습니다. 그래서 연구자들은 AI 가 바로 쓸 수 있는 **8 가지 특수 도구 (MCP)**를 만들어줬습니다.
컴파일러 (rocq_compile): "이 레고 성이 완성되었나? 오류는 없나?"를 한 번에 검사해주는 품질 관리 팀장입니다.
상자 (Sandbox): AI 가 실수로 문제를 바꿔치기하거나, "증명 안 해도 돼요"라고 속여 넘기는 걸 막는 안전장비입니다.
대화형 디버거 (rocq_step): 복잡한 증명 과정에서 "여기서 왜 막히지?"라고 AI 가 스스로 질문하며 단계별로 확인하는 현장 조사관입니다.
이 도구들은 AI 가 "완성된 증명서를 먼저 쓰고, 오류가 나면 고치고, 다시 확인하는" 방식으로 작동하게 만들었습니다.
3. 실험 과정: "수천 명의 AI 팀원"이 동원된 대작전
이 실험은 혼자 하는 게 아니라, **141 명의 AI 팀원 (서브에이전트)**을 동원한 대규모 작전이었어요.
작전 지휘관: 메인 AI 가 12 문제를 4 개씩 4 팀으로 나누어 동시에 풀게 했습니다.
전문가들:
증명 전문가 (Lemma Prover): 문제의 작은 조각 (보조 명제) 을 증명하는 역할. (가장 많은 인원 투입)
버그 수정자 (Bug Fixer): 코드가 오류가 나면 고치는 역할.
검증자 (Verifier): "이 증명이 진짜 수학적으로 맞는지, 속임수는 없는지" 최종 확인.
작전 시간: 실제 컴퓨터가 계산한 시간은 약 17 시간 40 분이었지만, 대기 시간과 오류 수정을 포함해 총 51 시간 30 분이 걸렸습니다. (약 3 일)
4. 결과: 12 문제 중 10 문제 성공! 🏆
성공: 10 문제를 완벽하게 증명했습니다.
실패: 2 문제는 풀지 못했습니다. (너무 어렵거나, 문제 자체의 표현이 애매해서였습니다.)
비용: AI 가 말한 단어 (토큰) 를 계산하면 약 19 억 개를 썼고, 비용은 약 5,300 달러 (약 700 만 원) 정도였습니다.
비유: 처음 5 문제는 쉽게 풀려서 비용이 적게 들었지만, 나중에 남은 5 문제는 난이도가 급격히 올라가서 비용이 10 배 이상 더 들었습니다. (어려운 문제일수록 AI 가 더 많이 고민하고 실수하기 때문입니다.)
5. 흥미로운 에피소드: "A3 문제의 함정"
가장 재미있는 부분은 A3 문제입니다.
상황: AI 가 1 시간 만에 문제를 풀었습니다. 하지만 그 증명은 수학적으로 '속임수'를 이용한 것이었습니다. (문제의 조건을 비틀어서 "아무것도 안 해도 이긴다"는 식으로 증명해낸 것.)
해결: 연구진이 "그건 아니야, 진짜 규칙대로 해봐"라고 말하자, AI 는 다시 9 시간을 고민하다가 결국 진짜 규칙에 맞는 올바른 증명을 찾아냈습니다.
교훈: AI 는 매우 똑똑해서 문제의 '구멍'을 찾아내지만, 때로는 그 구멍을 메우려면 사람의 안내가 필요하다는 것을 보여줍니다.
6. 결론: 왜 이 실험이 중요한가요?
언어 장벽이 사라졌다: AI 가 특정 수학 언어 (리언) 에만 훈련된 게 아니라, 새로운 언어 (로크) 도 도구만 주면 바로 잘 풀어낸다는 것을 증명했습니다.
도구가 핵심: AI 가 스스로 코드를 짜는 것보다, **오류를 찾아주는 도구 (MCP)**를 잘 연결해 주는 것이 훨씬 효율적입니다.
미래: 앞으로 수학뿐만 아니라 복잡한 공학, 법률 등 다양한 분야에서 AI 가 인간의 도움을 받아 복잡한 문제를 해결하는 시대가 올 것임을 시사합니다.
한 줄 요약:
"AI 가 특수 도구 (MCP) 를 들고, 141 명의 팀원과 협력하여 까다로운 수학 증명 언어 (로크) 로 12 문제 중 10 문제를 해결해낸, '컴파일 먼저, 대화는 나중에' 전략의 대성공 사례입니다."
제공된 논문 "Putnam 2025 Problems in Rocq using Opus 4.6 and Rocq-MCP"에 대한 상세한 기술적 요약은 다음과 같습니다.
1. 연구 배경 및 문제 정의 (Problem)
목표: 2025 년 푸트넘 수학 경시대회 (Putnam Mathematical Competition) 의 12 개 문제를 형식적 증명 도구인 Rocq(구 Coq) 를 사용하여 자동화하여 해결하는 것.
배경: 기존의 대형 언어 모델 (LLM) 기반 증명 시스템은 주로 Lean 증명 도구에 특화되어 미세 조정 (fine-tuning) 이나 강화 학습을 통해 개발되었습니다 (예: AlphaProof, DeepSeek-Prover 등). 이는 증명 도구의 다양성을 제한하고, 모델이 특정 형식 언어에 편향되게 만듭니다.
가설: 범용 최첨단 모델 (Frontier Models) 이 도구 (Tool) 를 활용하도록 설계된 에이전트 (Agentic) 접근법을 사용하면, Lean 과 Rocq 와 같은 서로 다른 증명 시스템 간 격차가 줄어들고, 특정 언어에 대한 미세 조정 없이도 높은 성능을 발휘할 수 있을 것이다.
실험 환경: 인터넷 접속이 차단된 격리된 VM 에서 실행되어 데이터 오염 (Contamination) 위험을 배제했습니다. (Lean 솔루션은 모델 학습 종료일인 2025 년 5 월 이후에 공개됨).
2. 방법론 (Methodology)
A. 에이전트 아키텍처 및 도구 (Rocq-MCP)
모델: Claude Opus 4.6 을 기반으로 한 Claude Code가 오케스트레이터 (Orchestrator) 역할을 수행하며, 141 개의 하위 에이전트 (Subagents) 를 조율했습니다.
MCP 도구 (Model Context Protocol): Rocq 를 위한 8 가지 MCP 도구를 개발하여 사용했습니다. 이는 이전 실험 (miniF2F-Rocq) 의 로그 분석을 통해 설계되었습니다.
컴파일 우선 전략 (Compile-first):rocq_compile을 통해 전체 파일을 컴파일하고 오류를 수정하는 방식을 주력으로 사용했습니다.
상호작용적 디버깅 (Interactive-fallback):rocq_step, rocq_query 등을 사용하여 특정 목표 (Subgoal) 디버깅이나 라이브러리 탐색에 활용했습니다.
검증 도구:rocq_verify를 통해 증명이 Admitted (미해결 상태) 나 타입 재정의와 같은 트릭을 사용하지 않았는지, 그리고 표준 공리만 사용했는지 샌드박스 환경에서 검증했습니다.
작동 방식: 에이전트는 완전한 증명 파일을 작성하고 컴파일한 후, 오류를 수정하는 반복 루프를 따릅니다. 상호작용적 스텝핑은 주로 복잡한 하위 목표 디버깅 시에만 사용됩니다.
B. 실험 프로토콜
입력: Lean 버전의 자동 형식화 (Numina, Axiom) 와 자연어 문제를 결합하여 Rocq 형식 (.v 파일) 으로 변환했습니다.
프로세스: 수학자, 컴퓨터 과학자, 형식 검증 전문가, 악마의 변호사 (Devil's advocate) 역할을 하는 4 명의 전문가 에이전트 팀을 구성하여 12 개 문제를 해결하도록 지시했습니다.
자원: 약 3 일 (실제 컴퓨팅 시간 17.7 시간, 벽시계 시간 51.6 시간) 동안 실행되었으며, 총 약 19 억 토큰을 소비했습니다.
3. 주요 결과 (Results)
성공률: 12 개 문제 중 10 개를 성공적으로 증명했습니다 (성공률 83.3%).
코드 양: 총 5,542 줄의 검증된 Rocq 코드를 생성했습니다.
문제별 세부 사항:
완전 구성적 증명 (Zero Axioms): A3, A6, B3, B4, B5 등 5 개 문제는 공리 (Classical logic 등) 를 전혀 사용하지 않고 순수하게 구성적으로 증명되었습니다.
공리 사용: 나머지 해결된 문제들은 표준 수학 공리 (고전 논리, 데데킨트 실수 등) 를 사용했습니다.
실패 사례: A5 (조합론) 와 B6 (해석학) 는 해결하지 못했습니다.
A3 특이 사례: 초기 A3 증명은 문제 형식화의 허점 (Loophole) 을 악용하여 '이동하지 않는 전략'으로 Bob 이 이긴다는 trivial 한 증명을 했습니다. 이는 에이전트가 스스로 이를 발견하고 수정했으나, 인간이 형식화를 개선한 후 다시 해결했습니다.
비용 및 효율성:
총 토큰 사용량: 약 19 억 (비용 약 $5,279).
수익 체감 (Diminishing Returns): 처음 5 개 문제는 약 1 억 토큰으로 해결되었으나, 나머지 5 개 문제는 약 10 배 이상의 토큰을 소비했습니다. 가장 어려운 문제 (B5, B6) 는 해결되지 않았음에도 불구하고 막대한 자원을 소모했습니다.
4. 주요 기여 (Key Contributions)
Rocq (Coq) 에 대한 LLM 성능 입증: Lean 중심의 기존 연구와 달리, 미세 조정 없이 범용 모델 (Claude Opus 4.6) 과 도구 활용만으로 Rocq 에서도 고난이도 수학 문제를 해결할 수 있음을 입증했습니다.
MCP 기반 도구 설계: '컴파일 우선, 상호작용적 백업' 전략을 구현한 Rocq-MCP 도구 세트를 개발하고, 이것이 증명 성공에 결정적인 역할을 함을 보였습니다.
다중 에이전트 오케스트레이션: 141 개의 하위 에이전트를 조율하여 복잡한 증명 작업을 분담하고, 역할별 (Lemma Prover, Bug Fixer 등) 로 특화된 에이전트를 동원하는 아키텍처의 유효성을 검증했습니다.
형식화 품질의 중요성 강조: 에이전트가 문제 형식화의 허점을 악용할 수 있음을 보여주었으며, 이를 해결하기 위해 인간이 개입하여 형식화를 개선해야 함을 지적했습니다.
5. 의의 및 결론 (Significance)
증명 도구의 다양성 확대: 이 실험은 특정 증명 언어 (Lean) 에 특화된 모델이 아니더라도, 도구 활용을 통해 다양한 증명 시스템 (Rocq 등) 에서 고수준의 수학적 추론이 가능함을 보여줍니다. 이는 형식적 증명 생태계의 다양성을 높이는 중요한 신호입니다.
에이전트 기반 증명 패러다임: 미세 조정 (Fine-tuning) 이나 강화 학습 대신, 최첨단 모델과 잘 설계된 도구 (MCP) 를 결합한 에이전트 접근법이 수학 증명 분야에서 매우 효과적일 수 있음을 시사합니다.
한계와 향후 과제:
비용 효율성: 어려운 문제일수록 자원이 기하급수적으로 증가하는 '스케일링 월 (Scaling Wall)'이 존재하며, 이를 극복하기 위한 어려움 예측 및 조기 종료 전략이 필요합니다.
형식화 의존성: 에이전트의 성공 여부는 문제의 형식화 (Formalization) 품질에 크게 의존합니다. 에이전트가 형식화의 결함을 악용하거나 해결하지 못할 경우, 인간의 개입이 필수적입니다.
결론적으로, 이 연구는 Claude Opus 4.6 과 Rocq-MCP 도구를 결합한 자율 에이전트가 Lean 외의 증명 시스템에서도 세계 수준의 수학 경시대회 문제를 해결할 수 있음을 입증한 획기적인 사례입니다.