기술 요약: AxDafny – Dafny에서의 에이전트 기반 검증 코드 생성

문제 정의

본 논문은 **에이전트 기반 코드 생성(agentic code generation)**의 맥야에서 형식 검증(formal verification)의 과제를 다룹니다. 테스트 케이스를 통해 실행 가능한 코드를 평가하는 일반적인 코드 생성 작업과 달리, 검증된 코드 생성은 모델이 실행 가능한 구현체뿐만 아니라, 형식 검증기가 정당성을 증명하는 데 필요한 증명 아티팩트(예: 루프 불변량, 단언문, 종료 인자 등)를 함께 생성해야 합니다.

저자들은 형식 방법론의 기존 AI 응용 분야에서 발생하는 격차를 식려냈습니다. 검증은 풍부한 피드백 신호(명세 위반, 누락된 주석, 처리되지 않은 엣지 케이스 식별)를 제공하지만, 높은 전문 지식이 요구되기 때문에 주류 AI 작업에서는 이를 활용하는 경우가 드뭅니다. 구체적인 문제는, Dafny(내장된 형식 검증 지원을 갖춘 언어) 내에서 프로그램 로직과 증명 구조를 반복적으로 개선하기 위해 검증기 피드백을 활용하는 프레임워크를 개발하는 것입니다.

방법론: AxDafny 프레임워크

저자들은 프로그램과 증명의 공동 합성을 위해 설계된 검증기 유도 수선(verifier-guided repair) 프레임워크인 AxDafny를 제안합니다. 이 시스템은 Lean 증명에 사용되었던 에이전트 아키텍처를 변형하여 반복적인 생성-확인-수선(generate–check–repair) 루프로 작동합니다.

1. 에이전트 아키텍처

프레임워크는 세 가지 핵심 구성 요소로 이루어집니다:

• 제안 에이전트 (Proposer Agent): 문제 설명, 원래의 명세, 그리고 이력을 바탕으로 완전한 Dafny 파일을 생성합니다. 결정적으로, 이 에이전트는 문제를 정의하는 requires(전제 조건) 또는 ensures(사후 조건) 절을 수정하지 않도록 제약되며, 대신 구현과 증명 주석에 집중합니다.
• 검토 시스템 (Reviewer System): 2단계 검증 메커니즘입니다:
  • 결정론적 검사 (Deterministic Checks): 원래의 명세가 보존되었는지 확인하고(약화 방지), "증명 우회" 구조(예: {:verify false}, assume, {:extern})를 거부하며, Dafny 검증기(dafny verify)를 실행합니다. 이를 통해 실패한 증명 의무(전제 조건, 사후 조건, 불변량, 종료)에 관한 구체적인 진단 메시지를 추출합니다.
  • LLM 기반 검토 (LLM-based Review): 정적 검사로 포착되지 않는 미묘한 속임수 패턴(예: 술어를 사소하게 참이 되도록 재작성하는 행위)을 탐지합니다.
• 메모리 모듈 (Memory Module): 이전 반복에서 얻은 교훈을 응축하는 "성찰 메모리(reflection memory)"를 유지합니다. 제안 에이전트는 마지막 시도의 즉각적인 이력(코드, 추론, 피드백)과 이후의 개선을 가이드하기 위한 누적된 통찰의 롤링 요약을 모두 전달받습니다.

2. 벤치마크

프레임워크를 평가하기 위해 저자들은 **LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny)**를 도입했습니다:

• 구성: LiveCodeBench-Pro에서 Dafny로 변환된 250개의 경진 대회 스타일 프로그래밍 문제로 구성되며, 난이도별(쉬움 100, 중간 100, 어려움 50)로 계층화되어 있습니다.
• 구축: 각 인스턴스는 자연어 문제, Dafny 메서드 시그니처, 그리고 형식 명세를 포함합니다. 구축 과정에는 LLM-as-judge 검토와 수동 검증을 포함한 엄격한 큐레이션이 포함되어, 원래 문제와의 의미론적 일치를 보장했습니다.
• 평가 프로토콜: 솔루션은 원래의 명세를 수정하거나 공허한 증명에 의존하지 않고 Dafny에서 검증되는 경우에만 수락됩니다. 보조 지표로는 검증된 솔루션을 Python으로 컴파일하여 원래의 런타임 테스트 하네스에 대해 테스트합니다.

저자들은 또한 구현은 고정되어 있고 에이전트가 누락된 불변량과 단언문을 복구해야 하는 **증명 힌트 합성(proof-hint synthesis)**을 위한 기성 벤치마크인 DafnyBench에서도 평가를 수행합니다.

주요 기여

1. AxDafny 프레임워크: 반복적인 검증기 유도 수선을 통해 실행 가능한 코드와 필요한 증명 주석을 성공적으로 합성하는 에이전트 시스템입니다.
2. LCB-Pro-Dafny 벤치마크: 경쟁적인 환경에서 엔드 투 엔드 검증된 프로그램 합성을 평가하기 위한 새로운 대규모 벤치마크(250개 인스턴스)로, 형식 검증 분야의 런타임 제약이 있는 엄격한 벤치마크 부족 문제를 해결합니다.
3. 실증적 검증: 검증기 유도 수선이 직접 생성 베이스라인보다 증명 합성 및 전체 프로그램 합성 작업 모두에서 성능이 월등히 높음을 입증했습니다.

결과

논문은 두 가지 별개의 작업에 대한 성능을 보고합니다:

1. 증명 합성 (DafnyBench)

• 성능: Gemini-3.1-Pro를 사용한 AxDafny는 92.7% (725/782)의 인스턴스를 검증했습니다.
• 비교: 이는 가장 강력했던 이전 보고 베이스라인인 DafnyPro (86.2%)를 6.5 퍼센트 포인트 상회하는 수치입니다. 주목할 점은, AxDafny가 DafnyPro의 성공 핵심 요소였던 수동 큐레이션 증명 힌트 라이브러리에 의존하지 않고도 이 성과를 달성했다는 것입니다.
• 반복 역학: 이득은 초기 5번의 반복에 집중되어 있으며, 시스템은 빠르게 포화 성능에 도달합니다.

2. 프로그램 합성 (LCB-Pro-Dafny)

• 성능: AxDafny는 전체 작업의 **56.4%**를 검증했습니다.
  • 쉬움: 75.0%
  • 중간: 52.0%
  • 어려움: 28.0%
• 비교: 이는 단 한 번의 통과(pass@1) 성공률이 **11.6%**에 불과했던 직접적인 GPT-5.5 베이스라인보다 상당한 개선을 나타냅니다.
• 실행 가능성: 검증된 솔루션을 Python으로 컴파일하여 원래의 테스트 하네스에 실행했을 때, 많은 경우 기능적 부정확성이 아닌 시간 초과(TLE) 또는 **메모리 초과(MLE)**로 인해 실패했습니다. 이는 에이전트가 기능적으로 올바른 코드(검증기에 의해 증명됨)를 성공적으로 생성했음에도 불구하고, 경쟁 프로그래밍에 내재된 점근적 복잡도 제약을 충족하는 데는 종종 실패했음을 나타냅니다. 이는 Dafny 명세가 일반적으로 기능적 정확성은 강제하지만 성능 경계는 강제하지 않기 때문입니다.

의의 및 주장

본 논문은 검증기 유도 수선이 특히 구현과 함께 증명 주석을 합성해야 하는 복잡한 작업에서 검증된 코드를 생성하는 데 매우 효과적인 전략임을 주장합니다.

• 구별된 목표: 저자들은 검증 성공(검증기에 의해 증명된 기능적 정확성)과 런타임 성능(경쟁 프로그래밍 제약 충족) 사이의 결정적인 차이를 강조합니다. 결과는 에이전트가 프로그램이 올바르다는 것을 증명할 수는 있지만, 효율적인 구현을 생성하는 데는 실패할 수 있음을 보여줍니다.
• 확장성: 프레임워크는 추론 스케일링(반복적 개선)이 형식 검증 작업의 성능을 크게 높여, 단일 패스 생성의 한계를 넘어설 수 있음을 보여줍니다.
• 데이터 희소성: 논문은 Dafny 훈련 데이터의 상대적 희소성(Python보다 몇 자릿수 적음)이 여전히 과제임을 언급하지만, 에이전트 방식은 사전 학습 데이터에만 의존하는 대신 검증기 피드백을 활용함으로써 이 간극을 성공적으로 메웁니다.

이 연구는 LCB-Pro-Dafny를 논리와 증명을 모두 합성해야 하는 작업, 즉 에이전트 기반 코딩 연구를 위한 도전적인 테스트베드로 자리매김하게 합니다.