수학 난제 푸는 AI가 걱정스러운 이유 [오철우의 과학풍경]

지난달 오픈에이아이는 인공지능 모델이 도출한 수백건의 난제 풀이 결과를 무려 700편 넘는 연구 원고로 공개해 수학계를 당혹과 충격에 빠뜨렸다. 인공지능 기업의 잇따른 난제 해결 발표를 두고서, 수학자들은 수학 개념의 이해와 통찰 없이 이뤄지는 난제 풀이 속도 경쟁이 오히려 학문의 핵심을 훼손할 수 있다고 우려한다. 픽사베이

오철우 | 한밭대 강사(과학기술학)

수학의 노벨상이라 불리는 필즈상 수상자 25명이 지난 9월11일 긴급 공동성명을 발표해 언론의 주목을 받았다. 사흘 전 오픈에이아이가 이른바 ‘나비에-스토크스 방정식’과 관련한 묵은 수학 난제를 인공지능으로 풀었다고 밝힌 직후였다. 수학자들은 인공지능이 수학 연구에 기여하지만, 인간의 이해 속도를 추월하는 난제 풀이 속도 경쟁은 개념 이해와 통찰이라는 학문의 핵심을 훼손할 것이라며 우려했다. 우려는 멈추지 않고 오히려 커졌다. 지난달 6일 오픈에이아이는 수백건의 난제 풀이를 700편 넘는 원고로 공개해 수학계를 당혹과 충격에 빠뜨렸다.

난제를 푼다면 환영할 일인데도 수학자들이 왜 우려하는지를 처음엔 충분히 이해하기 어려웠다. 직업적 이해관계 때문인가 하는 생각마저 들었다. 하지만 찬찬히 들여다볼수록, 우려는 수학만의 문제가 아니며 지식 전반, 나아가 우리 사회와 맞닿아 있다는 생각이 든다.

필즈상 수상자인 테런스 타오 교수는 인공지능에 호의적인 편이지만 난제 풀이 경쟁이 결국 ‘증명의 소화불량’을 초래할 것이라고 경고한다. 검증을 거쳐야 하는 수학 증명이 인간의 이해 속도를 추월해 쏟아진다면, 논리와 의미도 다 이해되지 못한 채 수학은 소화불량에 빠지게 된다. 수학에 국한된 문제가 아니다. 다른 과학 분야에서도 연구 자동화로 미처 검증되지 않은 논문이 범람한다면, 과학뿐 아니라 사회 일반에 쓰이는 지식과 사실의 기준은 흔들릴 수 있다.

최근엔 증명 검증 방식에서도 우려가 제기된다. 수학계에서는 증명의 타당성을 보증하는 데 ‘린’(Lean)이라는 검증 프로그램을 널리 사용한다. 린은 논리 비약이나 오류가 없는지를 따져 증명의 논리 전개를 검사하는 일종의 컴퓨터 채점관이다. 수학 증명을 컴퓨터 프로그램이 다루는 형식논리 언어로 바꿔 작성한 다음 검사가 이뤄진다. 린 검증을 통과하면 증명의 논리 전개가 타당하다고 받아들여지기에, 오픈에이아이도 난제 풀이를 공개할 때 일부 결과들에 린 검증 자료를 첨부하기도 했다.

그런데 최근 린 검증이 충분히 믿을 만한지에 관한 의문이 새롭게 제기됐다. 실제로 오픈에이아이 인공지능이 검사용으로 작성한 형식 언어 원고가 실제 수학 증명 원고와 일부 일치하지 않는 문제가 사후 검증에서 밝혀졌다. 인공지능이 린 검증을 통과하는 데 유리한 방식으로 형식 언어를 작성했을 가능성이 제기된다. 또한 이와 별개로 유효하지 않은 증명이 린의 허점을 이용해 검증을 통과한 다른 사례도 보고됐다.

만일 금융, 에너지, 의료 같은 분야에서 난해한 수학에 기반해 짜인 시스템의 허점을 인공지능은 알지만 인간은 충분히 이해하지 못한다면, 그 약점은 인공지능을 통해 악용될 수 있고, 여러 피해가 현실 사회에 초래될 수도 있다.

인공지능의 능력 과시가 목적이 아니라면, 우리 세계를 위한 기술로서 인공지능은 인간의 이해 속도 안에서 통제되고 활용되어야 한다. 수학은 지금 다른 과학 분야와 우리 사회가 직면할 문제를 먼저 마주하는 중인지도 모른다. 그렇기에 수학자들의 우려에는 우리도 귀 기울여야 하는 목소리가 담겨 있다.