Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Motivation

• Known: Lean/MATHLIB 기반 formal reasoning 시스템(AlphaProof, SeedProver 등)은 대수·정수론에서 IMO 금메달 수준 성능을 달성했고, AlphaGeometry, SeedGeometry 등 기하 전용 시스템은 custom DSL 기반 symbolic reasoning으로 유사한 성과를 냈다. LeanEuclid, LeanGeo 같은 선행 연구가 Lean에서 기하 형식화를 시도했지만 System E 등 커스텀 공리계를 사용했다.
• Gap: 기존 geometry-in-Lean 연구(LeanEuclid, LeanGeo)는 표준 MATHLIB과 호환되지 않는 custom axiom system을 도입해 trusted computing base를 늘리고 생태계 통합을 저해하며, 문제 수가 1,100개 미만으로 대규모 학습에 부족하다. 또한 native MATHLIB 형식화는 위상적 구성이나 non-degeneracy 같은 암묵적 다이어그램 가정을 외부 solver에 위임하지 않고 명시적으로 처리해야 하는 고유한 난제를 안고 있다.
• Why: 기하와 대수/정수론이 서로 다른 형식 체계(custom DSL vs Lean/MATHLIB)로 분리되어 있으면 통합된 신경 정리 증명(neural theorem proving) 모델 개발이 어렵고 trusted computing base가 커지는 문제가 있으므로, 기하를 native MATHLIB로 통합하는 것은 formal reasoning 생태계 전체의 신뢰성과 확장성에 중요한 영향을 미친다.
• Approach: 제약 명시화(constraint explication), 구성 고정(configuration anchoring), 형식화 매핑(formalization mapping), 반복적 수정(iterative repair)의 4단계로 구성된 파이프라인을 통해 자연어 기하 문제를 EuclideanSpace R (Fin 2) 기반의 native MATHLIB Lean 4 정리로 변환한다.

Achievement

1. 대규모 데이터셋 구축: OMNI-Geometry(768개 대회 문제)와 Numina-Geometry(177,597개 문제)를 구축하여 기존 LeanEuclid/LeanGeo(<1,100개) 대비 압도적으로 큰 규모의 Lean 기하 형식화 데이터셋을 제공했다.
2. 형식화 품질 검증: 사람 전문가 평가에서 TOP1 48.89%, TOP5 73.33%의 정확도를 달성해 자동 형식화 파이프라인의 신뢰성을 입증했다.
3. 다운스트림 유용성 입증: MATHLIB 일반 문제로 학습된 Goedel v2가 별도 기하 학습 없이도 Numina-Geometry에서 13.6% 증명 성공률을 보였고, 데이터셋으로 추가 학습 시 15.1%로 향상되어 native MATHLIB 호환성이 지식 전이를 가능케 함을 보였다.

How

Figure 1. Overview of the EUCLEAN formalization pipeline. Left (Ambiguity in Input): The process begins with an informal

• Plane := EuclideanSpace R (Fin 2)를 기하 정의의 기초로 삼아 R2 내적 공간 위에서 기하를 정의하는 MATHLIB-native foundational strategy를 확립
• System E와 같은 opaque primitive type(Point, Line, Circle)과 custom axiom 대신 MATHLIB의 벡터 공간, MeasureTheory, Analysis 등 기존 생태계를 직접 활용
• 위상적 구성, 상대적 위치, non-degeneracy 등 암묵적 다이어그램 가정을 "prove-first" reasoning을 통해 명시적 제약으로 변환(constraint explication)하고 구성을 고정(configuration anchoring)
• 자연어 문제를 MATHLIB 구성 요소로 매핑(formalization mapping)한 뒤, 컴파일 오류나 의미적 불일치를 반복적으로 수정(iterative repair)하는 구조 인식형 생성 파이프라인 적용
• Human evaluation(180개 샘플)과 Goedel v2를 이용한 다운스트림 증명 실험으로 데이터셋 품질 검증

Originality

• 기하 형식화를 custom DSL/axiom system이 아닌 표준 MATHLIB 생태계에 native하게 통합한 최초의 대규모 시도
• 암묵적 diagrammatic assumption(non-degeneracy, topological configuration)을 외부 SMT solver에 위임하지 않고 언어모델이 명시적으로 식별·처리하도록 강제하는 "prove-first" 전략 도입
• 기존 LeanEuclid/LeanGeo 대비 100배 이상 규모(177,597개)의 Numina-Geometry 데이터셋 구축으로 기하 분야의 LeanWorkbook급 학습 자원 제공
• Goedel v2를 통한 zero-shot 지식 전이 실험으로 native MATHLIB 호환성이 통합 신경 정리 증명 모델 개발에 실질적으로 기여함을 실증

Limitation & Further Study

• TOP1 정확도가 48.89%에 그쳐 아직 완전 자동화된 고신뢰 형식화로 보기는 어렵고, 나머지 실패 사례에 대한 체계적 오류 분석이 본문 발췌에서 충분히 제시되지 않음
• Goedel v2의 증명 성공률 개선폭(13.6%→15.1%)이 상대적으로 크지 않아, 데이터셋 규모 대비 실제 정리 증명 성능 향상 효과는 제한적일 수 있음
• MATHLIB의 기하 인프라가 상대적으로 작고 빠르게 변화한다는 점이 언급되었는데, 이는 형식화 파이프라인의 장기적 유지보수 및 재현성에 리스크가 될 수 있음
• 후속 연구로 non-degeneracy 조건 자동 검증의 정밀도 향상, 더 다양한 기하 하위 분야(입체기하, 사영기하 등)로의 확장, 그리고 iterative repair 단계의 효율성 개선이 필요해 보임

Evaluation

총평: 기하 형식화를 표준 MATHLIB 생태계에 통합하고 대규모 데이터셋을 구축했다는 점에서 통합 신경 정리 증명 연구에 실질적 기여를 하는 견고한 작업이며, 다만 형식화 정확도와 다운스트림 성능 향상폭에서 개선 여지가 남아있다.