Lean2Isabelle: Factorized Cross-Assistant Proof Translation

Motivation

• Known: 기존 연구는 Lean 또는 Isabelle/HOL 각각의 assistant 내부에서 retrieval, verifier feedback, RL, proof repair 등을 활용한 same-assistant theorem proving을 발전시켜 왔으며, autoformalization 연구는 비형식 수학을 형식 진술/증명으로 변환할 때 type-checking만으로는 의미적 충실성을 보장할 수 없음을 지적해 왔다.
• Gap: 그러나 이미 검증된 Lean 증명을 다른 assistant(Isabelle/HOL)로 재사용하는 cross-assistant proof-level migration은 다뤄지지 않았으며, 실패가 target-statement 정합성, target proof 재구성, 혹은 두 단계의 cascade 중 어디서 발생하는지 구분하는 연구가 부재했다.
• Why: 서로 다른 proof assistant 생태계 간에 검증된 증명 자산을 재사용할 수 있으면 형식 수학 데이터와 모델 학습 자원의 파편화를 줄이고, 단일 assistant에 국한된 학습 문제를 넘어서는 일반화된 형식 증명 재사용이 가능해지므로 ML 기반 정리 증명 연구에 중요하다.
• Approach: Lean 정리와 증명을 입력받아 Isabelle/HOL target statement를 예측하는 statement 모델과, 그 statement에 조건화되어 완전한 Isabelle theory를 생성하는 proof 모델로 과제를 분리하고, Isabelle/PISA verifier 피드백 기반 GRPO로 proof 모델을 최적화한다.

Achievement

Figure 2. Training diagnostics and validation sweep. Left: verifier-feedback rates for equal-budget RL variants. Right:

1. 데이터셋 구축: FrenzyMath/Herald, LeanWorkbook, DeepSeek-Prover-V2 miniF2F 증명으로부터 Isabelle 검증 및 LLM 기반 semantic evaluation을 거친 Herald-ISA(26,104개), LeanWorkbook-ISA(9,683개), MiniF2F-DSP를 구성했다.
2. Statement-SFT 성능: LeanWorkbook-ISA와 MiniF2F-DSP에서 각각 86.0%, 85.7% EqStmt@1을 달성해 target statement 예측이 상당히 정확함을 보였다.
3. Reference-Statement에서 GRPO 개선: GRPO-MVP-DifficultyOrdered가 LeanWorkbook-ISA SemPass@1을 49.8%에서 54.3%로 향상시켜 verifier 기반 RL, MVP shaping, curriculum의 효과를 입증했다.
4. Predicted-Statement 종단 성능: 최종 시스템이 LeanWorkbook-ISA와 MiniF2F-DSP에서 각각 39.1%, 24.0% SemPass@1을 달성해 statement 예측과 proof 생성을 cascade했을 때의 실질 성능을 제시했다.
5. Source ablation을 통한 신호 검증: Lean 입력을 제거하거나 셔플하면 SemPass@1이 각각 45.3%, 43.2%로 하락해, 매칭된 Lean 증명 맥락이 실제로 유용한 신호를 제공함을 정량적으로 확인했다.

How

Figure 3. Curriculum exposure for the final GRPO-MVP-DifficultyOrdered run.

• 과제를 target-statement prediction과 statement-conditioned Isabelle theory generation으로 factorize
• Herald-ISA로 Statement-SFT와 Theory-SFT를 지도학습으로 초기화, Isabelle/HOL/AFP retrieval은 theory-teacher 구성 시에만 사용
• LeanWorkbook-ISA(9,683개, miniF2F-test overlap 제거)로 RL 및 주요 평가 수행
• GRPO 기반 proof translator를 Isabelle/PISA verifier feedback, Minimal Valid Progress(MVP) shaping, Difficulty-Ordered curriculum과 결합하여 학습
• Reference-Statement evaluation(검증된 target statement 고정, proof reconstruction만 측정)과 Predicted-Statement evaluation(statement+proof 모델 cascade, end-to-end 측정)을 분리 적용
• pass@k, EqStmt@1, SemPass@k 지표로 Herald-ISA, LeanWorkbook-ISA, MiniF2F-DSP에서 평가하고, verifier-only RL/MVP/curriculum에 대한 equal-budget ablation 수행
• source ablation(Lean 입력 제거, 셔플된 Lean proof 사용)으로 Lean context의 기여도 분석

Originality

• Lean-to-Isabelle 증명 이식이라는, 기존 same-assistant proving이나 informal-to-formal autoformalization과 구별되는 새로운 cross-assistant proof-level migration 문제를 정식화
• target-statement prediction과 statement-conditioned theory generation으로의 factorization을 통해 Reference-Statement/Predicted-Statement라는 이원 평가 체계를 도입해 오류 원인(statement 정합성 vs proof 재구성 vs cascade)을 분리 진단 가능하게 함
• Isabelle/PISA verifier feedback과 Minimal Valid Progress shaping, Difficulty-Ordered curriculum을 결합한 GRPO 학습 설계
• Herald-ISA, LeanWorkbook-ISA, MiniF2F-DSP 등 검증된 cross-assistant 병렬 자원을 직접 구축하여 이 문제 세팅 자체를 가능하게 함

Limitation & Further Study

• 성공 판정이 target-system checking과 LLM 기반 semantic evaluation의 조합에 의존하며, 저자들도 명시하듯 machine-checked cross-assistant preservation을 완전히 보장하는 인증(certificate)은 아니어서 semantic evaluator 자체의 오류/편향 가능성이 남는다
• Predicted-Statement 세팅에서의 SemPass@1(39.1%, 24.0%)이 Reference-Statement 대비 크게 낮아 cascade로 인한 성능 손실이 여전히 크며, 이 저하가 어느 하위 요인(statement 오류 전파, 학습 데이터 분포 등)에 더 기인하는지에 대한 세밀한 분석이 부족해 보인다
• 데이터셋(Herald-ISA, LeanWorkbook-ISA)이 아직 공개되지 않았고 향후 release가 "publication and release constraints" 해결에 좌우된다고 밝혀 재현성 측면에서 제약이 있다
• MiniF2F-DSP는 DeepSeek-Prover-V2가 생성한 Lean 증명에서 파생되어, 실제 인간 작성 증명이 아닌 모델 생성 증명에 대한 이식 성능이라는 한계가 있어 일반화 가능성 추가 검증이 필요하다

Evaluation

총평: 형식 증명 생태계 간 재사용이라는 실용적으로 중요하지만 상대적으로 덜 탐구된 문제를 명확한 factorization과 평가 체계로 정식화하고, verifier-grounded RL로 의미 있는 개선을 보인 견실한 초기 연구이나, 최종 end-to-end 성능과 semantic evaluator의 신뢰성 검증에는 추가 작업이 필요하다.