FIPO-Prover: Formalization-Oriented Informal Proof Optimization for Efficient Formal Theorem Proving

Motivation

• Known: LLM 기반 informal reasoning은 formal theorem proving을 위한 자연스러운 인터페이스로 활용되어 왔으며, sketch, retrieval, decomposition 등의 기법이 informal reasoning과 formal proof 구성 사이의 간극을 메우는 데 효과적임이 선행 연구들(Jiang et al., Wang et al., Zhao et al., Varambally et al.)을 통해 알려져 있다.
• Gap: 그러나 informal proof는 중간 단계와 의존관계를 압축·생략하는 반면 formal proof는 명시적인 local context와 추적 가능한 dependency, 실행 가능한 proof 구조를 요구하기 때문에, Isabelle 등에서 관측되는 검증 오류의 근본 원인이 실제로는 informal proof 구조 자체의 상류(upstream)에 있음에도 이를 진단·수정할 구조화된 표현과 메커니즘이 부재했다.
• Why: informal-to-formal 간극을 구조적으로 진단·복구 가능하게 만드는 것은 formal theorem proving의 확장성 있는 자동화를 위한 핵심 병목을 해소하는 문제이며, 단순 샘플링 증가가 아닌 중간 증명 상태 최적화를 통한 효율적 search 방향을 제시한다는 점에서 중요하다.
• Approach: informal proof를 step-level causal pair(cause, effect, dependency, verifier-aligned state, revision history)로 구조화한 FIP-state로 표현하고, 이를 노드로 verifier-feedback 기반 recovery transition을 엣지로 하는 동적 FIP 검색 그래프에서 revision, expansion, pruning, backtracking, memory-guided search를 결합해 최적화한다.

Achievement

Figure 4. Diagnostics of FIPO-Prover’s search and recovery behavior.

1. 성능 향상: MiniF2F-Test에서 73.77% pass@1, 80.33% pass@3을 달성하여 direct LLM formalization baseline 및 기존 search/decomposition 기반 프레임워크(더 큰 pass@N 예산을 사용한 baseline 포함)를 능가하였다.
2. 효율성 입증: 동일한 FIP-state 예산 하에서도 시스템이 효율적으로 동작함을 보여, 성능 향상이 단순 샘플링 증가가 아닌 FIP-state 자체의 최적화에서 기인함을 입증하였다.
3. 분석적 근거 제시: 최종 FIP-state가 더 높은 downstream formalization utility를 가지며, revision이 proof state를 더 explicit하고 projection-friendly하게 만들고, 여러 recovery transition이 상호 보완적으로 작동함을 분석을 통해 확인하였다.

How

Figure 3. Search-control strategies for efficient FIP optimization based on feedback-driven FIP graph transitions.

• 문제 정식화: 정리 T에 대해 direct generation(T→P*)이 아닌 중간 FIP-state r을 도입하고, 노드가 FIP-state, 엣지가 recovery transition인 동적 proof graph G=(N,E)를 탐색하는 문제로 재정의.
• FIP-state 표현: r=(C,G)로 정의하며, C는 step-level causal pair 집합 {ci=(xi,yi,di,si,hi)}(cause, effect, dependency, verifier-aligned state, revision history), G는 dependency graph.
• Root FIP-state Initialization: 초기 informal proof i0을 생성하고 fstruct(T,i0)로 FIP 표현으로 변환하며, LLM judge가 explicit/projection 가능할 때까지 반복.
• Projection 및 verifier feedback: FIP-to-FP Projection Map fproj(T,rt)를 통해 causal pair를 Isabelle 구성요소(local fact, Isar block, have/show, tactic call 등)로 매핑하고, Isabelle 결과(yt, ϵt)를 내부 오류 유형으로 정규화, causal pair에 오류를 역추적하여 recovery transition으로 라우팅.
• Feedback-Driven FIP Graph Transition Policy: 정규화된 feedback ϵt에 따라 Local FIP-state Revision(Explicitization, Direction Changing, Step Insertion, Redundancy Pruning, Executabilization), Projected-Candidate Repair, Causal-Pair Expansion, Upstream Causal Backtracking, Branch Pruning, Memory-Augmented FIP Search Policy 등의 recovery transition을 선택.

Originality

• informal proof를 단순한 자연어 sketch가 아니라 step-level causal pair와 dependency graph로 구조화한 FIP-state라는 새로운 중간 표현을 제안하여 진단·복구·투영(projection)이 가능하도록 함.
• informal-to-formal theorem proving을 verifier feedback 기반의 그래프 최적화 문제로 재정식화하여, direct formal search(O(|Pformal|))도 exhaustive informal search(O(|Pall|))도 아닌 O(D·TFIP) 복잡도의 새로운 탐색 레짐을 제시.
• Local Revision, Candidate Repair, Expansion, Upstream Backtracking, Pruning, Memory-guided policy 등 다양한 recovery transition을 통합한 그래프 중심 검색 시스템을 설계하여 blame localization과 feedback analysis를 탐색 제어에 직접 활용.

Limitation & Further Study

• 본문 발췌만으로는 각 recovery transition(특히 memory-augmented search policy)의 세부 구현과 LLM judge의 신뢰도, 오류 정규화(error normalization)의 정확도에 대한 심층 분석이 제한적으로 제시됨.
• 평가가 MiniF2F-Test 한 벤치마크와 Isabelle 한 verifier에 국한되어 있어, Lean 등 타 formal system이나 더 크고 다양한 정리 집합에 대한 일반화 가능성은 추가 검증이 필요함.
• FIP-state 초기화 및 반복 과정에서 발생하는 계산 비용(LLM 호출 횟수 등)에 대한 구체적 비용-효율 트레이드오프 분석이 부족해 보이며, 후속 연구에서 다양한 verifier·언어로의 확장과 비용 효율성에 대한 정량적 비교가 필요함.

Evaluation

총평: informal-to-formal theorem proving의 근본적 간극을 구조화된 causal pair 표현과 verifier-guided 그래프 검색으로 해결하려는 시도가 독창적이며, MiniF2F-Test에서의 강력한 실험 결과가 이를 뒷받침하지만, 단일 벤치마크·단일 verifier 평가로 인해 일반화 가능성에 대한 추가 검증이 필요하다.