OpenAI의 수학 증명은 우리 자신을 비춘다

TL;DR

• OpenAI가 내부 모델로 생성한 수학 결과 372개를 공개했으며, 거의 모두 단일 에이전트에 단일 프롬프트를 입력해 결과당 약 3시간의 연산으로 얻었고, 일부는 형식 검증을 통과했지만 사람은 아직 그 이유를 이해하지 못함.
• 결과 다수에는 모든 단계를 소프트웨어로 검사하는 Lean 형식화가 포함돼 증명의 타당성을 뒷받침하지만, 검증 커널은 의미를 보증하지 않음.
• 유니크 게임 추측의 증명이라고 주장된 결과에는 기존에 알려진 코드와 다른 재귀적 구성 및 노이즈 테스트를 이용하는 새 코드가 등장함.
• 언어 모델은 수학자들이 쓴 증명과 교재, 강의 노트 등을 압축하고 재조합한 결과물이므로, 이 증명은 외계의 산물이 아니라 인간의 지식이 낯선 형태로 되돌아온 것임.
• 이해를 거치지 않고 옳음을 판정하는 방식은 수학의 사회적 실천과 지식의 전달에 도전을 제기하며, 필즈상 수상자 25명도 대규모 결과 생성이 유망한 연구 영역을 고갈시킬 수 있다고 경고함.

깃허브에 공개된 증명

• OpenAI는 어제 수학 결과 372개를 깃허브에 공개함. 결과는 내부 모델에서 나왔으며, 거의 모두 단일 프롬프트를 단일 에이전트에 입력해 생성했고 결과 하나당 연산 시간은 대략 3시간임.
• 결과 다수에는 린(Lean) 형식화가 포함됨. 소프트웨어 프로그램이 증명의 모든 단계를 검사하므로 증명은 타당할 가능성이 높음.
• 일부 결과는 참이라고 인증됐지만, 아직 어떤 사람도 그 이유를 이해하지 못함. 2년 전, 어쩌면 작년에도 이런 문장은 쓸 수 없었음.
• 읽히지 않는 증명은 이전에도 있었음. 네 색 정리, 헤일스의 케플러 추측 증명, 한 심사자가 모두 검토하기에는 너무 긴 분류 결과 등이 그 사례임.
• 과거의 증명은 사람이 선택한 방식으로 길었고 다른 사람이 단계별로 살펴볼 수 있었음. 경우 분석이 복잡하더라도 그 전략은 인간의 것이었음.
• 깃허브의 증명은 다름. 증명의 전략을 누구도 소유하지 않으며, 검증 커널은 타당성만 보증할 뿐 의미에 관해서는 아무 말도 하지 않음.
• 우리는 이제 지금까지 우리 중 누구도 알지 못하는 것을 알고 있음.

낯익은 것이 낯설게 돌아오는 경험

• 처음에는 인간이 만든 존재가 발견했지만 인간은 이해하지 못하고, 어쩌면 이해할 수도 없는 증명보다 더 낯선 것은 없다고 느꼈음.
• 프로이트는 1919년 에세이 「섬뜩함」에서 독일어 *unheimlich*를 살펴보고, 오래전부터 익숙하게 알고 있던 것으로 되돌아가는 두려운 것들을 가리키는 말이라고 결론 내림.
• 섬뜩함은 외계적인 것이 아니라, 익숙한 것이 알아볼 수 없는 모습으로 돌아오는 경험임. 아이와 거의 똑같은 인형, 도플갱어, 내 집이면서도 내 집이 아닌 집이 그 사례임.
• 결과 중 하나는 복잡도 이론가 다나 모슈코비츠가 평생 연구해 온 문제인 유니크 게임 추측의 증명이라고 주장됨.
• 스콧 애런슨이 전한 모슈코비츠의 실시간 반응에 따르면, 그 증명은 재귀적 구성으로 만든 새롭고 기이한 코드를 제안하고 노이즈 테스트로 검사함. 이는 해당 분야에서 이미 알려진 두 코드와 모두 다름.
• 모슈코비츠는 이를 “외계인의 기이한 광기”라고 부르면서, 우리가 외계인에게서 배울 것이 많다고 덧붙임.
• ‘외계적’이라는 말은 자연스럽고, 처음에는 그렇게 느끼기도 했음. 하지만 이는 절반만 맞음. 외계의 증명자가 만든 유물이라면 그 존재 자체가 증명보다 더 큰 의미를 덮어버렸을 것임. 이번 증명은 그런 것이 아님.

우리에게서 나온 지능

• 인공지능을 좋아하든 싫어하든, 가장 두드러진 사실은 언어 모델이 우리에게서 만들어졌다는 점임.
• 이 경우 모델은 수학자들이 지금까지 쓴 모든 증명과 교재, 강의 노트, 늦은 밤 온라인 포럼 답변을 압축하고 재조합한 결과임.
• 결과는 우리의 표기법을 사용하고, 우리의 보조정리를 인용하며, 우리가 던진 질문에 답함. 수학은 인간의 활동 가운데서도 특히 인간다운 분야임. 그런데 그 결과는 그 결과를 만든 사람들에게 읽히지 않음.
• 모델은 우리이면서 우리가 아니며, 이 증명은 두 사실을 가장 분명하게 보여주는 증거임. 모델은 섬뜩함.
• 프로이트는 같은 에세이의 각주에서 기차의 침대칸에 홀로 앉아 있다가, 가운을 입은 나이 든 남자가 문으로 들어오는 것을 봤다고 씀. 그 남자를 바로잡으려고 일어선 뒤, 문 거울에 비친 자기 모습임을 깨달았고 그 남자가 싫었다고 기억함.
• 이 상황은 최초 접촉에 관한 이야기보다 프로이트의 일화에 더 가까움. 우리가 따라갈 수 없는 지능은 외부에서 오는 것이 아니라, 비스듬한 각도에서 포착된 우리 자신의 지능이며 그 모습이 충격적으로 낯설게 느껴짐.

이해와 옳음의 간극

• 수학은 진리의 집합인 동시에 사회적 실천임. 증명은 한 사람의 이해를 다른 사람에게 옮기는 수단이었으며, 옳음은 부분적으로 그 전달의 속성이었음.
• 증명은 다른 사람들이 이해를 완전히 마치기 전에도 세계에 관한 어떤 사실을 받아들이게 하는 수단이었음.
• 튜링의 정지 문제 결정 불가능성 증명은 거의 우스울 정도로 간단해 학생도 오후 한나절이면 따라갈 수 있음. 하지만 증명을 따라가는 일과 그 함의를 파악하는 일은 서로 다른 종류의 이해이며, 그 함의는 증명 자체에 들어 있지 않음.
• 정지 문제 결과가 계산과 수학, 어떤 절차가 알 수 있는 것에 관해 뜻하는 바를 알아내는 데는 수십 년이 걸림.
• 유니크 게임 증명은 이 상황을 뒤집음. 복잡도 이론가들은 추측이 어떤 결과를 함의하는지 20년 동안 연구해 왔으며, 어떤 문제를 효율적으로 근사할 수 없는지에 관한 지도를 만들어 왔음. 이제 그 함의는 손에 쥐었지만, 누구도 아직 이해하지 못하는 증명이라고 주장된 결과가 있음.
• 필즈상 수상자 25명은 이 규모로 생성된 결과가 비옥한 연구 영역에 씨앗을 뿌리는 대신 그 영역을 소진할 수 있다고 이미 경고함. 이것이 실질적인 우려임.
• 인간 존재에 관한 우려는 더 분명함. 이해를 거치지 않고 옳을 수 있는 방식을 만들었으며, 그것을 우리의 이해로부터 만들어냄.

자기 자신에게도 불투명한 인간

• 프로이트라면 이 상황에 놀라지 않았을 것임. 그는 자기 주장을 다소 자기과시적으로나마 틀리지 않게 코페르니쿠스와 다윈에 이은 인간의 자존심에 대한 세 번째 큰 타격으로 놓았음. 자아는 “자기 집의 주인조차 아님”이라는 주장임.
• 우리는 결코 자기 자신에게 투명하지 않았음. 우리가 만든 것이 살펴볼 수 있을 만큼 작았을 때만 투명한 듯 행동할 수 있었음.
• 증명은 우리에게서 나왔지만 우리는 여전히 자기 자신에게 불투명하며, 이제 우리의 산물과 업적에도 불투명함.
• 프로이트는 침대칸 문 거울에서 자기 안의 낯선 이를 만났음. 어제 우리는 깃허브에서 우리의 낯선 이를 만났음.