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

기술 요약: 검증 조건(Verification Conditions)을 위한 신경 정리 증명(NTP4VC)

문제 정의
프로그램 검증은 소프트웨어 신뢰성의 초석이지만, 그 채택은 여전히 안전 필수 영역에 국한되어 있습니다. 주요 병목 현상은 검증 조건(VC)—프로그램의 정확성을 인코딩하는 논리적 명제—를 증명하는 데 필요한 수동 작업입니다. 자동 정리 증명기(ATP)는 특정 도메인에서는 뛰어나지만, 실제 세계의 VC에서는 빈번하게 실패하며, 이는 광범위한 수동 주석 및 증명을 필요로 합니다. 신경 정리 증명(NTP)은 수학 경시 대회에서 가능성을 보여주었으나, 프로그램 검증의 자동화된 VC 증명이라는 구체적이고 중요한 도메인에 대한 적용은 여전히 미개척 분야로 남아 있습니다. 또한, 기존의 정리 증명 벤치마크는 보조 보조 정리(auxiliary lemmas)나 수학적 퍼즐에 집중하는 경우가 많으며, 산업용 검증 파이프라인에서 생성되는 직접적인 VC를 다루지 않으며, 여러 형식 언어에 대한 지원도 부족합니다.

방법론
저자들은 대규모 언어 모델(LLM)이 VC 증명을 자동화하는 능력을 평가하기 위해 설계된 과업 및 벤치마크인 NTP4VC를 소개합니다. 방법론은 세 가지 핵심 구성 요소로 이루어집니다:

1. 코퍼스 추출 및 번역:

   • 본 벤치마크는 기존의 산업용 검증 프로젝트(예: Linux 커널 스케줄러, Contiki-OS 메모리 할당기)를 활용하며, 이는 Frama-C(C 코드를 위함)와 Why3(검증 백엔드로서)라는 확립된 파이프라인을 통해 처리되었습니다.
   • Lean과 같은 주류 NTP 언어에는 산업용 프로젝트를 위한 네이티브 VC가 부족하기 때문에, 저자들은 규칙 기반의 번역 파이프라인을 개발했습니다. 이 시스템은 Why3에서 VCs를 추출하여 Isabelle, Lean, 그리고 Rocq(구 Coq)로 번역합니다.
   • 번역은 의미론적 보존과 대상 언어에서의 관용적 표현을 보장하기 위해 약 2,400개의 전문가 작성 매핑 및 재작성 규칙(언어당)에 의존하며, 이를 통해 LLM 기반 번역의 불확실성을 피합니다.

2. 복잡화 과정(Complication Process):

   • 검증된 프로젝트에서 직접 추출된 VCs는 인간 개발자가 이미 충분한 주석(예: assert, lemma, 그리고 lemma 적용 주석)을 제공했기 때문에 종종 "너무 쉽습니다."
   • 도전적인 벤치마크 케이스를 만들기 위해, 저자들은 이러한 보조 주석들을 체계적으로 제거하는 복잡화 과정을 구현했습니다. 이는 VCs를 완전 자동화된 검증에 더 가까운 상태로 복원하여, 충분히 강력한 증명기를 가정할 때 증명 가능성은 유지하면서 난이도를 크게 높입니다.

3. 벤치마크 구축:

   • 최종 벤치마크는 7,500개 이상의 후보군에서 엄선된 600개의 VC로 구성됩니다.
   • 세트는 두 가지 범주 사이에서 균형을 이룹니다:
     • 프로그램의 진주(Pearls of Programs) (50%): 검증의 고충(알고리즘, 자료 구조, VerifyThis와 같은 경시 문제)을 포착하는 최소한의 작동 가능한 프로그램들.
     • 실제 C 검증(Real C Verification) (50%): 산업용 C 프로젝트(예: Contiki-OS, Linux 커널, X.509 파서)에서 유도된 VCs.
   • 난이도는 Why3의 가장 강력한 사전 정의된 ATP 전술인 Auto_Level_3가 20%에서 25% 사이의 통과율을 달성하도록 조정되어, 해결 가능한 문제와 미해결 문제가 섞여 있도록 보장합니다.

핵심 기여

• NTP4VC의 정의: 본 논문은 머신러닝 기반의 증명 생성을 적용하여 VC 증명을 자동화하는 과업을 공식적으로 정의하며, 이를 프로그램 검증의 핵심 병목 현상으로 식려합니다.
• 신뢰할 수 있는 추출 방법: LLM 대신 전문가가 작성한 규칙을 사용하여 산업용 검증 파이프라인으로부터 VCs를 추출하고 여러 ITP 언어로 번역하는 새로운 오픈 소스 방법을 제공하여 의미론적 충실도를 보장합니다.
• 최초의 실세계 다중 언어 벤치마크: Isabelle, Lean, Rocq에 걸쳐 자동화된 VC 증명을 구체적으로 겨냥한 최초의 벤치마크인 NTP4VC를 도입하였으며, 다양한 알고리즘 및 산업적 사례를 포함합니다.
• 포괄적 평가: 일반 목적의 LLM(예: GPT-4o-mini, Qwen3)과 특화된 정리 증명기(예: DeepSeek-Prover-V2, Goedel-Prover), 그리고 고전적인 "해머(hammer)" 증명기(Sledgehammer, CoqHammer)를 포함한 7개 모델에 대한 광범위한 평가를 수행합니다.

결과
평가는 현재의 NTP 모델들이 프로그램 검증에서 직면한 상당한 어려움을 드러냅니다:

• 낮은 통과율: 가장 성능이 좋은 모델조차 매우 낮은 성공률을 보입니다. 최고의 언어 특화 미세 조정 모델(Minilang)은 Isabelle에서 단 2.08% pass@1을 달성했습니다. 일반 목적 모델은 성능이 더 낮습니다 (예: GPT-o4-mini-high가 1.19% pass@1).
• 해머와의 비교: 고전적인 해머 기반 증명기들이 신경 모델보다 훨씬 뛰어난 성능을 보입니다. Sledgehammer는 Isabelle에서 18.00% pass@1을 달성했고, CoqHammer는 Rocq에서 **5.67%**를 달성했습니다.
• 오류 분석: 실패 모드는 수학적 벤치마크와 다릅니다. NTP 모델은 다음 사항에서 어려움을 겪습니다:
  • 구문 오류(Syntactic Errors): Isabelle 증명의 약 24%가 깊게 중첩된 공식에서의 괄호 불일치 또는 구문 문제로 인해 실패합니다.
  • 의미론적 혼란(Semantic Confusion): 모델은 종종 실용적으로 틀린 코드(예: Lean에서 선언적 전술 대신 명령형 할당 사용)를 생성하거나, 반복적이고 무의미한 전술 적용을 수행합니다.
  • 환각(Hallucination): 모델은 존재하지 않는 전술(예: Rocq에서의 why3)이나 정의되지 않은 상수를 자주 호출합니다.
• 도메인 특수성: 해머는 "Pearls of Programs"보다 "Real C Verification" 작업에서 현저히 더 나은 성능을 보이는데, 이는 고전적인 추론 기술(SMT 솔버)이 산업용 검증 시나리오에 고도로 최적화되어 있는 반면, NTP 모델은 두 도메인 모두에서 어려움을 겪고 있음을 시사합니다.

의의 및 주장
본 논문은 NTP4VC가 프로그램 검증을 위한 신경 접근법을 발전시키는 기초적인 벤치마크를 구축한다고 주장합니다. 결과는 현재의 NTP 역량과 실제 세계의 프로그램 검증 요구 사항 사이의 상당한 격차를 강조하며, 프로그램 검증이 수학 경시 문제와는 근본적으로 다른 추론 능력을 요구함을 나타냅니다. 저자들은 LLM이 가능성을 보여주기는 하지만, 길고 깊게 중첩되며 구문적으로 엄격한 VCs를 다루는 데 있어 상당한 진전이 필요하다고 주장합니다. 이 연구는 이러한 격차를 좁히기 위한 미래 연구를 이끌 수 있는 데 필요한 인프라(벤치마크 및 추출 파이프라인)를 제공합니다. 저자들은 벤치마크 케이스가 공식적으로 검증된 프로젝트에서 유도되었으나, 번역 파이프라인의 구현 버그로 인해 이론적으로 일부 케이스가 증명 불가능할 수도 있음을 인정하며, 이를 완화하기 위해 광범위한 조치를 취했음을 언급하며 겸허한 태도를 유지합니다.