🤖 AI

Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement

Goedel-Architect는 블루프린트 생성 및 정제 전략을 활용하여 MiniF2F, Putnam, IMO와 같은 도전적인 수학 벤치마크에서 기존 파이프라인보다 훨씬 낮은 비용으로 최첨단 성능을 달나하는 Lean 4 정리 증명을 위한 에이전트 기반 프레임워크입니다.

원저자: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fo

게시일 2026-06-05

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Jui-Hui Chung, Ziyang Cai, Zihao Li, Qishuo Yin, Rohit Agarwal, Simon Park, Rodrigo Porto, Narutatsu Ri, Ziran Yang, Shange Tang, Xingyu Dang, Hongzhou Lin, Mengdi Wang, Danqi Chen, Chi Jin, Liam H Fowl, Sanjeev Arora

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

당신이 레고 브릭으로 거대하고 정교한 성을 쌓으려고 한다고 상상해 보세요. 당신에게는 설계도가 있지만, 그것은 그림이 아니라 "탑을 쌓으려면 먼저 기초가 필요하고, 그다음 벽, 그다음 창문이 필요하다"라고 적힌 지시 사항 목록입니다.

문제는, 만약 당신이 한 번에 거대한 도약으로 탑 전체를 쌓으려 한다면, 중간에 막히거나 탑 중간쯤 올라갔을 때 기초가 잘못 만들어졌다는 것을 깨닫게 될 수도 있다는 점입니다.

Goedel-Architect는 이러한 수학적 "성"(형식적 증명)을 Lean 4라는 언어로 구축하기 위해 설계된 새로운 스마트 로봇 팀입니다. 이들은 한 번에 전체를 구축하려고 노력하는 대신, **블루프린트 생성 및 정교화(Blueprint Generation and Refinement)**라는 전략을 사용합니다.

작동 방식은 다음과 같이 간단한 단계로 나뉩니다:

1. 블루프린트 (마스터 플랜)

로봇이 건설을 시작하기 전에, 먼저 블루프린트를 그립니다.

이것은 무엇인가? 이것은 의존성 지도(dependency map)라고 생각하면 됩니다. 큰 수학 문제를 증명하는 데 필요한 모든 작은 단계(이하 "보조 정리/lemma")를 나열합니다.
작동 방식: 어떤 단계가 다른 단계에 의존하는지를 보여주는 화살표를 그립니다. 예를 들어, "벽이 완성되기 전에는 지붕을 만들 수 없다"와 같은 식입니다.
반전: 만약 수학 문제가 정말 어렵다면, 로봇에게 **자연어 증명(Natural Language Proof)**이 주어질 수 있습니다. 이것은 인간 수학자가 로봇에게 대략적인 스케치나 문제를 해결하는 방법에 대한 이야기를 들려주는 것과 같습니다. 로봇은 이 이야기를 사용하여 처음부터 더 정확한 블루프린트를 그립니다.

2. 건설 팀 (병렬 증명)

블루프린트가 준비되면, 로봇은 한 번에 한 단계씩 짓지 않습니다. 대신 전문화된 건설 팀(Lean 증명기)을 파견하여 모든 작은 단계들을 동시에 작업하게 합니다.

각 건설자는 자신의 특정 단계와 자신이 사용할 수 있는 단계들(의존성)만 살펴봅니다.
그들은 자신의 부분을 구축하려고 시도합니다. 성공하면, 그 부분의 블루프린트를 초록색으로 바꿉니다.
실패하면, 파란색(막힘) 또는 빨간색(고장 남)으로 바꿉니다.

3. 수정 루프 (정교화)

이 부분이 Goedel-Architect가 다른 로봇들과 차별화되는 지점입니다.

기존 방식: 많은 다른 AI 시스템은 문제를 해결하려고 시도하다가 막히면, 그 막힌 부분 하나를 계속해서 더 작은 조각으로 쪼개려고만 합니다. 이것은 마치 부서진 벽을 고치기 위해 같은 자리를 계속 망치로 두드리는 것과 같습니다. 이는 종종 막다른 길로 이어집니다.
Goedel 방식: 만약 건설자가 막히게 되면, 팀 전체가 멈춰 서서 전체 블루프린트를 살펴봅니다.
- 진단: 로봇은 "왜 실패했는가?"라고 묻습니다.
  - 케이스 A (빨간색): "아, 이 단계 자체가 사실이 아니구나!" (블루프린트에 잘못된 아이디어가 있었던 것입니다). 로봇은 문장을 수정합니다.
  - 케이스 B (파란색): "이 단계는 사실이지만, 지금 당장 구축하기에는 너무 어렵다." 로봇은 이 큰 단계를 두 개 또는 세 개의 더 작고 쉬운 보조 단계로 나눕니다.
- 수정: 로봇은 이 새로운, 더 작은 단계들을 포함하여 블루프린트를 다시 작성하고 다시 팀을 투입합니다.
- 효율성: 결정적으로, 이미 성공적으로 구축된 부분(초록색)은 초록색 상태로 유지됩니다. 로봇은 기존의 좋은 작업을 버리지 않고, 오직 고장 난 부분만 고치고 새로운 보조 단계를 추가합니다.

이것이 왜 중요한가요?

이 논문은 이 접근 방식이 두 가지 주요 이유로 "게임 체인저"라고 주장합니다.

믿을 수 없을 정도로 똑똑하고 정확합니다:
- 표준 고등학교 수학 문제 테스트(MiniF2F)에서 **99.2%**를 해결했습니다. 인간 스타일의 이야기(자연어)의 도움을 받으면 **100%**를 해결합니다.
- 더 어려운 대학 수준의 수학(PutnamBench)에서는 스스로 **75.6%**를, 약간의 도움을 받아 **88.8%**를 해결했습니다.
- 심지어 다른 오픈 소스 로봇들이 해결하지 못한 아주 최근의 매우 어려운 경시대회 문제들(IMO 2025 및 Putnam 2025 등)까지 해결했습니다.
믿을 수 없을 정도로 저렴합니다:
- 이러한 문제를 해결하는 다른 최고 수준의 로봇들은 실행하는 데 수천 달러가 드는 "블랙박스" 모델을 사용하는 경우가 많습니다.
- Goedel-Architect는 더 저렴한 오픈 소스 두뇌(DeepSeek-V4-Flash)를 사용합니다.
- 비용: PutnamBench 테스트 전체를 해결하는 데 Goedel-Architect는 약 294달러가 들었습니다. 그다음으로 우수한 오픈 소스 경쟁자는 약 163,000달러가 들었습니다. 이는 500배의 절감 효과입니다.

결론

Goedel-Architect는 단순히 못을 박으려고 노력하는 건축가가 아니라, 지도를 그리고, 병렬로 건설할 팀을 파견하며, 무언가 고장 나면 좋은 부분은 유지한 채 필요한 부분만 수정하여 전체 지도를 다시 그리는 숙련된 설계자와 같습니다. 이는 가장 비싸고 비밀스러운 AI가 없어도 가장 어려운 수학 문제를 풀 수 있다는 것을 증명하며, 단지 작업을 조직하는 더 스마트한 방법이 필요함을 보여줍니다.

기술 요약: Goedel-Architect

문제 정의

본 논문은 Lean 4에서의 형식적 정리 증명(formal theorem proving)의 과제를 다루며, 특히 고성능 독점 시스템과 접근 가능한 오픈 소스 파이프라인 사이의 간극을 메우는 것을 목표로 한다. 최첨단 AI 시스템들은 상당한 수학적 능력(예: IMO 금메달, 미해결 에르되시 문제 해결)을 입증해 왔으나, 이러한 증명들을 검증하기 위해서는 엄격한 형식화가 필요하다. 기존의 오픈 웨이트 솔루션들은 PutnamBench와 같은 어려운 벤치마크에서 낮은 점수(15% 미만)를 기록하며 어려움을 겪는 반면, 성능이 높은 시스템들은 미공개 모델이나 수천 달러의 비용이 드는 값비싼 독점 API에 의존한다. 핵심적인 어려움은 복잡한 정리를 증명 가능한 보조 정리(lemma)들로 효율적으로 분해하면서도, 재귀적인 막다른 길에 빠지거나 과도한 계산 비용을 발생시키지 않는 데 있다.

방법론

Goedel-Architect는 **청사진 생성 및 정제(blueprint generation and refinement)**를 중심으로 하는 에이전트 프레임워크이다. 재귀적인 하향식 분해나 단판 승부식(single-shot) 증명 생성에 의존하는 방식과 달리, 이 시스템은 전역 의존성 그래프(global dependency graph) 상에서 작동한다.

1. 청사진 생성 (Blueprint Generation)

프로세스는 타겟 정리에 도달하기 위해 형식적으로 기술된 정의와 보조 정리들의 의존성 그래프인 청사진을 생성하는 것으로 시작된다.

구조: 타겟 정리는 그래프의 유일한 싱크(sink) 노드이다. 각 노드는 정의 또는 보조 정리를 나타내며, 엣지는 선언된 의존성(즉, 어떤 보조 정리가 어떤 사실에 의존할 수 있는지)을 나타낸다.
입력: 정리의 형식적 문장이 항상 생성의 시드(seed)가 된다. 어려운 문제의 경우, 더 강력한 모델이 생성했거나 제공된 자연어 증명이 구조적 가이드 역할을 할 수 있다.
검증: 생성기는 Lean 컴파일러와 반복 대조하여 출력된 파일이 파싱되는지, 모든 노드가 타입이 맞는지(well-typed), 그리고 그래프가 비순환(acyclic)이며 연결되어 있는지 확인한다.

2. 병렬 정리 증명 (Parallel Theorem Proving)

초기 청사진( $G_0$ )이 생성되면, 시스템은 각 보조 정리 노드를 **도구가 장착된 Lean 증명기(tool-equipped Lean prover)**에 병렬로 할당한다.

컨텍스트: 특정 보조 정리에 대한 증명기는 전체 그래프가 아니라, 해당 보조 정리 자체와 선언된 의존성(가용 사실로서)만을 본다.
도구: 증명기는 타입 체크를 위한 Lean 컴파일러와 보조 정리 조회를 위한 Mathlib 검색 서비스를 활용한다.
진단: 만약 보조 정리가 실패할 경우, 증명기는 구조화된 진단을 반환한다. 여기에는 다음이 포함된다:
- 부정(Negation): 증명기가 반례를 찾는 경우, 부정된 문장에 대한 증명을 등록한다.
- 간극 분석(Gap Analysis): 보조 정리가 참이라고 믿어지지만 증명되지 않은 경우, 증명 체인의 어느 지점에서 끊김이 발생하는지 식출한다.

3. 청사진 정제 (Blueprint Refinement)

만약 일부 보조 정리가 미해결 상태로 남으면, 정제 모델이 실패 신호를 바탕으로 전역 청사진( $G_{k+1}$ )을 다시 작성한다.

전략: 정제에는 어려운 보조 정리를 더 작은 헬퍼 보조 정리로 분해하거나, 필요한 결과에 접근할 수 있도록 의존성을 재연결하거나, 증명 과정에서 거짓으로 판명된 문장을 수정하거나 삭제하는 작업이 포함된다.
보존: 이전 반복에서 성공적으로 증명된 보조 정리들은 그 시그니처를 유지한 채 '그린 노드(green nodes)'로 보존되어 계산 노력이 낭비되지 않도록 한다.
반복: 수정된 청사진은 병렬로 다시 증명된다. 이 루프는 모든 노드가 해결되거나 반복 예산이 소진될 때까지 계속된다.

주요 기여

청사진 중심 아키텍처: 본 논문은 재귀적 분해와 대조되는 전역 의존성 그래프 접근 방식을 도입한다. 이를 통해 병렬 증명 시도가 컨텍스트를 공유할 수 있으며, 정제가 로컬 수준이 아닌 전체 전략에 대해 동시에 작용할 수 있게 한다.
오픈 웨이트 최첨단 성능: 시스템은 미공개 모델이나 독점 프런티어 모델을 사용할 필요 없이, 오픈 웨이트 모델인 **DeepSeek-V4-Flash (284B-A13B)**를 백본으로 사용하여 최첨단 성능을 달성했다.
비용 효율성: 이 파이프라인은 유사한 고성능 시스템보다 훨씬 더 비용 효율적이다. 논문은 문제당 비용이 약 $0.44라고 보고했는데, 이는 다른 오픈 소스 파이프라인보다 최대 500배 저렴하며 독점 대안들보다도 몇 자릿수 더 저렴하다.
자연어 시딩 (Natural-Language Seeding): 프레임워크는 선택적인 자연어 증명이 특히 비국소적 구조(예: 순환 합, 약수 체인)를 가진 문제에서 초기 청사진의 효과적인 구조적 스캐폴드(scaffold) 역할을 할 수 있음을 보여준다. 이는 정제 루프를 위한 전략을 고정하는 데 도움을 준다.

실험 결과

시스템은 MiniF2F-test, PutnamBench, IMO 2025, Putnam 2025, USAMO 2026의 다섯 가지 벤치마크에서 평가되었다.

MiniF2F-test: 자연어 가이드 없이 99.2% pass@1 (244문제 중 242문제)를 달성했다. 선택적 자연어 시딩을 사용하면 244문제를 모두 해결(100%)하여 오픈 웨이트 시스템의 새로운 기록을 세웠다.
PutnamBench: 75.6% pass@1 (672문제 중 508문제)를 달성하여, Hilbert 파이프라인(pass@1840에서 70.0%)과 AxProverBase(pass@1에서 54.7%)를 능가했다. 자연어 가이드를 사용했을 때(pass@4), 해결률은 88.8% (672문제 중 597문제)로 증가했다.
IMO 2025: 6문제 중 4문제를 해결했다.
Putnam 2025: 12문제 중 11문제를 해결했다.
USAMO 2026: 6문제 중 3문제를 해결했다 (모델 학습 컷오프 이후의 문제들로 구성된 오염 없는 벤치마크이다).

비용 분석: PutnamBench에서 Goedel-Architect는 API 비용으로 672개 문제 전체를 해결하는 데 $294를 사용했다. 반면, 차세대 최고 수준의 오픈 파이프라인인 Hilbert는 단 한 번의 실행에 약 $163k~$ 170k를 소비한 것으로 보고되어, 엄청난 효율성 격차를 보여주었다.

의의 및 주장

저자들은 Goedel-Architect가 형식적 정리 증명의 새로운 **파레토 프런티어(Pareto frontier)**를 구축했다고 주장한다. 이는 거대한 독점 시스템(AlphaProof나 Claude Opus 4.5를 사용하는 시스템 등)에 필적하는 높은 수준의 성능을 매우 효율적인 오픈 웨이트 백본과 혁신적인 파이프라인 설계를 통해 달성할 수 있음을 입증한다.

논문은 전역 의 dependency graph(전체적인 정제를 가능케 함)와 오픈 웨이트 모델(DeepSeek-V4-Flash)의 결 сочета이 성공의 핵심 동력임을 강조한다. 이 시스템은 학술적 접근성과 최첨단 성능 사이의 간극을 효과적으로 메우며, 고수준의 형식적 증명을 이전보다 훨씬 적은 비용으로 실현 가능하게 만든다. 저자들은 가장 어려운 문제들에 대해서는 자연어 가이드가 성능을 크게 높여주지만, 핵심 파이프라인은 표준 벤치마크에서 가이드 없이도 견고하고 효과적임을 언급했다.