AI가 만든 나비에-스토크스 증명, '무엇이 검증됐는지'까지 기록하는 데이터베이스 실험

OpenAI가 9월 8일 나비에-스토크스 방정식의 유한시간 붕괴(finite-time breakdown)에 대한 AI 생성 증명과 이를 Lean으로 형식화한 결과를 함께 공개했다. 구성은 정지 상태의 유체에서 출발해 매끄러운 힘을 가하는 방식이며, 밀레니엄 문제의 '강제된(forced)' 변형을 다룬다. 8Braid는 이 공개물을 자사 데이터 시스템 8DB의 연구 워크로드를 시험하는 문제로 삼았다. 공개된 형식 검사를 재현하고, 한 대수 단계에 대해 명시적인 오차 허용 범위를 유도한 뒤, 그 결과가 데이터베이스를 거치면서 조용히 더 강한 주장으로 바뀌지 않는지 확인하는 것이 목표였다.

검증 절차부터 구체적이다. Comparator가 제출된 C/D 결과를 기대되는 형식 명제와 대조했고, Nanoda 커널과 Lean 기본 커널 양쪽이 해를 받아들였다. 기록된 공리 보고서에는 Lean의 표준 공리 세 개가 들어 있었다. 이 과정에서 소스 리비전, 의존성 핀, 검사기 신원, 실행 명령, 실제 결과가 모두 보존됐다. 이 검사들이 확립하는 것은 정확히 '형식 증명이 인코딩된 명제에 대해 승인됐다'는 사실이다. 명제가 물리적 문제와 어떻게 대응하는지 읽어내는 일, 그리고 그 결과를 새로운 상황에 적용하는 일은 별개의 작업으로 남는다.

8Braid가 파고든 지점은 Proposition 7.5다. 이 단계는 양의 공분산 분해를 사용하며, 두 기여분을 결합하는 가중치가 양수로 유지되어야 한다. 따라서 입력이 어느 정도까지 흔들려도 양수성이 깨지지 않는지에 대한 여유가 필요하다. 연구팀은 해당 단계의 정규화 좌표에서 충분 허용량을 유도하고 Lean으로 증명했다. 목표가 마진 m(0 < m < 1)을 가진 허용 원뿔 안에 머무르면, 네 개의 행렬 원소 각각에 m/4 이하의 오차가 있어도 양의 보정 가중치가 유지되고 행렬식은 최소 7/8로 남는다. 분수는 정확한 값이며, 결과는 샘플링한 점들이 아니라 명시된 실수 매개변수 영역 전체에서 성립한다. 별도의 Python 검사가 유리수 대수를 재구성하고, 독립된 Lean 증명이 일반 함의를 확인한다.

이 결과의 성격은 분명히 해둘 필요가 있다. 전체 구성에 적용하려면 원문이 제시한 해석적 오차 봉투(analytic error envelope)와 프로파일 경계가 여전히 필요하다. 원래 논증에 결함이 있었던 것은 아니고, 충분히 작은 상수를 추상적으로 남겨둔 것이다. 8Braid가 내놓은 것은 가정을 함께 붙인 명시적 조건부 경계다.

흥미로운 대목은 증거 철회 실험이다. 연구팀은 이 조건부 결과를 별도의 네이티브 8DB 연구 워크로드에 넣고, 보조정리의 가용성과 그것을 적용하는 데 필요한 의무(obligation)를 함께 추적했다. 그런 다음 이를 뒷받침하던 승인을 철회하고 저장된 상태를 다시 읽었다. 조건부 공분산 보조정리는 선언된 범위에서는 더 이상 '사용 가능'으로 지원되지 않았고, 실제 소스 구성에의 적용은 별도 의무가 미승인 상태로 그대로 남았으며, 무관한 과거 결과들은 기존 지원을 유지했다. 철회는 사용 가능한 지원의 기록을 바꿀 뿐 수학적 함의 자체를 거짓으로 만들지 않는다. 이 테스트는 네이티브 소비자와 별도 리더, 그리고 새 로컬 디렉터리에서의 재실행까지 통과했다.

배경에는 AI 에이전트가 제안한 결과를 연구 기록에 편입하기 전에 검사기를 세우자는 문제의식이 있다. 실행 중 검증(verification during execution)이라고 부를 만한 접근으로, 다항식 계수가 바뀌면 정확 항등식 검사가 실패하고, 잘못된 컨텍스트에서 온 아티팩트는 적용 가능성 검사에서 걸리며, 지원이 빠진 추론은 미승인 상태로 남는다. 에이전트는 다음 단계를 수정할 구체적인 이유를 얻게 된다. 다만 테스트 가능한 오류와 적절한 테스트 자체가 없는 주장은 구분되어야 하며, 후자는 여전히 사람의 판단이나 새로운 수학을 요구한다.

8Braid가 그리는 그림은 그래프, 벡터, 테이블, 시계열, 수학적 객체가 동일성과 출처, 거버넌스를 공유하는 데이터 시스템이다. 관찰에서 공식으로, 공식에서 테스트로, 테스트에서 그것이 뒷받침하는 결론으로 이동할 수 있어야 한다는 발상이다. 자사의 검증 열역학 진실 엔진(VTTE)이 제공하는 구간 기반 수치 도구로 이 정확한 부등식에 경계가 있는 입력을 공급할 수 있고, Sheaf 기법으로 합의 여부를 검사할 수 있다는 연결도 언급된다. 물리학이 이 필요를 가장 날카롭게 드러내지만, AI가 설계를 제안하거나 실험을 해석하고 엔지니어링 계획을 돕는 모든 상황에서 같은 핸드오프 문제가 나타난다.

주의할 전제도 원문이 직접 밝히고 있다. 이번 소비자는 고정된 Taylor-Green 연구 컨텍스트를 사용했고, OpenAI의 전체 구성을 수집하지도 않았으며 새로운 8DB 컨텍스트로 PDE를 독립적으로 인증하지도 않았다. 수학적 검사와 데이터베이스 증거 검사는 책임 범위가 다르다. 또한 엔드투엔드 에이전트의 오류율 감소나 프로덕션 수준의 지연 보장은 아직 측정되지 않았고, 이는 앞으로의 평가 대상으로 남아 있다.