d라이브러리

구글 연구팀이 수학 정리를 증명하는 인공지능 ‘HOList’를 만들어 화제입니다. 수학 정리를 증명하는 과정은 무척 복잡해서 인공지능이 하기 힘든 일 중 하나로 꼽혀왔습니다. 

연구팀은 미국 컴퓨터과학자 존 해리슨이 만든 증명 프로그램 ‘HOL Light’을 활용해 새로운 인공지능을 만들었습니다. 여기에 이미 수학자가 증명한 수학 정리 1만 개를 학습시키고, 수학적 귀납법처럼 수학자가 쓰는 증명 기술 41개도 학습시켰습니다. 그 뒤 입력하지 않은 수학 정리 3,225개를 증명하도록 했죠. 인공지능은 39% 정도인 1,253개의 정리를 정확하게 증명했습니다.

연구를 이끈 크리스찬 세게디 연구원은 “사람이 할 수 있는 증명을 전부 할 수 있게 만드는 게 목표”라며, “머지않아 실현 될 것”이라고 전했습니다. 

반면 인공지능으로 수학의 정리를 증명하는 것을 염려하는 의견도 있습니다. 제레미 아비가드 미국 카네기멜론대학교 철학과 교수는 “증명을 인공지능에게 맡기면 직접 증명하면서 새로운 개념을 찾거나 새로운 질문을 떠올리는 과정을 경험할 수 없다”고 말했습니다. 

정말 인공지능이 수학자처럼 증명하는 날이 올까요? 이번 연구 결과는 온라인 논문 게재 사이트 ‘아카이브(arXiv)’에 4월 5일 올라왔습니다.