OpenAI의 수학 문제 풀이 공개, 수학계가 요구한 기준에는 못 미쳐

OpenAI가 세계에서 가장 어려운 수학 문제들에 대한 수백 건의 풀이를 한꺼번에 공개했지만, 수학계가 프런티어 연구소를 위해 마련한 기준에는 아직 도달하지 못했다는 평가가 나왔다. 쟁점의 중심에는 모델이 내놓은 결과를 사람이 실제로 이해할 수 있느냐는 문제가 있다.

이번 공개에는 719편의 원고가 포함됐다. 이 가운데 모델이 어떤 사고 과정을 거쳐 결론에 이르렀는지 보여주는 사고 연쇄(chain of thought)를 함께 내놓은 것은 10편에 그쳤다. 증명을 기계가 검증할 수 있는 형태로 형식화하는 작업도 충분히 이뤄지지 않아, 42%는 이 과정을 거치지 않은 것으로 나타났다.

프린스턴 고등연구소가 운영하는 수학·인공지능 자문그룹(AGMAI)은 세계 각지 기관 소속 저명 연구자 9명으로 구성돼 있다. 이 그룹은 9월 말 프런티어 연구소가 수학 문제를 다룰 때 따라야 할 지침을 내놨는데, 첫 번째 요청이 독점 모델에 고급 수학 문제를 테스트하지 말라는 것이었다. OpenAI는 이번 공개에서 독점 모델을 열린 연구 문제로 평가한다고 명시했다. 자연어 증명과 형식화된 산출물을 서로 연결하는 기계 판독 가능 메타데이터를 포함하라는 요청 역시 이번 릴리스에서는 이행되지 않았다.

배경에는 지난번 자사 모델이 오랜 난제를 풀었다고 발표하면서 벌어진 논란이 있다. OpenAI는 같은 실수를 반복하지 않기 위해 엘리트 수학자 자문단과 상의했다고 밝혔지만, AGMAI는 권고가 얼마나 잘 지켜졌는지를 판단하는 일은 결국 수학 커뮤니티의 몫이라고 선을 그었다.

케임브리지대와 킹스칼리지런던 수학자들이 이번 주 공개한 논문은 이 문제를 구체적으로 드러낸다. AI 모델은 수학 문제를 풀 때 먼저 자연어 설명을 만들고, 이를 증명 보조 언어인 Lean 코드로 옮겨 컴파일하는 방식으로 정확성을 확인한다. 그런데 OpenAI가 유체의 복잡한 거동을 기술하는 나비에-스토크스 방정식에서 파생된 문제에 제시한 풀이에서는 자연어 증명과 Lean 코드 사이에 최소 두 곳의 불일치가 발견됐다.

저명한 수학자 테렌스 타오는 소셜 미디어에서 이런 접근을 비판했다. 목표가 해결되는 순간 분야 자체에는 관심을 두지 않는 AI 프롬프터들이 문제를 자율적으로 풀어내고 있으며, 그 결과를 두고 질문에 답하거나 강연을 할 만큼 AI 산출물을 이해하지도 못한다는 취지였다. 하버드대 수학과 멜라니 우드 교수는 모델이 어려운 문제의 답을 내놓는 시점에는 그것을 이해하는 사람이 없고, 바로 그때부터 일이 시작되는 것이라고 말했다.

개발자에게 이 사건이 던지는 질문은 분명하다. LLM이 자연어로 만든 추론을 Lean 같은 형식 언어로 자동 변환하는 파이프라인을 그대로 믿을 수 있느냐는 것이다. 형식 검증이 통과됐다는 사실만으로 원래의 자연어 주장까지 검증됐다고 결론 내리면, 번역 과정에서 생긴 의미 차이를 놓칠 수 있다. 자동 형식화를 평가나 에이전트 검증 루프에 넣으려면 산출물 사이의 대응 관계를 기록하는 메타데이터와 사람의 교차 검토를 함께 설계해야 한다.

물론 논문이 짚은 불일치가 두 해법 가운데 하나를 반증하는 것은 아니다. 문제는 모델이 스스로 만든 풀이를 사람의 개입 없이 형식화한 결과를 어디까지 신뢰할 수 있는지다. AGMAI는 권고 준수 여부에 대한 최종 평가는 수학 커뮤니티가 할 일이라고 밝혔고, TechCrunch가 이번 증명 공개에 대한 더 자세한 평가를 요청했을 때는 답하지 않았다.