Decompose, Structure, and Repair: A Neuro-Symbolic Framework for Autoformalization via Operator Trees

Motivation

• Known: 기존 autoformalization 연구는 few-shot prompting, supervised fine-tuning, reinforcement learning, retrieval-augmented generation 등을 통해 end-to-end LLM 기반 번역 성능을 향상시켜 왔으며, 최근에는 ARIA, SITA, DRIFT 등 system-level iterative 아키텍처로 발전하고 있다.
• Gap: 기존 방법들은 formal code를 flat sequence로 취급하여 수학 명제에 내재된 계층적 논리 구조를 무시하며, 이로 인해 semantic fidelity와 오류 국소화의 정밀성이 제한된다. 또한 대학원 수준까지 아우르는 신뢰성 높은 평가 벤치마크가 부족하다.
• Why: Formal mathematics의 ITP 채택을 가로막는 진입장벽(formal language의 학습 곡선, 수작업 formalization의 비용)을 낮추기 위해서는 정확하고 견고한 autoformalization이 필수적이며, 계층 구조를 반영한 표현이 이를 근본적으로 개선할 수 있다.
• Approach: NL statement를 논리적 구성요소(condition, conclusion)로 분해하고 이를 구조화된 operator tree(FL OPT)와 FL component로 동시에 매핑한 뒤, 이 topological blueprint를 활용해 sub-tree 단위로 오류를 정밀하게 국소화하고 복구하는 tree-guided repair 전략을 도입한다.

Achievement

Figure 4. A repair trajectory of the tree-guided repair process.

1. DSR 프레임워크 제안: operator tree를 활용해 논리 구조를 명시적으로 포착하는 neuro-symbolic 프레임워크를 제안하여 autoformalization 성능과 tree-guided repair의 정밀도를 동시에 향상시켰다.
2. PRIME 벤치마크 구축: Algebra, Analysis, Number Theory 등 다양한 분야를 아우르는 대학/대학원 수준의 156개 정리를 Lean 전문가가 formalize한 고신뢰 벤치마크를 도입했다.
3. State-of-the-art 달성: ProverBench, ProofNet, PRIME 전반에서 동일한 계산 예산 하에 기존 baseline 대비 일관되게 높은 Syntax Check(SC) 및 Consistency Check(CC) pass rate를 달성했으며, 더 큰 모델보다도 우수한 성능을 보였다.

How

Figure 3. Training Pipeline of the DSR Formalizer. (a) Data Construction: A structured corpus is built by aligning NL co

• Semantic Decomposition: Semantic Canonicalization(언어적 잡음 제거 및 암묵적 문맥 명시화)과 Structural Role Alignment(문장을 CONDITION/CONCLUSION으로 분류)를 통해 NL statement를 정제된 NL component들로 분해한다.
• Structured Translation: 각 NL component를 선형 코드 형태의 FL component와, 논리 구조를 트리 형태로 표현한 FL OPT(operator tree)로 동시에 번역하여, 구조적 정렬(structural alignment)을 통해 formalization 능력을 강화한다.
• Tree-guided Repair: Lean compiler의 컴파일 결과를 바탕으로, 오류가 발생한 FL statement의 impaired OPT를 식별하고, repair model이 sub-tree 단위로 해당 부분만 정밀하게 수정하여 전체 논리를 훼손하지 않고 오류를 교정한다.
• Training Pipeline: 구조화된 데이터 구성과 curriculum learning을 결합하여 모델이 operator tree supervision을 통한 구조적 prior를 학습하고 복잡한 계층적 출력을 점진적으로 숙달하도록 훈련한다(Figure 3).

Originality

• 자연어 명제의 계층적 논리 구조를 operator tree(OPT)로 명시적으로 표현하여 autoformalization에 도입한 최초의 시도로, 기존 flat sequence 기반 접근과 차별화된다.
• decomposition을 단순 전처리가 아니라 명제의 차원을 수학적으로 축소하여 후속 OPT 생성과 tree-guided repair를 가능케 하는 핵심 메커니즘으로 활용한다는 점에서 DRIFT 등 유사 연구와 목적이 근본적으로 다르다.
• 오류를 statement 전체가 아닌 sub-tree 단위로 국소화·복구하는 tree-guided repair 전략을 제안하여 global logic을 훼손하지 않으면서 정밀한 오류 교정을 달성한다.
• 대학원 수준의 다양한 수학 분야를 포괄하고 전문가가 직접 annotate한 PRIME 벤치마크를 새롭게 구축하여 신뢰성 높은 평가 기준을 제공한다.

Limitation & Further Study

• OPT 생성 및 sub-tree 정합(alignment) 과정의 복잡도와 오류 전파 가능성에 대한 심층 분석이 제한적일 수 있으며, OPT 구조 자체의 파싱 오류가 전체 파이프라인 성능에 미치는 영향에 대한 추가 검증이 필요하다.
• PRIME 벤치마크가 156개 정리로 규모가 상대적으로 작아 통계적 일반화에 한계가 있을 수 있으며, 더 다양한 수학 분야 및 난이도로 확장하는 후속 연구가 요구된다.
• DRIFT와 같은 retrieval 기반 접근과의 결합이 향후 과제로 언급되었을 뿐 실제로 통합·검증되지 않았다.
• 다른 ITP(예: Isabelle, HOL Light, Rocq)로의 일반화 가능성에 대한 검증이 Lean 4에 국한되어 있다.

Evaluation

총평: 계층적 논리 구조를 명시적으로 활용하는 neuro-symbolic 접근과 신뢰성 높은 PRIME 벤치마크를 통해 autoformalization 분야에 실질적이고 참신한 기여를 한 우수한 연구로 평가된다.