한 줄 요약
StochBench는 Lean 4 기반의 확률과정 분야 대학원 수준 정리 450개를 포함한 도메인별 정리 증명 벤치마크로, Opus 4.8 기반 에이전트가 15분 제한 내 34.9% 증명 성공.
핵심 기여도
- 450개의 대학원 수준 확률과정 문제를 포함한 Lean 4 기반의 StochBench 벤치마크 제시.
- 각 문제는 자연어 원문과 함께 제공되며, Markov chain, martingale, Brownian motion 등 10개 주제를 다룸.
- Opus 4.8 기반 에이전트가 15분 제한 내 157개(34.9%)의 정리 증명 성공.
- Mathlib 환경에서 정의되지 않은 인프라가 필요한 문제도 포함, 추상화 수준 차이를 반영.
핵심 아이디어
기존 정리 증명 벤치마크는 수학 경시 문제 위주로 구성되어 특정 분야의 실용적 수학을 대표하지 못한다. StochBench는 확률과정이라는 학문 분야를 집중적으로 다루며, 이론적 깊이와 실제 수학적 표현 간의 일관성을 유지한다. 문제는 직접 정의를 사용하는 *direct* 타겟과 가설을 전제로 하는 *abstracted* 타겟으로 구분되며, 이는 Lean의 형식적 검증 시스템과 호환된다. 이는 기존 벤치마크가 포괄성보다는 도메인 내 일관성을 우선시한다는 점에서 차별화된다.
기술적 접근법
- **Lean 4** 환경에서 작성된 450개의 정리 목표.
- **Mathlib** 라이브러리와 공유 정의를 기반으로 문제를 구성.
- **lean4skills**, **Lean LSP MCP server**, **loogle**, **leansearch**를 활용한 에이전트 평가.
- **Opus 4.8** 기반 에이전트가 15분 제한 내 정리 증명 시도.
- 증명은 `Lean` 컴파일러가 검증하며, `sorry`, `sorryAx`, 추가 가정 없이 완전히 수용된 경우만 성공으로 간주.
주요 결과
- Opus 4.8 기반 에이전트는 450개 문제 중 157개(34.9%)를 정확히 증명.
- 주제별 성능 차이가 존재하며, 일부 문제는 라이브러리 지원 부족이나 정의 누락으로 인해 실패.
- **Martingale**, **Markov chain**, **Brownian motion** 등 주요 주제에서 일관된 성능 차이 관찰.
- 일부 문제는 측정 가능성, 적분 가능성, 비공집합 가정 누락 등 형식화 결함으로 인해 실패.
의의 및 한계
StochBench는 확률과정이라는 학문 분야의 형식적 증명 능력을 평가하는 데 기여하며, 기존 벤치마크가 부족했던 도메인 특화 평가를 가능하게 한다. 특히, **Lean**의 형식적 검증 시스템과 자연어 문제 간의 일관성을 유지한 점에서 학술적 가치가 있다. 그러나 일부 문제는 Mathlib 라이브러리에서 필요한 정의가 누락되거나, 인프라가 부족해 형식화가 어려운 한계가 있다. 또한, 단일 에이전트와 단일 예산 기반의 평가이므로, 다른 모델 간 비교는 제한적이다.
실용적 활용
StochBench는 확률과정을 다루는 통계학, 머신러닝, 금융공학 등 분야에서 형식적 증명 도구의 성능을 평가하는 데 활용 가능하다. 또한, **Lean** 기반 수학 도우미 시스템의 개선과 학습 데이터셋으로도 사용될 수 있다.