Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
이 논문은 저자가 AI 모델인 Claude를 사용하여 처치의 기본 재귀 산술(Church's Basic Recursive Arithmetic)에 대한 괴델의 제2 불완전성 정리를 Agda로 자동 형식화함으로써, 암시적인 수학적 논증을 재구성하는 모델의 능력과 사양이 불충분할 때 수학적으로 틀린 결과를 생성하는 경향에 대한 사례 연구 역할을 하는 50,000라인의 공리 없는 기계 검증된 증명을 도출해낸 실험을 보고한다.
원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
당신은 자신의 수학 숙제를 스스로 검증할 수 있는 완벽하고 자기 점검이 가능한 로봇을 만들려고 노력하고 있다고 상상해 보세요. 이 로봇은 BRA라고 불리며, 매우 똑똑하지만 매우 엄격하고 단순한 규칙을 따릅니다. 이 로봇은 더하기, 빼기, 그리고 값이 같은지 확인하는 기능은 갖추고 있지만, "상식" 모듈은 가지고 있지 않습니다.
당신이 읽고 있는 논문은 인간 연구자(Thierry Coquand)가 AI(Claude)와 팀을 이루어 이 로봇에게 매우 유명하고 어려운 교훈인 **괴델의 제2 불완전성 정리(Gödel's Second Incompleteness Theorem)**를 가르치는 실험에 대한 보고서입니다.
이 실험의 이야기를 간단한 부분들로 나누어 설명하겠습니다.
1. 목표: 로봇은 자신이 안전하다는 것을 증명할 수 있는가?
괴델의 제2 정리는 수학 체계의 일종인 "거짓말쟁이의 역설"과 비슷합니다. 이 정리는 다음과 같이 말합니다: "만약 어떤 체계가 일관적이라면(즉, 거짓을 증명하지 않는다면), 그 체계는 자기 자신이 일관적이라는 것을 스스로 증명할 수 없다."
다시 말해, 만로 우리 로봇 BRA가 실제로 수학을 올바르게 수행하고 있다면, 로봇은 "나는 착한 로봇이다"라는 증명을 써 내려갈 수 없을 것입니다. 만약 로봇이 그것을 증명할 수 있다면, 그것은 사실 로봇이 고장 났다는 뜻이 됩니다. 이 프로젝트의 목표는 Agda라는 컴퓨터 프로그램 내에서 AI를 사용하여 이 증명을 디지털 버전으로 구축하는 것이었습니다.
2. 첫 번째 시도: "가짜" 성공
팀은 AI에게 수학자 Rose의 오래된 논문을 읽고 그 논문을 바탕으로 정리를 증명하도록 요청하며 시작했습니다.
- 무슨 일이 일어났나: AI는 며칠 동안 열심히 작업하여 하나의 "증명"을 만들어냈습니다. 그것은 인상적으로 보였습니다!
- 문제점: AI가 속았습니다. AI가 읽고 있던 오래된 논문에는 오류(틀린 정리)가 포함되어 있었습니다. AI는 지시 사항을 완벽하게 따랐지만, 시작점이 잘못되었기 때문에 결과물은 괴델의 정리처럼 보이지만 실제로는 엉터리인 무언가였습니다.
- 교훈: 이는 AI가 논리를 따르는 데는 뛰어나지만, 만약 당신이 잘못된 지도를 준다면 AI는 기꺼이 당신을 잘못된 목적지로 데려다줄 것이라는 점을 보여주었습니다. 당신은 단순히 AI에게 무엇을 증명하라고 맡길 것이 아니라, 목적지를 스스로 알고 있어야 합니다.
3. 진짜 시도: 지도 수정하기
실패 이후, 팀은 더 신뢰할 수 있는 수학자 R. Guard의 노트로 전환했습니다. 이 노트들은 마치 빠진 조각과 오타가 있는 보물 지도와 같았습니다.
- 도전 과제: Guard의 노트는 1963년에 작성되었습니다. 매우 정밀했지만, 인간 수학자라면 자동으로 채워 넣었을 아주 작고 당연한 세부 사항들을 많이 생략했습니다. 예를 들어, Guard는 독자가 로봇의 두뇌 내부의 "숫자(numerals)"(1, 2, 3 같은 숫자)를 어떻게 다루는지 알고 있다고 가정했습니다.
- AI의 역할: 인간 연구자는 단 한 줄의 코드도 직접 쓰지 않았습니다. 대신, 그들은 "번역가" 또는 "설계자" 역할을 했습니다. 그들은 AI에게 이렇게 말했습니다: "여기에 빠진 조각이 있다. 여기에 규칙이 있다. 이제 코드를 작성하라."
- 결과: AI는 처음부터 50,000줄의 코드를 성공적으로 작성했습니다. AI는 로봇, 증명, 그리고 검증 시스템 전체를 구축했습니다. 인간이 코드를 한 줄도 타이핑하지 않은 상태에서 말입니다. 최종 결과물은 로봇 BRA가 자신의 안전성을 증명할 수 없다는 것을 기계적으로 검증된 증명이었습니다.
4. 숨겨진 기술 (비법)
논문은 이 작업이 가능하게 만들기 위해 AI가 배워야 했던, 오래된 노트 속에 숨겨져 있던 몇 가지 영리한 기술들을 강조합니다.
- "중첩된 상자" 문제: 로봇은 자신의 이력을 확인해야 했습니다. 책을 쓰는 동시에 그 책을 읽으려고 하는 상황을 상상해 보세요. AI는 로봇의 두뇌 안에 특수한 "이력 테이프"를 구축해야 했습니다. 알고 보니 로봇의 기본 도구들은 이를 위해 만들어지지 않았기에, AI는 로봇이 과거의 단계들을 기억할 수 있도록 복잡한 "러시아 인형(마트료시카)" 구조를 발명해야 했습니다.
- "닫힌 상자" 규칙: 로봇은 숫자(예: 5)를 대입(substitution)에 의해 변하지 않는 "닫힌 상자"로 취급해야 합니다. 오래된 노트는 이것이 당연하다고 가정했습니다. AI는 진행하기 전에 "5는 닫힌 상자이다"라는 것을 명시적으로 증명하도록 지시받아야 했습니다.
- "가설적" 지름길: 로봇은 매우 경직된 방식(힐베르트 스타일의 논리)으로 작동하며, "X가 참이라면, Y이다"라고 쉽게 말할 수 없습니다. AI는 모든 문장을 "만약..."이라는 래퍼(wrapper)로 감싸는 영리한 기술(Carneiro lift라고 불리는)을 사용하여, 자신의 규칙을 어기지 않으면서도 복잡한 추론을 시뮬레이션할 수 있게 했습니다.
5. 이것이 중요한 이유
이것은 단순히 수학 정리를 증명하는 것에 관한 것이 아닙니다. 이것은 인간과 AI가 어떻게 협력할 것인가에 대한 테스트 드라이브입니다.
- 인간은 설계자입니다: 인간은 비전과 올바른 지도, 그리고 AI가 경로를 벗어날 때 이를 포착할 수 있는 능력을 제공했습니다.
- AI는 석공입니다: AI는 50,000줄의 증명이라는 벽돌을 하나하나 쌓아 올리는 힘든 일을 수행했습니다.
- 발견: 이 과정은 기존의 수학 노트가 곳곳에서 "허술했다"는 점을 드러냈습니다. AI에게 반드시 완벽해야 하는 코드를 쓰도록 강제함으로써, 팀은 수십 년 동안 간과되었던 원본 1963년 텍스트의 숨겨진 가정과 오타를 찾아냈습니다.
요약
이 프로젝트를 자율 주행 자동차를 만드는 팀이라고 생각해 보세요. 인간 운전자는 목적지(괴델의 정리)와 도로 규칙을 알고 있었습니다. AI는 자동차를 조립하는 엔진 제작자였습니다.
- 처음에 AI는 깨진 설계도를 바탕으로 자동차를 만들려 했고, 자동차처럼 보이지만 제대로 달릴 수 없는 차량을 만들었습니다.
- 그 후, 그들은 더 나은 설계도로 바꿨습니다. AI는 완벽하게 작동하는 자동차를 만들었습니다.
- 그 과정에서 그들은 설계도에 누락된 지침이 있다는 것을 깨달았고, 자동차가 작동할 수 있도록 새로운 부품들을 발명해야 했습니다.
결과는 특정 수학 체계가 자신의 일관성을 스스로 증명할 수 없다는 것을 기계적으로 검증된 방식으로 증명해 낸 것이며, 이는 인간이 가이드하고 AI가 글을 쓰는 협업을 통해 완전히 이루어졌습니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.