AI가 어려운 문제를 풀었다는 소식은 대개 모델의 능력으로 곧장 읽힌다. 9월 8일 OpenAI가 공개한 Navier-Stokes 방정식 관련 결과는 조금 다르게 볼 필요가 있다. 이번에 눈여겨볼 부분은 정답 주장 자체보다, 수천 개의 에이전트가 만든 긴 작업 결과를 사람이 다시 확인할 수 있는 형태로 남겼다는 점이다.
OpenAI의 공개 GitHub 저장소에는 Navier-Stokes와 Euler 방정식의 유한 시간 특이점 결과를 Lean 4로 형식화한 코드가 담겼다. 저장소 설명에 따르면 Navier-Stokes 쪽은 양의 점성에서 매끄러운 초기 조건과 외력을 갖는 경우, 전 공간 또는 주기적 공간에서 전역적으로 매끄러운 해가 존재하지 않는 사례를 다룬다. 이는 Clay Mathematics Institute가 제시한 문제 설명의 대안 C와 D에 대응한다고 적혀 있다.
여기서 특이점은 해의 어떤 값이나 변화율이 유한 시간 안에 무한대로 커지는 상황을 가리킨다. Navier-Stokes 방정식은 물과 공기처럼 점성이 있는 유체의 흐름을 기술한다. Clay Mathematics Institute도 이 방정식의 해가 존재하고 유일한지에 관한 기본 질문에 아직 증명이 없다고 설명해 왔다. 그래서 이번 공개는 AI 뉴스라기보다, 길고 복잡한 추론을 어떻게 검토 대상으로 바꿀 것인가를 생각하게 하는 사례다.
Lean이 확인하는 것과 확인하지 않는 것
Lean은 수학 명제와 증명 단계를 컴퓨터가 검사할 수 있는 형식 언어다. 사람이 작성한 수식 문서에서는 중간 생략이나 기호 해석의 차이가 남을 수 있다. 반면 형식화된 증명은 정해진 규칙 안에서 각 단계가 이어지는지를 검사한다. OpenAI 저장소는 Lean 4.34.0-rc2, Mathlib, Lake를 사용하며, 독립적인 증명 점검을 위한 Comparator 안내도 제공한다.
하지만 Lean이 통과했다고 해서 사람이 던진 원래 질문 전체가 자동으로 끝나는 것은 아니다. 먼저 형식화된 정리의 가정과 결론이 Clay가 제시한 문제와 정확히 같은지 확인해야 한다. 코드에 들어간 정의가 수학 논문의 정의를 충실히 옮겼는지도 별도 검토 대상이다. 형식 검증은 이 연결고리를 대신 판단하지 않는다.
Quanta Magazine은 이번 결과가 Lean으로 형식 점검됐다고 보도하면서도, 사람의 검토는 Lean에서 증명한 명제가 수학자들이 풀려 한 명제와 논리적으로 같은지 확인하는 데 남는다고 짚었다. 또한 결과의 수학적 의미와 선행 연구의 기여, 우선권은 시간이 지나며 검토될 사안이라고 전했다. 이 구분은 업무 자동화에서도 그대로 유효하다. 시스템이 규칙을 만족했다는 기록과, 그 규칙이 업무 목적을 제대로 표현했다는 판단은 다른 일이다.
10,000개의 에이전트가 남긴 산출물은 무엇인가
Quanta의 보도에 따르면 OpenAI는 공개되지 않은 내부 모델 위에서 약 10,000개의 자율 에이전트를 투입했고, Navier-Stokes 결과를 찾는 데 88시간이 걸렸다고 밝혔다. 이후 다른 AI 모델이 17시간 동안 Lean 형식화와 검증을 수행했다. 이 수치는 특정 업무에 그대로 옮길 성능 지표는 아니다. 거대한 병렬 계산, 연구자 감독, 매우 좁은 목표가 함께 있었기 때문이다.
그래도 작업 흐름은 참고할 만하다. 에이전트가 낸 초안이나 중간 아이디어를 최종 결과로 취급하지 않고, 다음 단계가 읽을 수 있는 명세와 검증 가능한 산출물로 바꿨다. 일반적인 개발팀이라면 Lean 같은 정리 증명기를 바로 도입하기보다 테스트, 스키마 검증, 재현 가능한 빌드, 변경 이력 같은 형태로 같은 원칙을 적용할 수 있다.
특히 여러 에이전트를 병렬로 돌릴 때는 메시지 수가 많다는 사실만으로 신뢰가 생기지 않는다. 어떤 가정을 공유했는지, 서로 다른 답안이 어디에서 합쳐졌는지, 최종 산출물을 누가 어떤 도구로 재검사했는지가 남아야 한다. 이번 사례의 가치도 10,000이라는 숫자보다 공개 저장소와 재실행 절차에 있다.
AX 실험에 옮길 때의 작은 기준
수학 연구 규모의 시스템을 만들 필요는 없다. 반복적인 AI 업무 하나를 고르고, 결과보다 검증 경로부터 작게 설계해 보면 된다.
- 검증할 문장을 먼저 쓴다. 예를 들어 계약서 요약이라면 “모든 금액과 날짜는 원문 위치와 함께 제시된다”처럼 판정 가능한 조건을 정한다. “좋은 요약”처럼 해석이 넓은 목표만 두지 않는다.
- 중간 산출물을 분리해 저장한다. 원문 추출, 구조화된 데이터, 초안, 검토 결과를 한 파일에 섞지 않는다. 어느 단계에서 오류가 생겼는지 다시 확인할 수 있어야 한다.
- 자동 검증의 경계를 공개한다. 형식 검사나 테스트가 통과한 항목과 사람이 맥락을 판단해야 하는 항목을 나눠 기록한다. 통과 결과를 품질 보증 전체로 부르지 않는 것이 중요하다.
아직 성급하게 결론 내릴 수 없는 부분
Navier-Stokes 결과가 Clay의 문제를 최종적으로 해결했는지는 OpenAI의 발표나 Lean 저장소만으로 확정할 수 없다. Clay의 공식 문제 페이지는 유체 흐름을 설명하는 방정식의 기본 성질을 밝히는 과제를 소개하지만, 이번 결과를 인정했다는 별도 발표는 확인하지 못했다. Quanta 역시 결과의 세부 의미와 선행 연구와의 관계를 더 살펴봐야 한다고 보도했다.
따라서 이 사례를 “AI가 사람 검토를 끝냈다”는 근거로 읽으면 안 된다. 오히려 반대에 가깝다. AI가 긴 추론을 만들 수 있게 될수록, 무엇을 기계적으로 확인했고 무엇을 전문가가 해석해야 하는지 더 선명하게 나눠야 한다. 실무에서 AI를 쓰는 사람에게 남는 질문도 같다. 결과가 그럴듯한가가 아니라, 다른 사람이 같은 입력과 기록을 보고 어디까지 재검사할 수 있는가를 확인해야 한다.
이번 공개는 그 질문에 완성된 답을 주지는 않는다. 다만 AI 결과를 검토 가능한 작업물로 바꾸는 방식이 모델 성능만큼 중요하다는 점은 분명히 보여 준다.