💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

이 논문은 LLM(Claude)을 사용하여 채이틴의 제1 불완전성 정리와 크리트만-라즈의 놀라운 시험 역설 버전의 제2 불완전성 정리를 Agda로 자동 형식화하는 사례 연구를 제시하며, 복잡한 계산 시뮬레이션을 구축하고 기계 검증된 증명을 생성하는 모델의 능력을 입증하는 동시에 수학적 추론에서의 현재 강점과 한계를 강조한다.

원저자: Thierry Coquand

게시일 2026-06-12

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Thierry Coquand

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

개요: 로봇에게 수학을 가르치기

매우 똑똑한 로봇(Claude라는 이름의 AI)과 매우 엄격하고 규칙에 얽매인 수학 교과서인 "기초 재귀 산술(Basic Recursive Arithmetic)"이 있다고 상상해 보세요. 이 교과서는 아주 구체적인 규칙이 있는 게임과 같습니다. 오직 기본적인 숫자 세기와 단순한 논리만을 사용할 수 있으며, 화려한 지름길이나 "마법" 같은 기술은 허용되지 않습니다.

이 논문의 목표는 로봇이 복잡하고 유명한 수학적 증명(수학에 한계가 있다는 내용)을 읽고, 인간이 단 한 줄의 코드도 작성하지 않은 채 이 모든 것을 그 엄격한 교과서의 언어로 완전히 다시 써낼 수 있는지 확인하는 것입니다.

결과는 **"예"**입니다. 로봇은 두 가지 깊이 있는 수학적 아이디어를 이 엄격한 언어로 성공적으로 번역해냈으며, 컴퓨터가 100% 정확하다고 검증할 수 있는 증명을 만들어냈습니다.

두 가지 핵심 아이디어

이 논문은 두 가지 유명한 개념에 초점을 맞춥니다: 채이틴의 증명(제1 불완전성 정리와 관련된 것)과 깜짝 시험 역설(제2 불완전성 정리의 한 버전)입니다.

1. "짧은 설명" 게임 (채이틴의 증명)

한정된 알파벳 세트를 사용하여 쓸 수 있는 모든 가능한 이야기를 담은 도서관이 있다고 상상해 보세요.

규칙: 어떤 이야기는 매우 짧고 설명하기 쉽습니다. 반면 어떤 이야기는 너무 복ло잡해서, 그 이야기를 설명하는 가장 짧은 방법은 그냥 이야기 전체를 그대로 다 적는 것뿐입니다.
문제: 채이틴의 증명은 어떤 이야기가 너무 복잡해서 짧은 프로그램으로는 설명될 수 없다는 것을 증명하려고 합니다.
로봇의 도전 과제: 이를 증명하기 위해 로봇은 수학 교과서 내부에 이야기를 읽고, 실행하고, 그것이 무엇을 하는지 확인할 수 있는 "기계"를 구축해야 했습니다.
장벽: 수학 교과서는 "프로그램을 실행하는 것"을 처리하기에는 너무 단순합니다. 왜냐하면 실행은 보통 교과서가 허용하지 않는 복잡한 함수(예: 아커만 함수)를 필요로 하기 때문입니다.
해결책: 인간 저자는 "간디/하워드 메이저레이션(Gandy/Howard majorisation)"이라는 기술을 제안했습니다. 이것을 로봇에게 연료 탱크를 주는 것이라고 생각하세요. 기계에게 영원히 실행하라고 요구하는 대신, 로봇은 프로그램이 끝나는 데 정확히 얼마만큼의 "연료"(단계)가 필요한지 계산합니다. 로봇은 연료가 다 떨어지기 전에 프로그램이 반드시 멈춘다는 것을 보장하는 특별한 "연료 게이지"를 만듭니다.
결과: 로봇은 스스로 이 연료 게이지를 구축했습니다. 만약 어떤 숫자를 "단순하게 설명하기에는 너무 복잡한 것"으로 설명하려고 시도한다면, 결국 논리적 모순(예: 0이 1과 같다는 결론)에 도달한다는 것을 증명했습니다.

2. "깜짝 시험"과 모래 더미

두 번째 부분은 유명한 역설을 다룹니다: 선생님이 다음 주에 깜짝 시험을 보겠다고 발표합니다. 학생들은 다음과 같이 추론합니다. 금요일에는 시험을 볼 수 없다(왜냐하면 목요일까지 시험을 보지 않았다면 금요일에 볼 것이라는 걸 알게 될 것이기 때문). 따라서 목요일에도 볼 수 없고, 이런 식으로 계속 추론하다 결국 시험은 아예 있을 수 없다는 결론에 도달합니다. 그런데 선생님이 수요일에 시험을 치릅니다. 그리고 그것은 깜짝 시험이었습니다.

이 논문은 이 논리(Kritchman과 Raz의 방식)를 사용하여 수학 체계가 자기 자신의 일관성(모순이 없다는 사실)을 스스로 증명할 수 없음을 증명합니다.

기존 방식: 이전의 증명들은 모순을 찾기 위해 날짜나 숫자의 개수를 세었습니다.
새로운 방식 (소리테스/모래 더미): 저자들은 이를 모래 더미 역설에 비유합니다.
- 모래 더미에서 모래 한 알을 제거해도 여전히 모래 더미입니다.
- 또 다른 한 알을 제거해도 여전히 모래 더미입니다.
- 계속해서 한 알씩 제거하다 보면 결국 모래가 하나도 남지 않게 됩니다. 하지만 정확히 어느 시점에 더 이상 "모래 더미"가 아니게 된 것일까요?
적용:
- 0부터 거대한 숫자 $N$ 까지의 숫자 목록이 있다고 가정해 봅시다.
- 논리는 다음과 같이 시도합니다: "이 모든 숫자가 짧은 설명을 가질 수는 없다."
- 로봇은 이를 단계별로 증명합니다. "만약 0부터 $N$ 까지의 모든 숫자가 짧은 설명을 가진다고 가정하면, 모순이 발생한다"라고 말합니다.
- 그런 다음 숫자를 하나씩 제거합니다. "좋다, 1부터 $N$ 까지의 숫자가 짧은 설명을 가진다고 해도 여전히 모순이 발생한다."
- 로봇은 숫자를 하나씩 계속 제거합니다 (마치 모래 알을 하나씩 빼내는 것처럼).
- 결국 목록이 비어 있는 지점에 도달하지만, 논리는 그럼에도 불구하고 모순을 강제합니다.
반전: 이 논문은 이것이 자기 참조의 "악순환"이 아니라, 모래 더미와 같다고 주장합니다. 모래 한 알(숫자 하나)을 안전하게 가져갈 수는 있지만, 계속해서 그렇게 하면 전체 구조가 무너집니다. 이 붕괴는 수학 체계가 스스로를 깨뜨리지 않고서는 자신이 안전하다(일관적이다)는 것을 증명할 수 없음을 입증합니다.

이것이 왜 중요한가 (논문에 따르면)

수학 보조 도구로서의 AI: 이 논문은 현재의 AI(Claude와 같은)가 복잡한 수학 증명의 아주 작고 지루한 세부 사항들을 처리할 수 있을 만큼 충분히 발전했음을 보여줍니다. AI는 파서를 구축하고, 기계를 평가하며, 인간이 보통 수동으로 수행해야 하는 논리적 단계를 처리할 수 있습니다.
구성적 수학 (Constructive Math): 이 논문은 "구성적 수학"(무언가를 말할 때 실제로 그것을 구축해야 하는 수학)에서 "부분 함수"(영원히 실행될 수도 있는 프로그램)라는 개념이 까다롭다는 점을 강조합니다. 로봇은 영원히 실행될 수도 있는 "루핑(looping)" 프로그램을 사용해야 했지만, 증명은 그것이 반드시 멈출 것임을 보장했습니다. 이는 AI가 정확하게 처리해낸 미묘하지만 결정적인 차이입니다.
마법 같은 기술 없음: 로봇은 어떠한 "전술(tactics)"(지름길)이나 화려한 라이브러리도 사용하지 않았습니다. 오직 기초적인 규칙만을 사용하여 처음부터 모든 것을 직접 구축했습니다. 이 덕분에 증명은 매우 견고하며 컴퓨터가 검증하기 쉽습니다.

결론

이 논문은 AI가 이제 형식 수학(formal mathematics)에서 강력한 파트너 역할을 할 수 있음을 보여주는 사례 연구입니다. AI는 높은 수준의 아이디어(예: "수학에는 한계가 있다")를 받아들여 이를 엄격하고 기계로 검증 가능한 형식으로 번역할 수 있습니다.

저자들은 AI가 인간의 가이드(예: "연료 탱크" 기술을 제안하는 것)를 필요로 하기는 하지만, 일단 가이드가 주어지면 AI가 자율적으로 코드를 작성하고, 논리를 구축하며, 전체 과정을 문서화할 수 있다고 언급합니다. 그 결과는 이러한 깊은 논리적 역설이 정확히 어떻게 작동하는지를 명확히 밝혀내고, 모호함을 제거하여 오직 딱딱한 논리적 사실만을 남기는, 완전히 검증된 증명입니다.

기술 요약: Chaitin과 놀라운 불완전성 정리의 자동 형식화

문제 및 배경
본 보고서는 대규모 언어 모델(LLM)인 Claude와 증명 보조기인 Agda를 사용하여 괴델의 제2 불완전성 정리를 자동 형식화한 이전 실험을 확장한다. 주요 목적은 계산의 내부 표현을 포함하는 복잡한 수학적 증명을 형식화하는 데 있어 현재 LLM의 능력과 한계를 조사하는 것이다. 본 논문은 두 가지 특정 대상을 목표로 한다: Chaitin의 제1 불완전성 정리 증명과 Kritchman-Raz의 "놀라운 시험 역설(surprise examination paradox)" 버전의 제2 불완전성 정리이다.

다루어진 핵심적인 기술적 과제는 대상 양화사(object quantifiers)와 표준 택틱스(tactics)가 결다는 기초 재귀 산술(Basic Recursive Arithmetic, BRA) 내에서 계산을 인코딩하는 것이다. BRA는 Guard가 정립한 체계로, 내부 평가 함수를 정의하는 것이 불가능하다(이는 Ackermann 함수와 유사하게 원시 재귀적 범위를 초과하기 때문이다). 이 문제는 메타 수준의 함수나 외부 라이브러리에 의존하지 않고, 프로그램과 그 실행 단계를 순수하게 대상 언어(object language) 내에서 완전히 표현할 것을 요구한다.

방법론
본 프로젝트는 인간 저자가 작성한 Agda 코드가 단 한 줄도 없는 "스파르타식(spartan)" 접근 방식을 채택한다. 즉, 형식화는 고수준의 수학적 설명을 바탕으로 Claude에 의해 자율적으로 생성되었다. 이 방법론은 다음의 기술적 전략에 의존한다:

삼진 문자 인코딩(Teyary String Encoding): 프로그램은 자연수로 표현되며, 이는 삼진 문자(숫자 1, 2, 3)로 해석된다. 이를 통해 최대 길이 $L^*$ 인 프로그램의 집합을 자연수의 단순한 초기 구간 $\{p < N\}$ (여기서 $N = 3^{L^*+1}$ )으로 취급할 수 있어, 복잡한 열거 메커니즘을 피할 수 있다.
CK 머신 구현: 전역 평가 함수의 필요성을 우회하기 위해, Claude는 연속(continuation) 스택 기반의 단계별 실행 머신(Landin CK 머신)을 자율적으로 구축했다. 이 머신은 표현식을 분해하고 연속 스택을 관리함으로써 계산을 단계별로 시뮬레이션한다.
Gandy/Howard Majorisation: 중요한 난관은 논리 내부에서 특정 함수 $f$ 가 특정 단계 내에 종료됨을 증명하는 것이었다. 단계 횟수는 메타 수준의 자연수가 될 수 없으므로, 저자들은 Claude가 Gandy/Howard majorisation 방법을 사용하도록 유도했다. 이는 원시 재귀를 통해 $f$ 의 실제 실행 시간을 확실히 상회하는 닫힌 조합자(closed combinator) fuel(f)를 정의하는 것을 포함한다. 이를 통해 인터프리터의 완전성을 BRA 내부에서 직접 기술하고 증명할 수 있게 된다.
Sorites로서의 놀라운 시험: 제2 불완전성 정리의 증명은 Kritchman과 Raz가 사용한 계수(counting) 논증을 피한다. 대신, 이 논증을 소라이테스(Sorites, 모래더미) 역설로 모델링한다. 이는 단계 $r$ 에 대한 외부 귀납법을 통해, 구간 $[r, N]$ 내의 모든 숫자가 짧은 설명을 가질 수 없음을 증명하는 방식으로 진행된다.

주요 기여 및 결과
본 논문은 Church의 기초 재귀 산술(BRA)에 대해 Agda에서 완전히 기계 검증된 다음의 결과들을 제시한다:

자동 형식화된 Chaitin의 정리: 시스템은 거짓말쟁이 문장을 Kolmogorov 복잡도로 대체하는 Chaitin의 증명을 성공적으로 형식화했다. 이 형식화는 명시적인 증명 변환기(proof-transformer) $G$ 를 생성한다. 정리는 만약 항 $w$ 가 비압축성 문장 $K(out(w)) > L^*$ 의 증명을 코딩한다면, $G \cdot w$ 는 $0=1$ 의 증명을 코딩한다는 것이다. 이는 증명 가능성에 대한 메타 이론적 부정이 아닌, 긍정적인 대상 수준의 함의(implication)로 공식화된다.
내부화된 제2 불완전성: 본 논문은 $T$ 가 자신의 일관성( $Con_T$ )을 증명한다면 $T$ 는 모순( $0=1$ )이라는 것을 보여주는 Kritchman-Raz 논증을 형식화한다. 증명은 $S(0)$ (비둘기집 원리)에서 $S(N+1)$ (모순)로의 하강으로 진행되며, 각 단계 $S(r) \to S(r+1)$ 은 일관성 가설을 정확히 한 번씩 소비한다.
구성적 통찰: 이 형식화는 구성적 수학에서 부분 함수(partial functions)의 역할을 강조한다. 구체적으로, 대각선 프로그램은 타겟을 찾을 때까지 유도 가능한 공식들을 열거한다. 이 프로그램은 외부적으로는 종료가 증명되지만, 그 크기는 종료 증명을 내부화하지 않은 채 계산된다. 이는 Blum의 속도 향상(speed-up) 현상의 발현을 보여준다. 즉, (외부 증명에 의해 전체성이 유지되는) 부분 재귀 프로그램을 허용함으로써, 내부적으로 종료를 인증해야 하는 프로그램보다 무한히 짧은 프로그램을 사용할 수 있음을 보여준다.

의의 및 주장
본 논문은 Claude와 같은 현재의 코딩 LLM이 지속적인 감독 하에 작동할 경우, 수학 논문의 세부적인 디테일을 이해하는 데 효과적인 도구임을 주장한다. 이 프로젝트는 다음을 입증하는 사례 연구 역할을 한다:

LLM은 고수준의 구조적 힌트에 의해 유도될 때, 복잡한 구문적 기제(파서, 평가 머신)와 논리적 논증(majorisation)을 자율적으로 생성할 수 있다.
타입 이론(특히 택스가 없는 Agda)은 계산과 코딩을 포함하는 구체적인 수학을 표현하는 데 적합하다. 왜냐하면 증명은 함수 외연성(function extensionality)이나 쿼션 타입(quotient types) 없이 직접 표현될 수 있기 때문이다.
형식화된 "놀라운(surprise)" 논증은 전통적인 놀라운 시험 역설보다는 소라이테스 역설에 더 가깝다. 왜냐하면 모순은 단일한 자기 참조 루프가 아니라, 건전한 단계들의 반복으로부터 발생하기 때문이다.

저자들은 타입 이론의 언어가 이러한 조합론적, 계산적 수학을 다루기에 완벽하지만, 비조합론적 객체를 유사한 자동화 수준으로 다룰 수 있는 형식 체계를 설계하는 것이 핵심적인 연구 과제로 남아 있다고 결론짓는다. 이 형식화는 Chaitin과 Kritchman-Raz의 원본 제시 내용에 담긴 암묵적인 세부 사항들을 명확히 하며, 최소한의 산술 체계 내에서 이러한 논증들에 대한 엄밀하고 기계로 검증된 기초를 제공한다.