Before Lean Checks: Candidate Exposure in Proof-Action Ranking

Motivation

• Known: TacticToe, GPT-f, LeanDojo/ReProver 등 학습 기반 guidance가 증명 탐색과 premise retrieval을 개선한다는 것은 잘 알려져 있으며, 이런 시스템들은 모델 규모, 탐색 폭, premise retrieval, tactic 생성에 초점을 맞춰 왔다.
• Gap: 기존 연구는 학습된 ranking이 실제로 Lean이 받아들일 수 있는 후보를 top-k 리스트 안에 남겨두는지(candidate exposure) 여부보다는, 정확한 trace match나 분류 정확도에 초점을 맞춰왔고, state-visible 정보와 future-tactic(hindsight) 정보를 명확히 분리하지 않았다.
• Why: 증명 에이전트는 Lean에 실제로 전달된 액션에 대해서만 verifier feedback을 받을 수 있으므로, ranking 단계에서 유효한 tactic이 숨겨지면 이후 어떤 검색이나 모델 개선도 그 피드백을 받을 기회 자체를 잃게 되어, AI4Math 파이프라인 전체의 병목이 될 수 있다.
• Approach: proof state에서 next-action 선택 이전에 보이는 state-visible 입력과 이후에만 알 수 있는 future-tactic 메타데이터(premises, tactic AST)를 분리하고, tactic-family 예측을 매개로 unguided retrieval, hard family routing, soft family prior(EPFP)라는 세 가지 랭킹 전략을 trace match와 실제 Lean 검증(500-state check)이라는 두 축으로 비교한다.

Achievement

Figure 2. Top-five trace exact match and Lean acceptance on the

1. Candidate exposure 개념화: 증명 실패를 tactic 생성 실패가 아니라 랭킹이 Lean-acceptable tactic을 top-k 밖으로 밀어내는 "handoff" 문제로 재정의했다.
2. State-visible vs future-tactic 분리: LeanDojo trace에서 흔히 섞여 쓰이는 next-action 이전/이후 정보를 명시적으로 구분하는 프로토콜을 제시했다.
3. EPFP 제안 및 검증: soft family prior(EPFP)가 hard family routing보다 대안을 더 많이 보존하면서 unguided retrieval과 trace-match 기준으로 경쟁력이 있음을 보였다.
4. 실제 Lean 검증으로 반증: 500개 held-out state에 대한 직접 Lean acceptance 측정에서는 unguided retrieval이 top-5 acceptance가 가장 높아, trace match만으로는 알 수 없는 결과를 드러냈다.

How

Figure 2. Top-five trace exact match and Lean acceptance on the

• 각 proof state s를 state-visible 표현 ϕ(s)로 매핑하고, 저장된 action의 학습 상태 sa와의 유사도 sim(ϕ(s), ϕ(sa))로 후보를 스코어링(unguided retrieval)
• tactic-family 모델 pθ(f(a)|ϕ(s))를 학습해 family를 예측
• EPFP는 rλ(s,a) = sim(ϕ(s), ϕ(sa)) + λ·pθ(f(a)|ϕ(s)) 형태로 soft하게 순위를 재조정하며 off-family 후보도 랭킹 가능하도록 유지
• hard family guidance는 예측된 top family를 lexicographic하게 우선시하는 게이트로 구성, true-family guidance는 상한선(ceiling)으로 포함
• mathlib4 curated subset에서 trace exact match(top-5)로 1차 비교, 이후 500개 중간 state에 대해 실제 Lean 실행으로 top-5 acceptance를 측정하여 두 지표를 대조

Originality

• Lean 증명 파이프라인에서 "ranking→verifier" 사이의 handoff를 candidate exposure라는 새로운 관점으로 정식화한 점
• state-visible 정보와 future-tactic(hindsight) 메타데이터를 엄격히 분리하는 평가 프로토콜을 제시한 점
• tactic-family 예측을 hard classification 문제가 아니라 ranking-control(soft prior) 문제로 재구성(EPFP)한 점
• trace match 지표와 실제 Lean acceptance 지표가 서로 다른 결론을 줄 수 있음을 직접 대조 실험으로 보여준 점

Limitation & Further Study

• mathlib4의 curated subset과 500개 state라는 비교적 작은 규모에서만 검증되어 일반화 가능성이 제한적임
• EPFP의 λ 하이퍼파라미터 선택 및 민감도 분석이 충분히 제시되지 않아 soft prior의 강건성이 불명확함
• unguided retrieval이 최종 Lean acceptance에서 가장 우수했다는 결과는 family prior 방식 자체의 실효성에 의문을 남기며, 왜 soft guidance가 근접하지만 능가하지 못하는지에 대한 심층 분석(예: family 예측 오류의 종류)이 부족함
• 향후 연구로는 더 큰 스케일의 라이브러리, 다양한 증명 보조 도구(Coq, Isabelle)로의 확장, family prior와 실제 tactic argument 생성 간의 상호작용을 함께 검증하는 실험이 필요함

Evaluation

총평: 랭킹 단계에서의 candidate exposure라는 관점은 AI4Math 커뮤니티에 실질적인 통찰을 주는 신선한 프레이밍이며, trace match와 실제 Lean 검증의 괴리를 명확히 보여준 실험은 후속 연구에 중요한 경고를 제공한다. 다만 실험 규모가 제한적이고 soft guidance가 unguided retrieval을 능가하지 못한 이유에 대한 분석이 더 필요하다.