Certifying Failed Lean Proof-Agent Searches with Exact Replay

Motivation

• Known: LLM은 Lean tactic을 제안하고 Lean이 이를 accept/reject하는 verifier loop를 통해 정리 증명 탐색을 수행할 수 있음이 알려져 있으며, 이는 검증 가능한 mathematical agent의 유망한 테스트베드로 여겨진다.
• Gap: 그러나 proof search가 실패했을 때 이것이 탐색(search) 자체의 문제인지, 제안된 tactic 후보(support)에 핵심 tactic이 누락된 것인지, 아니면 애초에 도달 불가능한 목표(out-of-reach goal)를 시도한 것인지 구분할 방법이 없어 실패한 탐색이 actionable하지 않다는 문제가 존재한다.
• Why: 실패 진단이 불가능하면 에이전트가 다음에 무엇을 시도해야 할지(새 후보 추가, 재탐색, 목표 포기) 결정할 근거가 없으므로, 이 문제를 부분적으로라도 exact하게 해결하는 것은 수학 에이전트의 신뢰성과 반복 개선(iteration) 파이프라인 구축에 중요하다.
• Approach: 각 도달한 Lean state에서 모델이 제안한 tactic들을 recorded support로 저장하고, 이 저장된 tactic들만을 고정된 depth·timeout 경계 내에서 재생(replay)하여 Lean-checked proof, closed certificate(저장된 어떤 tactic 경로도 목표를 증명하지 못함), 또는 timeout transcript 중 하나를 산출하는 방식을 취한다.

Achievement

closed certificate가 발생한 경우 in-scope lemma의 statement를 prompt에 추가하는 등의 결정론적 repair 정책을 적용하여, CSLib-Holes 벤치마크에서 oracle-free solved count를 10/100에서 39/100으로 끌어올렸으며 모든 repair가 Lean에 의해 재검증되었다.

How

• CSLib-Holes라는 공개 CSLib Lean 프로젝트에서 기계적으로 선정된 100개의 proof hole로 구성된 고정 벤치마크를 구축하고, 원본 증명은 에이전트에게 숨김
• Lean REPL 기반 파이프라인으로 tactic candidate, Lean transition, verifier 호출, timeout metadata, exact score pruning, replay repair를 기록
• BFS-Prover 기반 base replay로 10/100 해결, 74개 closed certificate 도출
• in-scope lemma statement를 prompt에 추가하는 repair(74건 중 16건 해결) vs. 매칭된 search-only widening(74건 중 6건 해결) vs. target-statement control(74건 중 12건 해결)을 비교
• 반복적인 Lean-checked candidate 추가를 통해 최종 39/100 해결까지 도달
• 각 repair 효과를 pooled exact McNemar test(p=0.227)로 통계 검정하여 failed-search frontier의 기여가 target statement 단독 대비 결정적인지 확인
• exact branch-and-bound variant로 완료된 최고 점수 경로 이후의 부분 경로를 pruning하여 verifier 호출 수 절감

Originality

• 실패한 proof search를 "탐색 실패 vs 후보 누락 vs 목표 도달불가"로 정확히 구분하려는 시도가 아니라, 저장된 recorded support에 대해서만 exact replay를 수행하여 이 중 일부(후보 소진 여부)를 정확하게(formal proposition으로) 판별하는 bounded audit 개념을 제시
• closed certificate라는 개념을 도입해, "이 후보 집합으로는 증명 불가능하다"는 negative signal을 Lean 검증 가능한 형태로 formalize
• CSLib-Holes라는 새로운 100건 벤치마크를 공개 CSLib 프로젝트로부터 기계적으로 생성하여 재현 가능한 오라클-프리 평가 체계를 구축
• in-scope lemma retrieval, search-only widening, target-statement control이라는 세 갈래 대조군을 두어 failed-search frontier의 실제 기여도를 통계적으로 검증하려 시도

Limitation & Further Study

• Proposition 1이 보장하는 것은 고정된 depth·timeout·candidate budget 하에서의 finite recorded support graph에 대한 negative 결과일 뿐, 정리 자체의 불가증명성이나 모델의 전체 분포에 대한 주장이 아니므로 certificate의 실질적 의미가 제한적임
• pooled exact McNemar p=0.227로 failed-search frontier가 target statement 단독보다 유의미하게 더 도움이 되는지가 directional일 뿐 decisive하지 않아, 핵심 주장(frontier 정보의 부가가치)이 통계적으로 확증되지 않음
• 100개 사례 중 23개만 proof-state oracle-clean subset이고 나머지는 command-level 검증에 의존하는 등 벤치마크 규모와 정합성이 제한적
• 결정론적 repair 정책(conjunction projection, Iff.trans 등)이 특정 유형의 증명에 한정되어 있어 일반화 가능성이 불확실하며, 후속 연구로 더 다양한 repair 정책과 더 큰 벤치마크로의 확장이 필요
• 특정 Lean 버전, toolchain, 모델(BFS-Prover-V2-7B, Qwen2.5-7B-Instruct)에 종속적이어서 다른 설정에서의 재현성 및 일반화가 추가로 검증되어야 함

Evaluation

총평: 실패한 Lean proof search에 대해 정확한 replay와 closed certificate라는 개념으로 일부 진단을 formal하게 만드는 실용적이고 명확한 아이디어이나, 핵심 주장인 failed-search frontier의 부가가치가 통계적으로 결정적이지 않아 워크숍 수준의 초기 탐색 연구로 평가된다.