🙋‍
저는 Luhui Dev로, Agent 엔지니어링을 분석하고 AI가 교육에 어떻게 적용될 수 있는지 탐구해 온 개발자입니다.
저는 Agent Harness, LLM 애플리케이션 엔지니어링, AI for Math, 그리고 교육 SaaS의 제품화에 집중하고 있습니다.

서론 (Introduction)

2026년 5월, DeepMind는 Advancing Mathematics Research with AI-Driven Formal Proof Search라는 arXiv 논문을 발표하며, 수학 연구를 위한 형식 증명 시스템(formal proof system)인 AlphaProof Nexus를 소개했습니다.

결과만 본다면, 이 논문은 AI가 수학 문제를 증명한다는 또 다른 이야기처럼 들릴 수도 있습니다. 이 시스템은 353개의 정식화된 Erdos 미해결 문제 중 9개를 해결했고, 492개의 OEIS 추측 중 44개를 증명했으며, 그래프 이론(graph theory), 최적화 이론(optimization theory), 대수 기하학(algebraic geometry), 가법 조합론(additive combinatorics), 양자 광학(quantum optics) 등 실제 연구 분야에서도 사용되었습니다.

하지만 AI + 교육 분야에서 작업하는 사람으로서, 제가 더 관심을 갖는 것은 그 이면에 있는 연구 경로입니다:

대규모 모델(large models)이 증명 아이디어를 제안하게 하고, Lean과 같은 형식 시스템(formal systems)이 이를 검증하게 하며, 특화된 증명 탐색기(proof searchers)가 국소적 목표(local goals)를 해결하게 하고, 멀티 에이전트 오케스트레이션(multi-agent orchestration)을 사용하여 실패, 부분적인 초안, 그리고 하위 목표(subgoals)를 재사용 가능한 탐색 자산으로 전환하는 것입니다.

이 에세이는 AlphaProof Nexus를 쉬운 언어로 분석합니다. 왜 이것이 존재하는지, 시스템이 어떻게 설계되었는지, 그리고 논문에 반영된 **네 가지 AI 수학 연구 패러다임(four AI math research paradigms)**에 대해 다룹니다.

1. AI for Math에 형식 증명(Formal Proof)이 필요한 이유

대부분의 사람들은 자연어(natural language)로 된 수학적 증명을 이해합니다:

A가 참이므로, B가 뒤따른다. 어떤 정리에 의해, C가 뒤따른다. 따라서 결론이 성립한다.

이 방식은 인간 수학자들에게는 통합니다. 왜냐하면 인간은 생략된 추론을 채워 넣을 수 있기 때문입니다. 하지만 AI에게는 심각한 문제가 있습니다: 대규모 모델은 증명처럼 보이는 텍스트를 쓰는 데는 능숙하지만, 그것이 실제로 무언가를 증명했다는 것을 의미하지는 않습니다.

그들은 다음과 같은 행동을 할 수 있습니다:

• 존재하지 않는 정리를 인용하거나;
• 핵심 단계를 건너뛰거나;
• 어려운 문제를 더 쉬워 보이지만 여전히 증명되지 않은 다른 문제로 대체하거나;
• 논리가 깨진 채로 자신감 있게 유도 과정을 작성할 수 있습니다.

따라서 DeepMind 논문의 핵심 출발점은 AI가 엄격한 시스템(strict system) 내부에서 작동하도록 만드는 것입니다.

그 시스템은 바로 Lean입니다.

Lean은 수학적 컴파일러(mathematical compiler)로 이해할 수 있습니다. 프로그래머가 코드를 작성할 때 컴파일러가 구문(syntax)과 타입 오류(type errors)를 확인하듯, 수학자가 Lean 증명을 작성하면 Lean은 모든 논리적 단계가 실제로 성립하는지 확인합니다.

만약 Lean이 증명을 수락한다면, 그 증명은 단순히 그럴듯한 수준이 아닙니다. 엄격한 기계 검증(machine checking)을 통과한 것입니다.

이것이 AlphaProof Nexus의 기본 개념입니다:

AI는 추측하고, 시도하고, 실패할 수 있지만, 최종 답변은 반드시 Lean 검증을 통과해야 합니다.

2. AlphaProof Nexus란 무엇인가?

AlphaProof Nexus는 단일 거대 모델(large model)도 아니고, 채팅 전용 수학 어시스턴트도 아닙니다. 이는 **AI 수학 연구 파이프라인 (AI mathematical research pipeline)**에 더 가깝습니다.

입력값은 미완성된 정리 증명이 포함된 Lean 파일입니다. 시스템은 Lean이 이를 수락할 때까지 증명을 반복적으로 수정, 완성 및 분해합니다.

다음과 같이 상상해 볼 수 있습니다:

[

AlphaProof Nexus proof search flowchart]

여기에는 몇 가지 중요한 역할이 있습니다:

• LLM: 증명 아이디어를 제안하고, Lean 코드를 작성하며, 오류를 수정합니다.
• Lean: 증명이 실제로 올바른지 확인합니다.
• AlphaProof: 특정 국소적 증명 목표(local proof goals)를 해결합니다.
• Rater Agent: 증명 초안들을 비교하고 어떤 것이 더 유망한지 판단합니다.
• Population DB: 미완성이지만 가치 있는 많은 증명 초안들을 저장합니다.
• SafeVerify: 원래의 정리를 수정하거나 허용되지 않은 공리(axioms)를 도입하는 등의 부정행위를 최종적으로 검사합니다.

3. 논문에 제시된 4가지 AI 수학 연구 패러다임

DeepMind는 네 가지 에이전트 구성을 비교합니다. 이는 AI 주도 수학 연구를 위한 네 가지 패러다임으로도 해석될 수 있습니다.

패러다임 1: 기본 에이전트 (Basic Agent)

첫 번째는 가장 기본적인 패턴인 **LLM + Lean 피드백 루프 (feedback loop)**입니다.

이는 코드를 작성하는 프로그래머와 매우 유사하게 작동합니다:

1. LLM이 미완성된 Lean 증명을 읽습니다.
2. 증명 코드를 채워 넣으려고 시도합니다.
3. Lean이 파일을 컴파일합니다.
4. Lean이 오류를 보고하면, 해당 오류들이 LLM으로 다시 전송됩니다.
5. LLM은 오류를 바탕으로 증명을 수정합니다.
6. 증명이 통과하거나 예산(budget)이 소진될 때까지 이 과정이 반복됩니다.

여기서 핵심 능력은 반복적인 시도와 수정(iterative trial and correction)입니다.

문제를 푸는 학생을 상상해 보십시오. 학생이 풀이를 작성하면, 선생님이 틀린 부분을 지적하고, 학생은 이를 수정합니다. 여기서 선생님은 사람이 아니라 Lean 컴파일러입니다. Lean은 아이디어가 우아한지(elegant)는 말해주지 않지만, 타입(type)이 틀렸는지, 목표(goal)가 해결되지 않았는지, 정리(theorem)가 일치하지 않는지, 또는 논리적 단계(logical step)가 누락되었는지는 엄격하게 알려줍니다.

이는 거대 모델(large model)에 매우 고품질의 피드백을 제공합니다.

논문에서 발견한 흥미로운 결론 중 하나는 기본 에이전트(Basic Agent)가 이미 강력하다는 점입니다.

사후 실험(post hoc experiments)에서 기본 에이전트는 9개의 성공적인 Erdos 사례를 재현할 수 있었으나, 더 어려운 문제일수록 더 많은 비용이 필요했고 효율성도 떨어졌습니다.

이는 기본 모델의 능력이 향상됨에 따라, 단순한 "생성 - 컴파일 - 수정" 루프가 이미 형식 수학(formal mathematics) 분야에서 매우 경쟁력 있는 베이스라인(baseline)이 되었음을 시사합니다.

교훈은 명확합니다. 거대 모델이 단 한 번에 완벽한 증명을 만들어낼 것이라고 기대하지 마십시오. 지속적으로 피드백을 주고 수정을 강제할 수 있는 환경 안에 모델을 두십시오.

패러다임 2: 기본 에이전트 + AlphaProof (Basic Agent + AlphaProof)

두 번째 패러다임은 기본 에이전트 위에 AlphaProof를 추가한 것입니다.

AlphaProof는 DeepMind가 이전에 개발한 형식 증명 탐색 시스템(formal proof search system)입니다. Nexus에서 AlphaProof는 주인공이 아닙니다. 그보다는 국소적인 증명 전문가(local proof specialist)에 가깝습니다.

LLM이 Lean 증명을 작성할 때, 다음과 같은 작은 목표(small goals)들에 자주 부딪히곤 합니다:

현재 문맥에서, 이 하위 주장(subclaim)을 증명하라.

어떤 하위 목표(subgoals)들은 기계적이지만 LLM이 작성하기에는 까다롭습니다. 또 다른 목표들은 일련의 전술(tactics), 즉 Lean 증명 명령어를 탐색하는 과정이 필요합니다. 이 시점에서 시스템은 로컬 목표(local goals)를 AlphaProof에 넘길 수 있습니다.

AlphaProof는 세 가지 종류의 결과를 반환할 수 있습니다:

• 증명을 찾아냄;
• 하위 목표가 실제로 거짓임을 증명함;
• 예산(budget) 내에서 증명을 찾는 데 실패함.

이는 LLM이 더 이상 모든 증명 세부 사항을 혼자서 감당할 필요가 없다는 점에서 중요합니다.

LLM은 전체적인 아이디어와 증명 구조를 책임지는 대학원생으로, AlphaProof는 로컬 기술적 세부 사항을 책임지는 전술적 탐색기(tactical searcher)로, 그리고 Lean은 최종 판결자로 생각할 수 있습니다.

논문은 또한 독립적인 AlphaProof만으로는 이러한 연구 수준의 미해결 문제들을 스스로 해결할 수 없다고 명시하고 있습니다.

실험에서 AlphaProof 단독으로는 9개의 Erdos 문제들을 해결하지 못했습니다. AlphaProof의 효과적인 위치는 더 큰 Nexus 시스템 내부이며, 그곳에서 로컬 증명 도구로서 작동합니다.

패러다임 3: 기본 에이전트 + 진화 (Basic Agent + Evolution)

세 번째 패러다임은 핵심 아이디어인 **진화적 탐색 (evolutionary search)**을 도입합니다.

수학적 증명은 종종 선형적이지 않습니다.

하나의 증명 경로는 중간에 막힐 수 있습니다. 다른 경로는 미완성이지만 핵심 아이디어에 더 가까울 수 있습니다. 세 번째 경로는 메인 정리가 완료되지 않았더라도 유용한 보조정리(lemmas)를 증명했을 수도 있습니다.

모든 에이전트 실행이 제로(zero) 상태에서 시작된다면, 많은 탐색이 낭비될 것입니다. 따라서 AlphaProof Nexus는 미완성된 증명 초안들을 증명 스케치(proof sketches)의 시드 개체군인 **개체군 DB (Population DB)**에 저장합니다.

그 후 시스템은 평가 에이전트(Rater Agent)를 사용하여 해당 초안들을 비교하고 어떤 것이 더 유망한지 결정합니다.

이는 진화와 다소 유사합니다:

• 각 증명 초안은 하나의 개체(individual)입니다;
• 에이전트들이 초안을 변이(mutate)시키고 다시 작성합니다;
• 평가자(rater)가 더 유망한 초안을 선택합니다;
• 시스템은 잠재력이 더 높은 경로에 연산 자원(compute)을 투입합니다.

어려운 점은 수학적 증명에서 성공 신호(success signals)가 매우 희소하다는 것입니다. 프로그램 최적화(program optimization)에서는 최적이 아닌 프로그램이라도 점수를 받을 수 있습니다. 하지만 형식적 증명(formal proof)에서는 증명이 완전히 성공하거나, 그렇지 않거나 둘 중 하나입니다.

중간 상태(Intermediate states)를 정량화하기는 어렵습니다.

DeepMind의 접근 방식은 모델에게 절대적인 점수를 부여하는 대신, 증명 초안의 품질을 비교하도록 요청하는 것입니다. 예를 들어 다음과 같습니다:

이 완성되지 않은 증명들 중에서 어떤 경로가 더 명확한가요? 남은 목표(goals) 중 어떤 것이 더 신뢰할 수 있어 보이나요? 어떤 것이 완료될 가능성이 더 높습니까?

그 후 시스템은 Elo 방식과 유사한 메커니즘을 사용하여 증명 초안의 순위를 매기며, 다음 두 가지 필요성을 균형 있게 맞추기 위해 P-UCB 스타일의 전략을 사용합니다:

• 높은 점수를 받은 경로를 계속 발전시키기;
• 충분히 시도되지 않은 경로를 탐색하기.

패러다임 4: 풀 피처드 에이전트 (Full-Featured Agent)

네 번째 패러다임은 논문에서 핵심적으로 홍보하는 시스템인 LLM + Lean + AlphaProof + Evolution입니다.

이는 앞서 언급한 기능들을 결합합니다:

• LLM이 증명을 작성하고, 수정하며, 보조 정리(lemmas)를 제안합니다;
• Lean이 각 단계가 올바른지 확인합니다;
• AlphaProof가 국소적 하위 목표(local subgoals)를 처리합니다;
• Evolution이 다양한 증명 경로를 저장하고 필터링합니다;
• Rater Agent가 어떤 초안에 더 많은 노력을 기울일지 판단합니다;
• SafeVerify가 최종 안전성 검증(safety verification)을 수행합니다.

이것이 AlphaProof Nexus의 완전한 형태입니다.

이 시스템이 수학 문제를 해결하는 방식은 고도로 자동화된 연구 팀과 유사합니다. 한 역할은 아이디어를 제안하고, 한 역할은 논리를 점검하며, 한 역할은 국소적인 기술적 문제를 해결하고, 한 역할은 다양한 방향을 검토하며, 한 역할은 과거의 시도들을 관리하고, 마지막 역할은 최종 승인을 수행합니다.

4. 핵심 설계: 증명 탐색은 부정행위를 방지해야 한다

AI 수학적 증명에는 특수한 실패 모드(failure mode)가 있습니다. 문제를 변경함으로써 증명을 더 쉽게 만들 수 있으며, AI는 종종 정확히 그렇게 하도록 학습됩니다.

원래 목표가 모든 자연수 n에 대해 성질 P가 성립함을 증명하는 것이라고 가정해 봅시다.

에이전트는 이를 몰래 다음과 같이 변경할 수 있습니다: 일부 자연수 n에 대해 성질 P가 성립한다.

또는 결론을 사실상 가정해 버리는, 허용되지 않은 공리(axiom)를 도입할 수도 있습니다.

Lean이 특정 로컬 체크(local checks)를 통과할 수도 있지만, 그것은 분명히 우리가 원하는 증명이 아닙니다.

따라서 AlphaProof Nexus는 다음과 같이 여러 계층의 안전 점검(safety checks)을 수행합니다:

• 정리(theorem)의 진술이 수정되었는지 확인
• sorry가 남아 있는지 확인
• 허용되지 않은 공리(axiom)가 도입되었는지 확인
• 증명이 원래의 문제와 진정으로 일치하는지 확인
• 샌드박스(sandbox) 내부에서 Lean 실행

이는 모든 에이전트 시스템(agent systems)에 유용합니다. 작업 목표(task objective)가 충분히 복잡할 때, 에이전트는 목표를 완수하는 대신 목표를 우회하는 법을 배울 수 있습니다. 강력한 검증 제약 조건(verification constraints)은 필수적입니다.

5. 논문의 실험 결과

DeepMind는 이 시스템을 여러 수학적 과제에 적용했습니다. 가장 대표적인 것은 Erdos 문제와 OEIS 추측(conjectures)입니다.

1. Erdos 문제

Erdos는 20세기 가장 중요한 수학자 중 한 명이었으며 많은 미해결 문제(open problems)를 남겼습니다. 논문에 따르면 이 시스템은 353개의 정식화된(formalized) Erdos 미해결 문제를 처리했으며, 그중 9개를 해결했습니다.

백분율이 낮아 보일 수 있지만, 이것들은 기초적인 경시 대회 문제들이 아닙니다. 이들은 연구 수준의 수학 문제들입니다.

2. OEIS 추측

OEIS는 정수 수열(integer sequences)에 대한 데이터베이스로, 수열 패턴에 관한 많은 추측을 담고 있습니다. 시스템은 492개의 OEIS 추측 중 44개를 증명했습니다.

이러한 유형의 과제는 많은 수열 추측이 정의(definitions)와 정리(theorems)로 깔끔하게 인코딩될 수 있기 때문에 정식 증명 시스템(formal proof systems)에 특히 적합합니다.

3. 실제 수학 연구에서의 배포

논문은 또한 이 시스템이 그래프 이론(graph theory), 최적화 이론(optimization theory), 대수 기하학(algebraic geometry), 가법 조합론(additive combinatorics), 양자 광학(quantum optics)을 포함한 여러 연구 분야에서 사용되었다고 밝히고 있습니다.

6. 맺음말

논문을 면밀히 읽은 후 제가 도달한 결론은 다음과 같습니다.

결론 1: LLM은 이미 정식 증명 탐색의 핵심 구성 요소가 될 수 있다

많은 이들이 거대 모델(large models)은 환각(hallucinate)을 일으키고, 단계를 건너뛰며, 무언가를 지어내기 때문에 엄밀한 수학에 취약하다고 말하곤 했습니다.

그것은 사실이지만, 불충분한 설명입니다.

만약 LLM (Large Language Model)에게 자연어 증명 (natural-language proof)을 직접 작성하도록 요청한다면, 그것은 신뢰할 수 없습니다. 하지만 Lean과 같은 엄격한 피드백 시스템 (feedback system) 내에 LLM을 배치한다면, 그것은 효율적인 탐색 엔진 (search engine)이 될 수 있습니다.

LLM의 가치는 항상 정답을 맞히는 데 있는 것이 아닙니다. LLM의 가치는 수많은 후보 경로 (candidate routes)를 제안하고, 컴파일러 피드백 (compiler feedback)을 바탕으로 이를 지속적으로 수정할 수 있다는 점에 있습니다.

결론 2: 단일 모델보다 멀티 에이전트 오케스트레이션 (Multi-Agent Orchestration)이 더 중요하다

AlphaProof Nexus의 핵심은 단 하나의 모델 버전이 어려운 문제를 해결할 수 있다는 것이 아닙니다. 핵심은 시스템이 역량을 생성 (generation), 검증 (checking), 탐색 (search), 평가 (rating), 캐싱 (caching), 그리고 확인 (verification)으로 분해한다는 점에 있습니다.