수학 증명 생성에서 무가치한 정리가 필연적인 이유

한줄 요약

형식 증명 검사기로 검증된 수학 정리 생성에서 가치 있는 정리를 모두 포함하려면 무가치하지만 참인 정리를 무한히 생성해야 함을 증명했다.

풀어야 하는 문제

AI가 증명 보조기와 결합하여 대규모 형식 수학을 생성할 수 있게 되었지만, 검증 가능한 정리와 수학자가 가치 있다고 여기는 정리 사이의 간극이 병목이 되고 있다. 이 연구는 검증 가능성과 가치의 관계를 이론적으로 모델링하여, 가치 있는 수학을 생성하는 데 필연적인 한계가 무엇인지 밝히고자 한다.

접근 방법

언어 생성의 극한 개념을 차용하여, 검증 가능한 형식 언어 F와 가치 있는 언어 H를 정의하고, H의 일부인 핵심 C가 문헌으로 주어진 상황에서 가치 있는 문장을 생성하는 문제를 형식화했다. 생성기는 F에 속하는 문장만 출력할 수 있으며, 출력은 가치 있음(H), 무가치함(F\H), 환각(F 밖)으로 분류된다. 네 가지 질문을 정식화하고 증명했다: (1) 검증자는 취향을 대체할 수 없음, (2) 검증자는 건전한 커버리지를 가능하게 함, (3) 무가치한 문장의 수에 따라 최적 커버리지가 급격히 달라짐(유한 시 α/2, 무한 시 1-α/2), (4) 두 체제 모두 압축 모델에서 구현 가능.

결과·기여

검증 가능성과 가치 사이의 근본적 간극을 이론적으로 증명하여, 완벽한 검증기로도 가치 있는 수학을 모두 생성하려면 무가치한 정리를 무한히 생성해야 함을 보였다. 이는 AI 수학 생성에서 '쓸모없는' 출력이 단순한 엔지니어링 문제가 아니라 필연적 현상임을 시사한다.