Lean 검증이 AI의 Navier-Stokes 증명을 보증하지 못하는 이유
Navier–Stokes Lost in Translation
AI가 자연어 수학 텍스트를 Lean으로 자동 형식화(autoformalisation)해 기계적으로 검증하는 방식이 확산되고 있다. 그러나 이 논문은 자연어의 의미를 충실히 반영한 번역 자체가 임의로 높은 Solvability Complexity Index(SCI=∞)를 가짐을 보인다. 즉, 정지 문제(SCI=1)보다도 어려운 작업이다. 실제 사례로 OpenAI가 발표한 Navier-Stokes 해의 폭발 증명에서 Lean 형식화가 자연어 원문과 대응하지 않음을 지적한다.
특히 우리는 OpenAI가 발표한 Navier-Stokes 증명을 포함하여, 형식화된 Lean 증명이 Navier-Stokes 방정식 해의 폭발에 대한 자연어 증명과 대응하지 않음을 보인다.
HN 토론
151- ComplexSystems
AI에 대한 늘상 있는 설전은 차치하고, 충격적인 주장은 이것인 것 같다:
"특히, 우리는 형식화된 Lean 증명이 나비에-스토크스 방정식 해의 폭발에 대한 NL 증명과 대응하지 않는다는 것을 보인다."
따라서 이 저자들은 OpenAI가 실제로 나비에-스토크스 문제를 전혀 증명하지 못했다고 주장하는 것으로 보인다. 내가 그들의 아이디어를 제대로 이해했다면, 그들은 LLM이 나비에-스토크스의 원래 "자연어" 아이디어를 올바르게 형식화하지 못했다고 주장하는 것이다. 만약 사실이라면, 그들이 내세운 Lean 증명은 실제로 나비에-스토크스의 증명이 아니라, 원래 자연어 아이디어를 잘못 번역한 것에 불과하다는 뜻이 된다. 만약 맞다면, 이는 정말 대담한 주장이며 다른 연구자들도 동의하는지 보고 싶다.
- buzzy_hacker
내가 제대로 이해했다면, 이것은 자연어 증명과 Lean 증명 사이의 동등성을 의문시하는 것이지, Lean 증명의 정확성을 의문시하는 것은 아닌가?
- stared
나비에-스토크스가 무엇인지 몇 마디로 상기하고 싶다면: https://p.migdal.pl/equations-explained-colorfully/#navier-s...
- vanyle
이 논문은 별 내용이 없다. 첫째, 자연어는 Lean만큼 정밀하지 않기 때문에 NL 논증을 Lean으로 번역하는 방법은 여러 가지가 있다. 그림 1에서 보듯이, LLM은 근에 관한 논증을 간결한 방식으로 번역하는 데 꽤 잘했다.
게다가 이 논문은 나비에-스토크스의 NL 논증이 Lean 논증보다 더 강력하다고 주장한다. 내가 이해하기로는 번역 LLM이 게을러져서, 추가적인 더 강한 주장 없이 정리를 만족시키는 최소한의 코드만 작성한 것이다.
수학 논문에서는 "그런데 참고로 이것은 실제로 [더 강한 주장]을 증명한다"라고 말하는 것이 흔하지만, 번역이라는 정확한 목표를 가진 AI는 결코 그렇게 하지 않을 것이다. 그 목표는 증명을 번역하는 것이지, 수학의 질을 높이는 것이 아니기 때문이다.
- infogulch
이 논문은 Lean 증명과 산문(pdf) 증명이 정확히 일치하지 않는다는 것을 보여준다. 하지만 Lean이 받아들인 Lean 정리가 Clay Institute가 발표한 원래 문제 진술과 동등하다면, 이 불일치는 증명 자체의 타당성에는 아무 영향을 미치지 않는다. 이는 결코 사소한 '만약'이 아니다: 문제를 정확하게 진술하는 것은 종종 증명만큼 어렵다. 검증 노력은 Lean 정리가 Clay Institute가 발표한 것과 동등한지에 집중해야 한다.
그렇긴 해도, Lean 증명과 pdf 사이의 간극은 해석 가능성 측면에서 짜증나는 일이며, 해석은 타당한 목표이긴 하지만, 그것이 증명의 타당성에 영향을 주지는 않는다.
- sigbottle
우리는 언젠가 의미 이론의 위기를 겪게 될까?
두 가지 실패 모드를 _가정_해 보자:
- Lean 커널에는 항상 버그가 있을 수 있다.
- 형식화된 진술이 _수학자들이_ "실제로 원했던" 것과 대응하지 않을 수 있다.
"뭐, 증명에 실수가 있을 수 있다는 주장을 하더라도, 해답보다는 문제 진술을 확인하는 것이 분명 더 쉽다"라는 논증을 펴는 것이 자연스러워 보인다.
(하나의 "좋은 성질"은, 에이전트가 _두 번째_ 기준에 따라 "하위 논증을 올바르게" 할 필요조차 없다는 것이다. 어쩌면 자연어 증명에서 형식적 대상과 미묘하게 다른 대상을 발명하지만, 모든 것이 검증을 통과할 수도 있다. _원래_ 진술이 대응한다는 것만 보장된다면, 유일한 가능성은 Lean 커널이다. 따라서 이 경우에는 무한 재귀하지 않는다.)
하지만 "정의"는 항상 정말 이상한 것이어서, 우리에게 좋은 이론이 있다고 생각하지 않는다? 질문을 표현하는 데 필요한 서술적 힘을 어떻게 정량화할 수 있을까? 수학에서는 종종 어려운 부분이 정의를 제대로 잡는 것이다. 그런데 정의 자체가 너무 복잡하고 검증 불가능해져서 아무도 그것을 어떤 것과도 대응시킬 수 없게 되면 어떨까? 음, 흥미로운 오래된 수학 문제 중 많은 것들은 "상대적으로" 간단한 문제 진술을 가지고 있어서 Lean으로 쉽게 형식화할 수 있는 것처럼 보이지만, Lean에 정말 만능 해결책이 있는지, 아니면 끝없이 거북이처럼 계속될지는 모르겠다.
AI가 계속 치솟는 한 아마 중요하지 않을 것이다 […]
- dooglius
예시들에 대한 고수준 설명을 보면, 이것은 "잘못된 번역"이라기보다는 LLM이 형식화하면서 증명을 조금씩 수정한 것에 가깝다고 생각한다. m+4와 m+5 사이를 오가는 것은 일반적으로 자연어 수학 진술을 파싱할 때 생기는 종류의 모호함과는 꽤 다른 일이다.
- Sniffnoy
음, 여기를 훑어봐도, OpenAI가 강제항이 있는 나비에-스토크스 폭발 대신 실제로 무엇을 증명했는지에 대한 진술이 어디에도 안 보인다. 도중에 사용된 다른 특정 진술들에 대해서는 그렇게 하는 곳이 보이지만, 헤드라인 결과에 대해서는 아니다.