번역 과정에서 의미를 잃은 Navier-Stokes

Lean 검증 통과는 생성된 형식 증명의 타당성을 확인하지만, 그 증명이 원래 자연어 논증을 충실하게 옮겼거나 자연어 증명 자체가 올바르다는 보장은 아님 자동 형식화에는 이미 정확히 형식화된 정리의 증명을 생성하는 작업과, 정의부터 증명까지 수학적 의미를 보존해 번역하는 작업이 있으며, 두 작업의 성공 기준은 다름 간단한 다항식과 대칭행렬 사례에서 AI는 잘못된 자연어 증명을 고치거나 올바른 논증을 다른 논증으로 대체해 컴파일되는 Lean 증명을 생성함 OpenAI가 발표한 Navier-Stokes 폭발 증명의 자연어 문서와 Lean 코드 비교에서는 추가 미분 차수, 압력 플럭스 추정식, 증명 방법이 서로 일치하지 않는 사례가 확인됨 자연어 증명의 정확성에는 통상적인 동료 심사와 검토가 여전히 필요함. 이 연구는 OpenAI 자연어 증명의 정오를 판정하지 않으며, Lean 번역의 의미 불일치만을 검토함 자동 형식화의 두 가지 성공 기준 첫 번째 유형은 정리의 명제가 이미 Lean으로 정확히 번역됐다는 전제에서, 자연어 증명을 입력받아 해당 정리의 형식 증명을 생성하는 작업임 sorry나 추가 공리 없이 Lean이 유효한 증명으로 받아들이고 컴파일하면 성공으로 간주함 이 기준은 원래 자연어 논증을 그대로 보존했는지까지 요구하지 않음 두 번째 유형은 수학 문서 전체를 의미에 충실하게 번역하는 작업임 정의, 정리, 명제, 증명뿐 아니라 개념과 결과 사이의 의존 관계도 보존해야 함 원문의 증명 검증이 목적이라면 형식 증명과 실제로 쓰인 논증 사이의 대응도 확립해야 함 다른 명제로 바꿔 증명하는 것은 원문의 의미를 보존한 번역이 아님 형식 증명의 정확성과 원문에 대한 충실성은 별개임 잘못된 자연어 증명을 올바른 형식 증명으로 바꿀 수 있음 두 증명이 모두 올바르지만 서로 다른 논증일 수 있음 자연어 문서가 형식 증명보다 강한 결과를 담고 있을 수도 있음 의미에 충실한 번역은 첫 번째 유형보다 훨씬 어려우며, 일반적인 경우 정지 문제보다 엄밀히 더 어려운 문제임 Lean은 형식화된 정리의 정확성을 확인할 뿐, 자연어 증명의 중간 논증과 보조정리까지 자동으로 검증하지 않으므로 동료 심사와 통상적인 검토를 생략할 근거가 되지 않음 기본 사례: 증명이 바뀌어도 Lean 검증은 통과함 예제 2.1은 (p(x)=x^3-x^2-x+1)이 (x\geq-1)에서 음이 아니라는 올바른 명제에 잘못된 자연어 증명을 붙인 사례임 자연어 증명...