기술 요약: CAM-Bench

문제 제기

대형 언어 모델 (LLM) 을 위한 기존 형식 정리 증명 벤치마크는 주로 올림피아드 스타일의 문제와 대수학 영역 (예: MiniF2F, PutnamBench, ProofNet) 에 초점을 맞추고 있습니다. 이러한 벤치마크는 형식적 추론의 발전을 이끌었지만, 계산 및 응용 수학 영역은 여전히 현저히 부족하게 다루어지고 있습니다.

응용 수학의 문제들 (예: 최적화, 수치 선형대수, 수치 해석) 은 고립된 정리 진술과 근본적으로 다릅니다. 이러한 문제들은 종종 다음에 의존하는 맥락 의존적입니다:

• 지역적으로 도입된 정의, 표기법, 알고리즘.
• 장 (chapter) 별 관례와 기본 결과.
• 연습문제에 명시적으로 기술되지 않았지만 충실한 형식화를 위해 필요한 유래된 가정.

현재 벤치마크는 모델이 이러한 지역적 가정을 추적하고, 교과서 맥락에 기반하여 증명을 분해하며, Mathlib4 와 같은 형식 라이브러리에 표준 보조정리 (lemma) 로 아직 존재하지 않는 기본 결과를 적용할 수 있는지 평가하는 데 어려움을 겪고 있습니다. "지역적 맥락"이 정리 진술 자체만큼이나 중요한 응용 수학 문제를 대상으로 하는 벤치마크가 필요합니다.

방법론

저자들은 최적화, 수치 선형대수, 수치 해석 분야의 778 개 교과서 연습문제에서 파생된 1,000 개의 증명 목표를 포함하는 Lean 4 정리 증명 벤치마크인 CAM-Bench를 소개합니다. 이 벤치마크의 구축은 맥락 의존적 연습문제를 자체 완결적이고 기계 검증 가능한 목표로 변환하도록 설계된 새로운 의존성 복구 및 형식화 파이프라인에 의존합니다.

1. 의존성 복구 및 충실화 파이프라인

교과서 연습문제의 자체 완결성 부재를 해결하기 위해, 저자들은 재귀적 의존성 확장 절차 (알고리즘 1) 를 개발했습니다:

• 재귀적 확장: 원시 연습문제에서 시작하여 시스템은 참조 (정리, 방정식, 알고리즘) 를 추출하고 정의된 깊이까지 해당 정의와 의존성을 재귀적으로 검색합니다.
• 하향식 자연화: 의존성 트리는 하향식으로 처리됩니다. LLM 자연화기는 충실된 표현을 병합하여 지역적 참조를 해결하고, 표기법을 표준화하며, 하위 정의가 상위 의존성에 사용되기 전에 통합되도록 전환을 매끄럽게 합니다.
• 암시적 조건 복구: 시스템은 원래 문제나 복구된 맥락에서 지원될 때만 필요한 가정 (예: 정의역 제한, 양수성, 볼록성) 을 명시화합니다. 이러한 충실화는 소스 기반입니다. 이는 누락된 의존성을 추측하지 않고, 복구할 수 없는 경우 이를 배제합니다.
• 다중 라운드 검토: 충실된 진술은 누락된 가정, 작업 편향 (task drift), Lean 적합성을 확인하기 위해 검증 루프를 거칩니다. 수리는 수학적 목표를 변경하거나 지원되지 않는 의존성을 발명하지 않고 지역적 결함만 수정하도록 제한됩니다.

2. 모듈화 주도 Lean 형식화

비형식적 목표가 확립되면, 시스템은 고정된 맥락, 블록 단위 구축 전략을 사용하여 이를 Lean 4 코드로 변환합니다:

• 의미적 블록 분해: 이질적인 연습문제는 유형화된 의미적 블록 (정의, 최적화 문제, 알고리즘, 정리 목표) 으로 분해됩니다. 이는 최종 정리 목표와 지원 맥락을 분리합니다.
• 점진적 번역: 시스템은 블록을 순차적으로 번역합니다. 이전에 승인된 선언은 고정된 읽기 전용 맥락으로 유지됩니다. 이는 연쇄 오류를 방지하고 실패를 현재 블록으로 국한시킵니다.
• 컴파일러 기반 및 의미적 수리:
  • 컴파일 수리: 블록이 컴파일되지 않으면, 수정기가 컴파일러 진단을 사용하여 지역적 패치 (구문, 유형 주석, 네임스페이스 해결) 를 생성합니다.
  • 의미 검토: 검토기는 컴파일 가능한 후보를 비형식적 블록과 비교하여 의미적 충실도 (변수, 가정, 결론의 보존) 를 확인합니다. 불일치는 의미적 재작성을 유발합니다.
• 이력 인식 제어: 시스템은 이전 실패 시도와 거부 이유를 기록하여 진동을 방지하고 후속 수리를 이전에 실패한 방향에서 벗어나도록 안내합니다.

3. 벤치마크 구축 및 검증

최종 데이터셋에는 원시 연습문제, 복구된 맥락, 정규화된 비형식적 정리, 그리고 최종 Lean 목표가 포함됩니다. 검증은 두 수준에서 수행됩니다:

• 소스 수준: 비형식적 목표가 교과서 연습문제에 충실하고 자체 완결적인지 확인합니다.
• Lean 수준: 형식 선언이 검토된 비형식적 목표를 보존하는지 확인합니다. 의미 검증 후 후보 선언의 92.5% 만 사용 가능하다고 판단되어, 충실한 자동 형식화의 어려움을 강조합니다.

주요 기여

1. CAM-Bench 데이터셋: 최적화, 수치 선형대수, 수치 해석을 아우르는 1,000 개의 Lean 증명 목표로 구성된 큐레이션 벤치마크입니다. 이는 원시 연습문제부터 기계 검증된 Lean 목표까지 추적 가능한 인공물을 제공하여 응용 수학 평가의 공백을 메웁니다.
2. 의존성 복구 파이프라인: 맥락 의존적 연습문제에서 충실한 Lean 목표를 구축하기 위한 새로운 방법입니다. 이는 재귀적 의존성 확장, 소스 기반 충실화, 그리고 표준 Mathlib4 보조정리가 아닌 지역적 정의와 가정을 처리하기 위한 제한된 수리를 결합합니다.
3. 종합 평가 및 오류 분석: 이 논문은 CAM-Bench 에서 최첨단 LLM 과 형식화 에이전트를 평가합니다. 이는 특정 실패 모드를 식별합니다:
   • 라이브러리/API 기반: 모델은 사용 가능한 Mathlib 인프라에 증명을 기반을 두지 못하고, API 를 환각하거나 연결 결과 (bridge results) 를 누락합니다.
   • 형식 표현: 유형 규칙 오류, 차원/인덱스 불일치, 그리고 강제 (coercion) 실패.
   • 증명 분해: 장기적 증명을 보조 보조정리로 분해하거나 복잡한 최적화/수치 논증을 제어하는 능력 부재.

결과

베이스라인 성능

• 비에이전트 모델: 가장 강력한 비에이전트 베이스라인 (예: Deepseek-v4-pro, Claude-sonnet-4-6) 조차도 낮은 검증된 Lean 정확도를 보였으며, 최상위 모델은 19.67% (Pass@32) 에 도달했습니다.
• 비형식적 vs 형식적 격차: 비형식적 정확도 (Pass@1 비형식적 정확도 약 70–84%) 와 검증된 Lean 정확도 (<20%) 사이에는 상당한 불일치가 있습니다. 모델은 고차원 논리를 포착하지만 엄격한 Lean 구문, 유형 규칙, 그리고 라이브러리 제약을 충족하지 못합니다.
• 에이전트 개선: 반복적 수리와 도구 사용을 수행하는 에이전트 증명 검색 시스템 (예: GPT-5.4) 은 성능을 크게 향상시켜 44.00% 의 검증 정확도에 도달했습니다. 그러나 이는 높은 토큰 비용 (~1.96M 토큰 vs 베이스라인의 ~0.26–0.70M 토큰) 을 수반했습니다.

외부 에이전트 평가

두 개의 외부 에이전트 시스템인 M2F와 Aristotle이 8 시간 시간 예산으로 200 개의 샘플링된 인스턴스에 대해 평가되었습니다:

• M2F: 200 개 인스턴스 중 143 개 (71.5%) 를 해결했습니다.
• Aristotle: 200 개 인스턴스 중 125 개 (62.5%) 를 해결했습니다.
• 이러한 개선에도 불구하고, 벤치마크는 포화 상태가 아닙니다. 많은 실패는 누락된 수학 인프라, 긴 보조 보조정리 체인, 그리고 최적화 특유의 추론으로 귀결되었습니다.

중요성과 주장

이 논문은 CAM-Bench 가 교과서 개념과 기본 정리에 의존하는 응용 수학 문제를 대상으로 함으로써 기존 형식 벤치마크에 중요한 보완재 역할을 한다고 주장합니다. 그 중요성은 다음과 같습니다:

1. 맥락 의존적 추론 평가: 이는 모델이 지역적 가정을 추적하고 맥락을 재구성하는 능력을 테스트합니다. 이는 실제 세계 형식화에 필수적이지만 고립된 정리 벤치마크에서는 종종 우회되는 능력입니다.
2. 시스템적 병목 현상 진단: 결과는 현재 LLM 기반 증명기가 구문뿐만 아니라 Mathlib 기반, 유형 규칙, 그리고 장기적 증명 분해에서도 어려움을 겪고 있음을 강조합니다.
3. 인프라 개발 촉진: 이 벤치마크는 형식 응용 수학의 진전이 더 강력한 Mathlib 인프라 (예: 행렬, 스펙트럼, 볼록성용) 와 장기적 증명 궤적을 관리할 수 있는 더 유능한 에이전트가 필요함을 시사합니다.

저자들은 겸손한 입장을 견지하며, 에이전트 시스템이 성능을 향상시키지만 벤치마크는 여전히 도전적이며, 결과는 해결된 문제가 아닌 현재 능력의 추정치로 간주되어야 한다고 명시합니다. 이 벤치마크는 수학 추론 시스템을 위한 더 넓은 평가 스위트의 구성 요소로 의도되었습니다.