🤖 AI

VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications

이 논문은 단순한 검증 통과를 넘어 정확하고 완전한 형식 명세를 생성하기 위해 검증 피드백을 기반으로 한 반복적 계획, 실행, 수정 사이클을 수행하는 에이전트 프레임워크인 'VeriAct'를 제안하고 그 우수성을 입증합니다.

원저자: Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes

게시일 2026-04-02

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Md Rakib Hossain Misu, Iris Ma, Cristina V. Lopes

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

이 논문은 **"소프트웨어가 정말로 올바르게 작동하는지 확인하는 '약속 문서'를 자동으로 만드는 기술"**에 대한 연구입니다.

소프트웨어 개발자들은 프로그램이 어떻게 작동해야 하는지 정해진 규칙 (명세, Specification) 을 적어두면, 컴퓨터가 그 규칙을 지키는지 자동으로 검사합니다. 하지만 이 규칙을 직접 쓰는 건 매우 어렵고, 최근에는 AI(대형 언어 모델) 가 대신 써주려고 합니다.

이 논문은 **"AI 가 쓴 규칙이 컴퓨터 검사에 통과했다고 해서, 진짜로 완벽하고 안전한 규칙일까?"**라는 의문에서 시작합니다.

주요 내용을 쉬운 비유로 설명해 드릴게요.

1. 문제: "시험에 합격했다" ≠ "진짜 공부를 했다"

상황: AI 가 소프트웨어의 규칙 (JML 이라는 언어로 작성) 을 써냈습니다.
기존의 방식: 컴퓨터 검사기 (Verifier) 가 "오류가 없네? 합격!"이라고 하면, 우리는 "AI 가 잘 썼구나"라고 생각했습니다.
실제 문제: 이 검사기는 **"규칙이 틀렸는지"**만 봅니다. 하지만 **"규칙이 너무 쉬워서 아무것도 안 걸러내는지"**는 모릅니다.
- 비유: 수학 시험에서 "정답은 100 점이다"라고만 적어두면, 어떤 답을 써도 "틀리지 않았으니 합격"이 됩니다. 하지만 이건 진짜 문제를 푼 게 아니죠.
- 논문이 발견한 사실: AI 가 쓴 규칙 중 상당수가 컴퓨터 검사에는 통과했지만, 실제로는 너무 단순하거나 잘못되어서 프로그램의 진짜 동작을 제대로 설명하지 못했습니다.

2. 새로운 도구: '스펙 하네스 (Spec-Harness)'라는 정밀 검사기

연구팀은 기존의 '합격/불합격'만 보는 검사를 넘어, 규칙의 진짜 품질을 측정하는 새로운 도구를 만들었습니다.

비유: 기존 검사가 "문법 오류가 있나?"만 본다면, 스펙 하네스는 "이 규칙이 진짜로 나쁜 입력을 막아내는가? (완전성)"와 "올바른 입력을 잘못 막아내지는 않는가? (정확성)"를 꼼꼼히 따져봅니다.
결과: 이 정밀 검사를 해보니, 기존에 '합격' 판정을 받았던 규칙들 중 상당수가 실제로는 쓸모없거나 위험한 것들이었습니다. 마치 "시험지에는 이름만 적어놓고 빈칸을 남긴 채 합격한 학생"처럼 말이죠.

3. 해결책: '베리액트 (VeriAct)'라는 똑똑한 AI 비서

이제 연구팀은 AI 가 규칙을 더 잘 쓰게 돕기 위해 VeriAct라는 새로운 시스템을 제안했습니다.

기존 방식: AI 에게 "이거 써줘"라고 한 번만 시키고 결과를 받았습니다. (일회성 주문)
VeriAct 방식: AI 가 규칙을 쓰고, 스펙 하네스로 검사를 받습니다.
- "여기 너무 약한 부분이 있어" → AI 가 수정
- "여기 너무 강한 부분이 있어" → AI 가 다시 수정
- 이 과정을 **반복 (Closed-loop)**해서, 컴퓨터 검사도 통과하고, 정밀 검사도 통과하는 완벽한 규칙을 만들어냅니다.
비유:
- 기존: 요리사에게 "맛있는 요리 해줘"라고 하고 한 번에 내보냄.
- VeriAct: 요리사가 요리를 만들고, 미식가 (스펙 하네스) 가 "소금 좀 더 넣어", "불 조절 좀 해"라고 피드백을 줍니다. 요리사는 그 말을 듣고 다시 맛을 보고, 미식가가 만족할 때까지 수십 번을 다듬어 최종 요리를 냅니다.

4. 결론: "합격"보다 "완벽"이 중요합니다

이 연구는 다음과 같은 중요한 교훈을 줍니다.

컴퓨터가 "OK"라고 해도 안심하지 마세요: AI 가 만든 규칙이 기계 검사에 통과했다고 해서, 그 규칙이 진짜로 안전하고 완전한 건 아닙니다.
피드백이 핵심: AI 가 한 번에 완벽할 수는 없습니다. 하지만 "왜 틀렸는지"에 대한 구체적인 피드백을 주고받으며 반복하면, AI 는 훨씬 더 똑똑하고 정확한 규칙을 만들 수 있습니다.
새로운 기준: 앞으로는 단순히 "검사에 통과했는가"가 아니라, "정말 필요한 모든 상황을 다 커버했는가"를 평가하는 것이 더 중요합니다.

한 줄 요약:

"AI 가 쓴 소프트웨어 규칙이 '시험에 합격'했다고 해서 안심하지 말고, **'진짜로 완벽하게 작동하는지' 반복적으로 다듬어주는 새로운 시스템 (VeriAct)**을 개발했습니다."

VeriAct: 검증 가능성 너머 - 정확하고 완전한 형식 명세 생성을 위한 에이전트 합성

이 논문은 자동화된 형식 명세 (Formal Specification) 생성 분야에서 검증 가능성 (Verifiability) 이 실제 명세의 품질 (정확성과 완전성) 을 보장하지 않는다는 근본적인 문제를 제기하고, 이를 해결하기 위한 새로운 평가 프레임워크와 에이전트 기반 합성 프레임워크를 제안합니다.

1. 문제 정의 (Problem)

소프트웨어의 신뢰성을 보장하기 위해 자바 모델링 언어 (JML) 와 같은 형식 명세가 필수적입니다. 최근 대규모 언어 모델 (LLM) 을 활용하여 JML 명세를 자동 생성하는 연구가 활발하지만, 다음과 같은 심각한 한계가 존재합니다.

검증 통과 ≠ 올바른 명세: 기존 연구들은 생성된 명세가 검증기 (Verifier, 예: OpenJML) 를 통과하는지 여부로 품질을 평가합니다. 그러나 검증기를 통과하는 것은 코드가 명세와 모순되지 않음을 의미할 뿐, 명세 자체가 정확하거나 (Correct) 완전한 (Complete) 것을 보장하지 않습니다.
허술한 명세의 위험: ensures true 와 같은 자명한 (trivial) 후조건은 어떤 입력에서도 검증기를 통과하지만, 실제 프로그램의 동작을 전혀 설명하지 못합니다.
수동 평가의 비효율성: 명세의 질적 차이를 구분하는 작업은 여전히 인간 전문가의 수동 평가에 의존하여 확장성이 떨어집니다.

2. 방법론 (Methodology)

저자들은 4 가지 주요 연구 질문 (RQ) 을 중심으로 체계적인 분석을 수행했습니다.

2.1 기존 접근법 비교 및 프롬프트 최적화 (RQ1 & RQ2)

비교 평가: 고전적 도구 (Daikon, Houdini) 와 프롬프트 기반 LLM 접근법 (SpecGen, AutoSpec, FormalBench) 을 SpecGenBench 와 FormalBench 데이터셋에서 비교했습니다.
프롬프트 최적화: 검증 피드백을 구조화하여 GEPA (Genetic-Pareto) 알고리즘을 활용한 프롬프트 최적화를 수행했습니다. 이는 검증 실패 원인을 분석하여 프롬프트를 진화시키는 방식입니다.

2.2 새로운 평가 프레임워크: Spec-Harness (RQ3)

검증 통과율 (Verification Rate, VR) 의 한계를 극복하기 위해 Spec-Harness라는 새로운 평가 프레임워크를 제안했습니다. 이는 Hoare Triple 기반의 심볼릭 검증과 입력/출력 변이 (Mutation) 테스트를 결합하여 다음 4 가지 지표를 측정합니다.

Post-Correctness: 알려진 올바른 실행에 대해 거짓 경보 (False Alarm) 를 발생시키지 않는가?
Post-Completeness: 잘못된 출력 (변이된 값) 을 올바르게 거부하는가? (허술한 명세는 이를 거부하지 못함)
Pre-Correctness: 유효한 입력을 불필요하게 거부하지 않는가?
Pre-Completeness: 무효한 입력 (경계값 등) 을 올바르게 차단하는가?

2.3 제안 시스템: VeriAct (RQ4)

검증 피드백과 Spec-Harness 피드백을 폐루프 (Closed-loop) 로 통합한 VeriAct라는 에이전트 프레임워크를 개발했습니다.

작동 방식: LLM 에이전트가 초기 명세를 생성 $\rightarrow$ OpenJML 로 검증 $\rightarrow$ 오류 분석 및 수정 $\rightarrow$ Spec-Harness 로 품질 평가 $\rightarrow$ 기준 미달 시 반복 수정.
핵심: 단순한 검증 통과가 아닌, 명세의 정확성과 완전성을 직접 피드백으로 활용하여 명세를 점진적으로 정제합니다.

3. 주요 결과 (Results)

3.1 검증 통과율의 오해 (RQ1 & RQ2)

고전적 도구: Houdini 는 높은 검증 통과율 (SpecGenBench 기준 86.7%) 을 보였으나, 이는 단순한 템플릿 기반의 허술한 명세 때문이었습니다.
프롬프트 기반 접근: LLM 기반 접근법도 검증 통과율은 높았으나, 프롬프트 최적화 (GEPA) 를 거치더라도 성능의 한계 (Ceiling) 에 도달했습니다.
결론: 검증 통과율만으로는 명세의 실제 품질을 판단할 수 없습니다.

3.2 Spec-Harness 의 발견 (RQ3)

MVR (Meaningfully Verified Rate) 의 붕괴: 검증 통과율 (VR) 이 높았던 대부분의 명세가 Spec-Harness 평가에서는 정확성이나 완전성 기준을 충족하지 못해 MVR 이 급격히 떨어졌습니다.
- 예: Houdini 는 VR 86% 에서 MVR 2% 로 붕괴했습니다.
- LLM 기반 접근법도 VR 대비 MVR 이 크게 낮았으며, 특히 FormalBench(복잡한 제어 흐름) 에서는 MVR 이 거의 0% 에 가까웠습니다.
이는 기존 연구들이 "검증 통과"를 품질 지표로 잘못 사용했음을 시사합니다.

3.3 VeriAct 의 성과 (RQ4)

성능 향상: VeriAct 는 프롬프트 기반 및 최적화된 베이스라인을 모두 능가했습니다.
- SpecGenBench 에서 MVR 을 +5% 향상.
- FormalBench 에서 MVR 을 +12% 향상.
메커니즘: VeriAct 는 검증기를 통과하더라도 Spec-Harness 에서 '완전성 부족'이 발견되면 이를 피드백으로 받아 명세를 강화 (Tightening) 하는 과정을 반복하여, 검증 가능하면서도 정확하고 완전한 명세를 생성했습니다.

4. 주요 기여 (Key Contributions)

포괄적 평가: 고전적 도구와 LLM 기반 접근법을 통합적으로 평가하여, 높은 검증 통과율이 실제 명세 품질을 반영하지 못함을 실증했습니다.
프롬프트 최적화의 한계 규명: 구조화된 피드백을 통한 프롬프트 최적화가 검증 통과율을 높일 수는 있으나, 명세의 정확성과 완전성 문제를 해결하는 데에는 한계가 있음을 보였습니다.
Spec-Harness 제안: 검증 통과/실패를 넘어, Hoare Triple 논리와 변이 테스트를 기반으로 명세의 **정확성 (Correctness) 과 완전성 (Completeness)**을 정량적으로 측정하는 자동화된 평가 프레임워크를 개발했습니다.
VeriAct 개발: 검증 피드백과 Spec-Harness 피드백을 폐루프로 결합한 에이전트 프레임워크를 통해, 검증 가능하고 정확하며 완전한 형식 명세를 자동 생성하는 새로운 패러다임을 제시했습니다.

5. 의의 및 결론 (Significance)

이 연구는 형식 명세 생성 분야에서 **"검증 통과 (Verifiability)"**와 "실제 품질 (Quality)" 사이의 간극을 명확히 드러냈습니다. 단순히 검증기를 통과하는 명세를 생성하는 것을 넘어, 명세가 프로그램의 의도된 동작을 얼마나 정확하게 포착하고 있는지를 평가하고 개선하는 것이 필수적임을 강조합니다.

VeriAct와 Spec-Harness는 LLM 이 생성한 명세를 단순히 '통과/실패'로 판단하는 것을 넘어, 에이전트가 스스로 명세의 결함을 발견하고 수정할 수 있는 구조를 제공합니다. 이는 소프트웨어 신뢰성 공학 분야에서 자동화된 형식 명세 생성의 실용성을 크게 높일 수 있는 중요한 진전으로 평가됩니다.