기술 요약: Construction–Verification: Lean 4를 이용한 응용 수학의 형식화에 관한 벤치마크

1. 문제 정의

MiniF2F 및 ProofNet과 같은 현재의 자동 정리 증명(Automated Theorem Proving) 벤치마크는 주로 선언적 명제(declarative propositions)의 논리적 검증(즉, 해의 존재성을 증명하는 것)에 집중되어 있습니다. 이러한 패러다임은 응용 수학(applied mathematics) 분야에는 불충분합니다. 응용 수학의 주요 목표는 단순한 존재성 증명이 아니라, 구체적인 값, 실행 가능한 알고리즘 또는 구조적 변환을 도출하는 것이기 때문입니다.

기존 데이터셋은 이 영역에서 두 가지 결정적인 한계를 가집니다:

1. 범위 격차(Scope Gap): 볼록 해석학(convex analysis), 최적화(optimization), 수치 대수(numerical algebra), 고차원 확률론(high-dimensional probability)을 포함한 학부 수준 이상의 응용 수학에 대한 커버리지가 부족합니다.
2. 구성적 결핍(Constructive Deficit): "구성-검증(construction-verification)" 워크플로우를 강제하지 못합니다. 응용 수학에서는 모델이 정답의 정당성을 증명하기 전에 반드시 구체적인 솔루션(예: 알고리즘 또는 특정 값)을 먼저 합성해야 합니다. 현재의 벤치마크는 모델이 비구성적 택틱(non-constructive tactics, 예: 특정 최적값을 계산하지 않고 극값 정리 등을 통해 존재성만을 증명하는 방식)을 사용하여 이 과정을 우회할 수 있게 함으로써, 모델의 계산적 추론 능력을 왜곡하여 보여줍니다.

2. 방법론

Construction–Verification 프레임워크

저자들은 Lean 4를 사용하여 구성(Construction) 후 **검증(Verification)**이라는 두 단계의 워크플로우를 구조적으로 강제하는 형식화 패러다임을 제안합니다. 이 프레임워크는 모델이 정의를 선행하지 않고 비구성적인 지름길을 이용하는 것을 방지합니다. 이 프레임워크는 세 가지 특정 유형의 응용 수학 과제를 다룹니다:

• 평가 문제(Evaluation Problems): $\exists x, Q(x)$를 증명하는 대신, 에이전트는 매개변수 $V$에 기반하여 해 $x(V)$를 계산하는 함수 def x (V) := ...를 정의한 다음, $Q(x(V), V)$를 증명하는 정리를 작성해야 합니다. 함수의 시그니처는 입력을 원시 매개변수로 엄격히 제한하여, 모델이 대상 속성을 이용해 구성을 "속이는" 것을 방지합니다.
• 알고리즘 설계 문제(Algorithm Design Problems): 에이전트는 반복 프로세스(예: 경사 하강법)를 나타내는 재귀 함수를 정의해야 합니다. 이 과제는 $n+1$번째 단계를 위한 전이 규칙(loop body)을 채워 넣은 후, 수렴성이나 단조성과 같은 속성을 증명할 것을 요구합니다.
• 표현 변환(Representation Transformation): 에이전트는 로우(raw) 문제 인스턴스를 타겟 정형 형태(canonical form)로 모델링해야 합니다(예: 그래프 컷 문제를 스펙트럴 클러스터링 정식화로 변환). 이는 새로운 도메인, 제약 조건, 목적 함수를 정의하고, 소스 문제와 타겟 문제 사이의 완화(relaxation) 또는 등가 관계를 증명하는 과정을 포함합니다.
• 정리 증명(Theorem Proving): 순수한 논리적 추론 능력을 측정하기 위해 전통적인 연역적 과제의 베이스라인 서브셋이 포함됩니다.

벤치마크 큐레이션 (AMBER)

저자들은 네 가지 핵심 도메인을 아우르는 AMBER(Applied Mathematics BEnchmark for Reasoning) 데이터셋을 소개합니다:

1. 볼록 해석학 (Convex Analysis)
2. 최적화 (Optimization)
3. 수치 대수 (Numerical Algebra)
4. 고차원 확률론 (High-Dimensional Probability)

데이터 소스 및 난이도: 문제는 고전적인 교과서(예: Boyd & Vandenberghe, Vershynin)에서 추출되었으며 난이도별로 분류되었습니다 (Easy: 표준 연습문제; Hard: 박사 과정 자격시험 수준).
형식화 및 검증: 숙련된 Lean 사용자들에 의해 각 서브필드당 50개의 문제가 형식화되었습니다. 검증은 LLM 기반의 의미론적 체크와 Mathlib 기여자들에 의한 엄격한 수동 교차 검증의 2단계 과정을 거쳤습니다.
복잡도 지표: 본 벤치마크는 높은 **의미론적 의존성 밀도(semantic dependency density)**를 특징으로 합니다. 의존성 그래프 분석($k=3$)을 사용했을 때, AMBER는 평균 164.21의 의존성 밀도를 보였으며, 이는 MiniF2F(29.72), ProofNet(33.95), FATE(53.14)보다 현저히 높습니다. 이는 복잡한 수학적 개념을 검색하고 추론하는 데 더 깊은 능력이 요구됨을 나타냅니다.

3. 주요 기여

1. 패러다임 전환: 존재적 명제를 검증하는 것에서 구성적 솔루션을 합성하는 것으로의 전환을 제안하며, 이를 통해 형식적 과제를 응용 수학의 계산적 직관과 일치시켰습니다.
2. AMBER 벤치마크: 다양한 난이도 수준을 가진 핵심 응용 도메인을 다루며, 단순한 정리 증명을 넘어 알고리즘 설계 및 표현 변환과 같은 복잡한 과제를 포함하는 포괄적인 데이터셋을 제공합니다.
3. 형식화 패턴: 비구성적 추론에 대한 엄격한 구문적 장벽을 설정하는 평가, 알고리즘 설계 및 표현 변환을 위한 특화된 Lean 4 템플릿을 제공합니다.
4. 경험적 분석: 현재의 뉴로-심볼릭 시스템이 겪는 근본적인 트레이드오프, 즉 국소적 택틱 숙련도(특화된 증명기)와 고수준 알고리즘 합성(일반 모델) 사이의 긴장 관계를 체계적으로 규명했습니다.

4. 실험 결과

모델 성능

저자들은 일반 목적의 추론 에이전트(DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro)와 특화된 정리 증명기(Goedel Prover-32B, Kimina Prover-72B)를 포함한 다양한 모델을 평가했습니다.

• 전반적인 난이도: 모든 모델의 성능이 현저히 낮습니다. "Hard" 서브셋의 경우, 거의 모든 모델의 성공률이 0에 가깝습니다.
• 일반 모델 vs 특화 모델: 순수 수학 벤치마크의 경향과는 반대로, 일반 목적의 추론 모델이 특화된 정리 증명기보다 일관되게 높은 성능을 보였습니다.
  • Pass@16 (Full AMBER): 일반 모델은 4.50%~6.00%를 달여낸 반면, 특화 증명기는 4.00%를 기록했습니다.
  • Pass@16 (Hard Subset): 일반 모델은 0%~0%를 기록했으며(Easy 서브셋에서는 일부 변동 있음), 특화 증명기 역시 매우 고전했습니다.
• 절제 연구(Ablation Study): construction-verification 프롬프트 전략은 100개 문제 서브셋에서 8%의 성공률을 기록하여, 표준 코드 완성(6%) 및 전통적인 proof-only 프롬프트(5%)보다 우수한 성능을 보였습니다. Proof-only 프롬프트는 모델이 비구성적 지름길(예: Classical.choice)을 사용하도록 유도하는 경우가 빈번했습니다.

오류 분석

DeepSeek-R1 모델의 오류 메시지 3,189개를 분석한 결과는 다음과 같습니다:

1. 환각 (Hallucination, 47.3%): 가장 흔한 실패 모드로, 존재하지 않는 정리나 정의를 호출함 (예: convexHull eq sInter).
2. 형식화 역량 부족 (Formalization Competence, 32.7%): 유효한 택틱을 잘못 적용하거나 부가 조건을 충족시키지 못함.
3. 불완전한 출력 (Incomplete Outputs, 15.2%): 완전히 실행 가능한 코드를 제공하지 못하며, 특히 복잡한 귀납적 단계에서 sorry 플레이스홀더를 남겨둠.
4. 포맷/구문 오류 (Formatting/Syntax, 4.8%): 기본적인 마크다운 또는 구문 오류.

5. 의의 및 주장

본 논문은 현재의 자동 형식화 환경이 "택틱 과적합(tactical overfitting)" 현상에 직면해 있다고 주장합니다. 증명 코퍼스에 대해 광범로 미세 조정된 특화 모델들은 일반적인 지시 이행 능력이 저하되는 경향을 보입니다. 이들은 모든 구조적 과제를 순수한 정리 증명 과제로 취급하여, 응용 수학의 다단계 요구 사항(예: 증명 전 함수 정의)을 간과하는 경우가 많습니다.

반면, 일반 목적 모델은 비형식적 의도와 형식적 구문 사이를 연결하는 데 필요한 다재다능함을 유지하며, 검증 단계에 진입하기 전 수학적 객체를 성공적으로 합성합니다. 저자들은 응용 수학의 형식을 발전시키기 위해서는 단순한 증명 탐색을 넘어, 고수준의 알고리즘 추론과 엄격한 형식 검증을 통합하는 뉴로-심볼릭 시스템으로 나아가야 한다고 결론짓습니다. AMBER 벤치마크는 단순한 논리적 타당성이 아닌 구성적 합성을 요구하는 표준을 제공함으로써, 형식화된 응용 수학의 경계를 확장하는 미래 연구의 토대가 될 것입니다.