AI, 필즈상 프로젝트 증명 5일 만에 끝내… 머리 복잡해진 수학계

美 수학 AI ‘가우스’發 파장
인간 연구팀 2년 넘긴 증명 과제
AI는 5일 만에 형식화 작업 완료
현재 졸업 앞둔 박사과정생 실력… “인간, 증명하며 배울 기회 뺏겨”

미국의 AI 스타트업 ‘매스’는 필즈상 수상자 연구팀이 2년간 진행한 공개 형식화 프로젝트 협업을 진행하던 중 자체 개발한 AI ‘가우스’로 5일 만에 단독 형식화를 완성해 발표했다. 수학자들은 AI 발전 속도에 놀라움을 표하는 한편 여전히 사람 연구자에겐 증명 과정을 손수 따라가며 이해하는 시간이 필요하다고 강조했다. 게티이미지뱅크

수학계 노벨상으로 불리는 필즈상 수상자 연구팀이 2년 넘게 공개적으로 진행하던 수학 증명 형식화 프로젝트를 인공지능(AI)이 단 5일 만에 끝냈다. 수학자들은 AI 발전 속도에 놀라움을 감추지 않으면서도 ‘복잡한 속내’를 내비친다. 문제 해결보다 연구자들이 직접 증명을 따라가며 이해하고 수학 지식을 쌓는 과정 자체도 중요하기 때문이다.

형식화는 수학자가 쓴 증명을 컴퓨터가 한 줄씩 논리적으로 검증할 수 있는 코드로 바꾸는 작업이다. 논리적 오류나 누락된 가정을 잡아낼 수 있어 수학계에서 중요하게 여긴다.

● AI가 단번에 끝낸 형식화… “배울 기회 잃는 것”

올 2월 미국 AI 스타트업 ‘매스(Math Inc.)’의 시스템 ‘가우스(Gauss)’가 2022년 필즈상 수상자 마리나 뱌조우스카 스위스 로잔연방공과대(EPFL) 교수팀이 2년 넘게 진행하던 8차원 케플러 추측 증명 형식화 작업을 5일 만에 완료했다. 24차원 형식화도 2주 만에 끝냈다.

케플러 추측은 정해진 공간에 구를 가장 촘촘하게 쌓는 방법을 묻는 문제다. 뱌조우스카 교수는 이를 8차원과 24차원에서 풀어 필즈상을 받았다.

연구팀은 2024년 3월 코드와 작업 계획을 공개해 외부 수학자들도 참여할 수 있는 형식화 프로젝트를 시작했다. 형식화 과정에서 나온 정리와 개념을 공개 수학 라이브러리 ‘매스립(mathlib)’에 축적하고, 연구자들이 증명을 직접 이해하도록 하는 게 목적이다.

AI 사용도 허용했다. 매스 소속 연구자도 참여했고 AI가 생성한 일부 결과도 받아들였다. 다만 공개 협업을 통해 형식화 과정에서 필요한 정리와 개념을 함께 축적하는 방식을 추구했다.

지난해 가을 매스는 중간 결과 일부를 공유했지만 이후 진행 상황을 전혀 알리지 않았다. 그러던 올해 2월 매스가 가우스의 새로운 버전으로 5일 만에 전체 형식화를 완료했다고 발표했다.

연구팀에 속한 이시우 EPFL 박사후연구원은 가우스 결과가 “중요한 정리를 자동으로 형식화했다는 점에서 의미 있다”면서도 “코드 품질이 낮아 매스립 기준에 맞추려면 수정이 필요하다”고 밝혔다.

더 근본적인 아쉬움도 있다. 그는 “전체를 AI가 자동으로 완성하면서 사람이 직접 증명을 배우는 기회를 잃는 측면이 있다”며 “갑자기 형식화를 완료했다는 연락을 받아 기분이 좋지 않았고, 이런 과정이 알려지면서 매스가 수학자들 사이에서 비판을 받았다”고 전했다. 연구팀은 가우스와 별개로 자체 기준에 맞는 형식화를 올해 안에 마무리할 계획이다.

● “반년 새 딴 세상”… 수학계가 본 AI

수학자들이 체감하는 AI 발전 속도는 예상보다 훨씬 빠르다. 올 5월 오픈AI는 내부 추론 모델이 1946년 헝가리 수학자 에르되시 팔이 낸 ‘단위 거리 문제’의 특정 추측에서 반례를 찾아냈다고 발표했다. 에르되시는 평면에 점들을 배치할 때 같은 거리로 떨어진 쌍의 수가 아무리 배열을 바꿔도 일정 수준 이상 늘어날 수 없다고 추측했는데 AI가 이를 뒤집는 배열을 찾아낸 것이다. 에르되시가 상금까지 내걸었지만 80년간 풀리지 않았던 문제였다.

이규환 미국 코네티컷대 수학과 교수는 에르되시 문제 반례 발견을 “충격적인 사건”으로 꼽았다. 그는 “이산기하학과 수론을 연결해서 푼 건데 두 분야는 서로 매우 달라 둘 다 잘 아는 수학자도 드물다”며 “AI가 그 연관성을 찾아 문제를 해결했다는 게 놀랍다”고 설명했다.

이어 “6개월 전만 해도 AI가 박사과정 1∼2학년 학생을 데리고 일하는 것 같았는데 이제는 졸업을 앞둔 박사과정생 수준까지 올라왔다”며 머지않아 박사후연구원 수준까지 올라올 수 있다고 전망했다.

이승재 인천대 수학과 교수는 “증명의 오류를 잡아내거나 반례를 찾을 때 AI가 빠르다”고 밝혔다. 다만 “문제를 던져놓고 풀어줘 하는 식은 통하지 않는다”며 “질문을 쪼개 되짚어가며 써야 의미 있는 결과를 만들어낸다”고 강조했다.

이시우 박사후연구원은 “대부분의 수학자들이 AI가 논문으로 출판할 수 있는 수준의 결과를 금방 만들어낼 수 있다는 것을 인지하고 있다”며 “머지않은 미래에 모든 분야에서 전문가 수준의 연구를 할 것”으로 내다봤다. 다만 “학부생이나 대학원생처럼 수학 연구를 막 시작한 경우는 연구 실적보다 연구 능력을 기르는 것이 중요하기 때문에 꼭 필요한 경우가 아니면 최대한 스스로 먼저 하는 습관을 들여야 한다”고 강조했다.