Lean에서의 에이전트 기반 정리 증명기(Agentic Theorem Provers)의 비용-품질 트레이드오프 최적화

대규모 언어 모델(LLMs)은 Lean에서 형식적 증명(formal proofs)을 생성하는 워크플로에 점점 더 많이 사용되고 있습니다. 이러한 워크플로는 종종 문제를 더 작은 보조 정리(lemmas)로 분해하고, 많은 증명 시도(proof attempts)를 샘플링하며, 컴파일러 피드백을 사용하여 탐색을 안내합니다. 그러나 이러한 방식은 비용이 지나치게 많이 들 수 있으며, 궁극적으로 실패할 시도에 상당한 컴퓨팅 자원을 소비하는 경우가 많습니다. 본 연구에서는 데이터 평면(data plane)과 제어 평면(control plane)으로 구성된 액션 라우팅 에이전트(action routing agent)를 통해 이 문제를 해결합니다. 데이터 평면은 자연어 형태의 보조 정리 분해(lemma decompositions)를 생성하고, 이를 Lean으로 형식화하며, 결과로 나온 정리 및 보조 정리 대상에 대한 증명 시도를 샘플링합니다. 제어 평면은 이전의 실패한 Lean 시도들을 관찰하고, 성공 가능성과 추가 시도의 비용을 모두 추정하며, 현재 대상을 계속 증명할지 아니면 새로운 분해(breakdown)로부터 다시 시작할지를 결정합니다. PutnamBench의 하위 집합에 대해, 우리 에이전트는 고정 단계 베이스라인(fixed-step baseline) 대비 평균적으로 비용을 25.8% 감소시키면서도 성능을 유지하며 훨씬 적은 컴퓨팅 자원을 사용했습니다. 이러한 결과는 실패한 Lean 궤적(trajectories)이 에이전트 기반 정리 증명에서 비용 인식 자원 할당(cost-aware resource allocation)을 위한 실행 가능한 신호를 제공함을 시사합니다.