TL;DR

  • 수학 정리를 생성하고 증명하는 대형 언어 모델(LLM)이 늘어나는 가운데, 정리의 증명 길이와 진술 길이의 비율을 최적화하면 흥미로운 정리를 만들고 인간이 목표를 지정하지 않아도 확장되는 수학 라이브러리를 구축할 수 있음.
  • 정리의 내재적 흥미도를 증명 길이와 진술 길이의 비율로 정의하며, 이 지표가 정리의 후속 활용도를 나타내는 외재적 측정치와 강하게 상관됨.
  • 전제 집합이 주어졌을 때 증명의 난도를 흥미도와 활용도를 계산하는 기본 요소로 삼고, 최첨단 범용 모델보다 증명 난도를 정확히 예측하는 270억 파라미터 모델을 학습함.
  • 이 지표에 최적화한 모델은 더 흥미로운 정리를 생성하며, Mathlib과 실질적으로 또는 완전히 겹치는 정리의 비율을 91.9%에서 30.6%로 낮춤.
  • 시스템은 후보 정리를 생성하고 가장 흥미로운 정리를 선택해 자체 확장 수학 라이브러리에 반복적으로 추가하며, 추측 순위화와 형식 라이브러리 내 증명 탐색에 실용적인 신호를 제공함.

연구 배경

  • 대형 언어 모델(LLM)은 수십 년 동안 미해결 상태였던 문제를 포함해 고급 수학 문제를 해결하는 능력을 키우고 있으며, 이는 전례 없는 규모로 수학 지식을 확장할 가능성을 열어 줌.
  • 그러나 LLM이 더 많은 정리를 추측하고 증명할 수 있게 되더라도, 새로 생성된 수학 지식이 흥미롭거나 유용한지는 여전히 열린 문제임.

정리의 흥미도 측정

  • 정리의 내재적 흥미도를 증명 길이를 정리 진술의 길이로 나눈 값으로 정의함.
  • 이 내재적 지표가 정리의 후속 활용도를 나타내는 외재적 측정치와 강하게 상관됨을 보임.
  • 전제 집합이 주어졌을 때의 증명 난도를 이 지표들을 계산하는 데 유용한 기본 요소로 식별함.

모델 학습과 생성 결과

  • 증명 난도를 예측하는 270억 파라미터 모델을 학습했으며, 예측 정확도가 최첨단 범용 모델보다 높음.
  • 흥미도 지표를 최적화하면 더 흥미로운 정리를 생성하는 모델이 만들어짐.
  • Mathlib과 실질적으로 또는 완전히 겹치는 정리의 비율이 91.9%에서 30.6%로 감소해, 학습 분포 밖의 수학을 생성할 수 있음을 보임.

자체 확장 수학 라이브러리

  • 시스템은 후보 정리를 생성하고, 후보 가운데 가장 흥미로운 정리를 선택하며, 이를 바탕으로 자체 확장 수학 라이브러리를 반복적으로 구축함.
  • 제안한 지표는 추측의 순위를 매기고 형식 수학 라이브러리 안에서 증명 탐색을 이끄는 실용적이고 정량적인 신호임.
  • 이 프레임워크는 사람이 목표 정리를 제공하지 않아도 가치 있는 진술을 선택할 수 있는, 자체 확장 및 기계 검증 수학 라이브러리로 나아가는 경로를 제시함.

논문 정보

  • 제목: *Learning to Discover Interesting Mathematics*
  • 저자: Niket Patel, Ahmad Rammal, Amaury Hayat, Remi Munos, Julia Kempe
  • 제출일: 2026년 9월 23일
  • arXiv:2609.28603 [cs.LG]
  • DOI: https://doi.org/10.48550/arXiv.2609.28603