다중 에이전트 증명 자동 형식화에 대한 효율적인 테스트 시간 최적화

Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization

완전한 증명 자동 형식화는 자연어로 작성된 방대한 수학적 증명을 형식적으로 검증된 추론과 연결하여, 검증 가능한 수학적 추론의 한계를 높이는 방법을 제시합니다. 문장 수준의 형식화와 달리, 증명 자동 형식화는 여러 단계에 걸쳐 주장, 맥락 및 종속성을 조정해야 하는 장기적인 과제이며, 최근 들어 집중적으로 연구되기 시작했습니다. 현재 접근 방식은 비용이 많이 드는 모델 훈련에 의존하거나 추론 시간에 과도하고 지침 없는 수정을 적용합니다. 이에 따라, 우리는 ToMap이라는 다중 에이전트 프레임워크를 소개합니다. ToMap은 증명 자동 형식화를 분해기-형식화기-증명기의 파이프라인으로 구성하며, 형식적 검증과 증명의 품질에 대한 의미론적 기준을 통해 효율적인 테스트 시간 최적화를 수행합니다. 모든 에이전트에 테스트 시간 컴퓨팅을 분산하는 대신, 병목 현상 분석을 수행하여 분해기를 중요한 병목 지점으로 식별했습니다. 분해기의 원자적이고 독립적인 증명 단위의 품질은 다운스트림 에이전트가 각 단계를 성공적으로 형식화하고 증명할 수 있는지 여부에 직접적으로 영향을 미칩니다. 따라서 ToMap은 형식화기 및 증명기를 하위 실행기로 취급하고, 테스트 시간 컴퓨팅을 분해기 개선에 효율적으로 집중합니다. 이러한 개선은 GEPA에서 영감을 받은 루프를 따르며, 후보 분해에 대한 프롬프트를 발전시키고, 공식 검증 진행 상황과 의미론적 증명 기준을 함께 사용하여 다음 분해 업데이트를 안내하는 파레토 최적지를 정의합니다. ProofFlowBench 데이터 세트에 대한 실험 결과, ToMap은 구문 정확성과 의미 충실성을 모두 기준으로 이전 최고 방법보다 19.0% 향상된 성능을 보였으며, 더 낮은 테스트 시간 비용이 필요했습니다. 확장성 분석 결과, 대부분의 성능 향상은 분해 진화의 몇 번 반복 내에 나타나며, 이는 테스트 시간 예산 선택에 대한 지침을 제공합니다.

Full-proof autoformalization bridges extensive mathematical proofs in natural language with formally validated reasoning, offering a pathway to elevate the ceiling of verifiable mathematical reasoning. Unlike statement-level formalization, proof autoformalization is a long-horizon challenge requiring coordination of claims, contexts, and dependencies across many proof steps, yet has only recently come under focused study. Current approaches either rely on costly model training or apply excessive, unguided repair at inference time. To this end, we introduce ToMap, a multi-agent framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline with efficient test-time optimization guided by formal verification and semantic rubrics for proof quality. Rather than distributing test-time compute across all agents, we perform bottleneck analysis and identify the Decomposer as the critical bottleneck: the quality of its atomic, self-contained proof units directly determines whether downstream agents can successfully formalize and prove each step. ToMap therefore treats the Formalizer and Prover as downstream executors and efficiently focuses test-time compute on Decomposer refinement. This refinement follows a loop inspired by GEPA, evolving prompts over candidate decompositions and using formal verification progress together with semantic proof rubrics to define a Pareto frontier that guides the next decomposition update. Experiments on ProofFlowBench show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness, while requiring lower test-time cost. Scaling analysis shows that most gains emerge within a few iterations of decomposition evolution, guiding test-time budget selection.