기술 요약: 자동 소프트웨어 검증을 위한 코드 에이전트 활용

문제 정의

형식 검증(Formal verification)은 소프트웨어의 정확성에 대해 가장 강력한 보증을 제공하지만, 수동 증명 구성에 드는 막대한 비용으로 인해 역사적으로 확장성 확보에 실패해 왔습니다. Coq와 같은 대화형 정리 증명기(ITP)는 전문가가 단계별로 증명을 구성해야 하며, 이는 동시성(concurrency)과 공유 가변 상태(shared mutable state)로 인해 증명이 어렵고 시간이 많이 소요되는 분리 논리(separation logic, 예: Iris)와 같은 복잡한 영역에서 더욱 심화되는 병목 현상을 야기합니다.

기존의 자동화된 접근 방식은 시스템 내에 고정된 인간 설계 증명 전략을 내장하여 이를 해결하려고 시도합니다. 이러한 시스템은 일반적으로 LLM이 하나의 택틱(tactic)을 예측하거나, 전제(premise)를 검색하거나, 목표를 재귀적으로 분할하는 것과 같은 특정 패턴을 따르도록 제약을 가합니다. 그러나 이러한 방식은 다음과 같은 두 가지 결정적인 한계를 가집나다:

1. 부분적 커버리지: 가용 벤치마크에서 12%~48%의 성공률만을 달성합니다.
2. 제한된 범위: 벤치마크가 주로 순차적 프로그램이나 단순한 데이터 타입에 집중되어 있어, 실제 세계의 검증 과제를 정의하는 동시성 및 미세한 메모리 추론이라는 어려운 차원을 누락합니다.

또한, 이러한 시스템은 증명이 어떻게 구축되는지를 규정하는 수작업 기반의 "스캐폴딩(scaffolding)"에 의존합니다. 본 논문은 이러한 스캐폴딩이 불필요하며 오히려 제한적이며, 범용 코드 에이전트의 역량을 온전히 활용하는 것을 방해한다고 주장합니다.

방법론: Aria 시스템

저자들은 일반 목적의 LLM 코드 에이전트(구체적으로 Claude Opus 4.7에서 실행되는 Claude Code)를 검증 하네스(verification harness)와 결합한 Aria를 제안합니다. 이전 연구와 달리, Aria는 Coq 특유의 증명 전략, 전제 선택기, 또는 분해 휴리스틱을 에이전트에 강요하지 않습니다. 대신, 에이전트에게 전체 렘마(lemma)를 부여하고 접근 방식을 자유롭게 선택할 수 있는 권한을 줍니다.

아키텍처

Aria는 3계층 아키텍처로 작동합니다:

1. 모델 계층 (Model Layer): 현재의 목표, 컨텍스트, 피드백이 포함된 구조화된 프롬프트를 기반으로 후보 증명을 생성하는 상태 비저장(stateless) LLM 백엔드입니다.
2. 에이전트 계층 (Agent Layer): 세션을 관리하고 컨텍스트(정의, 이전 렘마)를 검색하며 모델의 응답을 해석하는 오케스트레이터입니다. 명령줄 인터페이스(CLI)를 통해 비대화형 방식으로 에이전트를 구동합니다.
3. 하네스 계층 (Harness Layer): 신뢰의 닻(trust anchor) 역할을 합니다. Coq 커널을 래핑하여 정책 검사를 강제합니다. 후보 증명을 커널에 제출하며, 거부될 경우 실패한 단계, 에러 메시지, 미결 목표 등의 정밀한 피드백을 에이전트에게 전달하여 수정을 유도합니다.

하네스 훅 언어 (HHL)

주요 기여 중 하나는 검증 하네스를 정의하는 데 사용되는 선언적 언어인 HHL입니다. HHL을 통해 엔지니어는 에이전트의 동작(예: Write, Edit, Bash와 같은 도구 호출) 전후에 실행될 "훅(hook)"을 지정할 수 있습니다.

• Pre-hooks (전처리 훅): 동작 전 제약을 강제합니다 (예: Admitted 차단, 새로운 임포트 금지, 또는 위험한 셸 명령 방지).
• Post-hooks (후처리 훅): 동작 후의 결과를 검증합니다 (예: Coq 커널을 실행하여 증명을 검증하거나, 렘마 커버리지를 확인하거나, 린터를 통해 Iris 코딩 컨벤션 준수 여부를 확인).
• 재시도 루프 (Retry Loop): 시스템은 피드백 기반 루프로 실행됩니다. 하네스가 증명을 거부하면 에러가 에이전트로 피드백되어 증명을 수정하게 합니다. 이 과정은 렘마당 최대 30회까지 반복됩니다.

주요 운영 속성

• 건전성 (Soundness): Coq 커널에 의해 수락된 증명만이 성공한 것으로 간주됩니다. 커널은 무결한 오라클 역할을 하며, 잘못된 출력은 통과할 수 없습니다.
• 완전성 (Completeness): 하네스는 대상 렘마가 실제로 증명되었는지, 아니면 조용히 누락되거나 약화되었는지(예: Admitted를 통한) 확인합니다.
• 종료 (Termination): 타임아웃 체크를 통해 발산하거나 종료되지 않는 택틱이 시스템을 멈추게 하는 것을 방지합니다.
• 자율성 (Autonomy): 시스템은 무인으로 실행됩니다. 인간 전문가는 택틱을 작성하거나, 목표를 조사하거나, 실행을 재시작하기 위해 개입하지 않습니다.

실험 결과

저자들은 네 가지 서로 다른 벤치마크에서 Aria를 평가하였으며, 모든 설정에서 실패 제로 및 전문가 개입 제로로 100% 커버리지를 달성했습니다.

1. Iris Core (Coq): 주요 벤치마크로, 고차 동시성 분리 논리(higher-order concurrent separation logic)의 최첨단 상태를 나타내는 네 가지 핵심 모듈(algebra, bi, base_logic, program_logic)에 걸친 4,257개의 렘마로 구성됩니다.
   • 결과: 4,257개 렘마 모두 증명 완료.
   • 효율성: 첫 번째 시도에서 79.2% 해결; 렘마당 평균 재시도 횟수는 0.51회. 총 모델 시간은 약 380시간 소요.
2. RustBelt (Coq): Rust 표준 라이브러리(동시성 및 내부 가변성 타입인 Arc, Mutex, RwLock)에 대한 안전성 증명을 검증합니다.
   • 결과: 217개 렘마 모두 증명 완료.
   • 의의: 이 접근 방식이 단순히 논리 자체뿐만 아니라 그 위에 구축된 소프트웨어에서도 작동함을 입증합니다.
3. reglang (Coq): 정규 언어 이론 라이브러리로, 이전의 LLM 증명기들이 가장 낮은 성능을 보였던 벤치마크입니다 (Rango는 약 12.5%만을 증명함).
   • 결과: 318개 렘마 모두 증명 완료.
   • 비교: 이전 시스템들은 8개 중 1개 정도 겨우 처리했으나, Aria는 모두 증명했습니다.
4. iris-lean (Lean 4): Iris를 Lean 4 증명기로 포팅한 버전으로, 아직 포팅되거나 증명되지 않은 렘마들을 대상으로 합니다.
   • 결과: 72개 렘마 모두 증명 완료.
   • 의의: 이 접근 방식이 Coq에 국한되지 않으며 Lean 커널에서도 작동함을 보여줍니다.

모델 비교

논문은 프라이빗 모델인 Claude Opus 4.7을 오픈 소스 모델(Kimi K2.6, DeepSeek V4 Pro)과 비교했습니다. 오픈 소스 모델은 더 단순한 렘마를 증명할 수는 있었으나, 길고 복잡한 증명(예: 50줄 초과)에서는 어려움을 겪으며 재시도 예산을 소진하는 경우가 많았습니다. 반면 프라이빗 모델은 200줄이 넘는 증명도 안정적으로 구성했습니다.

주요 기여

1. 하네스 + 코드 에이전트 패러다임: 고정된 증명 전략을 가진 시스템보다, 검증 하네스와 결합하여 스스로 전략을 선택할 수 있는 자유를 가진 범용 코드 에이전트가 더 우수함을 입증했습니다. 이는 이전에 도달하지 못했던 가장 어려운 분리 논리 증명에 대해 완전한 커버리지를 달달성했습니다.
2. Iris 및 RustBelt 검증: LLM이 전문가 수준의 최첨단 소프트웨어 검증 라이브러리(Iris)와 그 다운스트림 애플리케이션(RustBelt)을 완전히 자동적으로 증명할 수 있음을 보여준 첫 번째 실증적 증거입니다.
3. HHL (Harness Hook Language): LLM 에이전트 주변에 재사용 가능하고 감사 가능한 검증 정책을 정의하기 위한 선언적 언어로, 에이전트의 추론과 정당성 보증을 분리합니다.

의의 및 주장

본 논문은 고정된 증명 전략이라는 "스캐폴딩"이 불필요하다고 결론짓습니다. 유능한 에이전트에게 전체 렘마를 넘겨주고 하네스를 통해 건전성, 완전성 및 종료를 강제함으로써, 시스템은 복잡한 증명 탐색 공간을 자율적으로 탐색할 수 있습니다.

저자들은 이 접근 방식이 Iris뿐만 아니라 그 위에 구축된 전체 소프트웨어의 수동 증명 병목 현상을 제거할 수 있다고 주장합니다. 결과는 현재의 최첨단 모델들이, 제약된 인간 설계 전략이 아닌 엄격한 검증 루프에 의해 가이드된다면, 최첨단 검증 소프트웨어 개발을 위한 증명을 완전히 자동적으로 수행할 수 있음을 시사합니다. 본 논문은 명세 생성(specification generation) 문제를 다루는 것이 아니라, 엄격하게 증명 합성(proof synthesis) 단계에 집중합니다.