기술 요약: 다중 에이전트 증명 자동 형식화(Autoformalization)를 위한 효율적인 테스트 시점 최적화

1. 문제 정의

전체 증명 자동 형식화(Full-proof autoformalization)는 광범위한 자연어 수학 증명을 Lean과 같은 증명 보조 도구 내에서 형식적으로 검증 가능한 추론으로 변환하는 것을 목표로 합니다. 단일 정리(Theorem) 수준의 형식화가 하나의 정리만을 번역하는 데 집중하는 것과 달리, 전체 증명 자동 형식화는 수많은 증명 단계 전반에 걸쳐 주장(Claims), 문맥(Contexts), 의존성(Dependencies)을 조정해야 하는 장기적 관점(Long-horizon)의 과제입니다.

현재의 접근 방식들은 두 가지 주요 한계점에 직면해 있습니다:

1. 비용이 많이 드는 학습: 많은 방법론이 대규모 지도 미세 조정(Supervised Fine-tuning)에 의존하지만, 증명 수준의 쌍을 이룬 감독 데이터(Paired supervision data)가 부족하기 때문에 이는 매우 어렵습니다.
2. 비효율적인 테스트 시점 최적화: 기존의 추론 시점 방법들은 종종 전체 파이프라인 전체에 대해 과도하고 가이드가 없는 복구 또는 반복적인 정교화(Refinement)를 적용합니다. 전체 증명 설정에서는 검증 피드백(예: Lean 에러)이 긴 생성 체인 이후에나 도착하며, 어떤 상위 결정이 실패를 유발했는지 밝혀내는 경우가 드뭅니다. 이는 제한된 테스트 시점 연산량을 무분별한 재시도가 아닌 타겟팅된 개선에 투입하는 것을 어렵게 만듭니다.

2. 방법론: TOMAP 프레임워크

저자들은 TOMAP(Test-time Optimization for Multi-Agent Proof autoformalization)을 소개하며, 이 과업을 분해자(Decomposer)-형식화 도구(Formalizer)-증명 도구(Prover) 파이프라인으로 구조화합니다. 핵심 혁신은 시스템의 결정적인 병목 구간을 식별하고 이를 타겟팅하는 효율적인 테스트 시점 최적화 전략입니다.

2.1 다중 에이전트 파이프라인

시스템은 세 가지 특화된 에이전트로 구성됩니다:

• 분해자 ($D$): 비형식적 증명을 명시적인 의존성을 가진 원자적이고 자기 완결적인 하위 명제(Proof units)로 나눕니다.
• 형식화 도구 ($F$): 각 자연어 하위 명제를 형식적인 Lean 문장으로 번역합니다.
• 증명 도구 ($P$): 각 형식화된 목표를 증명하기 위한 태틱 스크립트(Tactic scripts)를 생성합니다.
• 검증 도구 ($V$): 조립된 증명 파일을 검증하는 외부 Lean 체커입니다.

2.2 약점 분석 (Weak-Link Analysis)

최적화를 수행하기 전, 저자들은 테스트 시점 연산이 가장 높은 수익을 창출하는 지점을 결정하기 위해 "약점 분석"을 수행합니다. 다른 단계들을 고정한 채 각 단계(분해자, 형식화 도구, 증명 도구)에 개별적으로 개입함으로써, 엔드 투 엔드 검증 성공의 회복 가능성(Recoverability)을 측정합니다.

• 발견: **분해자(Decomposer)**가 결정적인 병목 구간입니다. 자연어 증명 단위(주장, 가정, 의존성)의 사양을 수정하는 것이 형식적 문장(45.1%)이나 증명 스크립트(33.7%)를 수정하는 것보다 최종 검증 성공(51.1% 정확도) 측면에서 훨씬 더 높은 이득을 가져옵니다.
• 시사점: 고품질의 원자적이고 자기 완결적인 증명 단위는 다운스트림의 형식화 및 증명 작업을 형식화 도구와 증명 도구의 역량 범위 내에 있는 국소적 작업으로 감소시킵니다.

2.3 테스트 시점 최적화 전략

TOMAP은 형식화 도구와 증명 도구를 고정된 다운스트림 실행기로 취급하고, 모든 테스트 시점 연산을 분해자를 정교화하는 데 집중합니다. 최적화는 GEPA 스타일(Reflective Prompt Evolution) 루프를 따릅니다:

1. 후보 풀(Candidate Pool): 주어진 입력에 대한 후보 분해안들의 풀을 유지합니다.
2. 루브릭 점수 산정(Rubric Scoring): 비용이 많이 드는 Lean 검증기를 즉시 호출하는 대신, LLM 기반의 "루브릭 판사(Rubric Judge)"가 다음 세 가지 차원에 따라 후보들을 점수 매깁니다:
   • 의미적 충실도(Semantic Faithfulness): 원래의 자연어 증명과의 일치 여부.
   • 증명 가능성(Provability): 각 단위가 자기 완결적이고 논리적으로 완전한지 여부.
   • Lean 친화성(Lean Friendliness): 명확성, 가정의 명시성, 그리고 모호성 회피 정도.
3. 파레토 가이드 진화(Pareto-Guided Evolution): 후보들은 루브릭 점수를 바탕으로 파레토 프런티어(Pareto frontier) 상에서 평가됩니다. 성찰적 LLM 제안자(Proposer)는 고성능 후보를 선택하고, 루브릭 피드백을 바탕으로 이를 비판하며, 수정된 분해안을 제안합니다.
4. 검증 게이팅(Verification Gating): 높은 품질 임계값(루브릭 통과)을 충족하는 후보들만이 비용이 많이 드는 실제 Lean 검증을 위해 다운스트림 형식화-증명 파이프라인으로 전달됩니다.

이 이중 설계는 검색을 유도하기 위한 저렴하고 밀도 높은 대리 피드백(루브릭)과, 유망한 후보에게만 예약된 비용이 많이 드는 충실한 검증 사이의 균형을 맞춥니다.

3. 주요 기여

• 병목 구간 식별: 본 논문은 약점 분석을 통해 증명 분해 품질이 전체 증명 자동 형식화의 성공을 결정하는 주요 결정 요인임을 실증적으로 입증하였으며, 이를 통해 최적화의 초점을 전체 파이프라인에서 분해자 인터페이스로 전환했습니다.
• TOMAP 프레임워크: 검색과 검증을 분리하는 새로운 테스트 시점 최적화 방법을 제공합니다. 이는 다중 목적 루브릭 피드백과 파레토 선택을 사용하여 증명 분해를 진화시키며, 검색 단계 중 발생하는 값비싼 Lean 호출에 대한 의존도를 크게 낮춥니다.
• 효율성 및 성능: 대규모 학습 없이도 효율적인 추론 시점 최적화에 의존하여 최첨단(SOTA) 결과를 달합니다.

4. 실험 결과

실험은 PROOFFLOWBENCH(학부 수준 문제 184개)와 miniF2F(고등학교 수준 문제 244개)에서 수행되었습니다.

• 성능: TOMAP은 학습 기반 베이스라인(예: ProofBridge)과 학습이 필요 없는 베이스라인(예: PROOFFLOW, Monotonic) 모두를 능가합니다.
  • PROOFFLOWBENCH에서 TOMAP(Gemini3-Pro 사용)은 최상의 기존 방법보다 결합된 구문적 정확성(Syntactic Correctness) 및 의미적 충실도(Semantic Faithfulness) 점수를 19.0% 향상시켰습니다.
  • miniF2F에서는 결합 지표에서 **8.2%**의 향상을 달성했습니다.
• 의미적 충실도: TOMAP은 단일 모델 생성기(Monolithic generators)보다 원래 증명의 의미 구조를 보존하는 데 있어 월등히 뛰어납니다. 이는 다른 방법들이 의미적으로는 틀리지만 구문적으로는 유효한 Lean 코드를 생성하는 경향을 방지합니다.
• 비용 효율성: TOMAP은 단순한 베이스라인보다 더 많은 테스트 시점 연산을 요구하지만, 전체 파이프라인을 광범위하게 반복 재시도하는 방법들과 비교했을 때 더 낮은 총 비용으로 더 높은 성공률을 달로합니다.
• 스케일링 분석: 절제 연구(Ablation studies)에 따르면 대부분의 성능 향상은 분해 진화의 초기 몇 회 반복 내에 발생하며, 이는 테스트 시점 예산을 선택하는 데 실질적인 가이드를 제공합니다.

5. 의의 및 주장

본 논문은 전체 증명 자동 형식이 근본적으로 **분해 품질(Decomposition quality)**의 문제라고 주장합니다. 분해자를 가장 피드백 회복력이 높은 단계로 식별함으로써, 저자들은 자원을 단순히 형식화나 증명을 반복적으로 재시도하는 데 쓰는 대신 자연어 증명 구조를 정교화하는 데 집중함으로써 효율적인 테스트 시점 최적화를 달성할 수 있음을 보여줍니다.

TOMAP의 의의는 다음과 같습니다:

1. 비형식적 증명과 형식적 검증 사이의 간극을 더 충실하게 메움으로써 검증 가능한 수학적 추론의 한계를 높입니다.
2. 복잡한 미세 조정 접근 방식에 대한 확장 가능한 학습 불필요(Training-free) 대안을 제공합니다.
3. 인과 분석을 통해 식별된 "약점"을 우선순위에 둠으로써 다중 에이전트 시스템에서 제한된 테스트 시점 연산을 할당하는 실용적인 프레임워크를 제공합니다.

저자들은 벤치마크 규모의 증명에 국한된다는 점과 입력된 비형식적 증명이 올바르다는 가정 등 한계점을 언급했습니다. 잘못된 증명 단계를 탐지하고 수정하는 것은 향후 연구 과제로 남겨두었습니다.