# CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean

### 저자

Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen

### 💡 개요

본 논문은 계산 및 응용 수학 분야의 언어 모델 기반 자동 정리 증명 성능을 평가하기 위한 1,000개의 Lean 증명 목표로 구성된 CAM-Bench를 제안한다. 기존 벤치마크가 올림피아드 스타일 및 대수학 문제에 집중된 것과 달리, CAM-Bench는 최적화, 수치 선형대수, 수치 해석 등 응용 수학 분야를 포괄한다. 텍스트북 연습 문제를 기반으로 지역적 정의와 개념을 복원하는 파이프라인을 통해 문제의 공식화와 Lean으로의 변환을 수행했으며, 모델들의 증명 실패 패턴을 분석하여 향후 연구 방향을 제시한다.

### 🔑 시사점 및 한계

- CAM-Bench는 기존 벤치마크에서 소외되었던 계산 및 응용 수학 분야의 자동 정리 증명 연구를 촉진할 수 있다.

- 텍스트북 기반 문제 구성 및 의존성 복원 파이프라인은 실제 수학 교재의 복잡성을 반영하는 데 기여한다.

- LLM이 지역적 가정 추적, 기본 결과 적용, 증명 분해, 장기 증명 제어 등에 어려움을 겪는다는 점이 밝혀져, 이 분야의 모델 개선을 위한 구체적인 지침을 제공한다.

- 텍스트북 기반으로 구성된 문제들은 Mathlib4에 직접적으로 존재하지 않는 개념들에 의존할 수 있으며, 이는 벤치마크의 적용 범위를 제한할 수 있다.

[PDF 보기](https://arxiv.org/pdf/2605.17255)

For the site tree, see the [root Markdown](https://slashpage.com/haebom.md).