Faithful Autoformalization via Roundtrip Verification and Repair

Motivation

• Known: Autoformalization은 NLP의 빠르게 성장하는 연구 분야로, 주로 syntactic validity나 downstream task 성공 여부로 평가되어 왔으며, prover나 compiler feedback을 활용해 formalization 품질을 개선하는 연구들이 존재한다. 또한 code generation 분야에서는 test suite를 통한 round-trip correctness가 평가 신호로 활용된 바 있다.
• Gap: 기존 평가 방식은 syntactic validity나 downstream task 성공에만 의존하여 semantic fidelity를 직접적으로 검증하지 못하며, 오류가 발견되어도 end-to-end regeneration에 그칠 뿐 의미가 어디서 손실되었는지 진단하는 방법이 없었다. 특히 statutory/regulatory text와 같이 자연스러운 oracle(예: theorem-proof 관계)이 존재하지 않는 도메인에서는 ground-truth 없는 검증이 더욱 어려운 문제였다.
• Why: 법률 조문과 같이 정답 formalization이 존재하지 않는 실제 도메인에서 LLM이 생성한 formal representation의 신뢰도를 자동으로 검증하고 오류를 국소화하여 수정할 수 있다면, 규제·법률 등 안전이 중요한 분야에서 LLM 기반 autoformalization의 실용적 적용 가능성을 크게 높일 수 있다.
• Approach: 자연어 문장을 formalize(T1)-back-translate(T2)-재formalize(T3)하는 3단계 roundtrip 파이프라인을 구성하고, 최초 formalization과 roundtrip formalization 간 SMT 기반 logical equivalence를 검사하여 불일치 시 LLM judge를 통한 stage-level diagnosis와 scoped repair를 반복 적용한다.

Achievement

Figure 4. NLI drift rate among UNSAT (formally equivalent) and SAT (not equivalent) post-repair rules under Full repair,

1. Formal equivalence가 semantic faithfulness를 예측함을 입증: 두 도메인과 두 모델 전반에서, full repair 시스템 하에 equivalence check를 통과하지 못한 규칙은 통과한 규칙보다 1.4배~2.5배 더 높은 NLI drift를 보였다.
2. Diagnosis-guided scoped repair의 우수성 입증: diagnosis 단계가 신뢰할 만할 때(Claude가 diagnosis 수행) scoped repair가 가장 낮은 비용으로 가장 높은 verified-equivalence rate를 달성했으나, GPT가 diagnosis를 수행하면 신뢰도가 낮아져 우위를 상실했다. diagnosis만 Claude로 교체하면(pipeline과 repair는 GPT 유지) 다시 낮은 비용으로 명확한 우위를 회복했다.
3. Diagnosis 단계가 병목임을 규명: pipeline이나 repair operator가 아니라 diagnosis function의 신뢰도가 scoped repair 성능의 핵심 병목임을 실증적으로 확인했다.

How

Figure 2. The roundtrip autoformalization framework. (A) The pipeline produces two formal encodings of x and an SMT solv

• Texas Transportation Code(150개 규칙)와 Texas Parks and Wildlife Code(77개 규칙) 두 statutory 도메인에서 실험을 수행
• Claude Opus 4.6과 GPT-5.2 두 LLM을 사용하여 파이프라인, repair, diagnosis 역할을 조합
• target formalism은 many-sorted first-order logic이며, equivalence check는 SMT solver로 수행
• yorig와 yrt가 불일치(SAT, 즉 반례 존재)하면 LLM judge가 (x, yorig, x′, yrt) 네 가지 아티팩트를 검토하여 first-failed stage를 {1,2,3} 중 하나로 진단하고 scoped repair를 통해 해당 stage만 재생성
• no repair, random stage selection repair, full-pipeline regeneration 세 가지 baseline과 비교
• 독립적인 post-hoc 검증 신호로 bidirectional NLI drift를 측정하여 formal equivalence 결과와의 상관관계를 분석
• 최대 5회의 LLM 기반 syntax correction을 허용하여 문법적 well-formedness를 보장

Originality

• ground-truth formalization 없이 순수 roundtrip(재formalize) 구조만으로 faithfulness 신호를 얻는 검증 프레임워크를 제안
• 단순 accept/reject 이진 신호를 넘어 stage-level(어느 translation 단계에서 오류가 발생했는지)까지 진단하는 diagnosis function을 도입
• 진단된 stage에 한정하여 재생성하는 scoped repair 개념을 제시하여 전체 파이프라인 재생성 대비 효율성을 추구
• SMT 기반 formal equivalence와 독립적인 NLI drift 지표를 함께 사용하여 formal equivalence가 실제 semantic faithfulness의 대리 지표로 유효함을 실증적으로 검증
• 수학 중심이 아닌 규제/법률 텍스트(non-mathematical, no natural oracle 존재)에 autoformalization 신뢰성 검증을 최초로 적용

Limitation & Further Study

• yorig와 yrt가 일치하더라도 두 formalization이 원문 x와 다른 지점에서 안정화(fixed point)될 가능성이 있어, formal consistency가 faithfulness의 충분조건이 아님을 저자들도 인정
• diagnosis function 자체의 신뢰도가 모델(GPT-5.2)에 따라 낮아질 수 있어 diagnosis가 병목이 되는 근본적 한계가 존재하며, 이를 해결할 diagnosis 개선 방법론은 제시되지 않음
• 자연어 semantics를 formal하게 명시하는 것은 범위를 벗어난다고 명시하여, diagnosis가 관찰 가능한 아티팩트에만 의존하는 근본적 한계가 있음
• 평가 도메인이 두 개의 Texas 법전(교통, 공원/야생동물)으로 제한적이며, first-order logic 기반 SMT라는 특정 formalism에 대한 실험만 수행되어 Lean 등 다른 formalism으로의 일반화는 추후 검증 필요
• workshop paper(ICML AI for Math Workshop) 형태로 분량이 짧아 세부 실험 설정과 통계적 유의성 검증이 제한적으로 제시됨

Evaluation

총평: ground-truth 없이 autoformalization의 신뢰성을 진단하고 국소적으로 수정하는 실용적이고 참신한 프레임워크로, 법률 도메인이라는 도전적인 영역에서 formal equivalence와 semantic faithfulness 간 상관관계를 실증했다는 점에서 의미가 크지만, diagnosis 신뢰도 문제와 fixed-point 오류 가능성 등 근본적 한계에 대한 심화 분석이 후속 연구로 필요하다.