Reformalization of the Jordan Curve Theorem

Motivation

• Known: 기존에는 자연어 수학 텍스트를 형식 증명으로 변환하는 autoformalization 연구가 활발했으며, 서로 다른 proof assistant 간 증명을 옮기는 low-level logical translation 기반의 proof transfer 방법들도 오랫동안 연구되어 왔다. JCT는 HOL Light(약 6만 줄, Hales, 2005)와 Mizar(14년 소요)에서 각각 formalize된 유명한 사례이다.
• Gap: 기존 logical translation 기반 proof transfer는 논리적 foundation의 불일치(dependent type theory, higher-order logic, set theory 등)와 library alignment 문제로 인해 부자연스럽거나 매우 제한적인 시스템 간에만 적용 가능했다. 특히 correct-by-construction 번역은 결정론적이고 완전해야 하는 제약 때문에 원 증명의 정신(spirit)을 보존하지 못하는 근본적 한계가 있었다.
• Why: LLM 기반 agentic 파이프라인이 서로 다른 foundation과 library를 가진 proof assistant 간에도 대규모의 비trivial한 수학적 증명을 사람의 개입을 최소화하면서 실용적으로 전이할 수 있음을 보임으로써, formal mathematics 생태계 간 지식 이전과 라이브러리 통합에 실질적인 가능성을 제시한다.
• Approach: Mizar/HOL Light의 기존 형식 증명을 정확한 명세(specification)이자 상세하고 정확성이 보장된 증명 스케치로 활용하여, LLM 에이전트가 target proof assistant의 library, 검색 도구, 검증 루프를 사용해 idiomatic한 native proof development를 구성하도록 하는 agentic reformalization 파이프라인을 설계했다.

Achievement

1. 세 가지 reformalization 성공: Mizar→Lean, HOL Light→Lean, HOL Light→Agda 세 방향 모두에서 JCT를 sorry나 추가 axiom 없이 완전히 검증된 형태로 재형식화하는 데 성공했다.
2. 실용적 효율성 입증: 원본 formalization이 수개월~14년 걸린 것과 달리, 각 reformalization은 약 1주일, 실질적 human involvement는 최대 이틀 이내로 완료되어 LLM 기반 proof transfer가 실용적 규모로 가능함을 보였다.
3. 파이프라인 설계 지침 도출: dependency 추출, proof sketch 및 library alignment, proof filling의 3단계 워크플로우와 실패 패턴, guardrail 설계에 대한 실무적 교훈을 정리했다.

How

• Step 1 (메타데이터 추출): Mizar proof checker(및 mizar-rs)의 중간 산출물(intermediate text format)을 활용해 source file 간 dependency graph와 최종 JCT 진술에 이르는 정리들의 의존관계를 추출한다.
• Step 2 (proof sketch 및 library alignment): dependency graph와 MML source를 에이전트에 제공해 Mizar source file 당 하나의 Lean 파일을 생성하도록 지시하고, 개념을 target library의 기존 정의와 정렬(alignment)한다.
• Step 3 (proof filling): 생성된 sketch에 대해 LLM과 검증 루프(verification loop)를 반복 적용하여 실제 tactic 증명을 채워 완전히 컴파일되는 development를 완성한다.
• 평가 지표로 human involvement 시간, 정리/줄 수/tactic 수, 컴파일 시간, 기존 library 재사용 비율, 소요 일수, LLM 비용 등을 정성적 경험 보고와 함께 정량적으로 기록한다.

Originality

• autoformalization의 변형으로서 "reformalization"이라는 새로운 과제를 정식으로 정의하고 명명함
• 자연어가 아닌 서로 다른 formal proof assistant 간의 형식 증명 자체를 소스로 사용하는 LLM agentic 파이프라인을 제시
• Mizar, HOL Light, Lean, Agda라는 foundation과 tooling 성숙도가 상이한 네 개 시스템을 조합한 3방향 case study를 통해 소스/타겟 시스템 특성이 reformalization 성공에 미치는 영향을 비교 분석
• correct-by-construction 방식이 아닌, 증명의 아이디어(spirit)를 보존하는 방식으로 foundation mismatch와 library alignment 문제를 우회하는 관점 제시

Limitation & Further Study

• 본문 발췌가 Mizar→Lean reformalization의 초반 단계까지만 제공되어, HOL Light→Lean, HOL Light→Agda의 구체적 방법론과 최종 정량적 결과(정리 수, 시간, 비용 등)를 확인할 수 없음
• 단일 정리(JCT)에 대한 세 가지 사례 연구로 일반화 가능성이 제한적이며, 다른 종류의 정리나 더 다양한 proof assistant 조합에 대한 추가 검증이 필요함
• 시간·비용 지표가 vendor-dependent하고 proof size가 복잡도의 부실한 proxy임을 저자들 스스로 인정하고 있어, 정량적 비교의 엄밀성이 제한적임
• 향후 연구로 다양한 정리 유형에 대한 reformalization 벤치마크 구축과 파이프라인의 자동화 수준을 높이는 방향이 필요해 보임

Evaluation

총평: LLM 기반 agentic 파이프라인을 통해 서로 다른 proof assistant 간 대규모 형식 증명을 실용적 시간 내에 전이할 수 있음을 JCT라는 상징적 사례로 설득력 있게 보여준 흥미로운 case study이며, formal mathematics 생태계 간 지식 이전이라는 중요한 방향을 제시한다.