Technical Report for AI4Math-2026 Track 1: Automated Semantic Alignment Verification and Error Categorization of Lean 4 Formalizations via Decomposition-Guided Auditing

Motivation

• Known: 기존 연구들은 autoformalization의 semantic fidelity 평가를 binary correctness label이나 embedding 유사도 기반 scalar score로 축소했으며, FormalAlign, FMC, DSR, DNA 등 decomposition 기반 프레임워크들이 formal statement 생성 품질 개선에 decomposition을 활용해왔다.
• Gap: 기존 접근들은 correctness를 이진 판정하거나 scalar 유사도로만 평가하여 quantifier 오류, hypothesis 약화, type mismatch 등 다양한 오류 원인을 세밀하게 진단하지 못하며, decomposition은 주로 formal statement 생성 목적으로만 활용되고 semantic auditing의 진단적 표현으로는 사용되지 않았다.
• Why: Lean 4 기반 autoformalization의 신뢰성 있는 자동 검증은 정리 증명, 형식 검증, 수학 지식 관리, AI 보조 과학적 추론 등에 폭넓게 기여할 수 있으며, 오류를 세밀하게 국소화하고 분류할 수 있어야 실질적인 디버깅과 모델 개선이 가능하다는 점에서 중요하다.
• Approach: informal statement를 조건과 결론으로 구조화한 중간 표현으로 분해한 뒤, 이를 semantic auditing의 진단 기준으로 삼아 alignment verdict 예측, correction 생성, 오류 localization, hybrid symbolic-LLM 기반 SCI 오류 분류를 수행하는 4단계 파이프라인을 구축했다.

Achievement

Figure 1. Overview of the proposed semantic alignment verification pipeline. Given an informal mathematical statement an

1. 파이프라인 제안: informal statement decomposition, verdict 예측 및 추론, correction 생성 및 오류 segmentation, SCI 오류 분류의 4단계로 구성된 모듈형 파이프라인을 설계함.
2. 성능 달성: 공식 FormalRx benchmark에서 최종 시스템이 Overall score 0.3397, Verdict F1 0.7327, Correction accuracy 0.7671을 기록함.
3. 핵심 발견: 지나치게 세분화된 multi-stage 파이프라인보다 semantic reasoning과 correction generation을 tightly coupled하게 결합한 접근이 더 우수한 성능을 보였고, symbolic heuristic이 SCI 분류에 보완적 신호로 효과적임을 확인함.

How

Figure 1. Overview of the proposed semantic alignment verification pipeline. Given an informal mathematical statement an

• Stage 1 (Informal Statement Decomposition): DSR에서 영감을 받아 전용 prompt로 informal statement를 Conditions(전제, 가정, 도메인 선언, 가설)와 Conclusion(정리의 목표)으로 분해하며, quantifier 보존, atomic condition 추출, implicit type 완성 등의 구조적 제약을 부과함.
• Stage 2 (Verdict 예측 및 추론): 분해된 semantic 구조를 기준으로 Lean 4 문장과의 불일치(quantifier, hypothesis, operator, constant, domain, conclusion 등)를 LLM 기반으로 감사(auditing)하여 semantic alignment 여부를 예측함.
• Stage 3 (Correction 생성 및 오류 segmentation): 오정렬로 판정된 경우 최소 수정된 correct Lean 4 statement를 생성하고, 원본과 correction 간 token-level differencing을 통해 오류 위치를 자동 localization함.
• Stage 4 (SCI 오류 분류): 저-엔트로피 symbolic edit에는 결정론적 rule-based token substitution 탐지를, 고차원적 semantic discrepancy에는 model-based classification을 결합한 hybrid classifier로 28개 SCI 카테고리를 분류함.
• 모든 LLM 추론은 Qwen/Qwen3-235B-A22B 모델을 사용했으며, 대규모 평가를 위해 fallback, retry, concurrent processing, resumable execution 등의 엔지니어링 요소를 포함함.

Originality

• 기존 decomposition 기반 접근들이 주로 formal statement 생성 품질 향상을 목표로 한 것과 달리, decomposition 결과를 semantic auditing의 진단적 참조(diagnostic reference)로 재해석하여 활용함.
• quantifier 보존과 atomic condition 추출 등 Lean 4 문법 구조와의 호환성을 높이기 위한 세밀한 prompt 설계 원칙을 제시함.
• 결정론적 rule-based token substitution과 model-based classification을 결합한 hybrid symbolic-LLM SCI classifier를 통해 오류 분류의 해석 가능성과 정확도를 동시에 추구함.

Limitation & Further Study

• Overall score(0.3397)가 Verdict F1(0.7327)이나 Correction accuracy(0.7671)에 비해 크게 낮아, SCI 세분류나 localization 등 세부 하위 태스크에서 상당한 성능 저하가 존재함을 시사하나 본문 발췌에서 그 구체적 원인 분석은 제한적임.
• 단일 LLM(Qwen3-235B-A22B)에 의존하는 구조로, 다른 LLM 백본이나 fine-tuning 대비 접근법과의 비교가 부족해 일반화 가능성 검증이 제한적임.
• decomposition 단계에서의 오류(예: 잘못된 quantifier 추출, type 완성 오류)가 후속 단계 전체에 전파될 위험이 있어 파이프라인의 강건성에 대한 정량적 오류 전파 분석이 필요함.
• 후속 연구로 decomposition 정확도 자체에 대한 별도 평가, 더 tightly coupled된 아키텍처와의 체계적 비교, 다양한 LLM 백본에 대한 ablation이 요구됨.

Evaluation

총평: 챌린지 참가를 위한 실용적이고 잘 구조화된 파이프라인을 제시하며 decomposition 기반 diagnostic auditing이라는 아이디어는 흥미롭지만, Overall score가 낮게 나타나는 이유에 대한 심층 분석과 다른 백본/설계와의 비교 실험이 보강되면 기여도가 더욱 명확해질 것이다.