프로그램 검증을 위한 에이전트 기반 증명 (Agentic Proving)

최근 에이전트 시스템 (Agentic systems)은 형식 수학 (formal mathematics) 분야의 자동 정리 증명 (automated theorem proving)을 위한 최첨단 접근 방식으로 부상했습니다. 이러한 능력이 프로그램 검증 (program verification)까지 얼마나 확장될 수 있는지 평가하기 위해, 우리는 검증 가능한 코드 생성 (verifiable code generation)을 위한 Lean 4 벤치마크인 CLEVER 상에서 에이전트 기반 증명 프레임워크를 통해 Claude Code를 평가합니다. 우리의 결과에 따르면, Claude는 문제의 98.8%에 대해 논쟁의 여지 없이 유효한 명세 (specifications)를 생성하며 (이 중 81.3%는 벤치마크의 올바른 부분에 대해 CLEVER의 동형 기반 점수 산정 (isomorphism-based scoring) 방식에 의해 승인됨), 문제의 87.5%에 대해 올바른 정답 명세 (ground-truth specifications)를 기준으로 구현을 인증하며, 자기 일관적인 전제 (self-consistent premises)를 가진 항목들에 대해 엔드 투 엔드 (end-to-end) 프로그램 생성 및 검증 파이프라인에서 98.1%의 성공률을 달성합니다. 모든 단계에 걸쳐, Claude는 자신의 시도에 대해 고품질의 피드백을 추가로 제공하며 (수동 검토를 통해 확인됨), 실패의 근본 원인과 데이터셋 내에 남아있는 버그를 식별합니다. 이러한 발견은 기존 프로그램 검증 벤치마크의 난이도와 현대적인 에이전트 기반 증명기 (agentic provers)의 능력 사이의 불일치가 커지고 있음을 강조하며, 더욱 엄격하고 버그에 탄력적인 (bug-resilient) 평가 방법론, 특히 생성된 명세에 대한 동형 기반 점수 산정 방식의 대안이 필요함을 시사합니다. 더 넓게는, 우리의 결과는 컴파일러 인 더 루프 (compiler-in-the-loop) 에이전트 패러다임이 현재 기초적인 프로그램 검증을 위한 가장 효과적인 접근 방식이라는 실증적 근거를 제공합니다.