최근 인공지능(AI)이 수학 정리의 형식 증명(formal proof)을 생성하는 능력이 발전하고 있지만, AI가 만든 증명이 원본 자연어 증명(natural language proof)의 의미를 충실히 반영하지 못할 수 있다는 연구 결과가 나왔습니다. 형식 증명이 유효하더라도, 그 과정이나 결론이 원본과 달라질 수 있다는 점이 핵심입니다. 이는 AI 기반 수학 도구의 신뢰성과 활용 범위에 중요한 질문을 던집니다.
이번 연구는 자동 형식화(automated formalization)의 두 가지 성공 기준을 제시합니다. 첫째는 주어진 명제에 대해 유효한 형식 증명을 생성하는 것이고, 둘째는 수학 문서 전체의 의미를 보존하며 번역하는 것입니다. OpenAI가 발표한 나비에-스토크스(Navier-Stokes) 방정식의 폭발 증명(finite time blowup proof)을 자연어 문서와 Lean 코드(Lean proof)로 비교 분석한 결과, 역연산자 추정식에서 필요한 미분 차수가 Lean 쪽에서 하나 더 많아 더 약한 결과를 도출했습니다. 또한 압력 플럭스 추정식과 증명 방법에서도 차이가 발견되었는데, 자연어 증명은 리스 변환(Riesz transform)을 사용하는 반면 Lean 증명은 소볼레프 매장(Sobolev embedding)과 다른 횔더 부등식(Hölder inequality) 지수를 사용해 다른 결론에 이르렀습니다. 이는 AI가 원본 증명의 논증을 그대로 옮기기보다, 유효한 다른 논증으로 대체하거나 변형할 수 있음을 보여줍니다.
이러한 불일치는 AI가 생성한 형식 증명이 단순히 '컴파일 가능한' 유효한 증명이라고 해서 원본 자연어 증명의 정확성이나 의도를 완전히 담보하지 못한다는 것을 의미합니다. 수학적 증명의 자동 형식화는 오류를 줄이고 검증을 자동화하는 데 큰 잠재력을 가지고 있지만, 현재로서는 여전히 인간의 동료 심사(peer review)와 면밀한 검토가 필수적이라는 점을 시사합니다. AI가 수학적 추론의 복잡한 뉘앙스와 미묘한 의미를 완벽하게 포착하기 위해서는 더 많은 연구와 발전이 필요하며, 이는 AI 기반 수학 도구의 실제 적용에 있어 중요한 고려사항이 될 것입니다.