OEIS Open: How many conjectures can language models turn into theorems?

기술 요약: OEIS OPEN

문제 정의
본 논문은 수학의 미해결 연구 문제를 해결하는 AI 시스템의 능력을 평가하기 위한 체계적인 벤치마크가 부족하다는 점을 다룹니다. HorizonMath 및 FrontierMath: Open Problems (FM:OP)와 같은 기존 벤치마크는 솔루션이 구체적인 객체(예: 그래프, 다항식)로서 찾기는 어렵지만 검증은 쉬운 "생성기-검증기(generator–verifier)" 격차에 의존합니다. 저자는 이러한 접근 방식이 연구 수학의 대다수를 포괄하지 못한다고 주장하며, 연구 수학은 단순히 객체를 제시하는 것이 아니라 일반적인 명제를 증명하는 것을 요구하는 경우가 많기 때문입니다. 또한, 기존 벤치마크는 형식적 증명보다는 수치적 증거를 수용하는 경우가 많고, 오류가 발생하기 쉬운 수작업 기반의 검증 코드를 사용하며, 해결 불가능한 문제를 포함할 수도 있습니다.

저자는 언어 모델(LM)이 Lean 증명 보조 도구 내에서 형식적 증명(또는 반증)을 생성함으로써 자율적으로 수학적 추측을 해결할 수 있는지 테스트하기 위해 설계된 벤치마크인 OEIS OPEN을 제안합니다.

방법론

• 데이터셋 구축: 이 벤치마크는 온라인 정수 수열 백과사전(OEIS)에서 추출한 492개의 미해결 추측들로 구성됩니다. 이 추측들은 원래 Tsoukalas 등[6]에 의해 Lean으로 수집 및 형식화되었습니다. 선택 과정에서는 자동 정리 증명에 적합하면서도 사소하지 않고 수학적으로 흥미롭지만 너무 유명하지는 않은 문제를 찾기 위해 2,649개의 OEIS 추측을 필터링했습니다. 정수 수열에 집중함으로써, 이 문제들이 긴 라이브러리 의존성을 요구하는 복잡한 정의보다는 기초적인 연산을 포함하므로 형식화 오류의 위험을 최소-화했습니다.
• 평가 프레框架 (Framework): 진화적 탐색을 사용하는 AlphaProof Nexus와 같은 특수하고 복잡한 에이전트를 사용했던 이전의 시도들과 달리, 본 평가는 Inspect 라이브러리로 구축된 단순하고 오픈 소스인 에이전트 하네스를 사용합니다. 기본 에이전트는 bash 셸, 텍스트 에디터, 리소스 모니터라는 세 가지 도구를 갖춘 ReAct 스타일의 루프를 활용합니다. 환경에는 Mathlib을 포함한 Lean 4, SageMath, 그리고 Python 라이브러리(sympy, mpmath, numpy)가 포함됩니다.
• 보안 및 검증: "무단 수정"(예: 공리 주입, 환경 조작)을 방-지하기 위해, 각 시도는 세 개의 격리된 Docker 컨테이너에 분산되어 수행됩니다:
  1. 에이전트 컨테이너: 모델이 증명을 생성하는 곳.
  2. 컴파일 컨테이너: 제출된 소스가 바이너리 아티팩트(.olean)로 컴파일되는 깨끗한 환경.
  3. 스코어러(Scorer) 컨테이너: SafeVerify(lean4checker의 변형)를 실행하여 제출된 바이너리를 대상 정리와 대조하여 검증.
  • SafeVerify는 제출물이 표준 세 가지 공리(propext, Quot.sound, Classical.choice) 외에 추가적인 공리를 도입하지 않고, 검증되지 않은 메타프로그래밍 기법에 의ền하지 않으며 정확히 대상 문장을 증명하는지 확인합니다.
• 실험적 변체: 본 연구는 다양한 조건 하에서 모델을 평가합니다:
  • 예산: 전체 세트(492개 문제)에 대해 문제당 $50의 캡을 적용하고, 무작위로 선택된 100개 문제의 하위 집합(OEIS OPEN LITE)에 대해서는 $200의 캡을 적용합니다.
  • 에이전트 복잡도: 단순한 기본 에이전트를 위임(delegation), 지속적 메모리, 할 일 목록(todo-lists) 기능을 갖춘 "DeepAgent" 변체 및 476,000개의 arXiv 수학 논문 스냅샷에 접근할 수 있는 변체와 비교합니다.

주요 결과

• 성능:
  • 전체 OEIS OPEN 세트($50 예산)에서, Claude Opus 4.8은 30%(147/492)의 추측을 해결했습니다. GPT-5.5는 26%, Gemini 3.5 Flash는 22%를 해결했습니다.
  • 이 결과는 유사한 비용에서 동일한 추측 중 9%(44/492)만을 해결한 이전의 최첨단 시스템인 AlphaProof Nexus(Tsoukalas 등)를 크게 상회합니다.
  • OEIS OPEN LITE 하위 집합($200 예산)에서는 성능이 향상되어, Claude Fable 5는 44%의 성공률을, GPT-5.6 Sol은 43%의 성공률을 달성했습니다.
• 비용 효율성: 해결된 추측당 평균 비용은 $6(GPT-5.5)에서 $10(Claude Opus 4.8) 사이였으며, 최대 $47였습니다.
• 복잡성 및 데이터의 영향:
  • 에이전트에게 수학 문헌(476k arXiv 논문)에 대한 접근 권한을 제공하는 것은 LITE 세트의 성능을 향상시키지 않았습니다.
  • 더 복잡한 DeepAgent 아키텍처를 사용하는 것도 단순한 기본 에이전트에 비해 성능을 개선하지 못했습니다.
• 스케일링: 해결률은 지출 예산에 따라 로그 선형적으로 상승하는 것으로 보입니다. 저자는 $200 예산이 있다면 현재 최고의 모델들이 492개 중 약 216개의 추측을 해결할 수 있을 것으로 추정하며(현재$50에서 147개), 이는 추론 컴퓨팅을 더욱 확장하면 더 많은 결과를 얻을 수 있음을 시사하지만, 그 비용은 기하급급수적으로 증가할 것입니다.

의의 및 주장

본 논문은 OEIS OPEN이 고도로 특화되고 맞춤화된 에이전트 아키텍처 없이도 현재의 언어 모델이 적절한 비용으로 자율적으로 미해결 연구 추측을 해결할 수 있음을 보여준다고 주장합니다.

• 자율성: 결과는 언어 모델이 복잡한 맞춤형 시스템에 의해서만 시도되었던 문제들을 해결함으로써 독립적으로 연구 수학의 경계를 넓힐 수 있음을 시사합니다.
• 단순성: 최소한의 "ReAct" 에이전트의 성공은 AI의 "쓰라린 교훈(bitter lesson)"을 뒷받침합니다. 즉, 모델에게 단순하고 일반적인 도구를 제공하는 것이 복잡하고 문제 특화적인 구조를 규정하는 것보다 종종 더 나은 성능을 낸다는 것입니다.
• 벤치마크 유용성: 본 연구는 수치적 증거와 수작업 검증기의 함정을 피하면서, 형식적 증명을 수학적 벤치마킹의 실행 가능하고 엄격한 표준으로 확립합니다.
• 추측의 성격: 저자는 해결된 특정 추측들의 수학적 중요성에 대해 겸허한 태도를 취합니다. 저자는 이 문제들이 수학자들에 의해 제안된 미해결 문제들이지만, 대부분은 이전에 거의 주목받지 못했을 가능성이 높다고 언급합니다. 이 데이터셋은 유명하고 높은 프로필을 가진 문제(예: 리만 가설)를 푸는 테스트라기보다는 "열린 연구"의 대리 지표 역할을 합니다.

한계점
저자는 다음과 같은 몇 가지 한계를 인정합니다:

1. 형식화 오류 위험: 정수 수열이 이 위험을 줄여주기는 하지만, 데이터셋의 일부 추측은 Lean에서 잘못 형식화되었을 수 있으며, 이로 인해 의도보다 해결하기 쉬울 수 있습니다.
2. 범위: 이 벤치마크는 Mathlib에서 형식화 가능한 문제들로 제한되어 있어, 모든 연구 수학을 다룰 수는 없습니다.
3. 데이터 누수: 일단 추측이 해결되면, 그 증명이 미래 모델의 학습 데이터에 포함되어 향다면 성능 지표를 부풀릴 가능성이 있습니다.
4. 축소(Reductions): 이 벤치마크는 추측 또는 그 부정을 증명하는 것만을 수용하며, 수학자들이 높게 평가할 수 있는 다른 유명한 미해결 문제로의 축소를 인정하지 않습니다.

결론적으로, 본 논문은 OE-IS OPEN을 견고하고 안전하며 확장 가능한 벤치마크로 제시하며, 이를 통해 최소한의 에이전트 복잡성으로도 자율적인 수학 연구를 수행할 수 있는 범용 언어 모델의 성장하는 능력을 밝혀냈습니다.