🤖 machine learning

OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving

이 논문은 올림피아드 수학 기반의 증명 모델을 전문가 반복(expert iteration) 데이터 큐레이션과 특화된 선호 학습(preference learning) 기법을 통해 학부 수준의 최적화(optimization) 영역으로 효과적으로 전이시킨 'OptProver'를 제안합니다.

원저자: Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

게시일 2026-04-28

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Chenyi Li, Yanchen Nie, Zhengyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

1. 배경: "수학 올림피아드 금메달리스트가 공대생이 된다면?"

지금까지의 AI 수학 모델들은 주로 '수학 올림피아드' 스타일의 문제를 잘 풀도록 훈련되었습니다. 마치 논리 퍼즐이나 창의적인 사고력을 요구하는 퀴즈를 잘 푸는 '천재 소년'과 같죠.

그런데 문제는 이 천재 소년에게 갑자기 '공학 수학(최적화)' 책을 던져주면, 갑자기 버벅거리기 시작한다는 겁니다. 왜 그럴까요?

올림피아드 수학: "이 퍼즐의 규칙을 찾아내서 논리적으로 풀어봐!" (창의적 추론)
최적화 수학: "이 복잡한 함수에서 가장 낮은 지점을 찾기 위해, 기존의 정해진 공식과 도구(라이브러리)를 아주 정교하게 사용해!" (전문 도구 활용)

기존 AI는 올림피아드식 '창의적 사고'에는 익숙하지만, 공학에서 쓰는 '특수한 도구와 복잡한 공식'을 사용하는 법을 배우려 하면, 오히려 예전에 배웠던 논리력까지 까먹어버리는 '지식의 충돌(Catastrophic Forgetting)' 현상을 겪습니다.

2. 문제점: "맞는 말인데, 쓸모없는 말만 하는 AI"

연구진은 AI를 공학 수학으로 훈련시킬 때 두 가지 큰 벽을 발견했습니다.

지식의 망각: 새로운 공식(최적화)을 배우느라 예전에 잘하던 논리 문제들을 다 까먹음.
길을 잃은 탐험가 (Stagnant Tactics): AI가 수학 문제를 풀 때 한 단계씩 나아가는데, 문법적으로는 맞는 말(예: "이 식을 이렇게 변형하자")을 하지만, 정작 문제 해결에는 전혀 도움이 안 되는 **'헛스윙'**을 계속하는 겁니다. 마치 미로에서 벽을 짚으며 "이 벽은 딱딱하네?"라고 말만 하고 앞으로 나아가지 못하는 것과 같습니다.

3. 해결책: "OptProver의 3단계 특훈"

연구진은 이 문제를 해결하기 위해 **'OptProver'**라는 새로운 훈련법을 만들었습니다.

① 1단계: 스스로 깨우치기 (Self-Distillation)

AI에게 단순히 교과서를 읽히는 게 아니라, 스스로 수학 문제들을 풀어보게 합니다. 직접 풀어보고 "아, 이렇게 하니까 답이 나오네!"라고 성공한 경로만 골라서 다시 공부하게 만드는 '자기 주도 학습' 방식입니다.

② 2단계: "쓸모없는 말은 하지 마!" (Utility-Aware Preference)

이게 이 논문의 핵심입니다. AI가 문제를 풀 때, 문법적으로는 맞지만 문제 해결에 도움이 안 되는 '헛스윙'을 하면 "그건 틀린 거야!"라고 엄격하게 혼을 냅니다.

성공한 경로: "오, 아주 효율적으로 잘 풀었어! (칭찬)"
문법은 맞지만 제자리걸음인 경로: "말은 되는데, 시간 낭비야. 하지 마! (벌점)"
이렇게 함으로써 AI가 미로 속에서 헤매지 않고 가장 빠른 길로만 가도록 훈련시킵니다.

③ 3단계: "너무 어려운 건 일단 넘어가자" (Perplexity-Weighted)

AI가 공부하다가 너무 생소하고 어려운 단어가 나오면 당황해서 학습이 꼬일 수 있습니다. 그래서 너무 난해한 데이터는 가중치를 낮춰서, AI가 감당할 수 있는 수준부터 차근차근, 안정적으로 배우게 조절해 줍니다.

4. 결과: "올림피아드 실력은 유지하면서, 공학 수학까지 마스터!"

결과는 놀라웠습니다.

전문성 확보: 새로운 벤치마크(OptBench)에서 기존 모델들을 압도하며 최적화 문제를 아주 잘 풀게 되었습니다.
기초 실력 유지: 가장 중요한 점은, 공학 수학을 배웠다고 해서 예전에 잘하던 올림피아드 문제나 일반 수학 문제 실력이 떨어지지 않았다는 것입니다. 오히려 일반적인 수학 실력이 더 좋아지기도 했습니다.

요약하자면...

이 논문은 **"AI에게 새로운 전문 지식을 가르칠 때, 예전 실력을 잃지 않으면서도 '쓸데없는 헛스윙'을 하지 않고 핵심을 찌르는 법을 가르치는 똑똑한 훈련법"**을 제안한 것입니다. 덕분에 AI는 이제 단순한 수학 천재를 넘어, 실무적인 공학 수학까지 다룰 수 있는 '준전문가'로 성장할 수 있게 되었습니다.

[기술 요약] OptProver: 지속적 학습을 통한 올림피아드 수학과 최적화 이론의 가교 역할

1. 문제 정의 (Problem Statement)

최근 대규모 언어 모델(LLM) 기반의 형식 정리 증명(Formal Theorem Proving) 기술은 올림피아드 수준의 수학 문제(MiniF2F 등)에서는 뛰어난 성과를 보이고 있습니다. 그러나 다음과 같은 최적화(Optimization) 분야에서는 심각한 한계를 보입니다.

도메인 격차 (Domain Gap): 기존 모델들은 올림피아드 스타일의 문제에 특화되어 있어, 최적화 이론의 핵심인 볼록성(Convexity), 최적 조건(Optimality conditions), 알고리즘 수렴성 분석 등에 필요한 특수 형식(Formalisms)을 다루지 못합니다.
상호작용적 분포 변화 (Interactive Distribution Shift): 새로운 도메인(최적화)의 데이터를 단순히 미세 조정(Fine-tuning)할 경우, 모델이 기존에 학습한 일반적인 추론 능력을 상실하는 파괴적 망각(Catastrophic Forgetting) 현상이 발생합니다.
유효성 vs 유용성의 괴리 (Validity vs. Utility): 최적화 도메인의 새로운 택틱(Tactic, 증명 단계)들은 문법적으로는 옳더라도(Syntactically valid), 실제 증명을 진전시키지 못하고 탐색 공간만 넓히는 '정체된 단계(Stagnant steps)'를 생성하여 탐색 효율을 급격히 떨어뜨립니다.

2. 핵심 방법론 (Methodology)

본 논문은 올림피아드 수준의 증명 능력을 유지하면서 최적화 도메인으로 성공적으로 전이하기 위한 OptProver 파이프라인을 제안합니다.

① 대규모 자기 증류 (Large-Scale Self-Distillation via Expert Iteration)

단순히 교과서 데이터를 학습하는 대신, 전문가 반복(Expert Iteration, EI) 방식을 사용합니다.

Mathlib(수학 라이브러리)의 정리들을 시드로 사용하여 모델이 스스로 증명을 탐색하게 합니다.
검증된 성공적인 증명 경로(Verified trajectories)만을 추출하여 학습 데이터로 사용하여, 모델이 스스로의 성공적인 추론 스타일을 학습하도록 유도합니다.

② 유용성 인식 선호도 최적화 (Utility-Aware Preference Optimization, UAPO)

증명 과정에서 '문법적으로는 맞지만 증명에 도움이 되지 않는' 택틱을 제거하기 위해 도입되었습니다.

유용성 척도(Utility Scale) 정의: 증명 성공에 기여하는 단계( $u=2$ ), 문법 오류( $u=0$ ), 그리고 문법은 맞지만 증명을 정체시키는 단계( $u=1$ )로 구분합니다.
선호도 구성: 성공적인 경로의 택틱을 '선호되는 것( $a_w$ )'으로, 정체되거나 실패한 경로의 택틱을 '거부되는 것( $a_l$ )'으로 설정하여, 모델이 효율적인 증명 경로를 선택하도록 학습시킵니다.

③ 퍼플렉서티 가중치 DPO (Perplexity-Weighted DPO, PW-DPO)

학습의 안정성을 높이기 위한 기술입니다.

참조 모델(Reference model)에서 확률이 너무 낮은(Perplexity가 높은) 토큰은 학습 시 그래디언트(Gradient)의 변동성을 키워 불안정성을 초래합니다.
가중치 메커니즘: 토큰 수준의 퍼플렉서티를 계산하여, 확률이 낮은 토큰의 영향력을 줄이는 가중치( $w_t$ )를 적용함으로써 학습 안정성을 확보하고 파괴적 망각을 방지합니다.

3. 주요 기여 (Key Contributions)

OptBench 구축: 최적화 이론(기초, 볼록성, 알고리즘 분석)을 평가할 수 있는 400개의 Lean 4 기반 새로운 벤치마크를 제안했습니다.
새로운 학습 프레임워크: 단순 미세 조정을 넘어, 유용성(Utility)과 확률적 안정성(Perplexity)을 모두 고려한 선호도 학습(Preference Learning) 방법론을 제시했습니다.
효율적인 도메인 전이: 기존 올림피아드 모델의 능력을 보존하면서도 전문적인 최적화 증명을 수행할 수 있는 모델을 구현했습니다.

4. 실험 결과 (Results)

OptBench 성능: OptProver는 OptBench에서 **Pass@1 37.75%, Pass@32 55.25%**를 달성하며, 유사 규모의 모델 중 SOTA(State-of-the-art) 성능을 기록했습니다. (특히 알고리즘 및 기초 문제에서 강점)
범용성 유지: 최적화 학습 후에도 일반 수학 벤치마크인 MiniF2F와 ProofNet에서 성능 저하가 없거나 오히려 향상됨을 보여주어, 파괴적 망각 문제를 성공적으로 해결했음을 입증했습니다.
비교 우위: 기존의 Whole-proof generation(전체 증명 생성) 방식보다 Step-level proving(단계별 증명) 방식이 최적화 도메인의 복잡한 정의(Definition)를 다루는 데 훨씬 효과적임을 확인했습니다.

5. 의의 (Significance)

본 연구는 형식적 정리 증명 분야에서 **"특정 도메인으로의 지식 전이(Domain Transfer)"**가 단순히 데이터를 더 넣는 문제가 아니라, **"증명 탐색의 효율성(Search Efficiency)"**과 "기존 지식의 보존(Knowledge Preservation)" 사이의 정교한 균형을 맞추는 문제임을 규명했습니다. 이는 향후 AI가 수학적 전문 지식을 습득하고 자동화된 증명을 수행하는 데 있어 매우 중요한 방법론적 가이드를 제공합니다.