Goedel-Architect: 청사진 생성 및 정교화를 통한 형식적 정리 증명(Formal Theorem Proving)의 효율화

우리는 청사진(blueprint) 생성 및 정교화(refinement)를 중심으로 하는 Lean 4 기반의 형식적 정리 증명(formal theorem proving)을 위한 에이전트 프레임워크인 Goedel-Architect를 소개합니다. 청사진은 메인 정리(main theorem)로 구축되는 정의(definitions)와 보조정리(lemmas)의 의존성 그래프(dependency graph)입니다. 먼저, Goedel-Architect는 선언된 의존성(dependencies)과 함께 형식적으로 기술된 정의 및 보조정리의 청사진을 생성합니다. 이 청사진은 선택적으로 자연어 증명(natural language proof)에 의해 가이드될 수 있습니다. 그 다음, 도구(tool)를 갖춘 Lean 증명기(prover) 구성 요소가 관련 의존성을 사용하여 각각의 열린 보조정리 노드(open lemma node)를 병렬로 해결합니다. 실패한 보조정리는 결과적으로 전체 청사진의 정교화를 유도합니다. 이러한 전략은 재귀적 보조정리 분해(recursive lemma decomposition)를 사용하는 다른 주류 방식들과 대조되며, 막다른 전략(dead-end strategies)에서 비효율적으로 루프를 도는 문제를 방지할 수 있습니다. 오픈 웨이트(open-weight) 모델인 DeepSeek-V4-Flash (284B-A13B)를 백본(backbone)으로 사용하여, Goedel-Architect는 MiniF2F-test에서 99.2%의 pass@1을, PutnamBench에서 75.6%의 pass@1을 달성했습니다. 더 어려운 문제들에 대해 초기 청사진을 생성하는 선택적 자연어 증명 시딩(seeding)을 사용할 경우, 추가적으로 남은 두 개의 MiniF2F-test 문제를 해결하여 100%에 도달했으며, PutnamBench를 88.8%(597/672)로 끌어올렸고, IMO 2025에서 4/6, Putnam 2025에서 11/12, USAMO 2026에서 3/6를 해결했습니다. 이는 유사한 오픈 소스 파이프라인보다 비용을 최대 500배 낮추면서도 오픈 소스 파이프라인으로서 최첨단(state-of-the-art) 성능을 나타냅니다.