기술적 요약: Formal Conjectures

문제 제기

자동 추론 시스템, 특히 대규모 언어 모델 (LLM) 이 발전함에 따라 수학적 추론을 위한 기존 벤치마크는 다음과 같은 치명적인 한계에 직면해 있습니다:

1. 데이터 유출: 벤치마크 문제의 해결책이 종종 온라인에 공개되어, 진정한 추론과 암기를 구분하기 어렵습니다.
2. 비공개 평가: 유출을 방지하기 위해 일부 벤치마크는 평가 세트를 비공개로 유지하여 개방적이고 재현 가능한 연구를 방해합니다.
3. 과도하게 단순화된 기준: 많은 벤치마크가 복잡한 다단계 증명보다는 숫자와 같은 단순하고 기계가 확인 가능한 최종 답변을 검증하는 데 의존합니다.
4. 포화 상태: 기존 형식 벤치마크 (예: MiniF2F, PutnamBench) 는 포화 상태에 이르러, 모델들이 routinely 문제의 99% 이상을 해결함으로써 연구 수준의 수학에서의 진전을 측정하지 못하게 합니다.

AI 시스템의 형식 수학적 발견 능력을 정확하게 평가하기 위해, 기계가 확인 가능한 언어로 형식화된 연구 수준의 수학 문제로 구성된 오염이 전혀 없고 진화하는 벤치마크가 시급히 필요합니다.

방법론

저자들은 Lean 4의 Mathlib 라이브러리를 사용하여 2,615 개의 수학 문제 진술을 형식화한 오픈소스 진화형 벤치마크인 Formal Conjectures를 소개합니다.

데이터셋 구성

벤치마크는 두 가지 주요 범주로 나뉩니다:

• Research Open (1,029 개 문제): Erdős 문제, Kourovka Notebook, arXiv, MathOverflow 등 활발한 연구 분야에서 출처한 미해결 추측들입니다. 훈련 데이터에 해결책이 존재하지 않으므로 증명 발견을 위한 오염이 전혀 없는 테스트베드로 기능합니다.
• Research Solved (836 개 문제): 알려진 비형식적 증명을 가진 확립된 정리들로, 자동 형식화 능력을 벤치마크하는 데 사용됩니다.
• Other Statements (750 개 문제): 형식화 정확성을 검증하기 위해 교과서 수준의 문제, API 정의, 테스트 보조 정리 등을 포함합니다.

형식화 파이프라인 및 품질 관리

정확성을 보장하고 오형식화를 최소화하기 위해 이 프로젝트는 엄격한 협력 파이프라인을 채택합니다:

• 인간 개입 검토: 모든 기여물은 Lean 전문 지식과 도메인별 수학 지식을 모두 갖춘 인간에 의한 코드 검토를 거칩니다.
• AI 지원 감사: 자동 증명기 (예: AlphaProof) 와 LLM 을 사용하여 증명과 반증을 시도합니다. "해결된" 문제에 대한 성공적인 반증이나 미해결 문제의 증명 실패는 종종 오형식화를 드러냅니다.
• 오형식화 분류 체계: 저자들은 오류를 위한 3 단계 분류 체계를 정의합니다:
  1. 번역: 정확한 비형식적 진술을 Lean 으로 번역하는 과정의 오류.
  2. 미세명시: 비형식적 진술에 필요한 세부 사항이 부족한 경우의 오류.
  3. 출처: 비형식적 출처 텍스트 자체가 잘못되었거나 모호한 경우의 오류.
     현재까지 291 건의 오형식화가 식별되어 수정되었습니다.
• answer(sorry) 메커니즘: 맞춤형 Lean elaborator 는 특정 답변 (예: 숫자 또는 진리값) 의 발견과 그 정확성 증명을 분리합니다. 이를 통해 해결사는 증명 시도 전에 answer(sorry) 를 True, False, 또는 숫자와 같은 구체적인 값으로 대체할 수 있어, 값 발견과 검증을 분리합니다.
• @[formal_proof] 속성: 저장소를 경량화하기 위해 해결된 문제에 대한 증명은 종종 직접 저장되지 않고 외부에 링크되며, 증명 상태 (내부, 링크된 Lean 4, 또는 기타 시스템) 를 추적하기 위해 속성을 사용합니다.

평가 프레임워크

벤치마크는 객관적이고 엄격한 검증을 위해 Lean 4 커널을 활용합니다. 금지된 공리 (예: sorry) 에 의존하지 않고 커널이 증명 항을 수용할 때만 해결책이 정확합니다.

• 고정된 부분 집합: 저장소의 진화하는 특성에도 불구하고 안정적이고 재현 가능한 비교를 가능하게 하기 위해 저자들은 고정된 부분 집합을 제공합니다: FC100OpenSet1(100 개 미해결 문제) 과 FC100SolvedSet1(100 개 해결된 문제).
• 버전 관리: 릴리스는 특정 Mathlib/Lean 툴체인에 대한 특정 문제 세트를 고정하기 위해 2 부분 명명 체계 (예: bench-v1-lean4.27.0) 로 태그됩니다.

주요 결과

이 논문은 최첨단 시스템을 사용하여 고정된 부분 집합에 대한 기준 결과를 보고합니다:

• FC100OpenSet1 (증명 발견): 첫 번째 태그 릴리스 기준으로 모든 시스템의 기준은 **0%**이며, 이는 해당 집합의 오염이 전혀 없는 특성을 확인합니다.
• FC100SolvedSet1 (자동 형식화):
  • AlphaProof (1k 시뮬레이션): 45.0% 해결률.
  • AlphaProof (16k 시뮬레이션): 50.0% 해결률로, 증가된 컴퓨팅 자원에 따른 명확한 확장 신호를 보여줍니다.
  • DeepMind Prover Agent (개발 버전): 66.0% 해결률로, 모델 아키텍처와 방법론의 개선을 보여줍니다.

저자들은 이 벤치마크가 이미 실제 수학 발견을 촉진했다고 언급하며, 여기에는 AI 가 생성한 증명이 형식 진술을 정제하기 위한 감사 메커니즘으로 작용한 특정 미해결 추측 (예: Erdős Problem 124) 의 해결이 포함됩니다.

중요성과 주장

이 논문은 Formal Conjectures를 수학에 대한 AI 평가의 필수적인 진화로 위치시킵니다:

1. 오염이 전혀 없는 벤치마크: 데이터 유출 우려를 제거하고 연구 수준의 문제에서 진정한 수학 발견을 위한 첫 번째 대규모, 개방적이고 엄격한 테스트베드를 제공합니다.
2. 통합 인터페이스: 문제를 형식화하는 수학자와 이를 해결하려는 AI 시스템을 연결하는 중앙 허브 역할을 하여, 동시 감사와 신속한 확산을 촉진합니다.
3. 반복적 개선: AI 가 생성한 증명과 반증을 피드백 루프로 사용하여 벤치마크 자체의 정확성을 반복적으로 개선하고, 저장소와 원래 비형식적 문헌의 오형식화를 수정합니다.
4. 점재 가능한 신호: 고정된 부분 집합과 버전화된 스냅샷을 제공함으로써, 모델이 발전함에 따라 자동 추론 능력의 "점재 가능한 신호"를 측정하는 표준화되고 재현 가능한 방법을 제공합니다.
5. 형식 수학의 확장: FormalConjecturesForMathlib 디렉토리를 통해 필요한 정의와 보조 정리를 Mathlib 로 업스트림함으로써 더 넓은 형식 수학 생태계에 기여합니다.

저자들은 이 자원이 현재 진전을 측정할 뿐만 아니라 인간 전문 지식과 자동 추론을 연결함으로써 형식 수학적 발견의 최전선을 가속화하는 것을 목표로 한다고 결론지었습니다.