AI 수학 증명 진전, 호스킨슨 “예상 못했다”

본문

인공지능이 복잡한 수학 증명을 작성하고 형식 검증까지 수행하는 수준에 이르렀다는 평가가 나왔다. 오픈AI의 나비에–스토크스 방정식 관련 발표를 계기로 AI의 수학 추론 능력이 다시 주목받고 있다.찰스 호스킨슨(Charles Hoskinson)... 오픈AI의 나비에–스토크스 방정식 관련 발표를 계기로 인공지능의 수학 증명 능력이 주목받고 있다. 찰스 호스킨슨(Charles Hoskinson) 카르다노 창립자는 9일 공개된 방송에서 “AI가 이렇게까지 발전할 것이라고 예상하지 못했다”고 말했다. 그는 과거 AI가 수학자들의 협업을 돕는 역할에 머물 것으로 봤지만, 대규모언어모델(LLM)이 직접 증명을 작성하는 단계까지 나아갔다고 평가했다. 오픈AI는 내부 AI 시스템이 3차원 유체 흐름에서 유한 시간 안에 특이점이 발생할 수 있다는 증명을 제안했으며, 이를 린(Lean)으로 형식화했다고 밝혔다.

이 문제를 해결하면 100만달러(약 13억4100만원)의 상금이 걸려 있다.

형식 검증은 수학 명제와 증명 과정을 컴퓨터가 확인할 수 있는 언어로 바꿔 오류 여부를 점검하는 방식이다. 린은 수학 증명을 컴퓨터로 검증하는 증명 보조 시스템으로, AI가 제시한 결과를 사람이 다시 검토할 수 있는 형식으로 남긴다는 데 의미가 있다. 오픈AI는 연구자들의 특정 사용자 데이터가 문제 해결에 사용되지는 않았다고 밝혔지만, 익명화된 이용 데이터가 모델 개선에 간접적으로 활용됐을 가능성은 배제할 수 없다고 설명했다. 따라서 현재 논쟁은 실제 데이터 유출 사실보다 연구자가 AI 서비스에 어떤 자료를 입력하고 그 기록을 누가 통제하는지가 핵심으로 떠오른 상황에 가깝다. 카네기멜런대학교는 2021년 그의 2000만달러(약 268억2000만원) 기부로 형식수학 연구센터를 설립했으며, 이 센터는 린과 같은 증명 보조 도구를 활용해 수학 증명의 검증과 자동화를 연구한다.