[기획: AI 트렌드] OpenAI가 내놓은 수학 원고 722편, 형식화 파일에는 「unchecked」라고 적혀 있었다

GitHub에 올라온 AI 수학 원고 더미

10월 6일 OpenAI는 GitHub 저장소 openai/math로 AI가 쓴 수학 원고 722편을 공개했습니다. GitHub는 개발자들이 코드와 문서를 올려 함께 관리하는 사이트이고, 저장소는 그 안에서 한 프로젝트의 파일을 모아 둔 공간입니다. 원고에는 누구나 가져다 고쳐 다시 배포해도 되는 공개 라이선스인 Apache 라이선스가 붙었습니다. 다음 날 미국 방송사 Fox News는 이 공개를 OpenAI 내부 모델이 미해결 수학 문제 수백 건의 답을 찾았다는 소식으로 전했습니다.

원고 수가 곧 문제 수는 아닙니다. OpenAI는 원고 722편을 결과 묶음(family) 372개로 나눠 정리했습니다. 결과 묶음은 주된 결과 하나에 그것을 받치는 보조 논증과 같은 결론의 다른 증명까지 한데 묶은 단위입니다.

저장소 첫 화면의 안내 문서(README)에는 원고를 만든 과정이 적혀 있습니다. OpenAI는 평가 과정에서 모델에게 약 4,000문제를 냈고, 결과 하나에 평균 약 3시간의 ChatGPT Pro급 추론 연산을 썼습니다. 추론 연산은 모델이 답을 내기 전에 여러 단계를 밟아 생각하는 데 드는 계산입니다.

이렇게 나온 산출물을 결과 묶음과 원고로 정리한 뒤, OpenAI는 「유의성 문턱」을 적용해 지금의 목록을 만들었습니다. 중요하다고 볼 결과만 남기는 기준인데, 그 기준이 무엇인지는 README에 자세히 나와 있지 않습니다.

보도에 따르면 OpenAI는 8월에도 수학 원고와 증명 파일을 공개했고, 9월에는 유체의 움직임을 다루는 나비에–스토크스 방정식에 관한 증명을 얻었다고 주장했습니다.

OpenAI가 README에 직접 적은 단서

OpenAI는 README에 「결과마다 검증 단계가 다르다」고 적었습니다. 그 단계를 가르는 기준 하나가 형식 검증입니다.

형식 검증은 증명의 모든 추론 단계를 컴퓨터가 규칙대로 확인할 수 있는 언어로 다시 써서, 프로그램에게 검사를 맡기는 일입니다. 비유하자면 풀이의 모든 단계를 규칙집과 하나하나 대조하는 채점기입니다. 이 저장소에서 쓰는 언어는 Lean이고, 증명을 Lean으로 옮겨 적는 작업을 형식화라고 부릅니다.

OpenAI는 형식 검증을 거치지 않은 일부 결과에는 문제가 있을 수 있다고 적었습니다. 형식화를 거친 원고는 「많지만 전부는 아니다(many but not all)」라고만 밝혔고, 개수는 적지 않았습니다.

저장소에는 형식화 진행 상황을 정리한 파일도 있습니다. 이 파일의 형식화 범위 항목에는 「Partial progress」(일부 진행), 검토 상태 항목에는 「unchecked」(확인 전)라고 적혀 있습니다. 어느 원고가 완전히 형식화됐는지 짝지어 놓은 대응표는 이 파일에 없습니다.

같은 파일의 자동화 방식 항목은 「agent」입니다. 에이전트는 여러 단계의 작업을 이어서 처리하는 AI 프로그램입니다. 형식화 작업을 이런 프로그램으로 자동화했다는 표기입니다.

모델의 추론 과정을 줄여 적은 요약은 결과 묶음 372개 가운데 10개에만 붙어 있습니다. 원고를 쓴 모델은 이름을 밝히지 않은 비공개 내부 모델이어서, 밖에서 같은 과정을 다시 돌려 확인할 수도 없습니다.

OpenAI는 오류가 나오면 고쳐서 새 버전으로 남기고 이전 버전도 보존하겠다고 적었습니다. 먼저 내놓고 고쳐 가며 배포하는 소프트웨어의 공개 방식입니다.

수학자들도 학술지 심사 전에 원고를 arXiv 같은 프리프린트 서버에 먼저 올리곤 합니다. 프리프린트는 심사를 거치기 전에 공개한 원고이고, arXiv는 올라온 원고를 거르기만 할 뿐 내용을 심사하지 않습니다. 학술지 논문은 실리기 전에 같은 분야 전문가가 내용을 따져 보는 동료 심사를 거치는데, 이것도 전문가의 판단이지 모든 단계를 기계처럼 대조하는 검사는 아닙니다.

그러니 공개 뒤에 검사가 시작되는 것 자체는 새롭지 않습니다. 다른 점은 사람이 쓴 프리프린트에는 원고마다 그 결과를 책임지는 저자가 있다는 것입니다. 이번 원고 722편은 이름 없는 모델이 썼고 한꺼번에 나왔습니다. 고친 기록을 지우지 않겠다는 약속은 정직한 공개 방식이지만, 검사를 맡길 곳으로 OpenAI가 적은 커뮤니티 관리 저장소는 아직 「검토 중」입니다.

Lean 검증을 거친 결과에도 사람의 검사가 남는다

한 외부 개발자는 공개 시점의 저장소 내용을 직접 세어 그 집계를 GitHub에 올렸습니다. 이 집계에서 결과 묶음 372개 가운데 Lean 페이지가 있는 것은 235개, 원고만 있는 것은 137개였습니다. 이 숫자는 OpenAI의 발표가 아니라 바깥에서 저장소를 세어 본 집계입니다. 또 Lean 페이지가 있는지를 센 것이지, 묶음의 증명 전체가 형식화됐는지를 가린 것은 아닙니다.

이 외부 집계대로라면 분야별 차이도 큽니다. 논리와 조합론은 거의 모든 묶음에 Lean 페이지가 있었지만, 위상수학과 대수·복소기하는 일부에만 있었습니다. 한 사람이 센 집계이고, 이 차이가 분야의 성질 때문인지 작업 순서 같은 다른 이유 때문인지는 집계만으로 알 수 없습니다.

이 표는 이번 저장소의 작업 결과일 뿐, 어느 분야가 기계로 검사하기 어렵다는 증거는 아닙니다.

Lean 검사를 통과한 부분은 강한 보증입니다. 다만 형식화 파일의 자동화 방식이 「agent」였던 만큼, 무엇을 증명할지 옮겨 적는 일을 누가 했는지도 파일만으로는 알 수 없습니다. 그런데 채점기는 시험지에 적힌 문제를 기준으로 채점합니다. 형식화는 「무엇을 증명하는가」를 Lean으로 적는 데서 시작하고, 이 문장을 진술이라고 부릅니다. 진술을 원래 문제와 다르게 옮겨 적으면 엉뚱한 문제를 맞게 푼 증명도 검사를 통과합니다. 그래서 진술이 원래 문제를 제대로 옮겼는지는 사람이 읽어서 확인해야 합니다.

같은 외부 집계는 Lean 진술 파일 405개의 길이도 셌습니다. 진술 파일은 진술과 그에 필요한 정의를 함께 적은 파일입니다. 길이의 중앙값은 57줄이었습니다. 중앙값은 길이순으로 줄 세웠을 때 한가운데 오는 값입니다. 가장 긴 파일은 중앙값의 300배가 넘는 17,384줄이었습니다. 앞서 본 형식화 파일의 검토 상태 항목도 「unchecked」입니다. 이 항목이 정확히 무엇을 확인하는지는 파일에 정의돼 있지 않습니다. 그래도 Lean 검증을 거친 결과에는 진술 확인이라는 사람의 검사가 남아 있고, 거치지 않은 결과는 처음부터 사람의 검사에 달려 있습니다.

「틀렸다」가 아니라 「이렇게 내놓는 게 맞나」

공개 당일 OpenAI의 수학 자문단 AGMAI는 자문 역할이 곧 승인은 아니라는 취지로 반응했습니다. 출간은 사람들이 이해하고 수학계가 평가하는 과정의 시작이지 끝이 아니라는 취지도 함께 밝혔습니다.

보도에 따르면 AGMAI는 9월 미국 프린스턴 고등연구소를 근거지로 출범했고, Gowers·Hairer·Witten 등이 초기 위원입니다. 출범 당시 OpenAI는 속도 조절은 자문 범위가 아니라고 밝혔습니다.

미국 과학 잡지 Scientific American의 보도를 전한 요약에 따르면, 수학계에서는 공개 방식에 대한 비판이 나왔습니다. 8월 한 회의에서 합의된 출판 규범을 무시하고 대량으로 공개했다는 비판입니다. 우리가 검색한 범위에서는 주요 결과를 외부 수학자가 확인했다는 소식도, 내용 오류를 짚은 보도도 아직 없었습니다.

보도에 따르면 이번 공개보다 앞선 9월에는 필즈상 수상자 등이 공동 성명 「A Severe Misalignment of AI in Mathematics」를 냈고, Terence Tao도 서명했습니다. 필즈상은 수학계에서 가장 권위 있는 상으로 꼽힙니다. 성명은 OpenAI를 지목하지 않았고, 증명이 틀렸다고 주장하지도 않았습니다. 문제 삼은 것은 검증·귀속·공개 절차에 관한 규범이었습니다. 귀속은 결과를 누구의 업적으로 적느냐의 문제입니다. 지금까지 우리가 찾은 비판의 쟁점은 결과의 옳고 그름이 아니라 공개 방식이었습니다.

이 원고 더미에서 앞으로 확인할 것은 이렇습니다.

• 형식화 대응표. 어느 원고의 결과가 Lean으로 완전히 옮겨졌는지 짝지은 표가 나오는지 봅니다. 지금의 형식화 파일에는 이 표가 없습니다.
• 결과별 외부 확인. 외부 수학자가 개별 결과를 읽고 확인하거나 반박한 기록이 나오는지 봅니다.
• 수정 이력. 약속대로 오류를 고친 새 버전과 이전 버전이 함께 남는지 봅니다.

병목은 전체 진행 속도를 묶는 가장 느린 단계를 말합니다. 만드는 쪽은 결과마다 평균 약 3시간이라는 연산 규모까지 적어 두었지만, 검사하는 쪽은 맡길 곳조차 아직 「검토 중」입니다. 그래서 우리는 이번 공개에서 막혀 있는 단계가 증명을 만드는 일보다 검사하는 일이라고 봅니다. 사람이 받아 든 것은 풀린 난제의 목록이 아니라, 우리가 찾은 범위에서는 외부 수학자의 확인이 아직 나오지 않은 원고 722편입니다. 지금 저장소에 쌓여 있는 것은 검사 대기열입니다. 다음에 「AI가 미해결 문제 수백 건의 답을 찾았다」는 제목을 만나면, 그 결과가 어디까지 확인됐는지부터 보면 됩니다.