AI가 생성한 수학 논증을 신뢰하려면 어떻게 검증해야 할까. 최근 주목받는 방식 중 하나가 '자동 형식화(autoformalisation)'다. 자연어로 쓰인 수학 텍스트를 AI가 Lean 같은 형식 언어로 번역하면, 그 번역된 논증은 기계적으로 참·거짓을 검증할 수 있다. 형식 언어로 옮겨진 증명은 증명 보조기가 한 줄 한 줄 따져 오류가 없음을 확인해 주기 때문이다. OpenAI가 나비에–스토크스 방정식 해의 폭발(blow-up)에 관한 증명을 발표하면서 이 접근을 내세운 것도 같은 맥락이다. 그러나 arXiv에 올라온 한 논문(Navier–Stokes Lost in Translation)은 이 검증 체계가 생각만큼 든든하지 않다고 지적한다.
핵심 주장은 간단하다. 형식 언어로 옮긴 증명이 기계 검증을 통과했다는 사실은, 원래 자연어 논증이 옳다는 것을 보장하지 않는다는 것이다. 문제는 검증 단계가 아니라 그 앞의 '번역' 단계에 있다. 자연어 수학 텍스트는 본질적으로 모호함을 품고 있고, 이 모호함을 의미에 충실하게(semantically faithful) 해소해야만 올바른 형식화가 가능하다. 그런데 번역이 원문의 의미를 왜곡하면, 검증기는 원문이 아니라 '잘못 번역된 다른 명제'를 열심히 검증하게 된다. 그 결과는 참일 수 있지만, 그것이 참이라는 사실은 원래 자연어 증명에 대해 아무것도 말해 주지 않는다.
정지 문제보다 어려운 문제
논문이 제시하는 이론적 근거는 계산 가능성 이론에서 나온다. 자연어 수학 텍스트의 모호함을 해소하는 문제가 '풀이 가능성 복잡도 지수(Solvability Complexity Index, SCI)' 위계에서 임의로 높은 곳, 즉 SCI가 무한대에 해당한다는 것이다. 비교를 위해 저자들은 그 유명한 정지 문제(Halting problem)를 든다. 정지 문제의 SCI는 1이다. 즉 의미에 충실한 자동 형식화를 제공하는 일은, 정지 문제를 포함한 그 어떤 계산 문제보다도 어렵다는 이야기다. 이는 성능 좋은 모델을 더 키우거나 데이터를 늘린다고 해결되는 공학적 난제가 아니라, 원리적으로 알고리즘이 보편적으로 해낼 수 없는 종류의 문제라는 뜻이다.
저자들은 이 결과가 추상적 경고에 그치지 않도록, 실제로 AI가 자연어 명제와 증명을 Lean으로 옮기면서 발생한 오역 사례들을 함께 제시한다. 자연어 증명과 그 Lean '검증' 사이에 불일치가 생긴 경우들이다. 그리고 그 사례 안에 OpenAI가 발표한 나비에–스토크스 증명도 포함된다. 논문은 형식화된 Lean 증명이 해의 폭발에 관한 자연어 증명과 대응하지 않는다는 점을 보인다고 밝힌다. 다시 말해 Lean 쪽이 검증을 통과했더라도, 그것이 발표된 자연어 논증을 그대로 담아낸 것은 아니라는 지적이다.
실무자가 읽어야 할 지점
이 논의가 중요한 이유는 자동 형식화가 'AI가 만든 증명을 믿을 수 있게 해 주는 안전장치'로 자주 소개되기 때문이다. 검증기가 통과시켰다는 표현은 강한 신뢰 신호처럼 들린다. 그러나 검증기는 자신에게 주어진 형식 명제만을 다룰 뿐, 그 명제가 사람이 읽은 자연어 진술과 같은 것인지에 대해서는 아무 판단도 하지 않는다. 형식 체계의 신뢰성과 번역의 충실성은 전혀 다른 문제이며, 전자가 아무리 견고해도 후자가 무너지면 전체 보증은 성립하지 않는다.
소프트웨어 관점에서 보면 이는 익숙한 구도다. 사양을 코드로 옮길 때, 코드가 테스트를 모두 통과해도 사양 자체를 잘못 옮겼다면 의미가 없다. 번역된 사양이 원래 의도와 일치하는지는 결국 사람이 확인해야 하는 영역이다. 자동 형식화에서도 '형식 명제가 자연어 진술을 제대로 포착했는가'를 사람이 검토하는 과정이 생략될 수 없으며, 이 검토는 자동화하기 어려운 부분이라는 점을 논문은 원리 수준에서 뒷받침한다.
물론 이 논문의 주장에는 범위를 분명히 해 둘 필요가 있다. 논문이 겨냥하는 것은 형식 증명 보조기 자체의 정당성이 아니라, 자연어에서 형식 언어로 넘어가는 번역 단계의 보증 능력이다. 또한 SCI가 무한대라는 결과는 '의미에 충실한 번역을 범용적으로 자동 제공하는 것'의 불가능성을 말하는 것이지, 특정한 좋은 번역이 사람의 검토를 거쳐 존재할 수 있다는 가능성까지 부정하는 것은 아니다. 제시된 오역 사례들도 자동 형식화가 늘 틀린다는 증거가 아니라, 통과했다는 사실만으로 안심해서는 안 된다는 반례에 가깝다.
결국 이 연구가 남기는 실무적 교훈은 명확하다. AI가 생성하고 AI가 형식화한 수학적 주장이 '검증되었다'고 제시될 때, 그 검증이 정확히 무엇을 대상으로 한 것인지를 먼저 물어야 한다. 형식 명제의 진술문을 사람이 직접 읽고, 그것이 원래 자연어 주장과 같은 내용을 담고 있는지 확인하는 절차가 없다면, 기계 검증이라는 라벨은 신뢰의 근거가 아니라 오해의 출발점이 될 수 있다.