기술 요약: ITPEVAL – 상호작용형 정리 증명기 간의 형식적 번역 벤치마킹

1. 문제 정의

현재의 형식 정리 증명(formal theorem proving) 생태계는 파편화되어 있다. 대규모 언어 모델(LLM)이 자동 정리 증명 및 자동 형식화(autoformalization) 분야에서 상당한 성공을 거두었음에도 불구하고, 검증된 결과물들은 서로 호환되지 않는 상호작용형 정리 증명기(ITP) 내에 고립되어 있다. 각 시스템(예: Lean 4, Rocq, Isabelle, HOL Light)은 고유한 논리적 기초, 택틱(tactic) 언어, 그리고 수학적 라이브러리를 구현한다. 결과적으로, 한 시스템에서 증명된 정리는 다른 시스템에서 직접 호출될 수 없으며, 이는 형식화 작업의 중복을 초래하고 학습 기반 증명기를 위한 학습 가능한 데이터의 가용성을 제한한다.

교차 ITP 번역—정확성을 유지하면서 시스템 간의 형식적 증명을 변환하는 작업—은 체계적인 연구가 거의 이루어지지 않았다. "100가지 정리 형식화(Formalizing 100 Theorems)" 카탈로그나 Dedukti와 같은 상호운용성 프레임워크를 통한 기존의 노력들은 커버리지를 추적하거나 중간 표현을 통한 증명 교환을 가능하게 하는 데 집중할 뿐, 번ill역 품질을 평가하기 위한 표준화된 벤치마크를 결여하고 있다. 또한, 기존의 평가 방법론은 불충분하다. 단순한 타입 체크(type-checking)는 의미론적 정확성에 대해 높은 허위 양성(false-positive) 비율을 나타내며, 코드 번역 벤치마크는 ITP에 내재된 깊은 논리적 기초의 차이를 고려하지 못한다.

2. 방법론 및 벤치마크 설계

저자들은 ITPEVAL을 제시한다. 이는 네 가지 주요 ITP인 Lean 4, Rocq(구 Coq), Isabelle, HOL Light 간의 자동 형식 증명 번역을 평가하기 위해 설계된 최초의 벤치마크이다. 이 벤치마크는 두 가지 뚜렷한 논리적 기초, 즉 귀납적 구성의 계산론(Calculus of Inductive Constructions, CIC)과 고차 논리(Higher-Order Logic, HOL)를 포괄한다.

2.1. 데이터 구조

이 벤치마크는 난이도의 원인을 격리하기 위해 두 가지 별도의 티어로 구성된 1,560개의 소스 파일과 6,848개의 정리로 구성된다.

• 티어 A (제어됨): Babel-formal 벤치마크에서 유도된 64개의 자기 완결적이고 공리화된(axiomatized) 파일(660개 레마)을 포함한다. 이 파일들은 자체적인 정의와 가정을 포함하여 특정 증명기 전용 라이브러리에 대한 의존성을 피한다. 이 티어는 근본적인 번역 문제(예: 타입 이론, 유니버스 레벨, 암시적 인자)를 격리한다.
• 티어 B (생태계): 실제 커뮤니티 라이브러리에서 추출된 형식화 내용을 포함하며, API 불일치, 명명 규칙, 증명 스타일의 차이를 노출한다. 이 티어는 다음을 포함한다:
  • 모든 네 가지 시스템에 걸쳐 정렬된 Formalizing 100 Theorems의 232개 파일(4,924개 레마).
  • 다양한 경시 수학 콘텐츠를 제공하는 miniF2F의 1,264개 단일 정리 파일(문장만 포함).

설계 단계에서 **사방향 교차 요구사항(four-way intersection requirement)**을 강제한다: 누락된 데이터로 인한 혼란 없이 깨끗한 방향성 비교를 보장하기 위해 모든 파일은 네 가지 ITP 모두에서 형식화되어야 한다.

2.2. 번역 작업

ITPEVAL은 두 가지 주요 작업을 평가한다:

1. 문장 번역 (Statement Translation): 증명 본문을 자리 표시자(예: sorry)로 대체한 타겟 ITP 코드를 생성한다. 검증을 위해서는 생성된 파일이 타겟 시스템에서 타입 체크를 통과해야 한다.
2. 증명 번역 (Proof Translation): 자리 표시자 없이 완전하고 컴파일 가능한 증명 파일을 생성한다. 검증을 위해서는 전체 파일이 타겟 증명기에서 성공적으로 컴파일되어야 한다.

2.3. 검증 인프라

방법론의 핵심 구성 요소는 통합 다중 ITP 검증 인프라인 itpeval이다. 이기종 ITP 실행 모델(예: Isabelle 및 HOL Light의 높은 시작 비용)의 이질성을 해결하기 위해, 시스템은 다음을 채택한다:

• 상태 격리형 웜 백엔드 (State-isolated warm backends): 모든 체크가 신선한 환경에서의 아티팩트 검증과 관찰적으로 동일하도록 보장하여 선언 누출(declaration leakage)을 방지한다.
• 네이티브 타겟 증명기 체크: 모든 라벨은 표면적인 휴리스틱이 아닌 실제 타겟 ITP에 의해 생성된다.
• 적응형 스케줄링: 처리량을 관리하면서 파일당 체크 의미론을 보존하기 위해 지속적인 워커(persistent workers), 세션 배칭, 포크 서버를 사용한다.

2.4. 의미론적 동등성 체크

타입 체크가 필요조건이지만 충분조건은 아니라는 점을 인식하여, 저자들은 Lean 4 타겟을 위한 양방향 확장 정의적 동등성 (Bidirectional Extended Definitional Equivalence, BEq) 체크를 구현하였다. 이 결정론적 체크는 생성된 문장 $G$와 참조 문장 $R$이 제한된 증명 탐색을 사용하여 서로를 함의하는지($G \vdash R$ 및 $R \vdash G$)를 검증하며, 추가적인 모델 의존적 변동성을 피한다.

3. 주요 기여

1. 사방향 정렬 벤치마크: Lean 4, Rocq, Isabelle, HOL Light에 걸친 1,560개 파일과 6,848개 정리의 데이터셋으로, 라이브러리 의존성의 비용을 정량화하기 위해 제어 및 생태계 티어로 구조화되었다.
2. 통합 검증 인프라: 이기종 증명기 간의 확장 가능하고 재현 가능한 평가를 가능하게 하는 상태 격리형 클라이언트(itpeval)를 제공한다.
3. 체계적인 LLM 평가: 12개의 방향성 번역 쌍에 대해 다섯 가지 프런티어 및 오픈 웨이트 모델(GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B)을 평가하였다.
4. 의미론적 충실도 분석: 네이티브 타입 체크만으로는 의미론적 정확성을 과대평가할 수 있음을 입증하기 위해 BEq를 적용하였다.
5. 탐색적 라운드 트립 연구: 타겟 의존적 검증 패턴과 다중 ITP 컨텍스트의 잠재적 이점을 평가하기 위해 자동 형식화 및 자동 비형식화 루프를 조사하였다.

4. 결과

4.1. 번역 성능

• 문장 번역: 최고 성능 모델인 GPT-5.5는 전체적으로 29.1%의 pass@1을 달성했다. DeepSeek-V4-Pro가 27.1%로 그 뒤를 이었다. 다른 모델들(Gemini 14.0%, Qwen 및 Claude 10% 미만)은 성능이 크게 떨어졌다.
• 증명 번역: 성능이 현저히 낮아졌으며, GPT-5.5는 전체적으로 10.5%의 pass@1만을 달성했다.
• 티어 간 격차: 제어 티어(Tier A)가 생태계 티어(Tier B)보다 일관되게 쉬웠다. 증명 번역의 경우, GPT-5.5는 제어 파일에서 **29.7%**에 도달했으나 생태계 파일에서는 **5.2%**에 그쳤다. 이는 라이브러리 불일치(API, 명명, 자동화)가 논리적 기초의 차이보다 가장 큰 실패 원인임을 나타낸다.
• 방향성 비대칭성: 번역 난이도는 타겟에 따라 크게 달라진다. Isabelle과 HOL Light는 문장 번역에 강력한 타겟이지만, Isabelle은 증명 번역에서 가장 어려운 타겟이 된다. 논리적 기초의 유사성(예: CIC에서 CIC로)이 높은 성공률을 보장하지는 않으며, 타겟 생태계의 관습이 더 큰 역할을 한다.

4.2. 의미론적 동등성 (BEq)

miniF2F에서 검증된 Lean 4 문장 번역에 BEq를 적용했을 때:

• 검증된 번역 중 **54.0%**만이 동등성 체크를 통ผ่าน했다.
• Claude Sonnet 4.6은 검증된 번역 중 가장 높은 BEq 통과율(83.8%)을 보였으나, 다른 모델들은 34.5%에서 48.4% 사이였다.
• 이 결과는 문장이 구문론적으로 유효(타입 체크 통과)하더라도 의미론적으로 원래의 정리보다 약하거나 변형될 수 있음을 보여준다.

4.3. 라운드 트립 및 자동 형식화

다중 ITP 라운드 트립 연구(NL $\to$ Formal $\to$ NL $\to$ Formal)에서, Rocq와 HOL Light는 두 형식화 단계 모두에서 약 3분의 1의 출력을 검증한 반면, Lean 4는 11% 근처에 머물렀고 Isabelle은 최종 단계에서 4.3%로 떨어졌다. 다중 ITP 컨텍스트는 특정 모델-타겟 조합에 대해 잠재적 이점(예: Lean 4의 1단계 통과율을 4.8%에서 10.6%로 개선)을 보여주었으나, 결과가 모든 시스템에 균일하게 나타나지는 않았다.

5. 의의 및 주장

본 논문은 ITPEVAL이 형식 번역을 위한 최초의 체계적인 사방향 벤치마크를 제공하며, 주요 장벽이 논리적 기초 자체가 아니라 생태계 수준의 의존성(라이브러리, API 및 증명 관습)임을 밝혀냈다고 주장한다.

저자들은 다음을 강조한다:

• 네이티브 검증은 필수적이다: 표면적인 휴리스틱이나 타입 체크만으로는 의미론적 충실도를 평가하기에 불충식하다.
• 인프라가 중요하다: 신뢰할 수 있는 교차 ITP 평가를 위해서는 선언 누출과 같은 혼란 요인을 방지하기 위한 상태 격리형 검증이 필요하다.
• 향al 방향: 분야는 순수한 기초적 번역보다는 검색(retrieval), 라이브러리 매핑, API 정렬을 우선시해야 한다. 또한 본 논문은 제로샷 평가 설정, BEq의 Lean 4 타겟 제한, miniF2F와 같은 공개 데이터셋의 학습 데이터 오염 가능성 등의 한계를 언급한다.

이 연구는 형식적 번역의 진보를 측정하기 위한 토대를 마련하며, 향-후 시스템들이 견고한 ITP 생태계 간 상호운용성을 달려하기 위해서는 "라이브러리 불일치" 문제를 해결해야 함을 시사한다.