LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization

Motivation

• Known: verifier-in-the-loop 시스템(M2F, Automatic Textbook Formalization, Gauss 등)이 대규모 formal artifact를 생성할 수 있음이 알려져 있으며, miniF2F, ProofNet, PutnamBench 등 proof-only 벤치마크는 이미 주어진 formal statement를 증명하는 능력만을 측정한다.
• Gap: document-to-project formalization에서 어떤 runtime 메커니즘(큐 관리, 툴 접근, source checkpoint 등)이 completion, auditability, efficiency에 실제로 영향을 미치는지는 불명확했으며, 기존 연구는 이미 formal statement가 주어진 상태에서 증명만 채우는 세팅에 초점을 맞춰 왔다.
• Why: 전체 수학 논문을 처음부터 소스 충실성을 유지하며 buildable Lean project로 변환하는 것은 formal verification의 실용적 확산에 핵심적이며, 어떤 runtime 설계 요소가 실제로 성공률과 비용에 기여하는지 밝히는 것은 향후 대규모 autoformalization 시스템 설계에 중요한 지침을 제공한다.
• Approach: LeanFlow는 deterministic source preflight, source-map 기반 blueprint, statement/source gate, 프로그램적 prover queue, 그리고 LeanProbe라는 캐시 same-file verifier로 구성된 워크플로우를 도입하고, 두 개의 미공개 수학 논문(정수론, 측도론)에 대해 모델·워크플로우·툴셋 ablation을 통해 이를 검증한다.

Achievement

Figure 2. File-scoped proving loop. Failed checks update theorem-

1. 완료율 향상: Kimi-K2.6에서 full workflow는 두 document-level 프로젝트 모두 2000-call 예산 내에 완료했으나 no-queue variant는 예산 한계에 도달, workflow control이 결정적임을 보임.
2. 토큰 효율성: GPT-5.5에서는 모든 document-level variant가 완료되었으나, full workflow가 두 소스 모두에서 가장 낮거나 동률로 낮은 input-token 비용을 달성함.
3. 검증 속도 개선: LeanProbe가 growing-prefix Lake check 대비 약 9–14배 빠른 캐시 기반 검증을 제공함(Table 6).
4. 보완적 벤치마크 성능: RLM25의 PFR slice에서 75.7% BEq+ 달성, ICML 2026 AI for Math TCS challenge의 5개 프로젝트를 GPT-5.5 런에서 모두 해결함.

How

Figure 1. LeanFlow document-to-project pipeline. Dashed regions separate the formalizer and prover phases; the green sil

• Source artifact(D)를 deterministic preflight로 처리하여 블록, PDF, 참조, 지원 파일을 추출하고 모호한 TEX root를 거부
• Formalizer가 source span과 계획된 Lean declaration을 연결하는 project-local blueprint(source map)를 구축, dependency·proof note·scope change 기록
• Statement/source gate가 proof search 이전에 생성된 declaration type이 원본 소스 주장과 일치하는지 확인(statement type-checking, faithfulness 분리)
• Programmatic workflow manager가 theorem queue, failed-attempt memory, retry budget, verification record, log, checkpoint를 관리하며 한 번에 하나의 target만 진행, 외부 Lean 검증 통과 후에만 다음으로 이동
• LeanProbe(LeanInteract 기반)가 현재 declaration 이전까지의 Lean 환경을 캐시하여 저지연 진단·proof-state 피드백 제공, 최종 승인은 표준 Lean/Lake build로 수행
• 두 논문(Frisch & Vaserstein의 Pythagorean triples 논문, Lyons & Zumbrun의 Cramer–Wold 정리 논문)에 대해 queue management vs free-running, full Lean tool access vs terminal-only, source-blueprint checkpoint vs direct generation을 ablation
• Kimi-K2.6과 GPT-5.5 두 모델로 API calls, input/output tokens, task outcome을 측정

Originality

• formalizer(수학적 편집)와 prover(워크플로우 제어)를 명시적으로 분리하는 아키텍처 설계
• 생성된 각 Lean declaration에 대해 원본 소스 span과의 provenance(π(d))를 명시적으로 기록하는 blueprint 개념 도입
• proof search 이전에 statement/source gate를 두어 statement type-checking과 faithfulness를 분리 검증하는 절차
• LeanProbe라는 캐시 기반 same-file verifier를 새로 구현하여 proof-repair 루프의 지연시간을 크게 단축
• 기존 proof-only 벤치마크와 달리, 이전에 formalize된 적 없는 실제 전체 논문 두 편을 대상으로 한 document-level case study 설계

Limitation & Further Study

• 두 개의 case study 논문만을 대상으로 하여 일반화 가능성이 제한적이며, 저자들도 M2F 등과의 직접 비교가 재현 조건 차이로 어렵다고 인정함
• GPT-5.5 세팅에서는 모든 variant가 완료되어 성공/실패의 이분법적 차이가 나타나지 않아, workflow 이점이 토큰 효율성이라는 간접 지표로만 나타남
• 소스 문서 규모가 통제된 ablation을 위해 비교적 짧게 선택되어, 대규모 교재나 프로젝트급 소스에 대한 확장성은 검증되지 않음
• 후속 연구로 더 다양한 수학 분야와 더 큰 규모의 문서, 더 많은 모델에 대한 ablation이 필요함

Evaluation

총평: document-level autoformalization의 runtime 설계 요소를 체계적으로 분리해 실증한 케이스 스터디로, 실용적 통찰과 새로운 오픈소스 도구(LeanProbe)를 제공하는 의미 있는 workshop 논문이나, 두 사례만으로는 일반화에 한계가 있다.