OpenAI의 Navier-Stokes 증명, 수학을 코드로 옮기다 오역
OpenAI mistranslated mathematics into code for its Navier-Stokes proof
OpenAI가 깜짝 발표한 Navier-Stokes 문제 해법에는 사람용 증명과 컴퓨터용 증명이 따로 있었는데, 두 버전이 서로 일치하지 않는다는 지적이 나왔다. 수학자들은 이 오류가 증명 자체의 오류나 문제 해결 실패를 뜻하는 것은 아니라고 선을 그으면서도, AI가 생성한 수학적 결과를 언제나 신뢰할 수 있는지에 의문을 제기한다.
이 모든 대규모 언어 모델 생성 증명에 대해 반드시 해야 할 일은 사람이 그것을 읽어야 한다는 것이며, 이는 수학자들에게 엄청난 추가 부담을 만든다.
- krackers
- jey
이 헤드라인은 완전히 틀렸습니다. 적절한 코딩 비유는 이렇습니다. 자연어 논문은 코딩하기 전의 "설계 문서"였고, 그걸 Lean4 증명으로 코딩하다 보니 특정 세부 사항이 약간 어긋나 있다는 걸 깨닫고[1], 기계 검증 가능한 증명으로서 코드를 작성하는 과정에서 수정했다는 겁니다. 여기 있는 대부분에게 아주 공감 가는 상황일 겁니다. 하지만 논문, 즉 "설계 문서"는 나중에 수정되지 않았습니다.
저는 또한 이 "논문 먼저, 코드 나중" 접근 방식이 이제는 구식이라고 생각합니다. AI 지원 워크플로에서 현대적인 방식은 먼저 "유도 스케치 <-> 기계 검증 가능한 증명"을 반복하면서 결과를 점진적으로 구축하는 것입니다. 물론 중간에 `sorry` 자리 표시자를 남겨두고 나중에 채울 수 있으니, 완전히 상향식으로만 진행해야 하는 제약은 없습니다. 마지막으로, 관심 있는 최상위 진술(정리)에 대한 `sorry` 없는 증명을 얻고 나면, Lean 코드를 바탕으로 LaTeX로 설명을 작성하는 작업을 할 수 있습니다.
1. 자세한 내용은 https://arxiv.org/abs/2610.08144 를 보세요. 그들이 지적한 예로는 핵심 한계(bound)에 5개의 추가 도함수 차수가 필요했고(Lean에서도 그렇게 명시됨), 논문은 그 한계가 4개의 추가 도함수만으로도 성립한다고 주장했다는 점입니다.