Case study: proving sqrt(2) irrational with LPTP and an LLM

당신이 2천 년 넘게 인간을 당혹스럽게 해온 미스터리를 풀려는 탐정이라고 상상해 보십시오. 그것은 바로 '루트 2($\sqrt{2}$)'가 "유리수"인가 하는 문제입니다. 수학의 세계에서 유리수는 완벽한 분수, 즉 피자를 깔끔하게 한 조각 자른 것(3/4이나 5/2처럼)과 같습니다. 무리수는 분수로 나타낼 수 없는, 끝없이 이어지는 지저한 소수입니다. 루트 2는 한 변의 길이가 1인 정사각형의 대각선 길이이며, 고대 수학자들은 이것이 분수가 될 수 없는 지저운 숫자임을 증명했습니다.

이제 당신을 돕기 위해 매우 다른 두 가지 도구가 있다고 상상해 보십시오. 첫 번째 도구는 매우 엄격하고 로봇 같은 심판인 LPTP입니다. 이 도구는 매우 정밀하고 논리적인 언어(Prolog 기반)를 사용하며, 모든 단계가 수학적으로 완벽해야만 증명을 수락합니다. 만약 당신이 아주 작은 실수라도 한다면, 이 심판은 의사봉을 내리치며 "안 돼, 무효야"라고 말할 것입니다. 두 번째 도구는 **거대 언어 모델(LLM)**로, 세상에 쓰인 거의 모든 것을 읽은 매우 똑똑하고 창의적인 학생과 같습니다. 이 학생은 다음 이야기나 수학 문제의 다음 단계를 추측하는 데 능숙하지만, 때로는 그럴듯하게 들리지만 실제로는 틀린 사실을 지어내는 "환각(hallucination)" 현상을 보이기도 합니다.

오늘날 과학자들의 큰 질문은 이 둘을 결합할 수 있는가 하는 점입니다. 이 창의적인 학생이 증명을 작성하는 힘든 일을 하고, 엄격한 심판이 학생이 거짓말을 하지 않는지 모든 문장을 검사하게 할 수 있을까요? 이 논문은 바로 그 파트너십을 탐구하며, 루트 2의 무리수성을 테스트 케이스로 사용합니다.

---

위대한 증명 검증 팀워크

이 논문에서 저자들은 현대적인 AI(구체적으로 Claude라는 모델)를 사용하여 루트 2가 무리수임을 증명하는 데 도움을 주고자 했습니다. 하지만 여기에는 반전이 있습니다. 증명은 로봇 심판(LPTP)이 이해하고 검증할 수 있는 매우 구체적이고 엄격한 형식을 갖추어야 했습니다. 그들은 단순히 AI가 "그것은 참이다"라고 말하기를 원한 것이 아니라, AI가 실제 단계별 논리를 작성하고 이를 심판이 채점하도록 만들기를 원했습니다.

이야기는 간단한 아이디어에서 시작됩니다. 루트 2가 무리수임을 증명하려면 보통 그 반대를 가정합니다. 즉, 루트 2가 두 개의 정수 $p$와 $q$로 이루어진 분수이며, 두 수는 공약수를 갖지 않는다(서로소이다)고 가정하는 것입니다. 수학적 계산을 진행하다 보면, 결국 두 숫자 모두 짝수여야 한다는 모순에 부딪히게 되는데, 이는 두 숫자가 공약수(2)를 공유한다는 것을 의미합니다. 이는 두 수가 서로소라는 규칙을 깨뜨리며, 원래의 가정이 틀렸음을 증명합니다.

저자들은 AI가 이 증명을 LPTP의 엄격한 언어로 작성하도록 시도했습니다. 처음에는 AI가 이야기는 알고 있지만 요구되는 형식에 맞춰 에세이를 쓰지 못하는 학생과 같았습니다. AI는 단계를 건너뛰거나 논리적 비약을 시도했고, 이는 심판에게 받아들여지지 않았습니다.

여기서 팀워크가 일어났습니다. 저자들은 다음과 같은 피드백 루프를 설정했습니다:

1. AI가 증명의 한 단계를 작성하려고 시도한다.
2. 심판(LPTP)이 이를 검사한다.
3. 만약 심판이 오류를 발견하면, 논리가 깨진 정확한 지점을 지목한다.
4. 저자들은 그 오류를 AI에게 보여준다.
5. AI는 특정 오류를 수정하여 다시 시도한다.

이 과정은 마치 "뜨겁다, 차갑다" 게임과 같았습니다. 심판은 단순히 "틀렸다"라고 말하는 대신, "4단계에서 실수를 했다"라고 구체적으로 알려주어 AI가 경로를 수정할 수 있게 해주었습니다.

결과: 부분적인 승리

실험은 성공적이었지만 몇 가지 주의사항이 있었습니다. AI는 스스로 많은 작고 쉬운 퍼즐 조각들을 증명할 수 있었습니다. 예를 들어, "어떤 수가 짝수이면 그 제곱도 짝수이다"라거나 "2와 어떤 수를 곱하면 짝수이다"와 같은 것들을 성공적으로 증명했습니다. 저자들은 이를 "보조 정리(lemmas)"라고 부릅니다. AI는 이러한 것들을 정확히 해냈으며, 때로는 인간이 생각하지 못한 새로운 보조 아이디어를 제시하기도 했습니다.

하지만 증명의 가장 까다로운 부분, 즉 루트 2가 왜 분수가 될 수 없는지를 보여주는 특정 논리에 있어서 AI는 막혔습니다. AI는 스스로 적절한 경로를 찾지 못했습니다. 그래서 인간 저자들이 개입하여 AI에게 "힌트"를 주거나, 심지어 증명의 주요 구조를 직접 작성한 뒤 AI에게 작은 빈틈을 채우도록 요청해야 했습니다.

결국, 그들은 루트 2가 무리수라는 완전하고 형식적인 증명을 만들어냈습니다. 이 증명은 부분적으로는 AI가 작성했고, 전체적으로는 로봇 심판에 의해 검증되었습니다. 심판은 논리가 타당함을 확인하며 통과 판정을 내렸습니다.

이것이 의미하는 바

이 논문이 이제 AI가 스스로 모든 수학 문제를 풀 수 있다고 주장하는 것은 아닙니다. 실제로 저자들은 AI가 혼자서는 할 수 없다는 점을 명시적으로 보여주었습니다. 인간의 지도와 엄격한 검증 도구가 없다면, AI는 아마도 가짜이거나 망가진 증명을 만들어냈을 것입니다.

대신, 이 논문은 새로운 작업 방식을 제안합니다: 초안 작성자로서의 AI, 편집자로서의 인간, 그리고 팩트 체크 도구로서의 형식적 도구입니다. AI는 빠르고 창의적이어서 아이디어를 생성하고 세부 사항을 채우며, 형식적 도구(LPTP)는 환각과 오류를 잡아내는 눈을 뜨고 있는 감시자 역할을 합니다.

저자들은 또한 더 빠르게 작업을 수행할 수 있는 다른 자동 수학 도구들(ATP라고 불리는)을 테스트했습니다. 이 도구들은 빠르고 무료였지만, 인간이 읽기 어렵고 검증된 수학 라이브러리에 쉽게 추가될 수 없는 증명을 만들어냈습니다. AI 방식은 비록 더 느리고 인간의 도움이 필요했지만, 사람이 읽을 수 있고 향후 용도로 안전하게 저장할 수 있는 증명을 만들어냈습니다.

요약하자면, 이 논문은 우리가 인간의 직관과 기계의 정밀함 사이에서 하나를 선택할 필요가 없음을 보여줍니다. AI가 힘든 초안 작성을 맡고 엄격한 도구가 채점을 하게 함으로써, 우리는 인간이 배를 조종하고 엄격한 심판이 지도를 확인하는 한, AI가 복잡한 수학적 진리를 증명하도록 돕는 시스템을 구축할 수 있습니다. 루트 2는 여전히 무리수이지만, 이제 우리는 그것을 증명하는 새로운 협력적 방법을 갖게 되었습니다.