Evaluating the Robustness of Proof Autoformalization in Lean 4

Motivation

• Known: 기존 연구들은 LLM을 활용해 statement autoformalization과 proof autoformalization을 수행하는 다양한 모델(ProofBridge, ProofFlow, FormL4, StepProof 등)을 개발했고, Type Correctness(TC), Semantic Correctness(SC), proof-score 등의 지표로 curated dataset 상의 well-formed informal proof에 대한 formalization 정확도를 평가해왔다.
• Gap: 기존 평가는 모두 이상적으로 정제된(curated) informal proof에 대한 번역 정확도에만 초점을 맞추었고, informal proof가 문체적으로 변형되거나 세부 내용이 (반사실적으로) 변경되었을 때 formalization이 이를 충실히 반영하는지, 즉 robustness에 대한 평가는 전무했다.
• Why: 실제 환경에서는 informal proof가 다양한 문체와 품질로 작성되며 오류를 포함할 수도 있는데, robust하지 않은 autoformalizer는 이런 변형에 대해 정확성이 불안정해지거나 원래 증명으로 되돌리거나 스스로 다른 것을 추론해버려, 향후 FL 기반 검증으로 NL 추론의 오류를 탐지·피드백하는 데 걸림돌이 되므로 이 강건성 평가는 중요하다.
• Approach: NL theorem-proof pair에 global perturbation(전체 문체 변화 paraphrasing)과 local perturbation(값·기호·증명 단계의 국소적 변경, 반사실적 경우 포함)을 각각 적용하고, 이에 따른 FL formalization의 correctness 안정성과 faithfulness를 자동으로 측정하는 두 세트의 metric을 설계했다.

Achievement

Figure 2. Overview of the faithfulness metrics for local perturbations. We compare each Lean output against both the edi

1. 최초의 robustness 연구: proof autoformalization의 robustness를 다루는 첫 연구로서, global/local perturbation이라는 두 범주와 대응하는 자동 평가 지표를 제안했다.
2. 벤치마크 구축: miniF2F와 MATH-500에 두 perturbation을 인스턴스화한 벤치마크를 만들어 ProofBridge, ProofFlow 등 최신 모델을 포함한 7개 모델을 평가했다.
3. 취약성 발견: 모든 평가 모델이 global perturbation 하에서 correctness가 불안정하고, local perturbation 하에서는 대부분 faithfulness를 유지하지 못함을 실험적으로 보여 개선 여지가 크다는 것을 입증했다.

How

Figure 1. Correctness metrics pipeline for global perturbations. Type Correctness (TC) is checked by the Lean compiler,

• Global perturbation: Gemini-2.5-Flash(closed-source)와 Qwen3.5-397B-A17B(open-source) 두 LLM을 사용해 원본 NL proof(Orig)를 두 가지 모드로 paraphrase함 — free-form paraphrasing(-FF, 동일한 수학적 의미와 논리를 보존하며 다른 wording으로 재서술)과 step-by-step paraphrasing(-Step, 번호 매긴 단계로 재구성).
• Global perturbation 하에서는 Type Correctness 등 correctness metric의 pipeline(Fig 1)을 통해 formalization이 원본과 비교해 정확성을 유지하는지 측정.
• Local perturbation: NL 증명 내 단일 값, 기호, 또는 증명 단계를 (반사실적일 수 있게) 변경한 뒤, 생성된 FL proof가 원본을 그대로 유지(reverting)하거나 임의로 다른 것을 추론하지 않고 해당 변경을 충실히 반영하는지를 비교하는 faithfulness metric(Fig 2)을 설계.
• 이렇게 구성된 벤치마크로 ProofBridge, ProofFlow 등을 포함한 7개의 최신 proof autoformalization 모델을 평가.

Originality

• 기존 연구들이 다루지 않았던 proof autoformalization의 robustness라는 새로운 평가 축을 최초로 제시함.
• 문체 변화에 대한 일관성(global)과 세부 변경에 대한 충실성(local, 반사실적 변경 포함)이라는 두 가지 상호보완적 perturbation 범주를 설계하여 서로 다른 실패 모드를 포착함.
• LLM을 활용한 자동 perturbation 생성과 자동 correctness/faithfulness 측정 파이프라인을 결합해, 사람 개입 없이 대규모로 robustness를 정량화할 수 있는 벤치마크를 구축함.

Limitation & Further Study

• Perturbation 생성 자체가 LLM(Gemini-2.5-Flash, Qwen3.5)에 의존하므로, 이 LLM들이 도입하는 편향이나 오류가 벤치마크 품질에 영향을 줄 수 있음.
• miniF2F와 MATH-500이라는 비교적 제한된 두 데이터셋에만 벤치마크가 구축되어, 더 다양한 도메인이나 난이도의 수학 증명에 대한 일반화 가능성은 추가 검증이 필요함.
• 논문 발췌만으로는 local perturbation의 반사실적 변경이 실제로 수학적으로 항상 well-defined한 FL statement/proof를 만들어내는지에 대한 엄밀성 논의가 제한적으로 보이며, 후속 연구로 robustness를 개선하는 학습 기법(예: perturbation-aware fine-tuning)이나 FL 기반 검증과 결합한 오류 탐지 파이프라인으로의 확장이 필요함.

Evaluation

총평: Proof autoformalization 평가에서 그동안 간과되었던 robustness라는 중요한 축을 최초로 체계화하고 실증적으로 취약성을 드러낸 의미 있는 연구로, 향후 더 신뢰할 수 있는 NL-FL 브릿지 연구의 토대를 마련한다.