arXiv 논문: OpenAI 나비에-스토크스 증명, Lean 검증은 통과했지만 자연어 원본과 다른 명제를 증명함

나비에-스토크스가 뭔지 감 잡으려면 이 색깔 설명 글부터 보면 됨. 수식 전부 색으로 구분해서 설명해놨음.

이거 진짜 예쁘다. 수학 전부 이렇게 색으로 구분할 수 있으면 좋겠음.

음, 근데 운동량 밀도 수송 방정식이 뭔지는 이 글도 제대로 설명 못 함.

LLM 증명 보면서 계속 궁금했던 부분임. 수학은 논리지만 수학 글쓰기는 자연어라서 기호가 중복되고 관습은 생략되고 맥락에 많이 기댐. 모델이 명제를 형식 시스템으로 옮겨 증명에 성공해도 그게 수학자가 의도한 명제가 아닐 수 있음. 지금까지 발표된 LLM 증명도 사람이 뭘 증명했는지 뜯어보면 안 버틸 거라는 경고로 읽었는데, 이 해석 맞나?

자연어가 모호한 건 맞는데 Lean 형식화는 아주 잘 정의돼 있고 모호하지 않음. 진짜 문제는 형식 언어가 아니라 반대쪽 모호성이고, 쓸모 있고 정확한 번역이 극도로 어렵다는 점임.

나 최근 3주 동안 클로드랑 CS 논문 하나를 Lean으로 형식화했음. 형식화는 통과했는데 원본 논문에서 실수 여러 개가 나왔음. 조판 오류부터, 실제로는 arising resource에만 적용되는데 인쇄된 대로 전체 자원에 양화한 수식까지. 덕분에 쓸 만한 borrow checker는 얻었지만 논문에 인쇄된 계산법과 정확히 같은 건 아니었음.

논문을 손으로 재현해보면 흔한 경험임. 진짜 무서운 건 AI가 읽을 수 없는 형식 증명을 뱉어놓고 자연어 버전 단계를 사실상 거짓으로 서술할 때임. 자연어 버전이야말로 핵심 문제 해법에서 제일 중요한 부분인데, 그게 부풀려지면 해법 가치가 깎이고 동시에 해가 존재한다는 사실이 후속 연구를 막음.

2류 과학자 입장에서 제일 행복할 때가, 내 분야 핫한 논문을 코드로 옮겨보고 저자들이 체계적 오류를 냈다는 걸 보여줄 때임. 핫하고 틀린 논문에 관심이 쏠린다는 증거임.

논문 구현하다 보면 그런 세부에서 막히는데, 그때마다 주제 이해가 깊어져서 좋음. 다만 그런 세부 검토를 AI한테 넘기는 건 조심해야 함.

내가 이해한 게 맞으면 이건 자연어 증명과 Lean 증명의 동등성을 의심하는 거고, Lean 증명 자체의 정확성을 의심하는 건 아님?

Lean 증명이 자연어와 안 맞으면 의도한 명제를 검증한 게 아니게 됨. 논문에도 나옴. 자연어 증명이 형식 증명이 실제로 세운 것보다 강한 명제를 줄 수 있고, OpenAI의 나비에-스토크스 폭발 증명이 그 경우임.

Lean 증명이 맞다는 건 확인하기 쉬움. 그게 우리가 관심 있는 걸 증명하는지는 훨씬 어려운 문제임. 코드가 컴파일된다고 버그가 없다고 확신할 수 있나?

맞음. AI가 자연어 버전을 제대로 쓸 압력도 없고, 자동으로 판정할 방법도 없음.

증명하기 쉬운데 서로 동등하지 않은 명제가 많음. Lean이 뭔가를 증명했는데 그게 우리가 원하는 건지, 비슷하지만 결국 아닌 건지가 쟁점임.

자연어 증명에서 오류를 찾은 것도 아니고 그냥 둘이 다르다는 것 아님?

자연어 증명은 틀렸고 Lean 증명은 맞음. 사람도 비슷한 실수를 함. 스펙을 쓰고 코드로 옮겼는데 코드가 안 돌아가서 코드만 고치고 원래 스펙은 안 고치는 상황과 같음.

자연어 증명과 형식 증명이 '대응'하는지는 주관적인 문제임.

놀랄 일 아님. LLM이 직접 못 풀면 문제의 조건이나 맥락을 바꾸는 쪽을 선호한다는 건 거의 처음부터 알려져 있었음. 예전엔 데이터베이스 드롭이나 저장소 삭제였고, 이제는 수학 문제의 의미를 살짝 바꿔서 맞지만 무관한 답을 냄.

나도 영어에서 Go, Python, TypeScript, SQL로 옮길 때 AI를 썼는데 해석이 꽤 창의적이었음.

Lean 증명이 맞다는 걸 다투는 사람은 없음. 문제는 자연어로 옮기는 걸 잘못했다는 것임.

적어도 AI가 만든 증명은 커뮤니티가 검토하고 소화할 시간이 생길 때까지 '주장'이라고 불러야 함. AI 회사가 동료 검토 밖에 있다는 발상이 해로움.

Lean 증명의 정확성이나 그게 주장하는 추측을 실제로 증명한다는 걸 다투는 사람은 없음. 그걸로 문제는 해결된 것으로 보면 됨. 자연어 증명은 있으면 좋은 것.

내 추측엔 AI가 자연어로 먼저 증명하고 그다음 Lean 증명을 생성하는데, 그 과정에서 autoformalizer가 형식화 가능하게 만들려고 자연어 증명을 살짝 다시 쓰는 것 같음. 자연어 증명을 Lean에 맞춰 되돌리는 역방향 패스가 필요한 건가?

Lean 증명을 먼저 만들고 설명 패스를 돌리는 방법도 가능함. 그리고 이 논문은 두 증명의 진위를 의심하는 게 아니라, 자연어 서술이 형식 증명에 충실한지 아니면 그냥 틀렸는지, 혹은 둘 다인지를 묻는 것임.

수학자는 아님. 왜 항상 Lean만 쓰지 않고 자연어를 쓰나?

사람이 기계어 대신 코드를 쓰는 이유랑 같음. 다른 사람이 읽고 배우고 고칠 수 있어야 하니까.

Lean은 읽기 너무 어렵고 세부 수준이 높아서, 읽히는 보조정리조차 인간 작업 기억의 한계 때문에 진짜 이해가 어려움.

왜 항상 기계어로 쓰지 않는지와 같은 질문임.