Learned Interventions Inside Lean 4's grind

Motivation

• Known: SAT/SMT 분야에서는 NeuroSAT, Graph-Q-SAT, FastSMT 등 정적 feature 기반으로 branching·instantiation heuristic을 학습하는 연구가 다수 존재하며, 정리증명 분야에서는 tactic이나 proof step 단위로 학습하는 접근(LLM 기반 proof step 생성, premise selection, portfolio/algorithm selection 등)이 주류이다.
• Gap: 기존 연구들은 tactic 전체를 교체하거나 정적 feature로 검색 상태를 평가하는데, grind처럼 non-monotone 내부 검색을 가진 tactic에서는 always-on 학습된 heuristic이 한 증명을 살리는 대신 다른 증명을 깨뜨려 순이익이 거의 없고, branch explosion이 런타임 속성이라 정적 feature만으로는 예측이 불가능하다는 점이 규명되지 않았다.
• Why: 강력한 소수의 tactic(예: grind)이 자동 정리증명의 핵심 백엔드로 쓰이는 상황에서, 그 내부 검색 결정(instantiation, case-split 선택)을 안전하게 개선할 수 있다면 tactic 전체 재작성 없이도 광범위한 하위 증명 시도에 파급 효과를 줄 수 있다.
• Approach: stock grind를 먼저 실행하고 실패한 goal에 대해서만 학습된 개입(cost-aware e-match filter, bounded lookahead)을 적용하는 failure-triggered cascade를 설계하여, grind가 이미 풀 수 있던 증명을 절대 깨뜨리지 않도록 보장한다.

Achievement

held-out 855개 정리 집합에서 cost-aware e-match filter가 stock grind 대비 2개 더 풀고 약 5% 더 빠르게 실행되며, stock grind가 실패하는 지점에서만 실행되는 lookahead 단계는 timeout 나던 정리 5개를 추가로 증명한다. 또한 4개의 feature 기반 모델이 올바른 case split을 정적으로 예측하는 데 random보다 나을 게 없다는 negative result를 통해, branch explosion이 정적 feature로 포착되지 않는 런타임 속성임을 규명했다.

How

• Lean 4의 grind tactic 내부 action loop(solvers ▷ instantiate ▷ splitNext ▷ mbtc)에서 tactic을 포크하지 않고 개입 가능한 세 지점(e-match instance filter, split-target selection, premise augmentation)을 식별
• e-match filter: lemma identity, head symbol, conclusion/premise token, e-matching round, 과거 유용성 등 135차원 feature를 사용해 각 instantiation의 proof-relevance를 예측하는 3-layer MLP(135→64→32→1)를 binary cross-entropy로 학습, call site에서 저가치 instantiation을 drop
• lookahead(oracle) 실험: 여러 candidate가 있는 split 결정마다 각 candidate를 강제 선택해 나머지 증명을 고정한 채 grind를 재실행하여 실제 결과를 기록, NUMINA에서 4,120개 multi-candidate 결정으로부터 약 16K개의 forced-choice 결과 수집
• 오라클이 항상 가장 저렴한 split을 선택하도록 하여 capability 개선 효과를 측정
• split-target 예측을 위해 MLP 및 gradient-boosted tree 등 goal/candidate-level feature 기반의 4개 소형 모델을 학습해 static prediction의 한계를 검증
• e-match filter의 학습 데이터를 20배 확장해도 니치가 넓어지지 않음을 확인, lemma-identity 메커니즘 자체의 한계임을 시사

Originality

• non-monotone 내부 검색을 가진 자동화 tactic에서 always-on 학습된 heuristic이 실패할 수 있음을 실증하고, 이를 우회하는 failure-triggered cascade라는 안전한 배포 패턴을 제시
• tactic 전체를 대체하는 대신 tactic 내부의 특정 결정(instantiation filter, case-split lookahead)에만 학습을 적용하는 fine-grained 개입 방식
• static feature 기반 예측이 실패하는 지점을 oracle forced-choice 실험으로 정량적으로 규명하고, branch explosion이 dynamic(runtime) property임을 negative result로 명시적으로 보고
• Lean 4 grind tactic 내부에 실제로 동작하는 Lean-native 구현(sub-millisecond latency)으로 검증한 점

Limitation & Further Study

• e-match filter의 개선 폭(+2 solves, 5% 속도)이 크지 않고 데이터 20배 확장에도 니치가 확장되지 않아 lemma-identity 기반 메커니즘 자체의 근본적 한계가 존재
• case-split 예측에서 4개 모델 모두 random 수준에 그쳐 static feature의 한계는 확인했으나, 이를 대체할 효과적인 dynamic feature나 학습 방법은 제시하지 못함
• lookahead 방식이 stock grind 실패 이후에만 작동하므로, 추가 계산 비용(rerun 비용)이 발생하는데 이에 대한 비용 분석이 충분히 제시되지 않음
• 평가가 NUMINA 및 855개 held-out 정리라는 특정 벤치마크에 한정되어, 일반화 가능성에 대한 추가 검증이 필요
• 후속 연구로 dynamic/runtime feature를 포착할 수 있는 lookahead 기반 학습 방법의 확장, 그리고 다른 SMT/ATP tactic에 대한 일반화 검증이 필요

Evaluation

총평: non-monotone 검색을 가진 자동화 tactic 내부에 학습을 안전하게 통합하는 실용적이고 신중한 설계를 제시하며, positive result와 negative result를 모두 투명하게 보고한 점이 특히 신뢰할 만하다. 개선 폭 자체는 크지 않지만 failure-triggered cascade라는 설계 원칙은 다른 symbolic solver에도 적용 가능한 일반적 통찰을 제공한다.