OpenAI의 네이비어-스톡스 증명, 처음 알려진 접근과 달랐다

OpenAI의 Navier-Stokes 증명은 스페인 수학자들의 접근법을 그대로 따른 결과가 아니라, 세부 구조가 다른 방법을 사용한 것으로 전문가들이 파악하고 있습니다. 다만 대규모 LLM이 만든 Lean 증명과 논문 설명의 차이, 모델의 추론 경로를 확인하기 어려운 점은 남아 있습니다.

주제: AI 수학 개발 도구

에디터 노트

현재 가장 분명한 판단은 최종 증명의 수학적 접근이 스페인 프로그램과 다르다는 점입니다. 여러 연구 그룹의 분석이 그 차이를 뒷받침하지만, 이것만으로 초기 중간 결과의 영향이나 모델이 어떤 자료를 접했는지까지 밝혀지지는 않습니다. 댓글에서도 Lean이 검사한 형식 명제의 타당성과 그 명제가 의도한 문제를 표현하는지, 자연어 논문이 형식 증명을 제대로 설명하는지를 구분하자는 의견이 나옵니다. 이 구분은 증명의 검증과 이해를 같은 문제로 취급하지 않게 해줍니다. 논문과 Lean 증명의 불일치가 어느 부분에서 발생하는지, 그 차이가 결과의 해석에 어떤 영향을 주는지는 아직 남은 쟁점입니다.

AI 요약

OpenAI가 공개한 166쪽짜리 Navier-Stokes 증명은 처음에는 스페인 수학자 Diego Córdoba와 Luis Martínez-Zoroa가 제시한 접근법을 따른 결과로 알려졌습니다. 이 설명은 해당 접근법을 LLM으로 연구하던 Tristan Buckmaster와 Anthropic의 Levent Alpöge 사이에 공개 논쟁을 불렀습니다. 그러나 증명을 검토한 여러 수학자 그룹은 두 접근법의 유사성이 표면적이며, OpenAI의 최종 증명은 스페인 프로그램을 따르지 않는다는 쪽으로 판단하고 있습니다.

Navier-Stokes 방정식은 유체의 흐름을 기술합니다. Clay Mathematics Institute가 제시한 문제의 공식화에는 비현실적인 외력을 가해 유체 속도가 무한대로 발산하는 상황, 즉 blowup을 구성할 여지가 있습니다. OpenAI의 증명은 이런 외력을 이용합니다. 스페인 프로그램과 OpenAI의 방식은 이 허점을 활용한다는 점은 같지만, 외력을 만드는 방법은 다르다고 기사에 인용된 수학자들은 설명합니다.

10,000개 에이전트가 만든 증명

OpenAI는 수학 능력을 갖춘 LLM 복사본 약 10,000개를 에이전트 군집으로 운용해 증명을 구성했다고 밝혔습니다. 계산 시간은 약 88시간, 전체 토큰 사용량은 1,300억 개였습니다. 회사는 Buckmaster와 Alpöge의 큰 진전을 알게 된 뒤 수학 연구 자원을 투입했습니다. OpenAI는 모델이 Buckmaster의 자료를 보지 못했다고 주장했지만, 기사에 따르면 LLM의 블랙박스 특성 때문에 군집이 어떤 경로로 결론에 도달했는지는 확인하기 어렵습니다.

OpenAI는 초기에 더 작은 에이전트 팀으로 중간 결과를 증명했습니다. 일부 전문가는 이 단계가 스페인 프로그램을 따랐다고 봅니다. 하지만 최종 결과를 만든 대규모 군집은 완성에 다른 경로가 필요하다고 판단한 것으로 보입니다. 따라서 최종 증명의 접근법이 다르다는 사실만으로 스페인 프로그램이나 Buckmaster의 작업이 초기 과정에 영향을 주지 않았다고 단정할 수는 없습니다. 기사에서 Institute for Advanced Study의 Camillo De Lellis는 이 사안이 명확히 검증 가능한 수학적 사실만으로 결론 나기 어려워졌다고 말합니다.

Lean 검증과 사람이 읽을 수 있는 설명

에이전트는 논증을 Lean 코드로 작성했습니다. Lean은 형식화한 가정과 명제에 맞춰 증명의 논리 단계가 성립하는지 검사합니다. 하지만 코드가 검사기를 통과했다는 사실과 자연어 논문이 그 형식 증명을 정확히 설명한다는 사실은 별개의 문제입니다. 기사에 따르면 전문가들은 Lean 코드와 논문을 다른 LLM의 도움을 받아 분석하고 있지만, 증명의 전체 구조를 이해하는 데 시간이 걸리고 있습니다. 기사 작성 시점에도 누구도 증명을 완전히 이해하지 못했으며, OpenAI 역시 자사 모델이 만든 증명을 처음부터 이해하지 못했다고 기사는 짚습니다.

OpenAI는 지난주 추가로 약 400개의 결과를 공개했습니다. 기사에 따르면 그중 적어도 12개는 AI 이전 시대라면 수학자에게 필즈상 후보로 꼽힐 만한 결과였습니다. 그러나 이 평가는 결과의 검증과 이해가 끝났다는 뜻은 아닙니다. 기사에서는 연구자 수가 결과의 증가 속도를 따라가기 어렵다고 설명합니다.

Reddit 반응

@u/Cagnazzo82 — 그러면 다른 사람의 작업을 베꼈다는 이야기는 무너지고 있는 거네요. 우리가 이해한 게 그런 건가요?
- @u/Striking_Resist_6022 — 증명이 너무 빽빽하고 이해하기 어려워서 사람들이 틀렸다는 점이 처음부터 분명했던 건 아닙니다. 하지만 결정적 증거가 아니라 설득력 있는 이야기만으로 많은 사람이 입장을 굳힌 점은 분명했습니다. 결론이 맞았을 수도 있지만 지금 보니 확신이 지나쳤습니다.
@u/parbaner24 — 강제 Navier-Stokes 문제와 비강제 문제의 구분은 여기서 매우 중요합니다. 한 공식화에서 성립하는 결과가 수학자들이 관심을 둔 더 넓은 문제를 해결하지는 않을 수 있습니다.
@u/kittenTakeover — 사람들이 해법을 이해하기도 전에 왜 이게 올바른 해법이라고 그렇게 확신했는지 모르겠습니다. 그런 일이 어떻게 생기나요?
- @u/brownstormbrewin — Lean은 꽤 견고합니다. Lean으로 무언가를 증명했다면 대체로 타당합니다.
- @u/Anasynth — 하지만 그 '무언가'가 의도한 내용을 표현하는지는 어떤가요?
@u/Fast-Sir6476 — 요약하면 AI는 검증할 수 있는 수학·컴퓨터 언어인 Lean 증명과 자연어 증명을 만들었습니다. 자연어 증명은 Buckmaster의 작업에 기반한 것처럼 보였고, 그래서 큰 논란이 생겼습니다. 하지만 Lean 증명은 자연어 증명과 일치하지 않습니다. 현재 Lean 증명이 실제로 Navier-Stokes를 증명했는지 알 수 없습니다.
@u/Alchemistwiza — 논문에 적힌 주장과 Lean 명제를 하나씩 연결한 안내가 있으면 좋겠습니다. 그러면 결과가 검증됐는지와 수학자들이 논증을 이해하고 재사용할 수 있는지를 구분하기 쉽습니다. 새 전문가 분석은 스페인 프로그램 관련 주장에 답하지만, 결과의 출처에 관한 모든 질문까지 해결하지는 않습니다.
@u/404_Builds — 두 질문이 뒤섞이고 있다고 봅니다. 증명이 스페인 프로그램을 따랐는지, 형식화한 명제가 의도한 Navier-Stokes 결과인지 하는 질문입니다. 검사된 Lean 증명은 형식적 가정에서 논리가 전개되는 데 강한 신뢰를 줍니다. 그 가정이 논문과 일치하는지, 증명 전략을 설명하는지는 별도의 작업입니다.

원문: Scientific American / 번역·요약: Trawling

원문 보기 ↗토론 보기 ↗