Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

본 논문은 Lean 4 에서 형식적으로 검증된 정리와 증명들을 반복적으로 대규모 언어 모델에 피드백함으로써 새로운 증명하기 어려운 수학적 추측의 발견률과 성공을 획기적으로 향상시키는 컨텍스트 학습을 활용하는 추측-증명 루프 (CPL) 라는 파이프라인을 소개한다.

핵심

매우 똑똑하지만 약간 건망증이 있는 로봇에게 복잡한 수학 퍼즐을 푸는 법을 가르치려 한다고 상상해 보세요. 그 로봇은 대규모 언어 모델 (LLM) 이며, 퍼즐은 Lean이라는 엄격한 컴퓨터 언어로 작성된 형식 수학 증명들입니다.

이 논문은 이 로봇을 가르치는 새로운 방법을 소개하는데, 이를 **가설 설정 - 증명 루프 (Conjecturing-Proving Loop, CPL)**라고 부릅니다. 간단한 비유를 통해 그 작동 원리를 설명해 보겠습니다.

문제: "추측하고 확인하기" 함정

보통 사람들이 AI 에게 수학을 시킬 때, 퍼즐을 추측하고 한 번에 해결하도록 요청합니다.

• 비유: 학생에게 "수학 문제를 만들고 즉시 풀어라"고 요청한다고 상상해 보세요.
• 문제점: 학생은 게을러집니다. 해결하기 쉬운 문제 (예: "2 + 2 = 4") 를 작성합니다. 왜냐하면 그 문제들이 풀기 쉽기 때문입니다. 그들은 실패할 수 있다는 것을 알기 때문에 어려운 문제를 피합니다. 그 결과 AI 는 수천 개의 쉽고 지루한 증명들을 생성하게 되며, 어렵고 흥미로운 것들은 놓치게 됩니다.

해결책: "이 단계 춤" (CPL)

저자들은 이 과정을 **가설 설정자 (아이디어 생성자)**와 **증명자 (해결사)**라는 두 가지 명확한 역할로 나눕니다.

1. 가설 설정자 (건축가): AI 의 이 부분은 기존 수학 규칙들의 도서관을 살펴보고 새로운 아이디어 (가설) 를 생각해 냅니다. 아직 이를 해결하려고 시도하지는 않습니다. 단지 적어 두기만 합니다.
2. 증명자 (건설가): 이 부분은 아이디어를 받아들이고 이를 위한 증명을 구축하려고 시도합니다. 실패하면 다시 시도합니다. 성공하거나 시도 횟수가 소진될 때까지 계속 시도합니다.
3. 도서관 (기억): 증명자가 성공적으로 증명을 구축할 때마다, 그 증명은 도서관에 추가됩니다.

마법의 재료: 인-컨텍스트 학습 (In-Context Learning)
여기가 교묘한 부분입니다. 증명자는 원래 수학 규칙들만 보는 것이 아닙니다. 그것은 현재 세션 동안 이미 성공적으로 구축한 증명들의 도서관을 봅니다.

• 비유: 학생이 시험을 치른다고 상상해 보세요. 옛날 방식에서는 시험 시작 전에 암기한 것만 의존해야 했습니다. 하지만 이 새로운 방식에서는 학생이 문제를 올바르게 풀 때마다, 다음 문제를 tackling 하기 전에 자신의 해답을 읽을 수 있습니다. 그들은 자신의 최근 성공들로부터 "요령"과 "전략"을 배웁니다.

그들이 발견한 것

연구자들은 AI 가 아직 잘 알지 못하는 몇 가지 까다로운 위상수학 개념 (형태와 공간을 다루는 수학의 한 분야) 에 대해 이를 테스트했습니다.

• 양 vs 질: 옛날 방식 (한 번에 추측하고 해결하기) 은 더 많은 전체 정리들을 생성했지만, 대부분은 짧고 쉬웠습니다. 새로운 방식 (CPL) 은 더 적은 전체 정리들을 생성했지만, 훨씬 더 어렵고 길었습니다.
• 큰 승리: 새로운 방식은 "알파-열린 집합 (alpha-open sets)"에 관한 구체적이고 어려운 정리를 성공적으로 발견했는데, 옛날 방식은 20 번 시도한 후에도 단 한 번도 찾지 못했습니다.
• 성공으로부터의 학습: AI 에게 자신의 이전 증명들 도서관을 "요약지 (cheat sheet)" (컨텍스트) 로 제공했을 때, 그 컨텍스트 없이는 풀 수 없었던 어려운 정리들을 증명할 수 있었습니다. AI 가 평범한 영어로 정리를 증명하지 못했더라도, 유사한 성공적인 증명들을 본 후에는 Lean 코드로는 증명할 수 있었습니다.

결론

이 논문은 "아이디어 생성"과 "증명 해결"을 분리하고, AI 가 실시간으로 자신의 검증된 성공들로부터 학습하도록 함으로써, 그렇지 않으면 놓쳤을 더 어렵고 복잡한 수학 진리들을 발견하게 할 수 있다고 주장합니다. 마치 AI 에게 최종 시험을 치르기 전에 자신의 숙제를 공부하게 하여 출발선을 앞당겨 주는 것과 같습니다.

참고: 이 논문은 형식 수학 밖의 다른 실생활 응용 (의료 진단, 금융 예측 등) 에 대해 이 방법이 작동한다고 주장하지 않으며, 오직 수학 정리 생성 및 검증에 대한 이 방법에만 엄격하게 초점을 맞춥니다.

기술 요약

기술 요약: 컨텍스트 내 증명 학습을 통한 Lean 기반 LLM 을 활용한 새로운 정리 발견

문제 제기
대규모 언어 모델 (LLM) 은 형식적 정리 증명 분야에서 유망한 가능성을 보여주었으나, 다음과 같은 중대한 과제에 직면해 있습니다: 환각 현상이 발생할 수 있으며, 수학적 추측과 그 증명을 동시에 생성하는 것은 종종 사소하거나 쉬운 정리로 수렴하게 됩니다. 기존 접근법은 일반적으로 지도 미세 조정 (SFT) 이나 검증된 보상을 통한 강화 학습 (RLVR) 에 의존하는데, 이는 방대한 양의 훈련 데이터를 필요로 하며 폐쇄형 소스 모델에는 적용하기 어렵습니다. 또한, 현재 방법론들은 '증명하기 어려운' 정리를 발견하는 데 어려움을 겪는데, 이는 정리 생성 확률이 해당 정리를 즉시 증명할 수 있는 성공률에 크게 가중치를 두기 때문에 탐색이 단순하고 짧은 증명들로 붕괴되기 때문입니다.

방법론: 추측 - 증명 루프 (CPL)
저자들은 Lean 4 에서 수학적인 추측을 자동으로 생성하고 이를 검증하도록 설계된 파이프라인인 **추측 - 증명 루프 (Conjecturing-Proving Loop, CPL)**를 제안합니다. 이 프레임워크는 추측 생성과 증명 생성을 분리하며, 두 단계 모두에서 이전에 검증된 정리들의 라이브러리를 컨텍스트로 활용합니다.

이 파이프라인은 네 가지 주요 구성 요소로 작동합니다: 추측자 (Conjecturer, LLM 에이전트), 증명자 (Prover, LLM 에이전트), Lean 서버, 그리고 라이브러리 (Lean 코드 데이터).

1. 추측 단계: 추측자는 현재 라이브러리를 기반으로 Lean 4 형식의 새로운 수학 명제를 생성합니다. 이는 Mathlib4 나 현재 라이브러리에 있는 기존 정리들로 이미 증명 가능한지 확인하여 문법적 유효성과 신규성을 보장하기 위해 Lean 서버에 질의합니다.
2. 증명 단계: 각 유효한 추측에 대해 증명자는 형식적 증명을 구성하려 시도합니다. 핵심적으로, 증명자는 이전에 검증된 정리와 증명을 포함한 라이브러리를 컨텍스트로 부여받습니다. 이를 통해 LLM 은 모델 재훈련 없이 **컨텍스트 내 학습 (in-context learning)**을 통해 증명 전략을 학습할 수 있습니다. 증명자는 Lean 서버의 오류 메시지를 활용하여 시도를 정제하며, 최대 시도 횟수 (실험에서는 16 회로 설정) 까지 반복합니다.
3. 반복: 검증된 추측과 증명의 쌍은 라이브러리에 추가되며, 이는 이후 반복을 위한 컨텍스트로 활용됩니다.

이러한 분리는 시스템이 증명 난이도에 따라 탐색 자원을 할당할 수 있게 합니다. 명제와 증명을 동시에 생성하는 단순 루프 (SL) 와 달리, CPL 은 명제를 폐기하기 전에 단일 명제에 대해 여러 번의 증명을 시도합니다. 이는 생성된 정리의 분포를 단순히 증명하기 쉬운 것들이 아니라 증명 가능하지만 어려운 것들로 이동시킵니다.

주요 기여

1. 파이프라인 제안: 추측 생성과 증명 생성을 분리하여 더 길고 복잡한 증명들의 발견을 가능하게 하는 프레임워크인 CPL 의 도입.
2. 폐쇄형 소스 모델을 위한 컨텍스트 내 학습: 자체적으로 생성된 이전에 검증된 출력물로부터의 컨텍스트 내 학습을 통해 ChatGPT-o3 와 같은 폐쇄형 LLM 이 증명 능력을 향상시킬 수 있음을 입증하여, 매개변수 업데이트나 미세 조정의 필요성을 제거함.
3. 이론적 및 실증적 검증: 동시 생성 프레임워크에 비해 CPL 이 증명하기 어려운 정리를 생성할 가능성을 높인다는 이론적 모델을 제시함. 실험적으로는 CPL 이 기저 프레임워크가 찾지 못한 특정 연구 수준의 정리를 성공적으로 재발견했음을 검증함.

실험 결과
저자들은 Mathlib 에 정의되었으나 라이브러리에 아직 포함되지 않은 위상적 개념 (반개방성, $\alpha$-개방성, 그리고 전개방성) 을 사용하여 CPL 을 단순 루프 (SL) 기저 모델과 비교 평가했습니다. 목표는 두 개의 $\alpha$-개방 집합의 교집합이 $\alpha$-개방임을 주장하는 정리였습니다.

• 발견률: 20 회 실험에서 CPL 은 목표 정리를 5 회 발견했습니다. 반면, 평균적으로 훨씬 더 많은 정리 (106 개 대비 328 개) 를 생성한 SL 프레임워크는 목표 정리를 단 한 번도 생성하지 못했습니다. 피셔의 정확 검정 (Fisher's exact test) 은 이 차이가 통계적으로 유의미함을 확인했습니다 ($p = 0.024$).
• 증명 길이: CPL 은 SL 에 비해 문자 수 기준으로 훨씬 더 긴 증명 길이를 가진 정리를 생성했는데, 이는 프레임워크가 더 어려운 증명들로 초점을 이동시킨다는 이론적 주장을 뒷받침합니다.
• 컨텍스트의 효과성:
  • 재증명: 생성된 정리를 재증명할 때, 라이브러리를 컨텍스트로 제공하면 성공률이 91% 에서 99% 로 증가했습니다 ($p = 4 \times 10^{-35}$).
  • 목표 정리: 목표인 $\alpha$-개방 교집합 정리를 재증명하려 할 때, 생성된 라이브러리를 컨텍스트로 제공받은 증명자는 80 회 시도 중 7 회 성공했습니다. 라이브러리 없이 시도할 경우 실패율은 100% 였습니다.
  • 자연어 기저 모델: 자연어로 정리를 증명해 달라고 요청했을 때, ChatGPT-4o 는 종종 정리가 거짓이라고 판단하거나 잘못된 증명을 제공했으며, ChatGPT-o3 는 일관되게 정리가 거짓이라고 판단했습니다. 이는 해당 정리가 모델들의 사전 훈련된 지식 범위를 벗어났음을 시사합니다. Lean 4 에서의 성공은 생성된 라이브러리로부터의 증명 전략에 대한 컨텍스트 내 학습에 기인했습니다.

의의 및 주장
본 논문은 CPL 이 자체 생성된 검증된 증명들로부터의 컨텍스트 내 학습을 활용함으로써 LLM 이 비사소한 정리를 발견하는 데 있어 직면한 한계를 효과적으로 해결한다고 주장합니다. 저자들은 이 접근법이 LLM 에게 명시적으로 알려지지 않은 개념에 대한 명제들을 생성함으로써 Mathlib 과 같은 형식 수학 라이브러리를 자동으로 확장할 수 있게 한다고 강조합니다. 이 연구는 추측 단계와 증명 단계를 분리하고 반복적인 컨텍스트 충전을 결합하는 것이, 특히 전통적인 훈련 방법이 적용되지 않는 폐쇄형 소스 모델의 경우 신경망 정리 증명에 있어 실현 가능한 전략임을 시사합니다. 저자들은 겸손한 입장을 유지하며, 프레임워크가 알려진 연구 수준의 정리를 성공적으로 재발견했지만, 더 깊고 통찰력 있는 수학 명제를 위한 생성 과정을 정교화하기 위해서는 향후 연구가 필요하다고 명시합니다.