Claude, Lean을 사용하여 페르마의 마지막 정리를 형식화하다
Anthropic은 최근 대규모 연구 과제를 완료했습니다. 내부 모델이 11일 동안 작업하여 Lean 4 증명 언어를 사용해 페르마의 마지막 정리를 형식화했습니다.
이것은 새로운 수학적 발견이 아닙니다. 앤드루 와일즈(Andrew Wiles)는 1995년에 이 정리를 이미 증명했습니다. Anthropic이 수행한 작업은 기존의 증명을 코드로 변환한 것입니다. 이를 통해 컴퓨터가 모든 논리적 단계를 완벽한 확실성을 가지고 검증할 수 있습니다.
이 프로젝트의 규모는 엄청납니다: • 모델은 1,300만 줄의 Lean 코드를 생성했습니다. • 30,300개의 중간 정리를 증명했습니다. • 약 60억 개의 출력 토큰을 사용했습니다.
모델은 대부분 스스로 작동했습니다. 인간은 가끔씩 높은 수준의 지침만 제공했습니다. 프로세스는 아무도 지켜보지 않는 한밤중에 완료되었습니다. 시스템은 성공 여부를 자동으로 기록했습니다.
주목해야 할 두 가지 중요한 사항이 있습니다:
- 이 모델은 내부 연구용 도구입니다. 아직 API를 통해 접근할 수 없습니다. 현재 사용 중인 Claude 모델과는 다릅니다.
- 개발자들에게 진정한 가치는 Prove2Me라고 불리는 조정 레이어(coordination layer)에 있습니다.
Prove2Me는 오픈 소스 도구입니다. 작업 관리를 위해 의존성 그래프(dependency graph)를 사용합니다. 단순한 체크리스트 대신, 증명들이 서로 어떻게 연결되는지를 보여주는 지도를 생성합니다.
이 구조는 에이전트 워크플로우의 두 가지 주요 문제를 해결합니다:
- 여러 에이전트가 동일한 작업을 수행하는 것을 방지합니다.
- 에이전트에게 공유 메모리를 제공하여 주요 목표를 잊지 않게 합니다.
대부분의 에이전트 워크플로우는 시간이 지남에 따라 문맥(context)을 놓치기 때문에 실패합니다. 긴 채팅창 대신 공유된 외부 그래프를 사용하면 작업을 궤도에 유지할 수 있습니다.
에이전트 워크플로우를 구축한다면 Prove2Me 아키텍처를 연구해 보시기 바랍니다. Anthropic의 연구용 모델을 사용하지 않더라도, 그들이 작업을 조정하는 방식은 장기적인 작업(long horizon work)을 위한 청사진이 될 수 있습니다.
출처: https://dev.to/raxxostudios/claude-just-formalized-fermats-last-theorem-in-lean-3p36
선택 사항 학습 커뮤니티: https://t.me/GyaanSetuAi