요약
오픈AI의 나비에–스토크스 증명은 Lean 검증을 통과했지만, Lean 증명이 자연어 증명을 그대로 옮긴 것은 아니라는 논문입니다.
안데르스 한센 등 연구자 세 명이 arXiv에 올린 논문입니다. 오픈AI가 발표한 나비에–스토크스 방정식 해의 폭발(유한 시간 안에 해가 무한대로 치솟는 현상) 증명을 사례로, AI 자동 형식화(자연어 증명을 Lean 같은 형식 언어로 옮기는 일)의 한계를 짚었습니다.
왜 중요한가
- Lean 컴파일 통과를 AI가 쓴 수학 글의 검증으로 여기는 흐름에 정면으로 문제를 제기합니다.
- 저자들은 Lean 증명이 틀렸다고 하지 않습니다. 사람이 읽는 자연어 증명은 아직 검증되지 않았다는 뜻입니다.
핵심 내용
- 오픈AI의 Lean 증명은 자연어 논문의 논증을 의미 그대로 옮긴 번역이 아니라고 결론지었습니다.
- 자연어 증명의 한 부등식은 m+4번 미분으로 충분하다고 했지만, 대응하는 Lean 명제는 m+5번을 요구해 더 약합니다.
- 압력 관련 상계도 Lean 쪽은 다른 항과 다른 기법을 써서 원래 식과 비교하기 어렵다고 했습니다.
- 성공 기준이 컴파일 통과뿐이면 AI는 원래 논증이 막힐 때 다른 증명으로 갈아탈 수 있다고 설명했습니다.
- 뜻이 바뀐 번역도 컴파일은 통과하므로, 자연어의 모호함을 해소하는 일은 정지 문제보다 어렵다고 주장했습니다.
HN 반응
- 여러 이용자는 논문이 Lean 증명의 타당성이 아니라 두 증명의 대응 관계를 문제 삼는다고 짚었고, 최종 명제의 형식화는 정확하다는 데 대체로 동의했습니다.
- AI가 엉성한 부분을 Lean에서 고쳐 쓴 '증명 리팩터링'일 수 있다는 해석과, 고친 내용을 자연어 글에 되돌려 반영하는 과정이 빠졌다는 지적이 함께 나왔습니다.
AI를 둘러싼 늘 보던 입씨름은 제쳐 두면, 이 글의 폭탄 같은 주장은 아래 대목인 듯합니다.
"특히 우리는 형식화된 Lean 증명이 나비에-스토크스 방정식 해의 폭발(blow-up)에 대한 자연어(NL) 증명과 대응하지 않음을 보인다."
그러니까 이 저자들은 오픈AI가 나비에-스토크스를 애초에 증명하지 못했다고 주장하는 것 같습니다. 제가 제대로 이해했다면, LLM이 원래의 "자연어" 아이디어를 제대로 형식화하지 못했다는 주장입니다. 사실이라면 오픈AI가 내놓은 Lean 증명은 나비에-스토크스의 증명이 아니라, 원래 자연어 아이디어를 잘못 옮긴 다른 무언가라는 뜻이 됩니다. 이게 맞다면 정말 대담한 주장이고, 다른 연구자들도 동의하는지 보고 싶습니다.
아니요, 그런 주장이 아닙니다.
나비에-스토크스의 Lean 형식화가 올바르다는 데 이의를 제기하는 사람은 없습니다. 그러니 생성된 Lean 증명이 유효하다고 높은 확신을 가져도 됩니다.
저자들의 주장은 Lean 증명이 자연어 증명과 같은 증명이 아니라는 것입니다. 따라서 자연어 증명이 유효하다는 확신은 아직 가질 수 없습니다.
수학계가 따져 봐야 할 중요한 주장인 것은 맞습니다. 하지만 오픈AI가 NS를 증명했다고 주장하려면 Lean 증명만으로 충분합니다(학계의 예의 문제는 접어 두고, 상당한 확신을 가지고 말할 수 있습니다).
그러니까 AI가 나비에-스토크스의 자연어 증명을 썼고, 그걸 Lean으로 자동 형식화하면서 잘못 옮겼는데도, 결과적으로는 검증 가능한 나비에-스토크스 증명이 나왔다는 거네요? 그건 좀... 이상하지 않나요?
한두 달 전 수학·CS 분야 10대 진전 발표에서도 똑같은 일이 있었습니다. 비소픽군(non-sofic group) 구성이 틀린 선행 문헌에 기대고 있었거든요. 그걸 깨닫고 Lean 프로그램에서는 고쳤는데 서술본은 수정하지 않았습니다. 그래서 서술된 증명은 명시된 대로라면 틀렸고, Lean 증명과도 대응하지 않았습니다. 당시 이 일이 언론에서 거의 다뤄지지 않아 놀랐습니다. 아주 큰 위험 요인으로 보이는데 말이죠.
아니면 AI가 나비에-스토크스의 자연어 증명을 쓴 다음 Lean으로 다시 쓰기 시작했는데, 증명의 일부 접근이 틀렸거나 얼버무린 것이었거나 Lean으로 쓰기에 더 쉬운 방식이 있다는 걸 알게 되어 그에 맞춰 고쳤을 수도 있습니다. Lean에서 바뀐 내용을 자연어 쪽에 되돌려 반영하는 과정(backpass)이 없었으니 두 증명이 같을 수 없죠. 저는 이게 가장 그럴듯하다고 봅니다.
차이가 Lean에서 의도적으로 생긴 것이라면(주석 3.2에 나온 m+4 대 m+5처럼 환각으로 생긴 게 아니라면), 차이를 간단히 기록해 두고 그 변경 사항을 원래 자연어 증명에 되돌려 반영하면 해결됩니다. 반면 환각 때문이라면 앞으로도 계속 환각을 일으키지 않는다는 보장이 없으니, 왔다 갔다 몇 번을 거듭해도 끝내 같은 증명에 이르지 못할 수 있습니다(주석 3.4 참고).
순서가 어땠는지는 확실히 알 수 없겠지만, AI가 없어도 수학에는 "누군가 X의 증명을 내놨는데, 증명 자체는 틀렸거나 불완전하지만 X는 참인" 경우가 널려 있다고 생각합니다.
"불완전한" 증명이라는 관점으로 볼 수도 있습니다. X를 증명하는 자연어 논증이 있는데, 알고 보니 트럭이 지나다닐 만큼 큰 구멍이 나 있습니다. 그래서 그 구멍을 하나씩 메웁니다.
그러면 결과로 나오는 증명은 처음과 다릅니다! 나쁜 증명에서 출발해 올바른 증명에 이를 수 있는 겁니다. 가끔은요.
추신: 프랑스어를 하시는 분들(자동 더빙으로도 어느 정도는 될 겁니다)께 최근에 본 아주 깔끔하고 간단한 사례를 소개합니다. 비교적 단순한 이론에 대해 흔히 들 쓰는 증명인데, 거기에 커다란 구멍이 있고 그걸 메우려면 꽤 작업이 필요합니다 [0].
[0] https://www.youtube.com/watch?v=kQBu6NH1u3I
이 저자들도 이 Lean 형식화가 올바르다는 점을 반박하는 것 같지는 않습니다. 그렇다고 해서 생성된 Lean 증명이 이 N-S 폭발 문제의 유효한 증명인지 아닌지에 대해 새로운 정보가 생기는 건 아니라고 봅니다.
제가 이해하기로는 Lean 증명에 나온 명제들이 실제 나비에-스토크스 문제와 대응하지 않을 수도 있습니다. 그걸 확인하려면 수학적 통찰이 필요하고, 꽤 오래 걸릴 수 있습니다.
초록을 제대로 이해했다면(이 점은 크게 단서를 답니다), 증명하지 못했다는 얘기는 아닙니다. 자연어 증명 하나와 Lean 증명 하나, 이렇게 서로 동치가 아닌 증명 두 개를 내놓았다는 얘기입니다. 핵심은 Lean 증명이 자연어 증명을 형식적으로 검증한 것이 아니고, 자연어 증명 또한 Lean 증명을 읽기 쉽게 풀어 쓴 설명이 아니라는 점이라고 짐작합니다. 두 가지 모두 바람직한 성질일 수 있으니, 세트를 완성하려면 증명이 4개가 되겠네요.
컴퓨터 과학의 관점에서 결론은 뻔합니다. 정확한 번역이나 기계로 검증된 대응 관계 없이 표현을 두 가지 두는 것은 지속할 수 없습니다. 지금 있는 건 LLM으로 한 분위기 번역(vibe translation)뿐이에요. 방법론은 분명히 개선해야 합니다.
그리고 컴퓨터 과학의 관점이라면 당연히 인간을 치우고 모든 걸 Lean으로 직접 표현해서 컴퓨터가 계속 일을 하게 하자는 거겠죠!
;)
그래도 확실히 해 두고 싶은데요, 둘 중 어느 쪽이든 진짜 나비에-스토크스를 다루고 있긴 한가요? 아니면 결국 실제 문제와 상관없는 무언가에 대한 증명이 두 쌍 나오게 되는 건가요?
이것이 Lean에서 증명된 형식화입니다. 적어도 지금까지는 문제를 올바르게 진술한 것으로 여겨지고 있습니다.
https://github.com/google-deepmind/formal-conjectures/blob/8bf45ed70d48b2b2a501de9c00b26bfa38c573ee/FormalConjectures/Millenium/NavierStokes.lean
논문에 이런 대목이 있습니다.
"3.1. NL 논문이 Lean이 증명하는 것보다 강한 명제를 내세울 때
§2의 예시를 보완하는 사례로 시작합니다. 다음 예시에서는 AI 자동 형식화의 결과로, 더 약한 명제에 대한 다른 Lean 증명이 나옵니다."
Lean 버전이 나비에-스토크스 문제를 올바르게 진술한 것이 아닐 수도 있다는 얘기로 보입니다.
논문은 이렇게도 말합니다.
"주 3.4 (나비에-스토크스 증명에서 생길 수 있는 또 다른 오번역). 위의 예시들은 NL 증명과 Lean 증명을 모두 꼼꼼히 직접 확인해야 하는데, 이는 까다롭고 시간이 매우 많이 드는 작업이다. 게다가 예시를 두 개만 보였다고 해서 오번역이 이 두 경우뿐이라는 뜻은 아니다."
나비에-스토크스를 잘못 형식화했다고 주장하는 사람은 아무도 없어요.
네, NL 증명도 Lean 증명도 실제 나비에-스토크스 문제와 대응하지 않을 수 있습니다. 논문에서 인용합니다.
"주 3.4 (나비에-스토크스 증명에서 생길 수 있는 또 다른 오번역). 위의 예시들은 NL 증명과 Lean 증명을 모두 꼼꼼히 직접 확인해야 하는데, 이는 까다롭고 시간이 매우 많이 드는 작업이다. 게다가 예시를 두 개만 보였다고 해서 오번역이 이 두 경우뿐이라는 뜻은 아니다."
네, 하지만 제가 한 말과는 상관없는 얘기예요. 제 말은 나비에-스토크스 방정식 자체를 잘못 형식화했다고 주장하는 사람은 없다는 거였거든요.
그래도 그 사람들 주장은 자연어 증명과 Lean 증명이 서로 일치하지 않는다는 거잖아요. 자연어 증명은 Lean 증명으로 검증되지 않고, Lean 증명은 자연어 증명으로 "설명"되지 않는다고요.
제가 제대로 이해했다면, 그들이 Lean으로 증명한 것은 나비에-스토크스가 아니라는 뜻입니다. 자연어 증명이 맞는지 틀린지에 대해서는 아무 말도 하지 않고요.
나비에-스토크스는 정리가 아니라 방정식이므로 "나비에-스토크스의 증명"이라는 것은 존재하지 않습니다. 이 방정식은 점성 유체 흐름을 나타내는 편미분방정식 모델입니다. 이 모델이 올바른지는 한 번도 의심받은 적이 없습니다. 실제 유체 흐름을 정확하게 기술할 수는 없지만 꽤 좋은 근사라는 것, 그리고 여러 초기 조건에서 잘 거동하는 해가 존재한다는 것이 알려져 있죠.
제가 이해하기로 오픈AI가 증명했다고 주장하는 것은 이렇습니다. 이 방정식에 특정 초기 조건과 시간에 따른 "외력"(숟가락으로 유체를 젓는 것 같은 실제 힘일 수도 있고 다른 외적 효과일 수도 있습니다)을 주면, 유한한 시간 동안에만 유한한(따라서 물리적으로 타당한) 해가 존재하고 그 이후에는 특이점이 나타납니다. 유한한 시간의 끝에 다가갈수록 유체 일부의 속도나 압력이 무한대로 발산한다는 것입니다.
이 결과는 테렌스 타오가 02014년에 추측한 것인데, 외력이 없는 경우였습니다. http://arxiv.org/abs/1402.0290
L∃∀N 증명이 정말로 나비에-스토크스에 관한 것이라는 점은 꽤 확신해도 된다고 봅니다. 문제는 그 증명이 나비에-스토크스에 대해 말하는 내용이 우리가 생각하는 그 내용이 맞느냐입니다.
나비에-스토크스가 무엇인지 몇 마디로 짚어 보고 싶으시다면 https://p.migdal.pl/equations-explained-colorfully/#navier-stokes 를 참고하세요.
너무 멋지네요. 수학 전체에 색깔을 입힐 수 있으면 좋겠어요!!
할 수 있어요. 코드도 공개되어 있고 인터랙티브 편집기도 있습니다.
동의합니다. 브라우징하는 사이트에서 LaTeX 수식을 찾아 위키 같은 곳과 대조한 다음 수식에 수학판 구문 강조를 입혀 주는 Firefox/Chrome 확장 프로그램이 있으면 정말 멋질 겁니다.
PDF에서도 되면 더 좋고요.
저는 이미 뒤로 미뤄 둔 프로젝트가 너무 많아서... 하고 싶은 분은 가져가세요. 눈치 좀 챙기시고요.
LLM으로 비슷한 걸 실험해 봤습니다. 어떤 것들은 그럭저럭 해내더라고요.
더 흥미로운 건, 비전 모델에 img2img로 품사별로 색을 칠해 달라고 하면 최신 모델은 꽤 잘 해낸다는 점입니다.
눈에 확 띄는 것들이 대개 그렇듯, 사실 아무것도 설명해 주지 않아요.
흠.
저는 그게 운동량 밀도 수송 방정식의 개념을 제대로 설명해 준다고는 전혀 생각하지 않습니다.
내용보다 스타일이 훨씬 앞서는 자료예요.
제가 제대로 이해한 거라면, 이 글은 자연어 증명과 Lean 증명이 동등한지를 문제 삼는 것이지 Lean 증명이 올바른지를 문제 삼는 건 아니라는 거죠?
Lean 증명이 (문제를 풀기 위해 AI가 생성한) 자연어 증명과 맞지 않는다면, Lean 증명은 의도한 주장을 검증하고 있지 않다는 얘기로 들리는데요?
논문에서는 이렇게 말합니다. "세 번째 가능성은 자연어 증명이 형식 증명이 실제로 확립하는 것보다 더 강한 진술을 제시하면서, (당연히) 증명도 서로 다른 경우이다. 후자는 OpenAI가 발표한 나비에-스토크스 방정식의 폭발 증명에서 일어나는 일이다."