수학의 꽃 '증명'..AI가 함께 검증 [Science]

필즈상에 빛나는 숄체 교수
"인공지능이 문제 검증 도와"
증명된 여러 명제 학습한후
새로운 방법 찾아 제시하고
최적의 흐름 찾아내기도 해
아직은 보조자 불과하지만
압도적인 계산능력 무기로
새로운 '증명의 시대' 준비

[사진 출처 = pixabay]

머리를 감싸쥐며 종이 위에 펜으로 수식을 써 내려가는 모습. 여러 개의 방정식으로 가득 찬 칠판. 흔히 묘사되는 수학자의 모습이다. 수학자에겐 연구 장비 따위 필요 없이 펜과 종이만 있으면 된다는 우스갯소리도 있다.

그런 수학의 꽃으로 불리는 것이 '증명'이다. 수학자들은 사실로 전제된 공리에서 논리만으로 새로운 증명을 찾아 나선다. 그러나 새로운 증명을 발견해도 그대로 인정받는 것은 아니다. 수학자 또한 사람이고, 실수할 수 있기에 증명이 참인지 검증하는 절차를 거친다. 검증 과정에서 증명의 큰 틀에는 문제가 없으나 사소한 실수가 발견되는 경우가 있는 반면, 증명 전체가 흔들리는 중요한 실수가 발견되기도 한다.

펜과 종이로 대표되는 수학 증명에서 컴퓨터를 사용해 증명을 검증한 사례가 나오며 화제가 되고 있다. 주인공은 현대 수학계의 대표적 천재 페터 숄체와 케빈 버자드 임피리얼칼리지런던 교수. 숄체는 지난 6월 "이번 도전이 완전히 마무리되지는 않았으나, 증명에서 확신이 없던 모든 부분이 이번 실험으로 명확해졌다"며 "몹시 흥분되는 상황"이라는 내용의 글을 버자드의 블로그에 게시했다.

그는 또 "컴퓨터를 통한 증명 보조 프로그램이 어려운 증명을 합리적인 시간 안에 검증하는 수준이 됐다"고 설명했다.

컴퓨터를 통해 학부 수준의 정리를 다시 검증한 사례는 과거에도 있었다. 그러나 복잡한 현대 수학에서 새로운 연구에 대해 컴퓨터가 검증에 성공한 것은 이번이 처음이다.

숄체는 2018년 수학계의 노벨상으로 불리는 필즈상을 수상한 인물이다. 젊은 나이로 독보적 성과를 내며 만 24세에 본대학 교수로 임용됐다. 독일 역사상 가장 어린 교수다. 현재는 막스플랑크수학연구소 소장으로 재직하고 있다.

프로젝트가 시작된 것은 2019년. 숄체는 코펜하겐대의 수학자 더스틴 클라우센과 위상수학에 대한 개념을 전환해 기하학과 함수해석, 정수론 분야를 연결하는 계획을 제시했다. 네이처에 따르면 이들은 위상수학에 대한 기존의 접근 방식은 이 세 분야가 맞아떨어지지 않는 결과로 이어졌으나, 새로운 접근 방식으로 볼 경우 세 분야 연구가 같은 결론을 도출할 수 있다고 봤다. 클라우센은 "일종의 대통합"이라고 설명했다고 한다.

이들은 계획의 중요한 보조정리를 증명했다고 생각했으나, 증명의 기반이 되는 아이디어가 명확하게 밝혀지지 않아 보조정리의 증명 또한 맞는지 확신을 갖지 못하고 있었다고 한다.

클라우센은 네이처와 인터뷰에서 "정리가 너무 복잡했고, 숄체는 전체 증명이 무효화될 수 있는 작은 실수가 있을지도 모른다며 우려했다"면서 "설득력이 있어 보였지만 너무 참신했다"고 밝혔다.

네이처에 따르면 숄체는 2020년 12월 증명 보조 소프트웨어 전문가들에게 자신의 명제를 제시했다. 컴퓨터를 사용해 증명을 검증하는 방안을 시도하기 위해서다. 버자드와 독일 프라이부르크대의 수학자 요한 코멜린이 이끄는 팀이 이를 받아들였다. 버자드는 수학 학부 커리큘럼에 검증 프로그램을 다년간 운용해 온 인물이기도 하다. 여러 수학자들이 팀에 합류했고, 컴퓨터 과학자들의 도움도 이어졌다. 지난 6월 초 팀은 숄체가 가장 걱정하던 부분을 컴퓨터가 이해할 수 있는 언어로 번역하는 데 성공했고, 컴퓨터는 증명에 문제가 없다고 검증했다.

김완수 KAIST 수리과학부 교수는 "컴퓨터에 숄체가 시도하는 수학의 기본 개념을 가르치는 것부터 시작해 증명을 프로그램으로 검증하려는 시도를 했고, 단순히 검증을 떠나 더 최적의 증명을 찾아낸 것으로 보인다"고 했다. 이어 "증명에서 부자연스러웠던 부분이 컴퓨터의 검증을 거쳐 더 자연스러운 흐름으로 연결됐다고 숄체가 인정한 것"이라고 덧붙였다.

컴퓨터가 수학 증명을 검증하는 데는 인공지능(AI) 기반의 기계 학습이 사용됐다. 우선 인류가 증명해 온 여러 명제의 증명 과정을 컴퓨터가 이해할 수 있는 언어로 번역해 학습을 시킨다. 이 과정에서 컴퓨터는 수학자들이 통상적으로 어떤 주장을 증명하기 위해 어떤 기술을 어느 상황에 적용시키는지를 배운다.

이처럼 학습된 컴퓨터를 새로운 증명에 적용할 경우 증명 과정에 기술이 적절하게 사용됐는지 판단할 수 있다. 나아가서는 특정 명제를 증명하는 데 더 나은 방법을 제시하거나, 더 일반적으로 사용돼 온 방법을 제시할 수도 있을 것으로 전망된다.

버자드는 이번 성과에 대해 내년 6월 세계 최대 수학 학회인 ICM(International Congress of Mathematics) 2022에서 기조연설자로 나설 예정이다. 이번 프로젝트를 통해 과거에 비해 컴퓨터를 수학 연구에 활용할 수 있는 범위가 넓어진 것은 맞는다. 과거 증명 검증 프로그램은 대학 학부생 수준의 수학 증명에 주로 활용됐다. 수학 교과서에도 가끔 실수가 있고, 증명 내용에서 일부를 빠뜨리는 경우도 있었는데 검증 프로그램은 이런 문제를 잡아내는 정도였다.

그러나 이번 성과가 수학 연구 방법에 혁신적인 변화로 이어지기 위해서는 시간이 더 필요할 것으로 보인다. 숄체 역시 "현재로서는 수학자로서 창의적인 작업을 하는 데 프로그램이 어떻게 도움이 될지 확신하기 어렵다"고 밝혔다.

이번 프로젝트의 의미에 대한 평가도 엇갈렸다. 김 교수는 "아직 역할은 제한적이지만, 이번 성과로 수학자들에게 기존에 없던 새로운 무기가 생겼다고 볼 수 있다"고 밝혔다. 이어 "컴퓨터를 통한 증명 검증은 학부생 수준의 수학 단계에서만 먹힌다고 생각돼 왔는데 그 이상 진지하게 생각할 여지가 생긴 것"이라고 설명했다.

반면 한 수학과 교수는 "마이너한 분야에 유명한 수학자가 관심을 가지니 덩달아 주목받는 것 같다"며 "큰 진전으로 볼 수 있을지는 회의적"이라는 입장을 밝혔다.

새로운 증명의 검증에 컴퓨터가 활용된 것은 처음이지만, 과거에도 컴퓨터의 계산 능력을 활용해 사람이 하지 못한 증명을 해낸 사례는 있었다. '4색 정리' 증명이 가장 유명하다. 지도를 여러 부분으로 나누고, 맞닿은 부분은 구분되게 서로 다른 색을 칠하려 한다면 4가지 색이면 충분하다는 내용이다.

문제가 처음 제안된 것은 1852년. 그러나 많은 수학자들이 증명에 어려움을 겪으며 4색 정리는 오랜 기간 난제로 남았다. 1976년 미국 수학자 케네스 아펠과 볼프강 하켄은 컴퓨터를 활용해 평면에 나타날 수 있는 모든 모양을 1936개로 단순화했고, 이 조합에 모두 일일이 색을 칠하는 방법으로 증명을 해냈다.

유명한 수학 난제 골드바흐의 추측과 관련해서도 컴퓨터를 사용한 사례가 있다. 골드바흐의 추측은 '2보다 큰 짝수는 두 소수의 합으로 나타낼 수 있다'는 명제다. 단순해 보이는 이 명제를 증명하기 위해 수많은 수학자가 뛰어들었으나 모두 실패했다.

여전히 증명은 이뤄지지 않았으나 컴퓨터의 계산 능력을 활용해 거대한 수까지 골드바흐의 추측이 모두 들어맞는다는 것은 확인됐다. 1993년 수학자 마티 K 시니살로는 학회지 'Mathematics of Computation'에 컴퓨터를 사용해 골드바흐의 추측에 반례가 되는 수가 있는지를 계산했고, 4부터 4000억까지는 명제가 성립한다는 내용을 발표했다. 그는 논문에서 "이번 프로젝트에 총 170시간의 계산 시간이 사용됐다"고 설명했다.

[정희영 기자]

[ⓒ 매일경제 & mk.co.kr, 무단전재 및 재배포 금지]