논문리뷰

Math : 논문리뷰 : Gold-medalist Performance in Solving Olympiad Geometry with AlphaGeometry2

AI바라기 2025. 2. 7. 15:44

Overall Summary:

AlphaGeometry2 는 domain language 확장, symbolic engine 고속화, synthetic data 개선, novel search algorithm 도입, Gemini 기반 language model 활용 등 다각적인 개선을 통해 Olympiad geometry 문제 해결 성능을 gold medalist 수준으로 끌어올렸다. 특히 neuro-symbolic approach 와 knowledge sharing search 는 복잡한 geometry 문제 해결에 효과적임을 입증했으며, fully automated geometry problem solving system 구축 가능성을 제시했다. 향후 domain language 확장, advanced geometry technique 통합, auto-formalization 및 full proof generation 연구를 통해 더 발전된 geometry AI system 개발 기대된다.

쉬운 설명:

AlphaGeometry2 는 "수학 올림피아드 기하 문제" 를 푸는 인공지능인데, 기존 버전보다 훨씬 똑똑해졌어요. 마치 "금메달" 수준의 실력을 갖춘 거죠! 사람처럼 "보조선 긋기" 같은 창의적인 방법도 스스로 찾아내고, 어려운 문제도 척척 풀어냅니다. 특히 여러 개의 "생각하는 방식" (search trees) 을 동시에 사용하고, 서로 "정보 공유" 하면서 문제를 해결하는 새로운 전략 (SKEST) 이 핵심 비법이에요. 아직 풀지 못하는 어려운 문제도 있지만, 앞으로 더 똑똑해질 가능성이 아주 높은 "기하 문제 해결 전문가" 라고 할 수 있습니다!

 

 

 

 

AlphaGeometry2 논문 학습 노트

Purpose of the Paper:

  • AlphaGeometry (AG1) 의 한계 극복:
    • 제한적인 domain-specific language (선형 방정식, locus 문제 등)
    • 비효율적인 symbolic engine
    • 초기 language model 의 capacity 부족
  • Olympiad geometry 문제 해결 성능 향상 및 gold medalist 수준 달성 목표
  • fully automated geometry problem solving system 구축 위한 진전 보고 (natural language input → solution)

Key Contributions:

  • Expanded Domain Language:
    • Novelty: AG1 언어 확장하여 locus theorem, linear equation, non-constructive 문제 표현 가능
    • acompute, rcompute predicates 추가 (질문 유형 "Find x" 지원)
    • Locus problem 위한 새로운 predicate syntax 및 * token 도입
    • Topological/non-degeneracy 조건 명시적 표현 predicates 추가 (sameclock, noverlap, lessthan)
    • overlap predicate 및 cyclic_with_center predicate 도입 (non-distinct points handling 강화)
    • 문제 기술 시 predicate 사용 제한 완화 (non-constructive 문제 coverage 확대)
    • Contribution: IMO geometry 문제 coverage 66% → 88% 로 향상
  • Stronger and faster Symbolic Engine (DDAR2):
    • Novelty: DDAR1 대비 속도 및 robustness 향상, hard problem 해결 위한 핵심 기능 추가
    • Handling double points: 동일 좌표 다른 이름 점 지원 (proof reformulation 가능하게 함)
    • Faster algorithm: rule processing 효율성 증대 (search space cubic으로 감소), angle/distance rule implicit 처리
    • Faster implementation: C++ & pybind11 기반 Gaussian Elimination core computation 구현 (DDAR1 대비 300배 이상 속도 향상)
    • Contribution: 증명 탐색 및 synthetic data 생성 속도 향상, 복잡한 문제 해결 능력 강화
  • Better Synthetic Training Data:
    • Novelty: AG1 data generation 방식 개선 및 확장
    • Larger & more complex diagrams: diagram size 2배 확대, theorem complexity 및 proof complexity 증가
    • More types of theorems: locus type theorem 추가 생성 (movement dependency 개념 도입)
    • Better data distribution: question type 및 auxiliary point 포함 여부에 따른 data distribution 균형 향상
    • Contribution: language model 학습 효율성 및 generalization 성능 향상
  • Novel Search Algorithm (SKEST - Shared Knowledge Ensemble of Search Trees):
    • Novelty: multiple search trees 병렬 실행 및 knowledge sharing mechanism 도입
    • Search tree 종류: "Classic", "Tree predicting multiple auxiliary points", "Tree predicting different types of aux points uniformly"
    • Knowledge sharing: symbolic engine 증명 성공/실패 정보 공유, 다른 search tree 탐색 가이드
    • Contribution: proof search robustness 및 efficiency 향상, 다양한 탐색 공간 효과적 exploration
  • Better Language Model:
    • Novelty: Gemini architecture 기반 language model 도입 및 다양한 training setup 실험
    • Gemini architecture 활용: sparse mixture-of-expert Transformer 기반 모델
    • Training setups: scratch training, math pre-trained model fine-tuning, multimodal training (diagram image input)
    • Inference setup: top-k sampling (temperature t=1.0, k=32) 활용, 다양한 search tree 및 language model ensemble
    • Analysis string: LM input에 DDAR deduction 결과 (S1, S2, S3) 반영 (neuro-symbolic interface 강화)
    • Contribution: Olympiad geometry 문제 해결 능력 최고 수준으로 향상

Experimental Highlights:

  • State-of-the-art IMO geometry problem solving performance:
    • IMO 2000-2024 geometry problems (IMO-AG-50 dataset): 84% solve rate (42/50 문제 해결) 달성
    • Average gold medalist performance 초과
    • AG1 (54% solve rate) 대비 substantial performance leap
    • Hardest IMO shortlist problems (IMOSL-AG-30 dataset): 20/30 문제 해결
  • Ablation study:
    • Single search tree 최고 성능 beam size 128, beam depth 4, 32 samples
    • Inference setting (temperature, samples) 중요성 입증 (greedy decoding 대비 성능 향상)
  • Training time efficiency:
    • Language model 250 training steps (200M tokens) 만에 27/50 IMO 문제 해결 가능 (빠른 학습 속도)
  • Speed improvement:
    • DDAR2 (C++ implementation) DDAR1 (Python) 대비 300배 이상 속도 향상

Limitations and Future Work:

  • Domain Language Limitations:
    • Limitations: variable number of points, non-linear equations, inequalities 문제 미지원 → "solve geometry" 완전 해결에 제약
    • Future Work: domain language 확장 필요 (e.g., inequality 표현 predicates 추가)
  • Unsolved IMO & IMOSL Problems:
    • Limitations: IMO & IMOSL 문제 중 일부 (e.g., IMO 2018 P6, IMO 2023 P6) 해결 불가 → advanced geometry technique (inversion, projective geometry, radical axis) 필요
    • Future Work: DDAR 에 advanced geometry technique 구현 또는 Reinforcement Learning 기반 subproblem decomposition 및 strategy 학습 연구
  • Auto-formalization Improvement:
    • Limitations: natural language input → AlphaGeometry language 자동 변환 아직 완벽하지 않음 (human intervention 필요)
    • Future Work: formalization examples 및 supervised fine-tuning 활용 auto-formalization 성능 향상
  • Full Proof Generation with Language Model:
    • Limitations: language model alone 으로 full proof generation 아직 초기 단계, 완전 자동 증명 시스템 구축에 어려움
    • Future Work: inference speed 향상 및 hallucination 해결, language model 기반 partial solution 생성 및 verification 연구