Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving
이 논문은 Lean 의 `sorry` 플레이스홀더를 활용하여 실패한 하위 목표를 격리하고 독립적으로 해결함으로써, 기존 자동 정리 증명 시스템의 비효율적인 재생성 또는 과도한 문맥 길이 문제를 극복하는 새로운 에이전트 시스템 'Mechanic'을 제안하고 IMO 2025 및 Putnam 2025 와 같은 난이도 높은 수학 경시대회 벤치마크에서 증명 효율성을 크게 향상시켰음을 보여줍니다.
기존의 인공지능들은 퍼즐을 맞추다가 하나라도 조각이 잘못 끼워지면, 다음과 같은 두 가지 중 하나를 선택했습니다.
방식 A (전체 폐기): "아, 이 조각이 안 맞네?" 하고 퍼즐 전체를 다 버리고 처음부터 다시 시작합니다. (시간과 에너지 낭비가 심함)
방식 B (점점 길어지는 수정): 잘못된 조각만 고치려고 하지만, 고치다 보면 수정 내역이 너무 길어져서 기억력이 나빠집니다. "어디서부터 다시 시작했지?" 하는 혼란이 생기고, 결국 나머지 퍼즐 조각을 놓치게 됩니다.
2. Mechanic 의 혁신 (정밀한 외과 수술)
Mechanic 은 이 문제를 해결하기 위해 **"Sorry(죄송합니다)"**라는 마법의 스티커를 사용합니다. (Lean 이라는 수학 증명 프로그램에는 증명할 수 없는 부분이 있을 때 sorry 라는 명령어로 "여기는 나중에 채울게요"라고 표시할 수 있습니다.)
Mechanic 의 작동 원리는 다음과 같습니다.
수술실로 데려가기: 퍼즐을 맞추다가 틀린 조각이 발견되면, 전체를 버리지 않습니다. 대신 틀린 조각만 정확히 찾아냅니다.
스티커 붙이기: 그 틀린 조각을 떼어내고, 그 자리에 **"여기는 나중에 채울게요 (sorry)"**라는 스티커를 붙입니다.
비유: "이 부분만 고장 났으니, 이 부분만 떼어내서 수리실로 보내고, 나머지 잘 맞는 퍼즐 조각들은 그대로 두세요."
독립적인 수리: 떼어낸 그 작은 조각 (문제) 만을 따로 가져가서 집중적으로 해결합니다.
다시 조립: 작은 조각이 해결되면, 다시 원래 퍼즐의 그 자리에 끼워 넣습니다.
이 방식 덕분에 잘 맞는 부분은 계속 유지하면서, 틀린 부분만 집중적으로 고칠 수 있어 시간과 비용이 획기적으로 줄어듭니다.
🛠️ Mechanic 이 어떻게 일하는지 (3 단계 워크플로우)
Mechanic 은 세 명의 전문가 팀이 협력하여 일합니다.
설계자 (Reasoner):
수학 문제를 보고 "우선 대략적인 해결책 (개요)"을 자연어로 먼저 짭니다.
비유: "이 퍼즐은 이렇게 맞추면 되겠어"라고 먼저 구상하는 역할입니다.
감수자 (Verifier):
설계자가 만든 개요가 논리적으로 맞는지, 그리고 나중에 컴퓨터가 읽을 수 있는 형식 (Lean) 으로 바꿀 때 문제가 없는지 꼼꼼히 검사합니다.
비유: "여기 논리가 조금 어색한데, 다시 생각해 봐야 해"라고 지적하는 역할입니다.
수리공 (Prover & Sorrifier):
Prover: 개요를 컴퓨터가 이해하는 정확한 수학 언어 (Lean) 로 번역합니다.
Sorrifier (핵심 기술): 만약 번역된 코드가 오류를 뿜어내면, 어디가 틀렸는지 정확히 찾아내서 그 부분만 sorry 로 덮어씌웁니다. 그리고 그 부분을 잘라내어 새로운 작은 문제로 만듭니다.
🏆 왜 이것이 중요한가요? (실험 결과)
이론만 좋은 게 아닙니다. 연구진은 **IMO(국제수학올림피아드)**와 푸트남 수학경시대회 같은 아주 어려운 문제들로 이 시스템을 테스트했습니다.
결과: 다른 최신 인공지능들보다 훨씬 더 빠르고 저렴하게 문제를 해결했습니다.
이유: 불필요하게 전체를 다시 만들지 않기 때문입니다. 마치 자동차가 고장 나면 엔진 전체를 갈아끼는 대신, 고장 난 부품을만 교체하는 것과 같습니다.
💡 한 줄 요약
Mechanic은 수학 증명 AI 가 실수를 했을 때 "다시 처음부터" 하지 않고, "틀린 부분만 잘라내서 (Sorry)" 따로 고친 뒤 다시 붙이는 똑똑한 방식으로, 복잡한 수학 문제를 훨씬 효율적으로 해결하는 새로운 방법입니다.
1. 문제 정의 (Problem)
최근 대규모 언어 모델 (LLM) 기반 에이전트의 발전으로 자동 정리 증명 (Automated Theorem Proving, ATP) 의 성능이 크게 향상되었으나, 복잡한 수학적 추론이 필요한 문제에서는 여전히 한계가 존재합니다.
현재의 한계: 기존 시스템은 증명 시도 실패 시 주로 두 가지 전략을 취합니다.
전체 재생성 (Full Regeneration): 실패한 증명을 완전히 버리고 처음부터 다시 생성합니다. 이는 대부분 올바른 논리 구조를 가진 부분까지 폐기하여 비효율적입니다.
점진적 수정 (Iterative Fixing): 오류를 순차적으로 수정합니다. 이는 이전 진전을 유지하지만, 반복된 수정으로 인해 컨텍스트 길이가 과도하게 길어지고, 모델이 해결되지 않은 하위 문제 (subproblems) 에 집중하는 능력이 저하됩니다.
핵심 과제: 실패한 증명의 유효한 부분을 보존하면서, 오류가 발생한 국소적 영역만 정확하게 격리하여 해결하는 효율적인 워크플로우가 필요합니다.
2. 방법론 (Methodology)
저자들은 Mechanic이라는 새로운 에이전트 시스템을 제안하며, 이는 Sorrifier(소리파이퍼) 를 활용한 공식적 분해 (Formal Decomposition) 전략을 핵심으로 합니다. Lean 증명 보조기구의 sorry 플레이스홀더를 활용하여 오류를 정밀하게 격리하는 방식입니다.
핵심 구성 요소
Reasoner (추론기): 자연어 수준의 증명 스케치를 생성하고, 하위 목표 추출 시 필요한 전제를 합성합니다.
Verifier (검증기): 증명 스케치와 공식 증명의 논리적 타당성을 평가하며, 추출된 하위 목표의 정확성을 검증합니다.
Prover (증명기): Lean 코드를 작성하고 피드백을 기반으로 오류를 수정합니다.
Lean Toolkit: Lean 컴파일러, Mathlib 검색 도구 등을 포함합니다.
Sorrifier (핵심 혁신): 오류가 있는 Lean 증명에서 sorry 플레이스홀더를 사용하여 오류 블록을 격리하는 도구입니다.
작동 프로세스 (Workflow)
Mechanic 은 다음 4 단계 반복 과정을 따릅니다 (그림 2 참조):
비공식 증명 (Informal Prove): Reasoner 와 Verifier 의 피드백 루프를 통해 논리적으로 타당한 자연어 증명 스케치를 생성하고 정제합니다.
공식 증명 (Formal Prove): 생성된 스케치를 Lean 코드로 변환합니다. 컴파일 오류가 발생하면 검색 도구와 Verifier 의 전략적 피드백을 통해 수정을 시도합니다.
하위 목표 분할 (Subgoal Split - Sorrifier):
여러 번의 수정 시도 후에도 Lean 컴파일러가 증명을 받아들이지 못하면, Sorrifier가 작동합니다.
Sorrifier 알고리즘: 컴파일 오류를 보고받은 가장 안쪽 (innermost) 블록을 찾아 해당 부분만 sorry 로 대체합니다. 이는 의존형 타입 시스템에서 발생하는 연쇄 오류 (cascading errors) 를 방지하고, 유효한 코드 부분은 보존합니다.
sorry가 삽입된 각 위치는 독립적인 하위 목표 (Subgoal) 로 추출됩니다.
하위 목표 처리 (Subgoal Process): 추출된 각 하위 목표는 동일한 3 단계 프로세스 (비공식 증명 → 공식 증명 → 분해) 를 재귀적으로 거칩니다. 모든 하위 목표가 해결되면 apply 태크틱을 사용하여 원래 증명 구조에 재조립 (Assemble) 됩니다.
3. 주요 기여 (Key Contributions)
Sorrifier-Driven Formal Decomposition: 기존 방식이 전체 증명을 폐기하거나 컨텍스트를 길게 늘리는 대신, Lean 의 sorry 기능을 활용하여 오류를 '외과 수술'하듯 정밀하게 격리하고 해결하는 새로운 패러다임을 제시했습니다.
효율적인 재사용: 증명 구조의 유효한 부분은 보존하고 오류 부분만 재해석하므로, 불필요한 연산과 긴 컨텍스트 길이를 방지합니다.
계층적 증명 구조: 복잡한 증명을 독립적이고 검증 가능한 작은 하위 목표로 분해하여, 모델의 추론 능력을 극대화합니다.
4. 실험 결과 (Results)
Mechanic 은 IMO 2025(국제수학올림피아드) 와 Putnam 2025(미국 대학 수학 경시대회) 의 난이도 높은 문제들을 대상으로 평가되었습니다.
성능: Putnam 2025 의 12 문제 중 11 문제를 성공적으로 증명했습니다.
효율성:
시간 및 비용: 해결된 11 문제에서 평균 소요 시간 (114 분) 과 API 비용 ($18.5) 이 기존 최첨단 모델 (Hilbert, Seed, Axiom, Numina 등) 보다 현저히 낮았습니다.
증명 길이: 생성된 증명 코드의 줄 수와 보조 정리 (lemma) 의 수가 타 모델보다 적어, 더 간결하고 집중된 증명 스타일을 보였습니다.
구조적 특징: 증명 트리 (Proof Tree) 가 깊게 중첩되는 대신, 넓고 얕은 (wide but shallow) 구조를 형성하여 병렬 처리가 용이하고 효율성이 높았습니다.
모델 확장성: Gemini 3.1 Pro, Claude 4.5 Opus 등 다양한 LLM 을 Reasoner/Prover 로 사용했을 때에도 일관된 성능 향상을 보였습니다.
5. 의의 및 결론 (Significance)
비공식 추론과 공식 검증의 간극 해소: 자연어 수준의 논리적 흐름을 유지하면서, Lean 의 엄격한 형식적 요구사항을 충족시키는 효율적인 브릿지를 구축했습니다.
에이전트 설계의 패러다임 전환: 단순한 오류 수정을 넘어, 실패한 증명을 구조적으로 분해하고 재구성하는 '분해 기반 에이전트'의 가능성을 입증했습니다.
미래 전망: 고정된 파이프라인을 넘어, 문제의 난이도에 따라 비공식 증명 단계 생략이나 추가 수정 반복 등을 동적으로 조절하는 더 유연한 에이전트 개발의 기초를 마련했습니다.
요약하자면, Mechanic은 자동 정리 증명 분야에서 "실패 시 전체를 버리는 것"과 "오류를 반복 수정하며 컨텍스트를 늘리는 것" 사이의 딜레마를 해결한 획기적인 접근법으로, sorry 플레이스홀더를 활용한 정밀한 분해 전략을 통해 증명 효율성과 성공률을 동시에 비약적으로 상승시켰습니다.