검증 조건에 대한 신경망 기반 정리 증명: 실제 환경 벤치마크

Neural Theorem Proving for Verification Conditions: A Real-World Benchmark

정리 증명은 프로그램 검증의 핵심이며, 검증 조건(Verification Conditions, VCs)의 자동 증명은 주요 병목 현상입니다. 실제 프로그램 검증 과정에서 기존 자동 정리 증명기(Automated Theorem Provers, ATPs)가 증명할 수 없는 어려운 VCs가 자주 발생하며, 이는 광범위한 수동 증명의 필요성을 야기하여 실제 적용에 부담을 줍니다. 신경망 기반 정리 증명(Neural Theorem Proving, NTP)은 수학 경시대회에서 상당한 성공을 거두며, 기계 학습 접근 방식이 형식적 추론에 잠재력을 제공한다는 것을 보여주었지만, 프로그램 검증, 특히 VC 증명에 NTP를 적용하는 것은 아직 크게 탐구되지 않았습니다. 기존의 주석 합성 및 검증 관련 정리 증명 연구가 존재하지만, 자동 VC 증명이라는 근본적인 병목 현상을 구체적으로 목표로 하는 벤치마크는 없었습니다. 본 연구에서는 검증 조건에 대한 신경망 기반 정리 증명(Neural Theorem Proving for Verification Conditions, NTP4VC)을 소개하며, 이 과제에 대한 최초의 실제 환경 멀티 언어 벤치마크를 제시합니다. Linux 및 Contiki-OS 커널과 같은 실제 프로젝트에서 추출된 데이터와 Why3 및 Frama-C와 같은 산업용 파이프라인을 활용하여 Isabelle, Lean, Rocq와 같은 형식 언어에서 의미적으로 동일한 테스트 케이스를 생성합니다. 본 연구에서는 범용 대규모 언어 모델(Large Language Models, LLMs)과 정리 증명에 특화된 모델을 NTP4VC에 대해 평가합니다. 결과는 LLM이 VC 증명에서 잠재력을 보여주지만, 프로그램 검증에 있어 여전히 상당한 과제가 존재하며, 이는 향후 연구를 위한 큰 격차와 기회를 제시한다는 것을 나타냅니다.

Theorem proving is fundamental to program verification, where the automated proof of Verification Conditions (VCs) remains a primary bottleneck. Real-world program verification frequently encounters hard VCs that existing Automated Theorem Provers (ATPs) cannot prove, leading to a critical need for extensive manual proofs that burden practical application. While Neural Theorem Proving (NTP) has achieved significant success in mathematical competitions, demonstrating the potential of machine learning approaches to formal reasoning, its application to program verification--particularly VC proving--remains largely unexplored. Despite existing work on annotation synthesis and verification-related theorem proving, no benchmark has specifically targeted this fundamental bottleneck: automated VC proving. This work introduces Neural Theorem Proving for Verification Conditions (NTP4VC), presenting the first real-world multi-language benchmark for this task. From real-world projects such as Linux and Contiki-OS kernel, our benchmark leverages industrial pipelines (Why3 and Frama-C) to generate semantically equivalent test cases across formal languages of Isabelle, Lean, and Rocq. We evaluate large language models (LLMs), both general-purpose and those fine-tuned for theorem proving, on NTP4VC. Results indicate that although LLMs show promise in VC proving, significant challenges remain for program verification, highlighting a large gap and opportunity for future research.