에이전트 유도 트리 탐색을 통한 형식 검증의 자동화

형식 검증 (Formal verification)은 증명 가능한 올바른 소프트웨어로 가는 길을 제시하지만, 검증된 코드를 작성하는 비용이 여전히 매우 높아 실제 운영 환경에서는 거의 사용되지 않습니다. 최근의 대규모 언어 모델 (LLM)은 이 작업을 가속화할 수 있으며, 최근의 벤치마크들은 사양 (specifications)을 코드와 기계가 확인 가능한 정답 증명 (machine-checked proofs)으로 변환하는 능력을 측정합니다. 본 논문은 Lean 환경에서 이러한 LLM 기반의 검증된 코드 생성 ("vericoding")의 현황을 평가하고, 검증 성능을 향상시키기 위한 탐색 기반 방법론을 개발합니다. 먼저, 현재의 여러 벤더 모델 풀을 대상으로 vericoding-benchmark Lean 리더보드의 하위 집합을 재현하였으며, 그 결과 비추론 (non-reasoning) 성능은 미국 폐쇄형 소스 모델 (closed-source models)에서 대략 일정하게 유지되는 반면, 오픈 웨이트 (open-weight) 모델들은 약간 향상되었음을 확인했습니다. 우리는 mathlib 탐색 기능이 장착된 에이전트 루프 (agentic loop)를 통해 vericoding-benchmark의 반복적 방법론을 업데이트하였으며, 모델 성능이 크게 향상되고 에이전트 예산 (agent budget)에 따라 확장됨을 발견했습니다. GPT-5.4는 $K=50$번의 LLM 호출 시 423개의 사양에 대해 95.0%의 성능을 기록하며 벤치마크를 거의 포화 상태로 만들었습니다. 이어 우리는 두 가지 에이전트 유도 트리 탐색 (agent-directed tree-search) 공식을 설계했습니다: 부분 증명 상태 (partial-proof states)에서 분기하는 상태 기반 오케스트레이터 (state-based orchestrator)와 전체 서브 에이전트 컨텍스트 (full subagent contexts)에서 분기하는 컨텍스트 기반 오케스트레이터 (context-based orchestrator)입니다. 에이전트 베이스라인 (agent baseline)과 비교했을 때, 컨텍스트 기반 설계는 더 낮은 토큰 비용으로 더 넓은 범위의 중간 난이도 사양을 해결하는 반면, 에이전트 베이스라인은 중단 없는 반복이 가장 중요한 가장 어려운 사양에서 우위를 유지합니다. 결론적으로, 탐색 구조는 강력한 에이전트 베이스라인에 대해 선택적인 이점을 가지며, 자동화된 형식 검증의 진전을 측정하고 추진하기 위해서는 현대적 코드에서 추출한 더 도전적인 벤치마크가 중요함을 밝힙니다. 코드는 저자(leoy@mit.edu)에게 연락하여 요청 시 제공 가능합니다.