Release Date: 2023.03
Release Date: 2023.08
1. 서론
현대 수학에서 증명의 복잡성이 증가함에 따라 피어 리뷰에 상당한 도전이 되고 있습니다. 이런 챌린지를 극복하기 위해 Lean, Isabelle, Coq와 같은 형식적 수학 언어가 개발되었습니다. 이 언어들은 컴퓨터 검증 가능한 증명을 생성하는 데 도움을 주지만, 형식적 증명을 작성하는 것은 많은 노력과 전문 지식을 요구하며, 경험 많은 수학자들에게조차 챌린지일 수 있습니다. 이런 배경에서 자동 정리 증명의 중요성이 증가하고 있습니다.
2. 배경 및 관련 작업
자동 정리 증명은 인공지능 연구의 중요한 분야로 초기의 노력은 간단한 논리 프레임워크에 초점을 맞추었습니다. 이는 E와 Vampire와 같은 고효율 일차 정리 증명기의 개발로 이어졌습니다.
그러나 이런 도구들은 현대 증명 보조 도구에서 흔히 발견되는 복잡한 정리들을 다루는 데에는 약간 부족했습니다. 최근에는 심층 학습 모델과 모델 지향 검색 기술의 등장으로 이 분야가 새로운 활력을 얻었습니다.
고등학교 및 대학 수준의 수학 경시 문제를 형식적 진술로 변환하고, 이를 대규모 언어모델을 사용하여 증명을 생성하는 방법을 제안합니다. 접근 방식은 다음과 같은 수학적 구조를 따릅니다.
3. 접근 방식
접근 방식은 크게 네 가지 주요 과정으로 구성되며, Figure 1에서 시각적으로 제시되어 있습니다. 첫 단계에서는 대량의 비형식적 수학 문제로부터 형식적 수학 명제를 생성하는 작업에 집중합니다. 이후 자동 형식화된 명제들은 모델 점수화 및 가설 배제 방법을 통해 고품질의 명제를 선별합니다. 이 명제들은 DeepSeek-Prover 모델에 의해 증명되며, Lean 41이라는 형식 검증기로 그 정확성이 검증됩니다. 이 데이터들은 DeepSeek-Prover의 파인튜닝을 위한 합성 데이터로 사용됩니다. DeepSeek-Prover의 성능이 향상됨에 따라 이전에 설명된 과정을 반복합니다. 이 사이클은 DeepSeek-Prover의 개선이 미미해질 때까지 계속됩니다. 특히 증명 효율을 높이기 위해 원본 명제와 그 부정을 동시에 증명하는 방법을 사용하여, 원본 명제가 유효하지 않을 경우 즉시 그 부정을 증명함으로써 원본 명제를 신속하게 배제할 수 있는 장점이 있습니다.
3.1 자동 형식화 (Autoformalization)
비형식적 수학 문제로부터 형식적 명제 데이터를 생성하는 것은 상당한 양의 형식 명제가 필요합니다. 인터넷은 자연 언어로 표현된 수학 문제로 가득 차 있으며, 이를 자동 형식화함으로써 방대한 형식 명제 저장소를 생성할 수 있습니다. 특히 고등학교 및 대학 수준의 경쟁 문제가 주요 대상이며, 대수학과 수론을 중심으로, 조합론, 기하학, 통계학 문제도 다룹니다. 이런 문제들은 복잡한 해결 기법을 포함하고 있어, 정리 증명 능력을 개선하는 데 우수한 데이터를 구성합니다. 데이터셋은 온라인 자료에서 고등학교 및 대학의 연습문제, 시험, 경쟁 문제를 추출하여 구성되었습니다. 이 데이터셋은 869,659개의 고품질 자연 언어 수학 문제를 포함합니다.
3.2 품질 필터링 (Quality Filtering)
자동 형식화된 명제의 품질이 부적합한 문제를 해결하기 위해 점수 기준을 개발하고 miniF2F-valid 예제를 사용하여 DeepSeek-Prover 모델이 이런 명제의 내용 및 품질을 평가하도록 했습니다. 모델은 “우수”, “좋음”, “평균 이상”, “보통”, “미흡”의 범주로 각 형식 명제의 품질을 분류하도록 지시받았습니다. “보통” 또는 “미흡”으로 평가된 명제는 배제되었습니다. 또한 일관성 없는 가설에 기반한 명제는 유효하지 않은 가설임을 증명함으로써 배제되었습니다.
3.3 명제 증명 (Statement Proving)
고품질의 형식 명제가 생성된 후, 모델은 이런 명제의 증명을 탐색합니다. 전통적으로 언어 모델은 무차별적으로 증명 시도를 반복하며, 이는 자원 낭비가 심각합니다. 명제와 그 부정 사이의 논리적 대칭을 활용하여 증명 합성을 가속화했습니다. 이런 이중 접근 방식은 데이터 증강의 한 형태로, 모델에 의해 잘못 형식화된 원본 명제들도 데이터셋에 포함됩니다.
3.4 반복적 개선 (Iterative Enhancement)
DeepSeek-Prover의 성능 개선을 위해 반복적으로 모델을 파인튜닝하고 적용합니다. 이 반복 과정은 모델이 강화되고 효율이 향상됨에 따라 계속됩니다. 이 과정을 통해 모델은 점점 더 높은 품질의 정리-증명 쌍을 생성합니다.
4. 실험 (Experiments)
4.1 실험 설정 (Experimental Setup)
DeepSeek-Prover 모델은 수학 관련 토큰 1200억 개가 포함된 코퍼스에서 사전 훈련된 DeepSeekMath-Base 7B 모델을 기반으로 합니다. 이 모델은 글로벌 배치 크기 512와 일정한 학습률 \(1 \times 10^{-4}\)를 사용하여 파인튜닝되었습니다. 합성 데이터와 함께 6000의 워밍업 단계가 포함되었습니다. 성능 평가는 GPT-3.5와 GPT-4 등 다양한 베이스라인과 비교하여 이루어졌습니다.
4.2 주요 결과 (Main Results)
이 연구는 대수학과 수론에서 복잡한 수학 문제를 다룹니다. miniF2F와 FIMO 벤치마크를 사용하여 모델의 정리 증명 효과를 평가했습니다. ‘pass@k’ 메트릭은 모델이 생성한 첫 k 시도 중 최소 한 개의 유효한 증명을 찾는 시나리오를 나타냅니다.
miniF2F 벤치마크 결과
DeepSeek-Prover는 miniF2F-valid에서 60.2%, miniF2F-test에서 52.0%의 누적 점수로, GPT-4와 다른 방법들을 크게 앞섰습니다. 최고의 트리 탐색 방법인 Hypertree Proof Search조차 miniF2F-valid에서 최대 58.6%, miniF2F-test에서 41.0%의 성능을 보였습니다. DeepSeek-Prover의 확장성은 증가하는 계산 자원과 함께 성능이 개선되어, 복잡한 증명 시나리오를 효과적으로 처리함을 보여줍니다.
FIMO 벤치마크 결과
FIMO 벤치마크는 IMO 숏리스트에서 번역된 149개의 공식 문제로 구성되어 있습니다. 본 논문의 방법은 100번의 시도로 4개의 정리를 성공적으로 증명했으며, GPT-4는 단 한 개의 정리도 증명하지 못했습니다. 시도 횟수를 4096회로 늘렸을 때 추가로 하나의 정리를 더 증명하는 데 성공했습니다.
4.3 유효성 분석 (Ablation Studies)
4.3.1 대규모 자동 형식화의 효과성 (The Effectiveness of Large-scale Autoformalization)
자동 형식화된 데이터셋과 전통적인 데이터셋을 비교 분석한 결과, 자동 형식화 데이터로 훈련된 모델이 mathlib 데이터로만 훈련된 모델보다 향상된 성능을 보였습니다.
4.3.2 형식적 명제 평가의 효과성 (The Effectiveness of Formal Statements Scoring)
고점수 증명 데이터와 저점수 증명 데이터를 동일한 양으로 사용하여 파인튜닝한 결과, 고품질의 데이터를 사용한 모델이 낮은 품질의 데이터를 사용한 모델보다 4.5% 높은 성능을 보였습니다. 이는 모델이 명제의 품질을 정확하게 평가하고 효과적으로 필터링하는 데 유용함을 강조합니다.
4.3.3 반복적 강화의 효과성 (The Effectiveness of Iterative Enhancement)
데이터 합성에서의 반복 횟수와 정리 증명 성능 간에 명확한 상관관계가 있음을 보여줍니다. 연속적인 반복은 모델의 복잡한 증명 처리 능력을 파인튜닝할 뿐만 아니라 생성된 합성 데이터의 품질과 양을 크게 증가시킵니다.
4.3.4 합성 정리 증명 데이터의 확장성 (The Effectiveness of Scaling Synthetic Theorem Proving Data)
합성 정리 증명 데이터의 크기와 모델 효과성 사이에는 분명한 상관관계가 있습니다. 데이터 크기가 지수적으로 증가함에 따라 miniF2F 벤치마크에서의 성능이 비례적으로 향상되었습니다. 이는 대규모 데이터셋이 자동 형식화 질문에서 모델의 숙련도를 향상시키는 데 결정적인 중요성을 갖습니다.
5. 사례 연구 (Case Studies)
5.1 자동 형식화된 정리와 완성된 증명 (Autoformalized Theorem with Complete Proof)
문제: 다음 행렬의 행렬식이 0임을 증명하시오.
\[\begin{bmatrix} 1 & \cos(a-b) & \cos(a) \\ \cos(a-b) & 1 & \cos(b) \\ \cos(a) & \cos(b) & 1 \end{bmatrix}\]자동 형식화된 정리 (Lean):
example (a b : ℝ) :
Matrix.det ![![1, Real.cos (a - b), Real.cos a], ![Real.cos (a - b), 1, Real.cos b], ![Real.cos a, Real.cos b, 1]] = 0
이 접근 방식은 행렬과 그 행렬식의 대수적 표현을 Lean의 형식적 언어로 효과적으로 번역합니다. 이 자동 형식화 과정은 원본 수학 명제의 본질을 잘 포착하여, 실수 \(a\)와 \(b\)에 의존하는 3×3 행렬을 정의하고 그 행렬식이 0임을 언급합니다.
5.2 가설이 일관성 없는 정리의 자동 형식화 (Autoformalization of Theorem with Inconsistent Hypotheses)
문제: 실수 \(D\)와 비제로 실수 \(a, b, c\)에 대해, 다음 행렬의 행렬식이 \(D\)와 같음을 가정할 때, \(D^2 = 154\)임을 증명하시오.
\[\begin{bmatrix} a & b & c \\ 1 & 4 & 9 \\ 3 & 1 & 2 \end{bmatrix}\]자동 형식화된 정리 (Lean)
example (D : ℝ) (h₀ : ∀ a b c : ℝ, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 →
Matrix.det ![![a, b, c], ![1, 4, 9], ![3, 1, 2]] = D) : D ^ 2 = 154
초기 자동 형식화는 \(D^2 = 154\)가 모든 비제로 실수 \(a, b, c\)에 대해 일반적으로 적용된다고 잘못 가정합니다. 이 가정은 문제의 주장을 지지하지 않습니다. 모델은 이 불일치를 식별하고 가설의 터무니없음을 보여주는 반례를 제공합니다.
example (D : ℝ) (h₀ : ∀ a b c : ℝ, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 →
Matrix.det ![![a, b, c], ![1, 4, 9], ![3, 1, 2]] = D) : False := by
have h₁ := h₀ 1 2 3
have h₂ := h₀ 1 4 9
simp [Matrix.det_fin_three] at h₁ h₂
linarith
이런 예는 모델이 증명을 검증하고 가설의 불일치를 효과적으로 식별하는 능력을 잘 보여줍니다. 추가적인 세부 사항은 Appendix A.2에서 찾아볼 수 있습니다.