LemmaBench: 수학 분야 연구 수준의 LLM 성능을 평가하기 위한 실시간, 연구 수준 벤치마크

LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics

본 논문에서는 대규모 언어 모델(LLM)의 수학 분야 연구 수준의 능력을 평가하기 위한 새로운 벤치마크 접근 방식을 제시합니다. 기존 벤치마크는 주로 수학 연구를 대리하는 것으로, 대회 문제 또는 교과서 스타일의 문제 집합에 의존합니다. 이에 반해, 저희는 최신 수학 연구 결과를 직접 평가하는 업데이트 가능한 벤치마크를 구축했습니다. 이는 arXiv에서 보조정리를 자동으로 추출하고, 모든 가정과 필요한 정의를 명시하여 자체적으로 완결된 형태로 재작성하는 자동화 파이프라인으로 구성됩니다. 이 파이프라인을 통해 이전 벤치마크는 학습에 사용될 수 있지만, 미래의 평가에는 영향을 미치지 않으면서, 실제 인간 수학 연구에서 가져온 새로운 문제들로 벤치마크를 정기적으로 업데이트할 수 있습니다. 현재 최고 성능의 LLM을 벤치마크한 결과, 모델에 따라 증명 정확도가 10-15% 정도이며, 이는 LLM이 연구 맥락에서 인간 수준의 증명 능력을 갖추려면 아직 발전할 여지가 크다는 것을 보여줍니다.

We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15$\%$ accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.