에이전트 오케스트레이션을 통한 비용 효율적인 정리 증명 (Cost-Efficient Theorem Proving via Agent

프로그램 검증(Program verification)은 정리 증명기(theorem provers)에서 구성된 기계가 확인할 수 있는 증명을 통해 소프트웨어의 정확성을 확립합니다. 이는 유창하지만 정확성에 대한 보장이 없는 대규모 언어 모델(LLMs)이 생성한 코드에 특히 가치 있는 보장입니다. 하지만 거의 모든 기존의 증명기들은 어떤 샘플링 또는 탐색 예산이 들든 간에 단순히 통과율만을 추구하며, 성공 대 비용의 경계(success-vs-cost frontier)를 간과합니다. 그러나 실제 소프트웨어는 종종 수백 개의 상호 의존적인 정리 의무(proof obligations)를 가지므로, 규모에서 중요한 것은 하나의 정리를 증명할 수 있는지 여부가 아니라 얼마나 경제적으로 많은 정리를 증명할 수 있는가입니다. 우리는 CoCo-Prover를 소개하는데, 이는 비용을 기준으로 한 메타 레벨 결정(metalevel decision-making under cost)으로서의 비용 효율적인 프로그램 증명을 형식화합니다. 이 시스템은 두 가지 수준의 증명 그래프에 기반합니다: 각 선언 내의 AND/OR 증명 하이퍼그래프가 선언 전반에 걸친 보조정리 의존성 그래프(lemma-dependency graph)와 연결됩니다. 그리고 매 단계마다, 이는 다음 두 가지 질문에 답합니다: 어떤 열린 목표(open goals)를 선택할 것인가, 그리고 이 목표들에 대해 어떤 행동을 구매할 것인가. 선택은 증명 그래프 위를 지나는 위상적 과정으로 여전히 기호적(symbolic)입니다. 행동 선택은 메타 레벨 결정으로서의 에이전트 오케스트레이션을 통해 이루어집니다: 에이전트 라우터는 모든 유한 전문 호출(bounded specialist invocation)을 개별적으로 가격이 매겨진, 최선의 노력 계산으로 취급하며, 진화된 라우팅 규칙 하에서 증거가 축적됨에 따라 이질적인 전문 에이전트들을 구성과 함께 일치시킵니다. Lean 4 기반의 다섯 가지 프로그램 검증 벤치마크(함수 레벨 CLEVER, VERINA, AlgoVeri, 그리고 저장소 레벨 NTP4VC 및 Vero)에서, 우리는 CoCo-Prover가 프론티어 코딩 에이전트와 최첨단 LLM 기반 증명기를 포함한 베이스라인보다 더 나은 성공 대 비용의 경계를 달성함을 보여줍니다. 이는 모든 벤치마크에서 최고의 해결률을 달성하며 두 가지 벤치마크에서는 최대 100%를 달성합니다. 또한, 평가에 사용된 가장 강력한 LLM을 가진 가장 강력한 베이스라인과 비교하여 비용을 최대 30.9%까지 절감합니다.