범람과 수확: 극한 언어 생성의 관점에서 가치 있는 수학을 생성하기 위한 트라이비아(Trivia)의 증명 가능한 필요성

증명 보조 도구(proof assistants)와 결합된 AI 시스템은 이제 대규모로 형식 수학(formal mathematics)을 생성하고 있으며, 검증기(checker)가 확인할 수 있는 것과 수학자가 가치 있게 여기는 것 사이의 격차가 구속 조건(binding constraint)이 되었습니다. 우리는 가치 있는 수학의 생성을 '극한에서의 중첩된 언어 생성(nested language generation in the limit)'으로 모델링합니다: 멤버십 오라클(membership oracle, 증명 검증기)을 통해 접근 가능한 검증 가능한 형식 언어 $F$는, 정확한 밀도 $\alpha$를 가진 핵심 집합 $C \subseteq H$ (기존 문헌)의 적대적 열거(adversarial enumeration)를 통해서만 드러나는 미지의 가치 있는 언어 $H \in \mathcal{H}$를 포함합니다. 모든 출력은 가치 있거나 ($\in H$), 트라이비아(trivial, $\in F \setminus H$)이거나, 혹은 환각(hallucination, $\notin F$)입니다. 우리는 네 가지 질문을 해결합니다. 첫째, 검증기는 취향(taste)이 아닙니다: 광범위한 생성을 허용하는 집합은 정확히 오라클이 없는 모델의 집합이며, 이는 각 파이버(fiber-wise)별로 Angluin의 조건에 의해 특징지어집니다. 둘째, 검증기는 타당한 것만을 주장하면서 보이지 않는 모든 가치 있는 문장들을 포함하는 건전한 커버리지(sound coverage)를 구매합니다: 이는 검증기가 있을 때 가능하며, 없을 때는 불가능합니다; 이는 피할 수 없는 오류를 '거짓(false)'에서 '트라이비아(trivial)'로 재배치합니다. 셋째, 그리고 핵심적으로, 타이트한 가족(tight family)에 대한 날카로운 이분법(sharp dichotomy)이 존재합니다: 유한한 수의 트라이비아를 방출하는 생성기는 $α/2$의 최적 커버리지를 달성하는 반면, 소멸하는 비율(vanishing rate)이라 할지라도 무한한 트라이비아를 허용하면 최적값이 $1-α/2$로 급증합니다 (둘 다 후보 교집합으로 제시된 핵심 집합에 대해 타이트함). 하나의 생성기는 두 끝단 모두에 도달할 수 있습니다. 전이는 비율이 아닌 트라이비아의 개수에서 발생하며, 격차 $1-α$는 기록되지 않은 질량(unrecorded mass)입니다. 넷째, 두 체제 모두 수학의 압축 모델(compression model)에서 실체화됩니다. 완벽한 검증기도 취향을 대체할 수 없습니다: 옳지만 가치 없는 문장들의 무제한적인 흐름은 공학적 사고가 아니라 증명 가능한 필연성입니다. 왜냐하면 기록되지 않은 가치 있는 수학을 커버하기 위해서는, 무한하지만 점근적으로 무시할 수 있는(asymptotically negligible) 인증된 트라이비아의 흐름이 필요하기 때문입니다.