증명 보조기(proof assistants)를 사용한 형식 검증(Formal verification)은 소프트웨어에 강력한 정확성 보장을 제공하지만, 증명을 구성하는 과정 자체가 노동 집약적이며 상당한 전문 지식을 요구합니다. 최근 대규모 언어 모델(LLMs)을 기반으로 한 접근 방식들은 증명 합성(proof synthesis)을 자동화하는 데 유망함을 보여주었습니다. 하지만 이러한 접근 방식들은 일반적으로 모델을 경직된 전술 생성 루프(tactic-generation loop)에 구속하며, 이 과정에서 주변 시스템이 전제 검색, 증명 상태 관리, 백트래킹(backtracking) 등을 제어합니다.
저희는 Rocq를 위한 에이전트 기반 증명 합성 시스템인 ProofCoder를 소개합니다. 이는 이론 증명을 코딩 에이전트 관점에서 접근합니다. ProofCoder는 고정된 루프 내에서 전술을 생성하기보다는, 증명 탐색 전반에 걸쳐 연속적으로 추론하며, 증명 보조기 피드백을 사용하여 추가 정보를 수집할지, 증명 상태를 검사할지, 이전에 생성한 증명 조각을 수정할지, 또는 증명의 더 이전 지점으로 백트래킹할지를 결정합니다. 이를 통해 전술 수준이든 전체 증명(whole-proof) 수준이든 관계없이 증명을 반복적으로 구성하고, 복구하며, 개선할 수 있습니다.
저희는 AutoRocq 벤치마크에서 가져온 280개의 까다로운 검증 과제에 ProofCoder를 평가했습니다. 가장 성능이 좋은 설정에서 ProofCoder는 기존의 최첨단(state-of-the-art) AutoRocq 시스템 대비 증명 성공률을 47%에서 60%로 높였으며, 이는 비용은 절반 수준으로 약 27.7%의 상대적 개선에 해당합니다. 저희의 제거 분석(ablations)은 연속적 추론이 핵심 설계 선택임을 밝혀냈습니다. 이를 사용하지 않을 경우, 에이전트는 더 적은 보조정리(lemma)를 해결하고 훨씬 높은 비용을 지불하며, 네 번에서 여섯 번 더 자주 백트래킹하고, 스스로 수정한 내용을 더 빈번하게 폐기합니다. 전체 증명 및 전술 수준의 생성은 유사한 성공률을 달성하지만 서로 다른 탐색 및 복구 전략을 따릅니다. 이러한 결과들은 효과적인 자동화된 소프트웨어 검증이 단순히 개선된 전술 선택 이상의 것을 필요로 하며, 연속적 추론과 피드백 기반 증명 수정이 견고한 증명 합성의 필수 요소임을 시사합니다.