AI가 Lean으로 옮긴 수학 증명 검증이 원문 정확성을 보장하지 못한다

AI가 자연어로 쓴 수학 증명을 Lean 같은 형식 언어로 옮기고, 그 형식 증명을 기계적으로 검증하는 흐름이 자리를 잡고 있다. arXiv에 올라온 논문 하나가 이 흐름의 전제를 정면으로 건드린다. 형식 검증이 통과됐다는 사실이 원래의 자연어 논증이 옳다는 보장까지 해주지는 않는다는 주장이다. 논문 번호는 arXiv:2610.08144이고, Alexander Bastounis·Fabian Circelli·Anders C. Hansen 세 사람이 썼다.

핵심 논거는 번역의 의미 충실성(semantic faithfulness)에 있다. 자연어 수학 텍스트에는 모호성이 남아 있고, 이를 해소해야만 의미를 보존한 번역이 가능하다. 저자들은 이 모호성 해소 문제가 Solvability Complexity Index(SCI) 계층, 곧 산술 계층에서 임의로 높은 위치에 놓인다고 본다. SCI = ∞라는 결론이며, 이는 정지 문제(SCI = 1)를 포함한 어떤 계산 문제보다도 어렵다는 뜻이라고 논문은 설명한다.

이론에 그치지 않고 실제 사례도 붙였다. AI가 자연어 명제와 증명을 Lean으로 옮기면서 잘못 번역한 예들이 있고, 그 결과 자연어 증명과 Lean 쪽 '검증' 사이에 불일치가 생긴다는 것이다. 여기에는 OpenAI가 발표한 나비에-스토크스 방정식 해의 폭발(blow-up) 증명도 들어간다. 논문은 해당 Lean 형식 증명이 나비에-스토크스 해 폭발에 관한 자연어 증명과 대응하지 않는다고 지적한다.

autoformalisation은 AI가 생성한 수학 텍스트를 검증하는 수단으로 쓰임이 늘고 있다. 자연어를 형식 언어로 옮기고 나면 그 뒤의 검증은 기계가 처리할 수 있어서, 사람이 처음부터 끝까지 따라가며 확인할 필요가 줄어든다는 기대가 깔려 있었다. 이 논문이 겨냥하는 지점은 그 기대의 전제, 즉 번역이 원문의 의미를 그대로 옮겼다는 가정이다.

개발자 입장에서 이 결과는 검증 파이프라인 설계에 직접 걸린다. LLM이 만든 코드나 스펙을 형식 명세와 대조해 통과시키는 구조를 쓴다면, '형식 검증 통과 = 원문 정확'이라는 등식을 그대로 믿기 어려워진다. 번역 단계가 그 자체로 별도의 검증 대상이 되고, 자연어 쪽 모호성을 누가 어떻게 확정했는지가 기록으로 남아야 한다는 요구로 이어진다.

논문이 다루는 분야는 해석학(math.AP)과 AI(cs.AI), 논리학(math.LO)에 걸쳐 있다. 주제 분류상으로는 형식 검증과 AI 출력 신뢰성 문제의 교차점에 놓여 있다.

주의할 점도 분명하다. arXiv 프리프린트 v1 단계의 결과이고, 저자들이 제시한 것은 의미 충실한 번역이 임의로 높은 계산 복잡도를 갖는다는 이론적 결과와 개별 사례에서 관찰된 불일치다. autoformalisation을 통째로 무용지물로 선언하는 결론이 아니라, 번역의 의미 보존 문제를 검증 체계 안에서 다뤄야 한다는 문제 제기로 읽는 편이 정확하다.