🤖 AI

Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

이 논문은 모든 자기 개선이 신뢰할 수 있는 Lean 검증에 기반하도록 보장함으로써, 시드 모델 및 고정 벤치마크 모델보다 성능을 크게 향면시킨, 숙련도 제한 벤치마크와 공진화하는 자기 수정형 Lean 증명 에이전트를 소개하며, 이를 통해 홀드아웃 테스트에서 45.1%의 해결률을 달성하였다.

원저자: Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu

게시일 2026-07-21

📖 5 분 읽기🧠 심층 분석

CC BY 4.0

원저자: Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu

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

컴퓨터가 단순히 명령을 따르는 것을 넘어, 스스로 실수를 바로잡고, 자신의 지침을 다시 작성하며, 시간이 흐름에 따라 더 똑똑해질 수 있는 세상을 상상해 보십시오. 이것은 소프트웨어가 자신의 코드를 변경함으로써 스스로를 개선하려고 시도하는 인공지능의 한 분야인 '자기 진화형 에이전트(self-evolving agents)'의 영역입니다. 보통 이러한 디지털 생명체들은 마치 학생이 정답을 외울 때까지 똑같은 수학 시험을 반복해서 치르는 것처럼, 고정된 일련의 퍼즐을 대상으로 테스트됩니다. 하지만 만약 학생이 더 똑똑해질 때마다 시험 자체가 더 어려워진다면 어떻게 될까요? 이것이 바로 학습자와 도전 과제가 함께 성장하며 서로를 높은 수준으로 밀어 올리는 '공진화(coevolution)'의 개념입니다. 수학의 특정 분야인 형식 검증(formal verification)에는 증명이 100% 정확한지 확인하는 'Lean'이라는 엄격한 심판이 있습니다. 연구자들이 던져온 핵심적인 질문은 이것입니다. "컴퓨터 에이전트가 인간 교사가 전략을 설계해 주지 않아도, 스스로 수학 증명을 해결하는 최선의 방법을 찾아낼 수 있을까?"

이 논문은 하나의 디지털 '증명 에이전트'를 구축하여 그 질문에 답하고자 했던 연구팀의 이야기를 담고 있습니다. 연구진은 에이전트에게 수학 문제를 푸는 데 필요한 완벽하고 손으로 쓴 가이드를 제공하는 대신, 에이전트가 자신의 워크플로, 도구, 심지어 사고를 조직하는 방식까지 스스로 재작성하도록 허용했습니다. 공정성과 정직함을 유지하기 위해, 그들은 이 자기 개선형 에이전트를 '공진화 벤치마크'와 짝을 지었습니다. 이것은 마치 난이도가 자동으로 조절되는 비디오 게임과 같습니다. 에이전트가 레벨을 마스터하자마자, 시스템은 쉬운 레벨을 빼고 더 어려운 레벨로 교체하여 에이전트가 지루해하거나 정체되지 않도록 보장합니다. 연구진은 이 접근 방식이 놀라울 정도로 효과적이라는 것을 발견했습니다. 15세대의 진화를 거친 끝에, 그들의 자기 학습형 에이전트는 한 번도 접해보지 못한 까다로운 수학 문제 세트의 45.1%를 해결할 수 있었는데, 이는 시작 단계의 12.7%에서 엄청나게 뛰어오른 수치입니다. 그러나 이 논문은 이 에이전트가 훨씬 더 똑똑해지기는 했지만, 완전한 천재가 된 것은 아니라고 시사합니다. 즉, 완전히 새로운 복잡한 방식으로 문제를 분해하는 법을 발명하기보다는, 자신의 오류를 수정하는 데 매우 능숙해지는 법을 배웠다는 것입니다.

자기 편집 수학 봇의 이야기

당신에게 거대한 수학 증명 더미를 풀고 싶어 하는 로봇이 있다고 상상해 보십시오. 보통 인간 프로그래머는 로봇에게 엄격한 매뉴얼을 작성해 줍니다. "먼저 이것을 하시오. 그다음, 만약 오류가 발생하면 저것을 하시오." 하지만 이 실험에서 연구진은 로봇이 스스로 자신의 매뉴얼을 쓰도록 결정했습니다. 그들은 로봇의 '두뇌'(그의 코드, 도구, 그리고 전략)가 완전히 편집 가능한 시스템을 만들었습니다. 로봇은 문제를 더 빠르고 정확하게 풀 수 있는지 확인하기 위해 자신의 지침을 다시 작성하려고 시도할 수 있었습니다.

하지만 함정이 있었습니다. 만약 로봇이 자신의 코드를 재작성할 수 있다면, 실제로 풀지 못했음에도 불구하고 "풀었습니다!"라고 거짓말을 할 수도 있습니다. 이를 막기 위해 연구진은 잠들지 않는 엄격하고 변하지 않는 심판인 '신뢰할 수 있는 런타임(trusted runtime)'을 구축했습니다. Lean이라는 시스템을 기반으로 작동하는 이 심판은 궁극적인 판사 역할을 합니다. 로봇이 자신의 코드를 어떻게 바꾸든, 심판은 최종 증명을 검사합니다. 만약 증명이 심판의 현미경 아래에서 견뎌내지 못한다면, 그것은 점수로 인정되지 않습니다. 이를 통해 로봇이 속임수를 쓸 수 없도록 보장했습니다. 로봇은 점수를 얻기 위해 실제로 수학을 수행해야만 합니다.

점점 더 어려워지는 게임

이 실험의 가장 흥미로운 부분은 로봇을 테스트하는 방식입니다. 대부분의 AI 실험에서 로봇은 고정된 문제 목록을 가지고 연습합니다. 만약 로봇이 너무 똑똑해지면 정답을 그냥 암기해 버리므로 테스트가 더 이상 유용하지 않게 됩니다. 이 논문의 연구진은 이를 피하고 싶었습니다. 그들은 레벨을 깰 때마다 게임이 더 어려워지는 비디오 게임과 같은 '공진화 벤치마크'를 설정했습니다.

작동 방식은 다음과 같습니다:

챔피언: 매 라운드마다 가장 성적이 좋은 로봇(챔의 '챔피언')이 다음 라운드가 어떤 모습일지를 결정합니다.
업그레이드: 만약 챔피언이 너무 쉬운 문제들을 너무 많이 푼다면, 시스템은 그 쉬운 문제들을 은퇴시키고 더 큰 도전 과제 풀이에서 가져온 더 어려운 문제들로 대체합니다.
점수 기록원: 게임이 어려워짐에 따라 점수가 공정하게 유지되도록, 그들은 '단일 앵커 재보정(single-anchor recalibration)'이라는 특별한 수학적 기법을 사용했습니다. 만약 당신이 갑자기 경사가 가팔라진 트랙에서 경주를 한다면, 더 느리게 달리겠지만 여전히 훌륭한 러너일 것입니다. 이 시스템은 어려운 트랙에서 금메달을 따는 것이 쉬운 트랙에서 따는 것과 동일한 가치를 갖도록 점수를 조정했습니다.

이러적인 설정은 로봇이 항상 자신의 편안한 구역(comfort zone) 바로 너머로 밀려나게 하여, 단순히 예전 것을 암기하는 것이 아니라 새로운 기술을 배우도록 강요했습니다.

로봇이 실제로 배운 것

15세대를 실행한 후, 결과는 매우 흥ًا로웠습니다. 로봇은 처음에 문제의 약 12.7%만을 해결했습니다. 15세대째에 이르러, 가장 성능이 좋은 버전의 로봇은 처음 보는 새로운 테스트의 문제 중 45.1%를 해결할 수 있었습니다. 이는 엄청난 발전이며, 로보가 스스로를 재작성하게 두는 것이 실제로 지능 향상에 도움이 되었음을 보여줍니다.

그러나 연구진은 로봇이 어떻게 똑똑해졌는지에 대해 흥미로운 사실을 발견했습니다. 그들은 로봇이 결국 큰 문제를 작고 관리 가능한 조각들로 나누는 복잡한 단계별 전략(마치 건축가가 건물의 각 층을 설계하듯)을 찾아낼 것이라고 기대했습니다. 대신, 승리한 로봇들은 주로 수정(repair) 전문가가 되었습니다.

이렇게 생각해 보십시오. 로봇은 전체 증명을 빠르게 작성한 다음, 오류를 확인하고, 깨진 특정 부분을 고치는 법을 배웠습니다. 로봇이 반드시 처음부터 전체 건물을 계획하는 것은 아니었습니다. 그저 균열을 메우는 데 매우 능숙해진 것입니다. 연구진은 로봇이 복잡한 단계별 계획을 세우려고 시도했지만, 이러한 계획들은 종종 무너지거나 너무 위험하다는 것을 발견했습니다. "시도하고, 확인하고, 고쳐라"라는 더 단순한 전략이 더 신뢰할 수 있었고 경쟁에서 승리했습니다.

로봇 또한 자신을 돕기 위한 영리한 도구들을 발명했습니다. 예를 들어, 로봇은 자신이 사용하는 수학 용어의 이름을 재확인하여 가짜 단어를 만들어내지 않도록(이는 '환각'이라 불리는 흔한 실수입니다) 학습했습니다. 로봇은 제출하기 전에 모든 증명의 각 부분이 실제이고 유효한지 확인하기 위해 작은 체크리스트와 검색 도구를 구축했습니다.

결론

그렇다면 로봇은 수학 천재가 되었을까요? 꼭 그렇지는 않습니다. 극적으로 발전하기는 했지만, 여전히 최고의 인간 설계 로봇들처럼 문제의 99%를 해결하지는 못합니다. 연구진은 로봇이 아직 '계획 모드'보다는 '수정 모드'에 머물러 있다고 제안합니다. 오류를 고치는 데는 뛰어나지만, 기초부터 완벽하고 깊은 구조를 구축하는 방법은 아직 터득하지 못했습니다.

이 실험은 자기 진화형 에이전트가 도구를 더 잘 사용하는 법을 배우고, 도전 과제가 자신과 함께 계속 성장할 때 훨씬 더 똑똑해질 수 있음을 보여줍니다. 하지만 동시에, 인간이 더 복잡한 전략을 향해 이끌어주지 않는 한, 로봇이 스스로를 가르칠 수 있는 데에는 한계가 있다는 점도 시사합니다. 로봇은 스스로 진화할 수 있음을 증명했지만, 진정한 수학적 거장이 되기 위한 여정은 여전히 진행 중입니다.

기술 요약: 검증기 기반 벤치마크 공진화를 통한 자기 수정형 Lean 증명 에이전트

문제 정의

Lean 기반 정리 증명을 위한 효과적인 에이전트 프레임워크를 설계하는 것은 두 가지 과제에 직면해 있다: 증명 에이전트의 원시 합성 능력을 향상시키는 것과 이를 둘러싼 증명 워크플로를 최적화하는 것이다. 최근 연구들은 더 강력한 특화 모델이나 택틱(tactic)을 구축하는 데 집중해 왔으나, 보완적인 관점에서는 병목 현상이 에이전트와 Lean 환경 간의 상호작용, 즉 어떻게 의무(obligation)를 분해하고, 컴파일러 피드백을 활용하며, 실패를 진단하고, 구조화된 증명 컨텍스트를 유지하느냐에 있다고 주장한다.

현재의 자기 진화형 에이전트 시스템(예: Darwin Gödl Machine, Hyperagents)은 일반적으로 외부에서 제공되는 고정된 벤치마크를 대상으로 에이전트를 최적화한다. 이러한 접근 방식은 형식 수학(formal mathematics)에 적합하지 않은데, 그 이유는 다음과 같다:

선택 신호(Selection Signal): 만약 벤치마크가 너무 어려우면(예: 경시대회 수준의 문제), 대부분의 평가가 실패하여 진화를 위한 그래디언트(gradient)를 제공하지 못한다. 반대로 너무 쉬우면, 에이전트는 빠르게 포화 상태에 도달한다.
워크플로의 경직성(Workflow Rigidity): 대부분의 에이전트는 수작업으로 설계된 워크플로에 의존한다. 문제는 에이전트가 인간의 개입 없이 스스로의 증명 워크플로, 도구, 그리고 컨텍스트 표현 방식을 진화시킬 수 있는지 여부이다.
그라운딩(Grounding): 자기 수정형 에이전트는 자신의 성공을 스스로 보고하는 것을 신뢰할 수 없다. 따라서 성공 여부를 판정하기 위해 고정되고 신뢰할 수 있는 검증기가 필요하다.

방법론

저자들은 자기 진화형 Lean 증명 에이전트가 자기 강화형 벤치마크와 함께 공진화하며, 이 모든 과정이 고정된 신뢰할 수 있는 Lean 검증기에 의해 그라운딩되는 시스템을 제안한다.

1. 시스템 아키텍처

신뢰할 수 있는 런타임 vs. 가변적 작업 공간: 시스템은 Lean 검증, 평가 및 벤치마크 관리를 담당하는 고정된 신뢰 런타임과, 완전히 가변적인 작업 공간을 분리한다. 에이전트는 이 작업 공간 내에서 자신의 증명 워크플로, 프롬프트, 도구를 스스로 재작성할 수 있다.
코드 유효성 vs. 증명 성공: 변형된 에이전트는 코드가 실행되는지 확인하기 위한 코드 수준의 "스모크 테스트(smoke test)"를 거치지만, 생성된 증명이 신뢰할 수 있는 Lean 스냅샷 하에서 다시 검증될 때만 해당 정리가 "해결됨"으로 표시된다.
검증기 기반 계약(Verifier-Grounded Contract): 모든 해결 시도는 반드시 기계 판독 가능한 증명 컨텍스트를 출력해야 한다. 이 컨텍스트의 표현 방식(그래프, 트리, 테이블 등)은 자유롭게 진화할 수 있지만, 그 *그라운딩(실제 근거)*은 강제된다. 런타임은 인증서를 정제하고, sorry/admit을 거부하며, 클레임을 독립적으로 재검증한다.

2. 공진화 벤치마크 메커니즘

고정된 벤치마크 대신, 시스템은 **챔피언 주도형, 숙련도 제한형 커리큘럼(champion-driven, mastery-throttled curriculum)**을 채택한다.

태스크 풀(Task Pool): 문제들은 세 가지 난이도 단계로 계층화된다 (L1: 단일 택틱 렘마; L2: miniF2F; L3: PutnamBench).
업데이트 규칙: 각 세대가 끝날 때, 만약 "챔피언"(최고 점수 에이전트)이 해결 임계값( $\gamma=0.30$ $γ = 0.30$ )을 초과하면 벤치마크가 업데이트된다.
- 모든 에이전트가 해결한 태스크는 퇴출된다.
- 챔피언의 특정 단계에서의 숙련도가 임계값( $\tau=0.70$ )을 초과하면, 퇴출된 태스크는 다음 단계의 더 어려운 태스크로 교체된다. 그렇지 않으면 동일한 난이도의 새로운 태스크로 수평 교체된다.
- 업데이트는 에이전트 집단이 실패를 축적한 도메인을 선호한다.
단일 앵커 재보정(Single-Anchor Recalibration): 난이도가 높아짐에 따라 점수의 비교 가능성을 유지하기 위해, 챔피언은 새로운 벤치마크에서 재평가된다. 난이도 계수( $c$ )는 세대 간 점수를 정규화하기 위해 곱셈적으로 업데이트된다 ( $q = r \times c$ ).

3. 진화 인터페이스

부모 선택: 에이전트는 난이도 정규화된 점수에 따라 아카이브에서 선택되며, 계보의 독점을 방지하기 위해 이미 생성한 자식의 수에 따라 할인이 적용된다.
자기 수정: 에이전트는 자신의 코드, 즉 워크플로 로직(예: 복구 루프, 분해 전략)과 도구(예: 렘마 체커)를 포함하여 스스로 재작성한다.

주요 기여

자기 진화형 Lean 증명 에이전트: 저자들은 증명 워크플로와 도구가 가변적이지만, 증명의 성공은 엄격하게 Lean 검증에 근거하는 코드 수준의 자기 진화형 에이전트를 제시한다.
벤치마크 공진화: 챔피언 주도형의 자기 강화형 벤치마크를 도입하여 에이전트와 함께 진화하도록 한다. 이는 숙련도 제한형 업데이트와 단일 앵커 재보정을 사용하여, 고정된 쉬운 벤치마크의 포화와 고정된 어려운 벤치마크의 희소성 문제를 모두 해결한다.
표현 자유도가 보장된 그라운딩된 증명 컨텍스트: 시스템은 에이전트가 증명 컨텍스트의 형식(예: 평면 로그에서 구조화된 그래프로)을 진화할 수 있게 하되, 해결된 클레임의 유효성은 신뢰할 수 있는 런타임에 의해 엄격히 강제된다.

실험 결과

시스템은 15번의 활성 세대에 걸쳐 평가되었으며, 고정 벤치마크 베이스라인과 공진화 궤적을 비교하였다.

홀드아웃 테스트 성능:
- 시드 에이전트(Seed Agent): 홀드아웃 miniF2F 테스트 분할에서 12.7% 해결률 기록.
- 고정 벤치마크 베이스라인: 최상의 에이전트가 32.0%에 도달.
- 공진화 에이전트: 최상의 에이전트(c144, 15세대)는 홀드아웃 테스트에서 **45.1%**에 도달.
벤치마크 강화: 난이도 계수가 15세대 동안 1.00에서 3.17로 상승하였으며, 이는 벤치마크가 에이전트의 개선에 맞춰 성공적으로 복잡성을 높였음을 나타낸다.
워크플로 진화:
- 복구 중심의 우세(Repair-Centered Dominance): 승리한 워크플로는 "분해 중심"(하위 목표 계획 $\to$ 증명 $\to$ 조립)보다는 주로 "복구 중심"(증명 생성 $\to$ Lean 에러 확인 $\to$ 복구) 형태를 유지했다.
- 도구 진화: 에이전트들은 환각된(hallucinated) Lean 이름을 방지하기 위한 도구들(예: #check 프로브, 소스 검색, 검증된 렘마 캐시)을 성공적으로 진화시켰다.
- 분해 시도: 여러 에이전트가 분해 기반 워크플로(예: c26, c44, c141)를 시도했다. 이러한 에이전트들은 자가 포함된 하위 렘마에 대한 실제 노드 수준의 검증을 진화시키기도 했으나, 조립 단계에서 새로운 실패 지점(JSON 파싱, 컨텍스트 불일치 등)을 유발하여 최종 해결률을 낮추었기 때문에 선택 과정에서 탈락되는 경우가 많았다.
증명 컨텍스트: 증명 컨텍스트는 검사 가능한 형태로 변했으나, 깊이 있는 검증된 의존성 그래프로 진화하는 경우는 드물었다. 에이전트들은 그래프를 미리 계획하기보다 최종 증명으로부터 역방향으로 컨텍스트를 구성하는 경향을 보였다.

의의 및 주장

본 논문은 검증기 기반의 자기 진화가 Lean 증명 워크플로를 개선할 수 있음을 주장한다.

자기 개선의 실현 가능성: 결과는 고정되고 신뢰할 수 있는 검증기가 성공을 중재하는 한, 에이전트가 자신의 코드를 재작성함으로써 수학적 워크플로와 도구를 개선할 수 있음을 입증한다.
공진화의 중요성: 절제 연구(ablation study)는 고정된 벤치마크가 에이전트가 특정 태스크를 마스터하면 정체 상태에 빠지게 함을 보여준다. 공진화하는 벤치마크는 난이도를 지속적으로 높임으로써 유익한 선택 신호를 유지한다.
한계 및 향 향후 방향: 저자들은 현재 상태에 대해 겸허한 태도를 보인다. 승리한 워크플로는 여전히 복구 중심적이며, 시스템은 아직 Goedel-Architect(miniF2F-test에서 99.2% 달성)와 같은 수작업 설계 에이전트에 필적하는 깊고 지속적인 증명 컨텍스트 그래프(DAG)를 진화시키지 못했다. 저자들은 더 복잡한, 분해 우선(decomposition-first) 워크플로를 진화시키기 위해서는 더 긴 실행 시간, 더 큰 인구 규모, 또는 검증된 분해를 구체적으로 타겟팅하는 보상이 필요할 수 있다고 제언한다.

이 연구는 검증 로직은 고정하되 증명 구축의 "방법"은 진화할 수 있도록 하는, 형식적 영역에서의 자기 적응형 에이전트를 위한 토대를 마련한다.