뉴로-심볼릭 소프트웨어 검증: 대규모 심볼릭 추론을 통한 로컬 언어 모델의 성능 강화

루프 불변량 합성 (Loop invariant synthesis)은 형식 소프트웨어 검증 (formal software verification)에서 여전히 중심적이고 중추적인 병목 구간으로 남아 있습니다. 최근 LLM 기반의 뉴로-심볼릭 (Neuro-Symbolic) 도구들은 인상적인 해결률을 달성했습니다. 그러나 이러한 도구들은 독점적이고 종종 비용이 많이 드는 클라우드 API에 의존하며, 이는 소스 코드가 조직 외부로 유출될 수 없거나 비용이 중요한 요소인 개인정보 보호에 민감한 산업 현장 배포에 장애물이 됩니다. 우리는 심볼릭 불변량 생성 (symbolic invariant generation)을 로컬에 배포 가능한 오픈 웨이트 (open-weight) 언어 모델 및 ESBMC 검증 도구와 결합한 뉴로-심볼릭 파이프라인인 VerIbmc를 제시합니다. 우리의 파이프라인은 결정론적인 심볼릭 불변량 합성 단계와 구조화된 검증기 피드백에 의해 구동되는 반복적인 LLM 정제 루프 (iterative LLM refinement loop)를 결합합니다. 또한, 프롬프팅 전략이 다른 두 가지 유형의 파이프라인, 즉 Chain-of-Thought (CoT) 대 Tree-of-Thought (ToT)를 제공합니다. 우리는 5개의 벤치마크 패밀리(520개의 문제 중 피할 수 없는 오버플로가 발생하는 21개를 제외한 499개 문제 포함)에 대해 5개의 오픈 웨이트 모델(7B에서 120B 파라미터 범위)을 사용하여 광범위한 실험적 평가를 수행합니다. 전반적으로, 가장 우수한 단일 구성(GPT-OSS-120B)은 499개 문제 중 431개(86.4%)를 해결합니다. 또한, 가장 강력한 클라우드 API 도구들과 공유된 4개의 벤치마크 스위트에서 VerIbmc는 단일 로컬 머신에서 실행됨에도 불구하고 경쟁력을 보여줍니다. 평가 결과에 따르면, 심볼릭 불변량 합성은 LLM 호출 없이도 75개의 문제를 해결하며, 가장 약한 모델의 경우 최대 35개의 추가 문제를 해결하는 효과를 냅니다. 중요한 점은, 모든 추론이 오픈 웨이트 모델을 사용하여 완전히 단일 로컬 머신에서 실행된다는 것입니다. 즉, 클라우드 API나 독점 모델이 필요하지 않습니다. 종합적으로, 우리는 LLM 기반의 뉴로-심볼릭 접근 방식이 API 뒤에 갇힌 값비싼 독점 프런티어 모델에 의존할 필요 없이, 개인정보를 보호하고 에너지 효율적인 방식으로 불변량 합성에 효과적으로 사용될 수 있음을 입증합니다.