번역 과정에서 어긋난 나비에–스토크스 증명

AI 요약

AI가 작성한 수학 증명을 형식 언어로 옮겨 검증하는 방식이 주목받고 있습니다. Lean(린)으로 번역한 명제와 증명이 기계 검증을 통과하면 형식화된 내용의 증명은 확인할 수 있지만, 그 내용이 원래 자연어 글에서 의도한 명제와 증명을 보존하는지는 별개의 문제입니다. 이 논문은 두 단계 사이의 의미상 불일치를 다룹니다.

자연어에서 형식 언어로 옮길 때 생기는 문제

수학 글은 기호와 관례를 쓰지만, 문장에는 모호한 표현과 생략된 전제가 남습니다. 형식화를 하려면 문맥을 바탕으로 뜻을 정하고, 어떤 명제를 적을지 선택해야 합니다. 논문은 자연어의 모호성을 의미에 충실하게 해소하는 문제의 계산 복잡도가 Solvability Complexity Index(SCI) 계층에서 임의로 높은 수준에 이를 수 있다고 주장합니다. 저자들의 표현으로는 SCI가 무한대에 해당합니다. 따라서 자연어의 뜻을 보존하는 자동 형식화는 SCI가 1인 정지 문제(Halting problem)보다도 어려울 수 있습니다.

Lean은 형식화된 명제와 그 증명을 기계적으로 검사합니다. 하지만 검증기가 확인하는 대상은 입력된 형식 표현입니다. 자연어 문장을 올바르게 해석했는지, 형식화된 증명이 자연어 증명과 같은 논증인지까지 자동으로 보장하지는 않습니다. 논문은 이 간극을 실제 AI 형식화 사례로 보여줍니다. 자연어 명제나 증명을 Lean으로 옮기는 과정에서 뜻이 달라지고, 형식 증명이 자연어 글의 설명과 어긋나는 사례를 다룹니다.

나비에–스토크스 사례

저자들은 OpenAI가 발표한 나비에–스토크스(Navier–Stokes) 방정식 해의 폭주(blow-up) 증명도 사례에 포함합니다. 논문의 초록은 Lean으로 형식화된 증명이 자연어로 제시된 증명과 대응하지 않는다고 말합니다. 이 주장은 Lean 증명이 틀렸다거나, 형식화된 명제가 나비에–스토크스 문제를 잘못 표현했다는 주장과 같지 않습니다. 쟁점은 Lean 검증 결과가 함께 공개된 자연어 증명의 논증을 확인해 주는지입니다. 논문은 자연어 증명의 정확성 자체를 주장하지 않으며, 형식화 과정에서 생긴 불일치를 지적한다고 밝힙니다.

Hacker News 반응

• @ted_dunning — 자연어는 모호하지만 Lean 형식화는 잘 정의되어 있고 모호하지 않습니다. 여기서 실제 문제는 형식 언어가 아니라, 반대편에 있는 모호성을 유용하고 정확하게 번역하기가 매우 어렵다는 점입니다.
• @buzzy_hacker — 제가 제대로 이해했다면, 이 글은 자연어 증명과 Lean 증명이 동등한지 묻는 것이지 Lean 증명 자체의 정확성을 의심하는 것은 아니군요.
  • @dcre — 꼭 그렇지는 않습니다. Lean의 형식 명제가 맞다면 Lean 증명은 그 명제가 참이라는 데 상당한 확신을 줍니다. 다만 자연어 증명이 Lean 증명과 일치하지 않을 수 있으므로, 자연어 증명은 타당하지 않을 가능성이 있습니다.
• @empath75 — 최근 Claude와 3주 동안 컴퓨터 과학 논문의 borrow checker를 Lean으로 형식화했습니다. 형식화는 완료됐지만, 원 논문에는 조판 오류와 수식 오류가 여러 개 있었습니다. 형식 검증된 borrow checker를 얻었지만, 논문에 인쇄된 borrow calculus와 정확히 같지는 않았습니다. 출판 논문을 기계화하면 이런 경험이 흔하다고 봅니다. 생략된 단계와 얼버무린 설명이 많습니다.
• @infogulch — Lean 증명과 산문으로 쓴 증명이 정확히 일치하지 않는다는 점을 보여주는 글입니다. Lean의 정리가 원래 문제와 동등하다면, 두 증명의 불일치는 증명 자체의 타당성과는 무관합니다. 다만 문제를 정확히 진술하는 일이 증명만큼 어려울 수 있으므로, Lean 정리가 원래 문제와 동등한지 검증해야 합니다.
• @j2kun — AI가 생성한 증명은 다른 연구와 마찬가지로 학계가 검토하고 이해할 때까지 ‘문제를 풀었다는 주장’으로 다뤄야 한다고 생각합니다. AI 기업을 동료 검토의 예외로 취급하면 해롭습니다.
• @fasterik — 제가 이해한 바로는 Lean 증명의 정확성이나 실제로 증명하는 정리를 두고 다투는 사람은 없습니다. 그 정도면 문제를 해결했다고 볼 만하며, 자연어 증명은 있으면 좋은 설명입니다.

원문: arXiv / 번역·요약: Trawling