AI 클로드, 10년 걸릴 '페르마의 마지막 정리' 증명 검증 11일 만에

2000년 세계 수학의 해 기념 우표. 수학 역사상 가장 유명한 난제 중 하나인 '페르마의 마지막 정리'가 담겼다. Z. Ziegler, M. Ondrachek/Wikimedia Commons 제공 인간 수학자들이 약 10년이 걸릴 것으로 예상했던 '페르마의 마지막 정리'를 컴퓨터가 검증 가능한 코드로 변환하는 '형식화' 작업을 인공지능(AI)이 단 11일 만에 완료했다. 앤트로픽의 AI 모델 '클로드'가 수학 대표 난제 증명을 약 1300만줄의 코드로 변환하는 데 성공하면서 AI가 수학 연구의 검증 도구로 본격 활용될 가능성이 커졌다는 평가가 나온다. 7일(현지시간) 국제학술지 '네이처' 보도에 따르면 앤트로픽은 지난 4일 클로드의 고급 프로토타입 모델을 이용해 페르마의 마지막 정리 증명을 컴퓨터 검증 가능한 코드 형태로 완전히 형식화했다고 발표했다. 수학에서 '형식화'는 자연어와 수식으로 작성된 수학적 논증을 컴퓨터가 엄밀하게 검증할 수 있는 형식 언어로 바꾸는 작업이다. 사람이 논리 전개를 작성하는 데 그치는 것이 아니라 각 단계가 논리적으로 타당한지 컴퓨터가 하나씩 확인할 수 있도록 만드는 과정이다. 클로드는 수학 정리 증명에 널리 사용되는 프로그래밍 언어 '린'을 활용했다. 린은 마이크로소프트 리서치팀이 2013년 개발한 수학 증명을 검증하는 소프트웨어다. 페르마의 마지막 정리는 n이 3 이상의 정수일 때 x^n＋y^n＝z^n을 만족하는 양의 정수 x, y, z는 존재하지 않는다는 명제다. 17세기 프랑스 법률가였던 피에르 드 페르마가 1637년 여가시간에 디오판토스의 '산술'이라는 책의 여백에 이 같은 내용을 적고는 '여백이 부족해 증명 방법은 적을 수 없다'며 증명을 남기지 않아 350년 넘게 수학계의 대표적인 난제로 남았다. 수학계에 따르면 페르마의 마지막 정리는 지금까지 가장 많은 '틀린' 증명이 발표된 문제다. 1995년 영국의 수학자 앤드루 와일스가 증명을 완성했지만 그 역시 1993년 첫 증명을 발표한 당시 오류가 발견돼 증명을 수정해야 했다. 1995년 페르마의 마지막 정리를 증명한 앤드루 와일스 영국 옥스퍼드대 수학과 교수. C. J. Mozzochi, Princeton N.J/Wikimedia Commons 제공 와일스의 증명은 매우 방대한 현대 수학 이론을 토대로 한다. 당시 와일스가 발표한 논문은 100페이지가 넘었다. 내용이 매우 복잡해 동료 수학자들이 논리적 오류가 없는지 검증하는 데 2년 이상 걸렸다. 린으로 같은 내용을 검증하려면 최종 논증뿐 아니라 증명이 의존하는 수많은 정의와 기존 정리까지 컴퓨터가 이해할 수 있는 코드로 먼저 입력해야 한다. 케빈 버자드 영국 임페리얼칼리지런던 교수는 2024년부터 페르마의 마지막 정리를 형식화하기 위해 필요한 수천 쪽 분량의 선행 결과를 '매스립'에 추가하는 프로젝트를 이끌어왔다. 매스립은 린 기반 수학 지식 라이브러리다. 버저드 교수는 작업을 완료하는 데 약 10년이 걸릴 것으로 예상했다. 클로드는 독자적인 방식으로 같은 증명의 린 검증을 11일 만에 완료했다. 생성한 코드는 약 1300만줄 규모로 최종 증명에 이르기까지 단계별로 확인해야 하는 세부 정리 약 2만9500개가 포함됐다. 버저드 교수는 "2년 전까지만 해도 판타지라고 생각했던 일이 실제로 이뤄졌다"며 "그동안 와일스의 증명이 99.9% 옳다고 확신했는데 이번 형식화로 이제 100% 확신한다"고 말했다. 대니얼 리트 캐나다 토론토대 수학과 부교수는 "페르마의 마지막 정리를 형식화할 수 있다면 아마 무엇이든 형식화할 수 있을 것"이라고 말했다. 클로드가 만든 코드를 곧바로 수학자들이 공동 자산으로 활용할 수 있는 것은 아니다. 매스립은 여러 연구자가 기존 정의·정리를 재사용하도록 표준화해 구축한 공용 라이브러리지만 클로드가 구축한 대규모 코드 체계는 증명을 완성하고 검증하는 데 맞춰 독자적으로 구성됐다. 클로드 코드 일부를 매스립에 통합하는 것도 막대한 작업이 필요할 것으로 예상된다. AI가 각자 독립적인 수학 라이브러리를 대량으로 생성할 경우 서로 호환되지 않는 체계가 난립할 수 있다는 우려도 나온다. 그럼에도 수학자들은 AI와 자동 증명 검증 기술로 향후 논문 검토 방식이 효율적으로 바뀌기를 기대한다. 프레더릭 매너스 미국 샌디에이고캘리포니아대 교수는 "수학 논문은 갈수록 길고 복잡해져 동료평가만으로 오류를 모두 찾아내기 어렵다"며 "논문을 입력하면 증명이 맞다는 인증서를 제공하거나 오류 지점을 알려주는 시스템이 구현된다면 매우 유용할 것"이라고 말했다. Copyright Ⓒ 동아사이언스. All rights reserved. 무단 전재, 재배포 및 AI학습 이용 금지