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

LLM(Large Language Models)은 최근 형식 증명(formal proving) 벤치마크에서 강력한 성과를 거두었습니다. 그러나 기존의 평가 방식은 대회 스타일의 문제에 과도하게 집중되어 있으며, 모델이 더 길고 의존성이 풍부한 수학적 전개 과정에서 어떻게 행동하는지는 제대로 포착하지 못하는 경우가 많습니다. 우리는 대회 환경을 넘어 정리 증명기(theorem provers)를 평가하기 위해 설계된 Lean4 벤치마크인 TheoremBench를 소개합니다. 이 벤치마크는 약 100개의 고전적 정리(classical theorems)를 바탕으로 구축되었으며, 두 가지 상호 보완적인 형태로 제공됩니다. 하나는 인스턴스당 하나의 대상 정리를 포함하는 일반적인 메인 버전(plain main version)이고, 다른 하나는 각 정리를 메인 정리와 자동으로 추출된 지원 부정리(supporting subtheorems)로 구성된 구조화된 관련 증명 작업군으로 확장한 전제 버전(premised version)입니다. 이러한 설계는 최종 정리가 처음부터 증명되었는지 여부뿐만 아니라, 정리의 내부 증명 구조를 통한 부분적인 진행 상황까지 평가할 수 있게 합니다. 우리의 실험 결과, 명시적인 전제(explicit premises)를 제공하는 것이 Lean4 능력을 갖춘 증명 모델의 성능을 실질적으로 향상시킨다는 것을 보여줍니다. 종합적인 평가를 위해, 우리는 증명 행동의 질적 차이를 드러내는 정리 수준 커버리지(theorem-level coverage) 및 토큰 효율성(token-efficiency) 지표를 도입합니다. 결과에 따르면 현재의 증명기들은 쉬운 부정리(subtheorems)에 강하게 편향되어 있으며, 간결한 증명 계획(proof plans)보다는 길고 비효율적인 택틱 트레이스(tactic traces)를 통해 정리를 해결하는 경우가 많습니다. 따라서 TheoremBench는 형식적 추론(formal reasoning) 능력에 대한 더 세밀한 관점을 제공하며, Lean4 정리 증명기를 평가하기 위한 구조적 벤치마크 설계의 중요성을 강조합니다.