기술 요약: 자동 형식화를 위한 단조 참조 없는 정제

1. 문제 제기

대규모 언어 모델 (LLM) 이 수학적 추론을 발전시켰음에도 불구하고, 자연어 명제와 그에 수반되는 증명을 완전하고 기계적으로 검증 가능한 형식 명제와 증명으로 변환하는 **전체 명제 자동 형식화 (full-theorem autoformalization)**는 여전히 미개척 영역입니다. 기존 접근법은 주로 증명 부분에 '죄송합니다 (sorry)'라는 플레이스홀더를 사용하는 등 명제 형식화에만 초점을 맞추거나, 명제 생성과 정리 증명을 분리된 작업으로 취급하는 경향이 있습니다.

고품질 자동 형식화의 핵심 과제는 그 다차원적 성격에 있습니다. 성공적인 형식화는 다음과 같은 네 가지 요소를 동시에 충족해야 합니다:

1. 형식 유효성 (Formal Validity, FV): 정리 증명기 (예: Lean4) 에 의한 문법적 정확성과 기계적 검증.
2. 논리적 보존 (Logical Preservation, LP): 원본 자연어 명제의 논리적 구조와 의미적 정렬.
3. 수학적 일관성 (Mathematical Consistency, MC): 수학적 대상과 연산의 정확한 표현.
4. 형식 품질 (Formal Quality, FQ): 구조적 명확성, 간결성, 그리고 재사용성.

현재의 반복적 정제 방법은 이러한 차원들을 공동으로 최적화하는 데 어려움을 겪으며, 종종 한 측면 (예: 문법) 을 개선하는 대신 다른 측면 (예: 의미적 정렬) 을 희생합니다. 또한, 기존 방법들은 종종 정답 형식화나 인간의 선택 개입에 의존하여 참조 없는 설정에서의 적용 가능성을 제한합니다.

2. 방법론

저자들은 정답 형식화나 인간의 선택에 접근할 수 없는 테스트 시점에 작동하는 참조 없는, 반복적, 단조 최적화 과정을 제안합니다. 이 프레임워크는 정리 증명기와 LLM 기반 판정관 (judge) 으로부터의 피드백을 통합하여 전문화된 LLM 들의 앙상블을 안내합니다.

2.1 목적 함수

저자들은 네 가지 차원을 균형 있게 조정하기 위해 마스크된 복합 목적 함수 $J_{OA}(x)$를 정의합니다. 형식 유효성 ($\pi_{FV}$) 은 하드 제약 (마스크) 으로 작용하는 반면, 논리적 보존 ($\pi_{LP}$), 수학적 일관성 ($\pi_{MC}$), 그리고 형식 품질 ($\pi_{FQ}$) 은 소프트 차원으로 간주됩니다:
$$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$$
이 수식은 $\pi_{FV}=0$인 유효하지 않은 형식화는 소프트 점수와 관계없이 선택되지 않도록 보장합니다.

2.2 LLM 판정관과 불확실성

소프트 차원은 정확하게 계산하기 어렵기 때문에, 이 프레임워크는 점수를 추정하기 위해 LLM 판정관을 활용합니다. LLM 의 고유한 노이즈와 편향을 처리하기 위해 저자들은 다음과 같이 가정합니다:

• 점근적 안정성: 보정 후 판단이 안정화됨.
• 측정 가능한 불확실성: 실제 점수에 대해 일측 **하한 신뢰 구간 (Lower Confidence Bound, LCB)**을 설정할 수 있음.
  목적 함수는 LCB 기반 추정기를 사용하여 최적화되며, 이를 통해 선택 결정이 보수적이고 평가 노이즈에 대해 견고하도록 보장합니다.

2.3 생성기 역할과 반응성

이 프레임워크는 각 차원별 예상 개선을 모델링하는 **반응성 지도 (responsiveness map)**에 따라 LLM 역할을 세 가지 범주로 분해합니다:

1. 원회 생성기 (One-Off Generators, OOGs): 처음부터 초기 형식화를 생성합니다 (예: DeepSeek-Prover 와 같은 전문 수학 모델).
2. FV 수리기 (FV-Repairers, FVRs): 형식적으로 유효하지 않은 후보를 구체적으로 대상으로 하여 수정합니다 (예: 반복적 증명 수정이 가능한 모델).
3. 반복 생성기 (Recurrent Generators, REGs): LLM 판정관으로부터의 피드백 (특정 소프트 차원인 LP, MC, 또는 FQ 에 관한) 을 기반으로 현재 최선 후보를 정제합니다.

2.4 단조 수용 정책

이 과정은 후보 생성과 선택을 반복합니다. 보수적 수용 정책이 적용됩니다: 새로운 후보는 LCB 기반 추정 목적 점수가 현재 최선보다 엄격하게 높을 때만 수용됩니다. 이는 **인증된 단조 개선 (certified monotonic improvement)**을 보장하며, 선택된 형식화의 품질이 반복을 통해 결코 감소하지 않음을 의미합니다. 이 과정은 특정 조건 하에서 수렴하고 종료됨이 증명되었습니다.

3. 주요 기여

1. 공식 정의 및 프레임워크: 본 논문은 전체 명제 자동 형식화를 통합된 작업으로 공식적으로 정의하고, 이를 해결하기 위한 참조 없는 반복적 단조 과정을 제안한 최초의 연구입니다.
2. 마스크된 복합 목적 함수: 형식 유효성을 하드 제약으로 강제하면서 동시에 여러 소프트 차원 (LP, MC, FQ) 을 최적화하는 목적 함수를 도입했습니다.
3. 역할 전문화 앙상블: 자동 형식화 작업을 OOG, FVR, REG 역할로 분해하고, 특정 품질 차원에 가장 효과적인 생성기를 선택하기 위해 반응성 지도를 활용합니다.
4. 이론적 보장: 인증된 단조성, 수렴성, 그리고 과정 종료 가능성에 대한 이론적 증명을 제공하여, 현실적인 판정관 노이즈 하에서도 비감소적 진전을 보장합니다.
5. 실증적 검증: 이 프레임워크가 전문화 및 범용 LLM 의 강점을 효과적으로 앙상블하여 표준 벤치마크에서 고품질 결과를 달성함을 입증했습니다.

4. 실험 결과

이 방법은 Lean4 를 사용하여 miniF2F-Test와 ProofNet-Test에서 평가되었습니다. 프레임워크는 DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Seed-Coder-8B, Qwen2.5-7B, 그리고 판정관으로 GPT-4.1-mini 를 포함한 모델 앙상블을 활용했습니다.

주요 성능 지표:

• miniF2F: 100.00% 의 형식 유효성과 90.27% 의 전체 점수를 달성했습니다. 모든 차원에서 점수가 1 인 '완벽한' 형식화 비율은 49.18% 에 달했습니다.
• ProofNet: 77.96% 의 형식 유효성과 52.45% 의 전체 점수를 달성했으며, 17.74% 가 완벽한 형식화였습니다.

비교적 발견:

• 단조 대 베이스라인: 단조 과정은 수용 정책이 없는 Best-of-k(k 개의 출력 샘플링) 및 **반복적 자기 정제 (ISR)**보다 크게 우월한 성능을 보였습니다.
• 앙상블 대 단일 모델: 강력한 단일 모델 (GPT-5.4) 도 개선을 보였으나, 특정 역할에 할당된 더 작고 전문화된 모델들의 앙상블이 특히 형식 유효성 측면에서 더 우수한 성능을 달성했습니다.
• 견고성: 단조 경향은 서로 다른 LLM 판정관 계열 (예: Qwen 대 GPT) 과 인간 전문가에 의해 평가될 때도 유지되었으며, 이는 개선이 판정관 편향의 산물이 아님을 시사합니다.

5. 의미 및 주장

본 논문은 이 작업이 신뢰할 수 있는 자동 형식화를 향한 실용적이고 이론적으로 근거 있는 단계를 제공한다고 주장합니다. 참조 없는 방식으로 작동함으로써, 이 접근법은 광범위한 형식 라이브러리가 부족한 영역에서도 적용 가능하며, 수학 및 과학의 미개척 영역 형식화에 기여할 잠재력을 가지고 있습니다.

저자들은 이 프레임워크가 다음과 같은 AI 지원 자동 형식화를 위한 원칙적인 방법론을 제공한다고 강조합니다:

• 대규모 형식 검증 파이프라인에서 인간의 감독 필요성을 줄입니다.
• LCB 가정을 통해 판단의 불확실성을 명시적으로 정량화하고 제어합니다.
• 상호 보완적인 LLM 과 형식 검증기 피드백을 결합하면 증명 가능한 비감소 품질의 형식화를 생성할 수 있음을 보여줍니다.

이 연구는 계산 비용이 단일 통과 추론보다 높지만, 성능과 안정성의 상당한 향상으로 인해 그 트레이드오프가 정당화되며, 안전하고 신뢰할 수 있는 AI 지원 형식 추론에 대한 향후 연구의 길을 연다고 결론짓습니다.