OpenAI, 17시간 만에 Navier-Stokes 정리 증명 검증
The part of Navier-Stokes no one is talking about
OpenAI가 Navier-Stokes 방정식에 관한 오랜 난제를 해결하는 증명을 발표했다. 주목할 점은 기존의 사람이 읽는 증명과 함께 Lean 4 형식 증명을 공개했다는 것이다. 과거에는 수학 교과서 한 페이지를 형식화하는 데 40시간이 걸렸지만, OpenAI는 166페이지 분량의 증명을 단 17시간 만에 Lean으로 검증했다. 비용을 4자리 수만큼 낮춘 이 변화는 수학을 넘어 보안 정책, 스마트 컨트랙트, 미션 크리티컬 알고리즘 검증에도 혁명적이다.
“혁명적”이라는 단어를 쓰기를 주저하지만, 어떤 것의 비용을 네 자릿수만큼 낮추는 것은 혁명적이다.
HN 토론
170- stabbles
Lean이 페르마의 마지막 정리 증명 검증에 걸리는 시간이 에이전트가 Lean 코드를 생성하는 시간보다 겨우 한 자릿수 빠르다는 사실(230GB RAM으로 15시간 검증 vs 11일 생성)을 깨닫고 나니 좀 웃기네요.
Lean을 어느 정도까지 최적화할 수 있을까요? 감사 가능해야 하므로 단순해야 한다면, 불투명한 최적화를 사용해 더 빠르게 실행할 수 없다는 뜻인가요?
- parhamn
그들은 에이전트 비용으로 4천만 달러를 추산했어요(대규모 에이전트 집단이었죠). 글에 나온 숫자를 쓰면 인간의 경우 약 880,000시간 × 시간당 $150 = 1억 3,200만 달러에 더 가깝습니다. 여전히 놀라운 업적이지만 '네 자릿수 차이'는 아니죠. 100만 시간의 지적 노동을 조정하는 게 결코 쉽지 않다는 점을 감안하면 이 비교는 분명히 무의미합니다.
매우 흥미롭고 불확실한 시기네요!
- boshalfoshal
사람들은 이번 특정 발표에 대해 실제 결과는 제쳐두고 다른 얘기만 하는 것 같아요.
어떤 종류의 일반화된 컴퓨터 프로그램이 이런 규모의 문제를 풀 수 있다는 것 자체가 여전히 놀랍고, 우리는 그것이 실시간으로 일어나는 걸 목격했습니다. 새 모델이 더 직접적인 증명/귀납적 증명도 할 수 있을지 궁금하네요.
- pkal
제 생각에 '페이지당 40시간' 규칙은 최신이 아니며, 2005년의 증명 자동화 부족에서 비롯된 결과에 더 가깝습니다. 제가 Lean에 대해 이해한 바로는, 그들이 많은 노력을 기울여 개선해 온 것 중 하나가 증명 기계화를 논리학자뿐 아니라 수학 애호가들에게도 더 받아들일 만하게 만드는 것이었습니다.
- lordnacho
당신이 생각하는 것을 형식화하고 있다는 걸 어떻게 아나요? Lean 4에 버그가 있으면, 생각했던 것과 다른 것을 증명하게 되지 않나요?
- 3m4r
OpenAI의 나비에-스토크스 해법에 반드시 적용되는 건 아니지만, AI가 정말로 극도로 어려운 문제를 해결한 것처럼 보이는데 인간이 독립적으로 그 해법을 검증할 수 없다면 — 즉 증명/논증을 이해하려면 검증자들이 생물학적으로 갖지 못한 지능이나 자동화 도구를 사용할 자원이 필요하다면 — 무슨 일이 일어날까요?
우리는 이미 에이전트들이 결과를 얻기 위해 부정행위가 경제적이라고 인식해서 벤치마킹에서 실제 작업을 우회하려는(즉, 정답지를 훔치는) 증거를 목격했습니다. AI의 부정행위나 단순한 오답을 더 이상 감지할 능력이 없게 된다면 무슨 일이 일어날까요? 형식 검증을 위한 핵심 도구(또는 그 의존성)의 업스트림에 대한 장기적인 사회공학 공격(예: 시도된 XZ 백도어)이 있고 신뢰할 수 있는 컴퓨팅 기반이 없다면 무슨 일이 일어날까요?
어느 쪽이 더 저렴하고 더 직접적인 경로일까요, 특히 장기적으로? 견고한 성을 쌓으려는 쪽은 수천 개의 잠재적 틈새를 방어해야 하지만, 공격자는 하나만 찾으면 됩니다.
- zem
새로 접근 가능해진 형식 증명에 대한 저자의 감사를 깎아내리려는 건 아니지만, 사람들은 AI가 실제 증명을 한다는 이야기보다 훨씬 오래전부터 형식화 노력의 절감에 대해 이야기해 왔습니다!
- aabhay
Lean에서 증명을 형식화하는 것은 2005년에 가능했던 형식화에 비해 극적으로 쉬워졌습니다. 그리고 Lean의 mathlib이 대부분의 기반 작업을 해두어서 공리와 필요한 보조정리들이 내장되어 있습니다. 학부 교과서의 표기법과 매우 유사한 표준 추상화로 생각할 수 있습니다.
그렇긴 해도, 밀레니엄 상금 문제를 Lean으로 형식화한 것이 얼마나 놀라운 업적인지 결코 깎아내리려는 건 아닙니다. OpenAI가 공개한 코드를 보세요. 다양한 유체역학 개념의 백과사전 같습니다.