TheoremBench: 형식 수학에서의 정리 증명에 대한 LLM 평가

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

최근 LLM은 형식적 증명 벤치마크에서 뛰어난 성과를 거두었습니다. 그러나 기존의 평가는 주로 경쟁적인 문제에 집중되어 있으며, 모델이 더 길고 복잡한 의존성을 가진 수학적 전개 과정에서 어떻게 작동하는지를 제대로 반영하지 못하는 경우가 많습니다. 본 논문에서는 Lean4 벤치마크인 TheoremBench를 소개합니다. 이 벤치마크는 기존의 경쟁 환경을 넘어 정리 증명기를 평가하도록 설계되었습니다. TheoremBench는 거의 백 개의 고전적인 정리를 기반으로 구축되었으며, 두 가지 보완적인 형태로 제공됩니다. 첫 번째는 각 인스턴스당 하나의 목표 정리를 포함하는 일반 버전이고, 두 번째는 각 정리를 구조화된 관련 증명 작업의 집합으로 확장한 사전 조건 버전입니다. 이 디자인을 통해 모델이 최종 정리를 처음부터 증명했는지 여부뿐만 아니라, 정리의 내부적인 증명 구조를 통한 부분적인 진행 과정을 평가할 수 있습니다. 실험 결과, 명시적인 전제 조건은 Lean4 기능을 사용하는 증명 모델의 성능을 크게 향상시키는 것으로 나타났습니다. 포괄적인 평가를 위해, 본 논문에서는 정리 수준의 보장 범위 및 토큰 효율성 지표를 도입하여 증명 행동의 질적 차이를 보여줍니다. 결과는 현재의 증명기가 여전히 쉬운 부분 정리에 치우쳐 있으며, 종종 간결한 증명 계획보다는 길고 비효율적인 전술 추적을 통해 정리를 해결한다는 것을 보여줍니다. 따라서 TheoremBench는 형식적 추론 능력에 대한 더욱 세밀한 관점을 제공하며, Lean4 정리 증명기를 평가하기 위한 구조화된 벤치마크 설계의 중요성을 강조합니다.

LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.