TaoBench: 자동 정리 증명 LLM은 MathLib 범위를 넘어 일반화될 수 있는가?

TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

자동 정리 증명(ATP) 벤치마크는 주로 MathLib으로 형식화된 문제들로 구성되어 있어, 현재 ATP의 훈련 및 평가는 MathLib의 정의 체계에 크게 편향되어 있습니다. 그러나 최첨단 수학은 종종 탐색적이고 프로토타입 중심적이며, 표준 라이브러리와는 다른 맞춤형 구성에 의존합니다. 본 연구에서는 현재 ATP 시스템이 새로운 정의 체계에 적용될 때의 견고성을 평가하고, 표준 라이브러리 문제와 맞춤형 수학적 구성 간의 성능 차이를 조사합니다. 우리는 Terence Tao의 Analysis I에서 파생된 학부 수준의 벤치마크인 TaoBench를 소개합니다. TaoBench는 핵심 수학적 개념을 처음부터 구축하여 MathLib 정의에 의존하지 않도록 형식화하는 동시에, 처음부터 구축한 내용과 MathLib 구성을 혼합합니다. 공정한 평가를 위해, 우리는 각 문제에 대해 컴파일 가능한 독립적인 로컬 환경을 자동으로 추출하는 에이전트 기반 파이프라인을 구축했습니다. 정의 체계의 영향을 분리하기 위해, 우리는 모든 문제를 수학적으로 동등한 MathLib 표현으로 변환하여 TaoBench와 MathLib 표현을 쌍으로 만들어 직접 비교합니다. 최첨단 ATP 모델은 MathLib 체계 내에서 우수한 성능을 보이지만, 정의적으로 동등한 Tao 표현에서는 평균적으로 약 26%의 성능 저하가 나타났습니다. 이는 과제 난이도보다는 정의 체계 간의 제한적인 일반화가 주요 병목 현상임을 시사합니다. 따라서 TaoBench는 벤치마크 성능과 실제 적용 가능성 간의 격차를 강조하며, 연구 수학에 더 적합한 증명기를 개발하고 테스트하기 위한 구체적인 기반을 제공합니다.

Automated theorem proving (ATP) benchmarks largely consist of problems formalized in MathLib, so current ATP training and evaluation are heavily biased toward MathLib's definitional framework. However, frontier mathematics is often exploratory and prototype-heavy, relying on bespoke constructions that deviate from standard libraries. In this work, we evaluate the robustness of current ATP systems when applied to a novel definitional framework, specifically examining the performance gap between standard library problems and bespoke mathematical constructions. We introduce TaoBench, an undergraduate-level benchmark derived from Terence Tao's Analysis I, which formalizes analysis by constructing core mathematical concepts from scratch, without relying on standard Mathlib definitions, as well as by mixing from-scratch and MathLib constructions. For fair evaluation, we build an agentic pipeline that automatically extracts a compilable, self-contained local environment for each problem. To isolate the effect of definitional frameworks, we additionally translate every problem into a mathematically equivalent Mathlib formulation, yielding paired TaoBench-Mathlib statements for direct comparison. While state-of-the-art ATP models perform capably within the MathLib framework, performance drops by an average of roughly 26% on the definitionally equivalent Tao formulation. This indicates that the main bottleneck is limited generalization across definitional frameworks rather than task difficulty. TaoBench thus highlights a gap between benchmark performance and applicability, and provides a concrete foundation for developing and testing provers better aligned with research mathematics.