OpenAI는 이번 주 자사 모델이 고급 문제를 다룰 수 있는 능력을 보여주기 위해 어려운 수학 문제에 대한 수백 개의 해법을 공개했다. 그러나 이번 공개는 수학 연구자들로 구성된 자문 그룹이 마련한 지침을 완전히 준수하지 않았으며, 근본적인 질문을 다시 제기했다. 모델이 소프트웨어로 형식화할 수 있는 해법을 만들어내는 것만으로 충분한가, 아니면 수학자들이 이해하고 검토할 수 있어야 하는가?
Advisory Group on Mathematics and Artificial Intelligence (AGMAI)는 저명한 연구자 9명으로 구성되어 있으며, 프린스턴대학교 고등연구소가 주최한다. 이 그룹은 9월 말 수학 문제 해결을 위한 고급 모델을 개발하는 연구소들을 대상으로 지침을 발표했다.
연구자 지침을 부분적으로 준수
AGMAI는 권고 사항의 준수 정도를 평가하는 일은 궁극적으로 수학계에 달려 있다고 밝혔다. 주요 권고 중 하나는 상업적으로 소유된 모델을 대상으로 고급 수학 문제를 시험하는 것을 중단하라는 것이었다. 반면 OpenAI는 자사 모델을 평가하기 위해 공개된 연구 문제를 사용한다고 명시적으로 밝혔다.
OpenAI는 결과를 신속하게 공개하고 모델이 어떻게 결론에 도달했는지에 대한 정보를 제공하는 등 일부 원칙을 따랐다. 그러나 719개 원고 중 단 10개만 모델의 사고 과정을 포함했다. 또한 공개된 증명의 42%는 형식화되지 않았다.
이 그룹은 인간이 이해하기 어려운 증명은 공식 형식으로 변환해야 한다고 본다. 그러나 연구소가 결과 공개에 인간의 이해가 뒤따르도록 보장할 책임도 강조했으며, 이러한 결과가 실제로 과학적 의미를 갖도록 돕는 수학자들에게 자금을 지원할 것을 제안했다.
자연어와 Lean 코드 사이의 간극
모델은 일반적으로 먼저 자연어로 설명을 작성한 다음 이를 Lean으로 변환하려고 한다. Lean은 컴파일러가 실행 가능한 형식으로 증명의 일관성을 확인할 수 있는 프로그래밍 언어다. 그러나 자동 변환은 증명의 내용을 바꾸거나 설명이 말하는 것과 코드가 증명하는 것 사이에 단절을 만들 수 있다.
케임브리지대학교와 킹스 칼리지 런던의 수학자들이 발표한 논문은 OpenAI가 복잡한 유체의 거동에 관한 Navier-Stokes 방정식에서 파생된 문제에 대해 제시한 해법과 관련해, 자연어 증명과 연결된 Lean 코드 사이에서 최소 두 가지 차이를 기록했다. 이러한 차이가 두 해법 중 어느 하나가 반드시 틀렸다는 것을 입증하는 것은 아니지만, 인간의 개입 없이 모델이 자신의 해법을 공식적으로 작성하도록 맡기는 것에 대한 의문을 불러일으킨다.
AGMAI는 또한 텍스트 증명과 공식 버전을 연결하는 기계 판독 가능한 메타데이터를 포함할 것을 요청했지만, OpenAI는 이번 공개에서 이를 제공하지 않았다. “lost in translation”으로 알려진 이 논문의 저자들은 텍스트 증명과 자동 변환된 Lean 증명을 다른 증명과 동일한 수준의 동료 심사와 검토 없이 원칙적으로 받아들여서는 안 된다고 결론 내렸다.
이 소식이 중요한 이유
문제는 코드가 성공적으로 컴파일된다는 사실을 입증하는 데만 있는 것이 아니라, 코드가 실제로 텍스트가 설명하는 수학적 아이디어를 나타낸다는 점을 입증하는 데 있다. 전통적인 연구에서는 과학자들이 자신의 결과에 대한 책임을 지고, 논문과 강의 및 세미나를 통해 이를 논의한다. 이러한 과정은 오류를 발견하고 재사용 가능한 방법을 이해하는 데 도움을 준다.
반면 모델이 어려운 문제에 대한 해법을 만들어낼 때는 공개 시점에 이러한 인간의 이해가 존재하지 않을 수 있다. 따라서 현재 OpenAI의 결과는 문제의 끝이라기보다 과학적 검증 과정의 시작에 가까워 보인다. 이러한 증명을 수학계 내부에서 채택하기에 앞서 인간의 검토와 텍스트 및 공식 출력물 간의 연결은 여전히 충족되어야 할 두 가지 조건으로 남아 있다.