ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

Motivation

• Known: 기존 연구들은 자동 정리 증명(automated theorem proving)과 autoformalization에 대해서는 활발히 벤치마크를 구축해왔으며, Dedukti, Logipedia, OpenTheory 등 proof exchange를 위한 논리적 프레임워크와 Formalizing 100 Theorems 같은 정리 목록화 프로젝트가 존재한다.
• Gap: 그러나 서로 다른 ITP 간의 형식 증명 번역(cross-ITP translation)을 체계적으로 평가하는 벤치마크는 부재했으며, 유일한 선행 연구인 Babel-formal은 Lean과 Rocq 두 시스템, 14개 정렬 파일에 국한되어 있고, type-checking만으로는 의미적 정합성을 과대평가할 위험이 있다는 문제도 충분히 다뤄지지 않았다.
• Why: Cross-ITP translation이 가능해지면 검증된 결과가 여러 ITP 생태계 간에 이전되어 중복 형식화 노력을 줄이고 학습 기반 prover의 훈련 데이터를 확장할 수 있으며, autoformalization과 auto-informalization 연구에도 도움이 되기 때문에 중요하다.
• Approach: 저자들은 Lean 4, Rocq, Isabelle, HOL Light 네 시스템을 아우르는 controlled tier(공리화된 자족적 파일)와 ecosystem tier(실제 라이브러리 기반)로 구성된 벤치마크와, 상태 격리된(warm backend) 통합 검증 인프라 itpeval을 구축하여 LLM들의 statement 및 proof 번역 성능을 12개의 방향성 번역 쌍에 대해 평가했다.

Achievement

Figure 3. Statement translation pass@1 across all 4,680 directed

1. 4-way aligned cross-ITP benchmark 구축: 1,560개 소스 파일과 6,848개 정리를 포함하며 controlled tier(64개 파일, 660개 lemma)와 ecosystem tier(232개 Formalizing 100 Theorems 파일, 1,264개 miniF2F statement)로 구성해 12개 directed translation pair를 산출했다.
2. 통합 다중 ITP 검증 인프라 공개: 이질적인 theorem prover들을 공통 인터페이스로 노출하는 environment-keyed scheduling, state-isolated warm backend, per-artifact 진단 기능을 갖춘 검증기를 제공했다.
3. LLM 5종에 대한 체계적 평가: GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B를 대상으로 statement translation은 최고 29.1% pass@1, proof translation은 최고 10.5% pass@1을 기록했으며, controlled 정리는 29.7% 대 ecosystem 정리 5.2%로 라이브러리 불일치가 지배적 병목임을 확인했다.
4. BEq(Bidirectional Extended Definitional Equivalence) 검사 도입: type-checking을 통과한 miniF2F statement 번역 322개 중 54.0%(174개)만이 실제 의미적 동치를 만족함을 보여, native type-checking만으로는 의미적 충실도를 과대평가할 수 있음을 규명했다.
5. autoformalization/auto-informalization round-trip 연구: Rocq와 HOL Light가 Lean 4, Isabelle보다 형식화 대상으로서 더 용이하며, multi-ITP context 제공 시 Lean 4의 pooled 성공률이 4.8%에서 10.6%로 향상됨을 확인했다.

How

Figure 2. ITPEVAL verification infrastructure. Generated artifacts are filtered, cached, scheduled by environment, and c

• controlled tier: 자족적이며 공리화된(axiomatized) 파일로 구성해 특정 라이브러리 의존성을 배제하고 순수 논리적 기반 차이에 따른 번역 난이도만 측정
• ecosystem tier: Formalizing 100 Theorems 및 miniF2F에서 가져온 실제 라이브러리 정리로 API, naming convention, automation, proof idiom 차이를 노출
• itpeval 인프라: environment-keyed scheduling과 state-isolated warm backend를 통해 각 ITP의 native checking semantics를 보존하면서 아티팩트별 진단 제공
• 5개 LLM에 statement translation과 proof translation을 pass@k 방식으로 평가, native target prover로만 검증(표면적 heuristic 배제)
• Lean 4 대상에 대해 BEq(Bidirectional Extended Definitional Equivalence) 검사를 구현하여 type-check 통과와 실제 정리 의미 보존 여부를 별도로 측정
• autoformalization/auto-informalization round-trip 실험에서 단일 ITP context와 multi-ITP context를 비교

Originality

• Lean 4, Rocq, Isabelle, HOL Light 네 개 ITP를 아우르는 최초의 균형 잡힌 다자간(four-way) cross-ITP 번역 벤치마크로, 기존 Babel-formal(2개 시스템, 14개 파일)의 범위를 크게 확장
• 논리적 기반 차이(dependent type theory vs. higher-order logic)와 라이브러리/생태계 차이를 분리해서 측정하는 controlled/ecosystem 이원적 tier 설계
• type-checking만으로 평가하는 기존 관행의 한계를 지적하고 BEq라는 결정론적(deterministic) 의미 동치 검사를 도입해 검증
• 이질적 ITP들을 하나의 인터페이스로 통합하면서도 각 시스템의 native checking semantics를 보존하는 state-isolated warm backend 인프라 설계

Limitation & Further Study

• BEq 검사가 현재 Lean 4 타겟에 한정되어 구현되어 있어, 다른 ITP 쌍에도 일반화된 의미 동치 검사가 필요함
• ecosystem tier가 Formalizing 100 Theorems와 miniF2F라는 특정 소스에서만 추출되어, 더 넓은 범위의 실제 라이브러리(Mathlib 전체 등)를 포괄하지 못할 가능성
• 평가 대상 LLM이 5종으로 제한적이며, fine-tuning되지 않은 zero/few-shot 상황에서의 성능만 보고되어 특화된 형식 번역 모델과의 비교가 부족
• pass@k 및 BEq 통과율이 여전히 낮아(controlled tier proof translation 29.7%, ecosystem tier 5.2%) 실용적 자동 번역 시스템으로 사용하기엔 성능 개선이 더 필요하며, 후속 연구로 검증된 semantic equivalence checker의 다중 ITP 확장과 라이브러리 매핑 자동화 방법이 요구됨

Evaluation

총평: 형식 증명 생태계의 파편화 문제를 정면으로 다루며 최초의 균형 잡힌 4-way cross-ITP 벤치마크와 통합 검증 인프라를 제공한 견실한 기여로, type-checking의 한계를 드러낸 BEq 검사 도입도 방법론적으로 의미 있으나, 더 넓은 라이브러리 커버리지와 다중 ITP 대상 의미 동치 검사로의 확장이 향후 과제로 남는다.