Lean Disprove: Certified Counterexample Search for AI-Assisted Formal Mathematics

Motivation

• Known: LLM 기반 formal mathematics 연구는 PutnamBench, MiniF2F, ProofNet 등 참인 명제의 증명(proof construction)에 집중되어 왔으며, plausible이나 Nitpick, Nunchaku 같은 도구는 반례(counterexample)나 countermodel을 찾지만 Lean 커널이 검증하는 증명 항을 생성하지는 않는다.
• Gap: 거짓 명제를 증명 보조기(proof assistant) 안에서 커널 검증된 반례로 확정하는 전용 대화형 도구 지원이 부재했으며, 기존 방법들은 반례 후보를 제시할 뿐 이를 Lean 커널이 인증하는 항으로 끌어올리는 체계적 절차가 없었다.
• Why: 증명 시도에 앞서 명제가 이미 반증 가능한지 저렴하게 확인할 수 있으면 추론 예산을 절약할 수 있고, 커널 기반 검증을 통해 LLM 주도 형식화 파이프라인 전체의 신뢰성(verifiability)을 유지할 수 있다는 점에서 중요하다.
• Approach: decision procedure, finite enumeration, random sampling, 외부 SAT/SMT 스크립트 등을 포함하는 방법 레지스트리에서 목표의 profile에 따라 반증 방법을 선택하고, 후보 witness를 shape-specific negation term으로 조립해 Lean 커널이 수락할 때만 REFUTED로 보고하는 여섯 단계(profile-plan-work-checkpoint-review-continue/stop) 순환 구조를 사용한다.

Achievement

Figure 1. System overview of /disprove, an agentic coding com-

1. 문제 정식화: 증명이 아닌 반증(disproof)을 Lean 커널이 게이트하는 REFUTED/WITNESS-UNCERTIFIED/INCONCLUSIVE의 tri-state 과제로 최초로 명확히 정식화했다.
2. 대화형 여섯 단계 순환 시스템: 증거 기반으로 랭킹되는 동적 메뉴(지식 검색, 방법, 설정), 명시적 사용자 체크포인트, 감사 로그를 갖춘 순환 구조를 설계했으며, 이후 순환은 고정된 표가 아니라 누적된 증거로부터 방법을 재랭킹한다.
3. shape-aware 인증: 7가지 canonical goal shape에 대해 shape별 Lean recipe와 atom-tactic fallback cascade를 마련하고, 신뢰할 수 없는 외부 SAT/SMT witness를 커널 검증 항으로 끌어올리는 절차를 구현했다.
4. 오픈소스 구현 및 진단적 평가: lean4-skills 패키지로 공개하고, 16개 타겟 벤치마크에서 거짓 타겟 15개 전부를 인증했으며(bare decide baseline은 10개), 추가된 각 기능이 하위 단계가 놓친 타겟을 최소 하나 이상 추가로 인증함을 보였다.

How

Figure 1. System overview of /disprove, an agentic coding com-

• Target Profile 단계에서 목표의 shape·decidability·grid 특성을 프로파일링
• Plan 단계에서 지식 검색(knowledge search)을 수행해 method·config 후보를 선정
• Work 단계에서 선택된 method(decision procedure, finite enumeration, random sampling, 외부 SAT/SMT 스크립트 등)를 실행하여 미신뢰(untrusted) witness 후보 생성
• Checkpoint 단계에서 lake env lean으로 Lean 커널 게이트를 통과하는지 검사 (sorry·admit 부재, 승인된 axiom whitelist인 propext, Classical.choice, Quot.sound, 조건부 Lean.ofReduceBool만 허용)
• Review 단계에서 결과를 REFUTED/WITNESS-UNCERTIFIED/INCONCLUSIVE로 분류
• Accumulate 단계에서 증거 로그를 누적하고, Continue/Stop 단계에서 cycle·stuck-cycle·wall-clock 예산에 따라 순환을 재개하거나 종료

Originality

• 증명(proof) 중심이었던 LLM 형식수학 연구에서 반증(disproof)을 독립적인 일급 과제로 재구성(reframing)한 점
• 학습이 필요 없는(training-free) 고정 method registry 기반 오케스트레이션으로, Li et al. (2026a)의 LLM fine-tuning 접근과 차별화
• 외부 SAT/SMT solver의 미신뢰 witness를 Lean 커널 검증 항으로 끌어올리는 multi-method 통합
• WITNESS-UNCERTIFIED라는 새로운 진단적 중간 상태를 도입해 근접 실패(near-miss)를 명시적으로 구분

Limitation & Further Study

• 그래프 극한 이론에서의 동기 부여 사례(motivating failure, double-pin tree)는 /disprove가 실제로 인증하지 못한 사례로, 시스템의 현재 범위를 벗어난다는 한계가 저자들 스스로에 의해 인정됨
• 벤치마크가 16개 타겟으로 소규모(pilot)이며, Li et al. (2026b)의 3,000문제 벤치마크와 직접 비교하지 않아 폭넓은 일반화 가능성이 검증되지 않음
• 저자들의 registry는 decidable·finite·solver-amenable 목표에 특화되어 있어, 실수(real)·다항식·측도론적 명제 등 더 넓은 범주로의 확장은 향후 과제로 남겨짐
• shape·method coverage 확장 및 더 복잡한 수학적 대상(orbit, spectral moment 등)에 대한 반증 능력 향상이 필요함

Evaluation

총평: 증명 편중된 LLM 형식수학 생태계에서 커널 검증된 반증이라는 상보적 과제에 전용 대화형 도구를 최초로 제공한 실용적이고 참신한 시도이며, 작은 규모지만 명확한 진단적 벤치마크로 접근법의 타당성을 입증했다.