LLM이 형식적 증명 벤치마크에서 강력한 성과를 거두고 있지만, 기존 평가는 경쟁 형식 문제에 집중되어 있어 복잡한 수학적 개발에 대한 모델의 행동을 제대로 반영하지 못합니다.
TheoremBench는 Lean4 벤치마크로, 경쟁 환경을 넘어 형식적 정리 능력을 평가하기 위해 설계되었으며, 100개의 고전적인 정리를 기반으로 합니다.
본 벤치마크는 목표 정리만 포함하는 주 버전과, 자동으로 추출된 관련 하위 정리를 포함하는 프리미스 버전의 두 가지 형태로 제공되어, 전체 증명뿐 아니라 증명 구조 내 부분적 진행 상황도 평가할 수 있습니다.
실험 결과, 명시적 프리미스는 Lean4-capable prover 모델의 성능을 크게 향상시켰으며, 벤치마크 설계의 중요성을 강조합니다.