Graffiti3Loop: Generating and Resolving Formal Machine-Generated Graph Conjectures in a Loop

Motivation

• Known: 기존 formal-mathematics 벤치마크(예: PutnamBench)는 인간이 작성한 라이브러리나 올림피아드 문제집에서 가져온 정적 문제들로 구성되며, 이는 증명 완성 능력을 평가하는 데 유용하다.
• Gap: 기존 벤치마크들은 새로운 증거로부터 추측이 생성되고, 흥미로운 것으로 필터링되며, 이후 증명·반증·수정되는 실제 수학 연구 워크플로우를 부분적으로만 모델링할 뿐이며, machine-originated conjecture에 대한 증명/반증/가설 수정 벤치마크가 부재하다.
• Why: AI-for-mathematics 시스템이 단순 연습문제 풀이를 넘어 실제 수학적 발견 워크플로우(증거 검토, 가설 형성, 증명/반증, 가설 수정)에 참여할 수 있는지를 측정할 수 있는 새로운 평가 축을 제공하며, 기존 벤치마크가 이미 노출된 문제를 사용해 편향될 수 있다는 문제도 해결한다.
• Approach: GRAFFITI3의 유한 invariant table 기반 추측 생성을 Lean 4/mathlib 명제로 자동 번역하고, Lean-FRO Comparator로 제출된 증명이 의도된 형식적 도전 과제를 실제로 해결하는지 검증하는 파이프라인을 구축했다.

Achievement

Figure 2. Failure-mode counts for evaluated completions. Since no

1. GRAFFITI3BENCH-330 벤치마크 구축: GRAFFITI3에서 선택된 330개 그래프 이론 추측을 Lean 4 챌린지로 번역하고 provenance 메타데이터를 포함한 정적 벤치마크를 구성했다.
2. Lean-facing invariant interface 설계: native mathlib 개념, wrapper, 벤치마크 정의, deferred 항목을 분리하는 인터페이스를 구축했다.
3. Zero-tool 부정적 결과: Goedel-ProverV2-32B, DeepSeek-Prover-V2-7B, KiminaProver-72B 세 개 오픈웨이트 Lean prover가 330개 추측 전부에서 하나도 수락되지 않았으며, 이에 대한 실패 모드 분석(Lean API 누락, unsolved goal, answer block 누락, 부적절한 shortcut, 손상된 증명 조각)을 제공했다.
4. Tool-using agentic triage 성과: Claude Code 기반의 tool-using, human-guided triage가 42개의 Lean-checked 라벨(17개 증명, 25개 반증)을 산출했고, 85개는 계산적 counterexample을 찾았으며, 203개는 bounded counterexample search 후에도 참으로 남았다.
5. Tool 사용 vs 비사용 비교: tool 미사용 agentic baseline과의 대조를 통해 tool 사용이 novel mathematical problem 해결에 미치는 영향을 정량화했다.

How

Figure 2. Failure-mode counts for evaluated completions. Since no

• GRAFFITI3의 snapshot invariant table T와 grammar G로부터 base hypothesis B를 검출하고, support thresholding과 중복 slice 제거를 통해 pruned hypothesis family H를 구축
• 각 target invariant I⋆와 hypothesis h에 대해 h(G) ⇒ I⋆(G) □ f(G) 형태의 candidate relation을 생성하고, active table slice에서 반박되는 candidate를 제거, redundancy 및 empirical-envelope filter 적용
• Hazel을 이용해 survivor들을 순위화하고 예산 내 theory library C를 유지, 이를 Lean 4로 번역해 챌린지로 패키징 (Algorithm 1)
• Comparator를 이용해 모델 출력이 의도된 formal statement를 실제로 해결하는지(단순 컴파일이 아니라) 검증
• 세 개의 open-weight Lean prover에 대해 zero-tool baseline 실행 및 실패 유형 분류
• Claude Code 기반 tool-using agentic triage 및 tool 미사용 baseline 실행, 결과 비교

Originality

• 자동 추측 생성(GRAFFITI3)과 formal verification(Lean 4/Comparator)을 결합한 최초의 자율 루프를 제안
• 기존 static exercise corpus(PutnamBench 등)와 달리 machine-originated, 미검증(unseen) 추측을 사용해 벤치마크의 데이터 오염(contamination) 문제를 완화
• 단순 컴파일 여부가 아니라 의도된 statement 해결 여부를 검증하는 Comparator 활용 방식이 독창적
• proof, refutation, hypothesis-repair를 아우르는 discovery-workflow 지향적 벤치마크 설계

Limitation & Further Study

• 42개만 Lean-checked 라벨을 얻었고 나머지 288개는 미해결 상태로 남아 벤치마크의 실질적 커버리지가 제한적임
• tool-using triage가 human-guided라는 점에서 완전 자율 시스템의 성능을 측정한 것은 아니며, 재현성과 자동화 정도에 의문이 남음
• Lean 4/mathlib API의 미성숙성과 버전 민감성으로 인해 실패 원인이 수학적 난이도 때문인지 인터페이스 문제 때문인지 구분이 어려움
• bounded counterexample search로 참으로 남은 203개 항목은 실제 참임이 증명된 것이 아니라 반증되지 않았을 뿐이므로 후속 연구에서 완전한 증명/반증이 필요함
• 표본 크기(330개)가 제한적이며 그래프 이론 도메인에 국한되어 일반화 가능성 검증 필요

Evaluation

총평: machine-generated conjecture와 formal verification을 결합한 새로운 벤치마크 패러다임을 제시한 흥미로운 초기 연구이나, human-guided triage에 의존한 결과 해석과 낮은 해결률은 완전한 자율 시스템으로 나아가기 위한 추가 검증이 필요함을 시사한다.