SorryDB: 인공지능 검증기가 실제 Lean 정리를 완료할 수 있는가?

SorryDB: Can AI Provers Complete Real-World Lean Theorems?

본 논문에서는 GitHub에서 수집한 78개의 실제 형식화 프로젝트에서 추출한, 동적으로 업데이트되는 오픈 Lean 작업 벤치마크인 SorryDB를 소개합니다. 기존의 정적인 벤치마크와 달리, 종종 경쟁 문제로 구성된 벤치마크와 달리, SorryDB 벤치마크를 활용하여 개발된 도구는 커뮤니티의 요구사항에 부합하고, 수학자들이 더 쉽게 사용할 수 있으며, 복잡한 의존성을 더 잘 이해할 수 있습니다. 또한, SorryDB는 지속적으로 업데이트되는 작업 목록을 제공함으로써 테스트 데이터 오염을 완화하고, 에이전트가 새로운 형식 수학 프로젝트에 기여할 수 있는 능력을 평가하는 데 있어 강력한 지표를 제공합니다. 본 논문에서는 일반적인 대규모 언어 모델, 에이전트 기반 접근 방식, 그리고 특수 목적의 기호 증명기를 포함한 다양한 접근 방식을 평가하기 위해, SorryDB에서 선택된 1000개의 작업으로 구성된 데이터셋을 사용했습니다. 실험 결과, 현재의 접근 방식들은 상호 보완적인 관계를 가지는 것으로 나타났습니다. Gemini Flash를 기반으로 한 에이전트 기반 접근 방식이 가장 높은 성능을 보였지만, 다른 상용 대규모 언어 모델, 특수 목적 증명기, 또는 선별된 Lean 전술 목록보다 반드시 더 우수한 것은 아니었습니다.

We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.