망치를 휘두르기 위한 계획: Rocq 증명 자동화를 위한 난이도 인식 분해

AI가 생성한 코드가 급증함에 따라, 소프트웨어의 정확성을 보장하기 위해 Rocq 및 Isabelle과 같은 대화형 정리 증명기 (interactive theorem provers)를 통한 형식 검증 (formal verification)의 중요성이 점점 커지고 있습니다. 그러나 이러한 증명기에서 기계가 검증 가능한 증명을 생성하는 것은 여전히 병목 현상으로 남아 있습니다. 기존의 솔루션들은 증명 자동화에 있어 상호 보완적인 강점을 제공합니다. 대규모 언어 모델 (LLMs)은 고수준의 증명 전략을 제안할 수 있지만 국소적인 엄밀함 (local rigor)이 부족하며, CoqHammer와 같은 자동화된 택틱 (automated tactics)은 많은 국소적 목표 (local goals)를 안정적으로 해결할 수 있지만 장기적인 계획 (long-range planning) 능력이 부족합니다. 이 두 세계의 장점을 결합하기 위해, 우리는 증명 계획 (proof planning)과 증명 실행 (proof execution)을 분리하는 계획 기반 증명 합성 프레임워크인 Quarry를 제시합니다. 구체적으로, Quarry는 LLM에게 임의의 부보조정리 (sublemmas)를 포함하는 여러 증명 분해 (proof decompositions)를 능동적으로 제안하도록 요청하고, 임시로 허용된 부보조정리 하에서 Rocq를 통해 이를 타입 체크 (type-checks)하며, hammer 해결 가능성을 추정하는 증명 상태 기반 난이도 모델을 사용하여 후보들을 순위 매깁니다. 그런 다음 제한된 예산 내에서 부보조정리들을 재귀적으로 증명하여, 긴 증명을 hammer로 해결 가능한 의무 (obligations)의 시퀀스로 효과적으로 전환합니다. 우리는 SerAPI 및 CoqHammer 상에 Quarry를 구현하였으며, 여러 프런티어 LLM을 사용하여 다양한 벤치마크에서 이를 평가했습니다. 실험 결과, 해결 가능성을 인식하는 순위 매기기를 결합한 계획 기반 분해가 예측 가능한 비용을 유지하면서 자동화를 실질적으로 개선함을 보여줍니다. 균일한 10분 벽시계 시간 (wall-clock) 예산 하에서, Quarry는 세 가지 Rocq 벤치마크에 걸쳐 가장 강력한 베이스라인보다 성공률을 7%에서 13%까지 향상시켰습니다. 이러한 결과는 신경망 계획 (neural planning)과 기호 실행 (symbolic execution) 중 하나를 대체하는 것이 아니라, 이 둘을 조정함으로써 신뢰할 수 있는 증명 자동화를 달성할 수 있음을 입증합니다.