Divide and Abstract: Autoformalization via Decomposition and Abstraction Learning

Motivation

• Known: 기존 LLM 기반 autoformalization 연구는 in-context learning, fine-tuning된 autoformalizer, retrieval-augmented inference, 후처리 기반 majority voting/semantic ranking 등의 방법으로 informal statement를 target formal language(Lean, Isabelle 등)로 직접 번역하도록 LLM에 요구해왔다.
• Gap: 기존 접근법들은 (1) Mathlib과 같은 기존 라이브러리의 abstraction 풍부도에 성능이 종속되고, (2) nested quantifier·고차 객체를 포함한 복잡한 statement를 한 번에 생성하는 데 어려움을 겪으며, (3) Mathlib에 과적합된 fine-tuned 모델이 새로운 target language나 domain-specific language(DSL)로 잘 전이되지 않는다는 세 가지 근본적 한계를 가진다.
• Why: 이 세 가지 한계를 해결하면 학습 데이터가 부족한 low-resource DSL이나 최신 라이브러리 버전에서도 autoformalization 성능을 크게 끌어올릴 수 있어, neural theorem prover용 병렬 데이터 합성, 자연어 추론의 formal grounding, 중요한 정리·엔지니어링 시스템 검증 가속화 등 실질적 응용에 파급력이 크다.
• Approach: DNA는 별도 학습 없이 LLM 컨텍스트에 언어 문서를 제공하는 방식으로, 코퍼스 전체에서 공통 개념을 추출·형식화하여 target language를 확장한 뒤, 이를 이용해 개별 statement를 계층적으로 분해·번역·조합하는 두 단계 zero-training 프레임워크를 제안한다.

Achievement

1. 다중 모델·벤치마크 일관된 성능 향상: LeanEuclidPlus와 ProofNet-Hard에서 GPT-4.1/5, Claude-4-Sonnet, Qwen3 계열 등 다양한 모델 패밀리에 대해 baseline 대비 최대 8.6배(본문 결과 기준 최대 9.6배) 성능 향상을 달성했다.
2. 소형 모델의 대형 모델 성능 추월/근접: Qwen3-14B가 DNA 적용 시 1.0에서 9.6 success rate로 향상되었고, GPT-4.1-mini가 GPT-4.1 수준에 근접하는 등, DNA는 작은 모델이 훨씬 큰 모델의 baseline 성능을 따라잡게 한다.
3. Low-resource DSL 전이 성공: ProofNet-Hard에서 모든 baseline이 0%의 성공률을 보인 반면 DNA는 성공적인 formalization을 달성하여, 학습 데이터가 부족한 domain-specific language에도 효과적임을 입증했다.
4. Zero-training 특성: target formal language에 대한 별도 학습 없이 문서화(documentation)만 컨텍스트로 제공하여 작동하므로 plug-and-play 방식으로 다양한 언어에 즉시 적용 가능하다.

How

Figure 1. Overview of the Divide and Abstract (DNA) framework. (a) Phase I Language Extension: Given an informal corpus,

• Phase I: Language Extension — Step 1 Concept Extraction: 코퍼스에서 비모호(non-ambiguous)하고 잘 정의되며(well-defined) 추상적인(abstract) 수학적 객체·관계·함수 개념을 추출.
• Step 2 Concept Filtering: 중복 개념과 target language에 이미 formalize되어 있는 개념을 제거.
• Step 3 CDG Construction: 추출된 개념들 간의 의존관계를 나타내는 concept dependency graph(CDG)를 구성.
• Step 4 Concept Formalization: CDG의 topological ordering을 따라 개념을 순차적으로 formal language로 형식화하여 DSL을 확장.
• Phase II: Statement Formalization — 각 statement를 quantifier·premise·conclusion 구조에 따라 semi-formal한 절(clause)들로 계층적/재귀적 분해.
• 학습된 abstraction 라이브러리를 활용해 각 clause를 개별적으로 formal language로 번역.
• 번역된 clause들을 조합하여 완전한 formal statement를 구성.
• symbolic validator의 피드백을 이용해 결과를 refine.
• 평가는 correctness(추출된 개념의 비모호성·정의 타당성·추상성 비율)와 recall(전문가 oracle abstraction 대비 식별률) 두 지표로 5회 반복 실험 평균을 수동으로 측정.

Originality

• 기존 연구가 개별 statement를 독립적으로 formalize하던 것과 달리, 코퍼스 전체 수준에서 공통 개념을 추출해 재사용 가능한 abstraction 라이브러리를 구축하는 "abstraction learning" 단계를 도입한 점이 참신하다.
• statement를 quantifier-premise-conclusion 구조를 활용해 재귀적으로 분해하는 hierarchical decomposition을 formalization 파이프라인에 명시적으로 통합한 점이 독창적이다.
• 별도의 target-language fine-tuning 없이 문서(documentation)만을 컨텍스트로 제공하는 zero-training 설계를 통해 low-resource DSL 전이 문제를 다룬 접근이 기존 fine-tuned autoformalizer들과 차별화된다.

Limitation & Further Study

• Concept Extraction과 Concept Filtering 단계의 품질 평가가 자동화된 지표 없이 수동 평가(사람이 correctness/recall 판정)에 의존하고 있어 재현성과 확장성에 한계가 있다.
• 발췌된 본문에서는 CDG 구성, topological ordering, symbolic validator refinement 등의 구체적 알고리즘 세부사항과 실패 사례 분석이 충분히 제시되지 않아 방법의 강건성 판단이 어렵다.
• LeanEuclidPlus와 ProofNet-Hard 두 벤치마크에 국한된 평가로, 더 다양한 수학 분야(대수, 해석학 등)와 더 큰 규모의 코퍼스에 대한 일반화 가능성은 추가 검증이 필요하다.
• concept extraction 단계에서 발생할 수 있는 오류(잘못된 abstraction 정의)가 이후 Phase II 전체에 전파될 위험에 대한 오류 분석 및 완화 전략이 부족해 보인다.

Evaluation

총평: Autoformalization의 세 가지 근본적 한계(abstraction 부족, 복잡한 statement 처리, 언어 간 전이 실패)를 체계적으로 짚고, 이를 zero-training 방식의 abstraction learning과 hierarchical decomposition으로 해결한 실용적이고 참신한 워크숍 논문이다. 다만 concept extraction 품질에 대한 수동 평가 의존성과 벤치마크 범위의 제한은 향후 보완이 필요하다.