앤트로픽의 인공지능 모델 클로드가 1995년 앤드루 와일스 경이 증명한 페르마의 마지막 정리를 프로그래밍 언어 Lean으로 변환하는 자동 형식화 작업을 단 11일 만에 완수했다. 사람이 수년에 걸쳐 진행하던 엄밀한 논리 검증 작업을 다중 에이전트 기반의 자율 워크플로우로 단기간에 해결해낸 것이다. AI가 복잡한 수학적 정리의 완벽한 컴퓨터 검증까지 스스로 수행하는 단계에 도달했음을 보여주는 사례다.

클로드, 페르마의 마지막 정리 형식화 성공

앤트로픽은 수십 개의 클로드 에이전트를 결합한 다중 에이전트 워크플로우를 통해 페르마의 마지막 정리 증명을 Lean 언어로 성공적으로 형식화했다고 밝혔다. 1995년 앤드루 와일스 경이 완성한 복잡한 수학적 증명 구조를 컴퓨터가 엄밀히 검증할 수 있는 프로그래밍 언어 코드 형태로 전환한 것이다.

이 과정에서 인간 연구자의 역할은 초기 목표 정리의 제시와 시스템 설정, 그리고 간헐적인 우선순위 지정 및 피드백에 국한되었다. 실제 대규모 논리 전개와 증명 코드 작성은 클로드 에이전트들이 11일 동안 자율적으로 협력하며 수행했다. 이는 단순한 코드 생성을 넘어 대규모 자율 문제 해결 시스템으로서 AI 에이전트의 가능성을 증명한 결과다.

앤트로픽의 클로드 에이전트가 11일 만에 페르마의 마지막 정리 증명을 Lean 언어로 형식화했다.

1,300만 줄의 Lean 코드와 중간 정리

이번 프로젝트를 통해 생성된 Lean 코드는 약 1,300만 줄에 달한다. 이는 기존 수학 성과들을 모아놓은 대표적 Lean 라이브러리인 Mathlib 규모의 5배가 넘는 수치로, 지금까지 작성된 Lean 기반 형식 증명 중 역대 최대 규모다.

증명의 정교함을 보여주는 중간 정리 수치도 주목할 만하다. 클로드는 최종 증명 과정에서 약 29,500개(세부 집계 시 29,511개)의 중간 정리를 활용했으며, 전체 형식화 탐색 과정에서는 총 30,300개에 달하는 중간 정리를 증명했다. 이러한 대규모 중간 정리들이 철저히 검증되어 최종 증명으로 연결되었다.

최종 증명 과정에서 수만 개의 중간 정리가 검증되며 역대 최대 규모의 Lean 형식 증명이 완성되었다.

인간 연구 프로젝트와의 대조

이번 AI 성과는 인간 수학자 커뮤니티가 추진해 온 장기 프로젝트와 선명한 대조를 이룬다. 임페리얼 칼리지 런던의 케빈 버자드 교수는 5년간 100만 파운드의 연구비를 지원받아 페르마의 마지막 정리를 Lean으로 형식화하는 프로젝트를 진행하고 있었다.

버자드 교수는 클로드의 증명 결과를 Lean 검증 도구로 직접 확인한 뒤, 수학의 공리 외에는 어떠한 가정도 없이 정리를 증명해낸 특별한 자동 형식화 성과라고 평가했다. 인간 커뮤니티가 수년에 걸쳐 수행하려 했던 작업을 AI가 단 11일 만에 검증까지 완료한 셈이다.

5년 프로젝트로 추진되던 인간 수학자의 작업을 AI가 단 11일 만에 자율적으로 달성했다.

AI 자동 형식화가 가져올 변화

이번 성과는 수학 연구뿐만 아니라 소프트웨어 엔지니어링 전반에 중요한 시사점을 던진다. 다중 에이전트 워크플로우를 활용하면 수만 개의 의존성을 가진 대규모 논리 체계도 효율적으로 분산 처리하여 검증할 수 있음을 입증했기 때문이다.

소프트웨어 개발자들은 향후 이러한 에이전트 기반 자동 형식화 및 검증 기법을 복잡한 시스템 검증에 응용할 수 있다. 미션 크리티컬한 코드나 보안 프로토콜의 정밀 검증에 Lean과 같은 형식적 검증 언어를 결합하는 작업이 AI를 통해 획기적으로 대중화될 전망이다.

참고