Intent-aligned Formal Specification Synthesis via Traceable Refinement

Motivation

• Known: LLM을 이용한 자연어 기반 코드 생성이 확산되고 있으나 정확성 보장이 어려우며, formal verification은 프로그램이 formal specification(precondition/postcondition)을 만족함을 증명하여 이를 해결할 수 있다. 최근 연구들은 LLM이 specification이나 proof 생성을 보조할 수 있음을 보였다.
• Gap: 기존 intent-anchored 방식들은 생성된 specification이 의도된 모든 요구사항을 포착했는지 판단할 방법이 없고, type error나 proof failure 같은 거친(coarse) 신호에 의존하여 실패를 특정 요구사항으로 국소화(localize)하지 못한다. 반면 program-behavior-based 방법은 구현체를 신뢰 가능한 ground truth로 가정하므로 LLM이 생성한 버그 있는 코드에는 부적합하다.
• Why: Formal verification의 보증 강도는 근본적으로 specification 품질에 의해 제한되는데, 실세계 코드베이스에는 specification이 거의 없고 이를 작성하는 것은 전문성과 비용이 많이 들기 때문에, 고품질 specification을 자동으로 자연어 의도에 맞게 합성하는 것은 검증 가능한 코드 생성의 핵심 병목을 해결하는 데 중요하다.
• Approach: 자연어 문제 설명을 atomic requirement로 분해하고 요구사항별 targeted test(positive, negative-output, negative-input)와 traceability map을 생성한 뒤, Lean 명세를 검증-실패 귀속-국소 수정하는 반복적 refinement 루프를 통해 intent-aligned specification을 합성한다.

Achievement

Figure 2. Temperature vs. Spec Pass@1 for different SFT configurations. Lower temperatures consistently yield better per

1. VERINA SpecGen 벤치마크 SOTA 달성: Claude Opus 4.5로 86.6%를 달성하여 여러 모델 패밀리와 규모에서 baseline 대비 최대 31.8점 개선을 보였다.
2. 대규모 trajectory distillation 데이터셋 구축: VeriSpecGen의 refinement trajectory로부터 343K개의 고품질 instruction-response 학습 예제를 생성했다.
3. 훈련을 통한 큰 폭의 성능 향상 및 전이: Qwen3-4B-Instruct-2507과 Qwen3-Coder-30B-A3B를 해당 데이터셋으로 fine-tuning하여 VERINA SpecGen 점수를 62-106% 상대적으로, VERINA CodeGen 점수를 54-72% 상대적으로 향상시켰으며, out-of-domain 수학 추론과 일반 코딩 벤치마크로도 이득이 전이됨을 보였다.
4. 컴포넌트 필요성 검증: ablation을 통해 프레임워크의 모든 구성요소가 유효한 refinement에 필수적이며, 특히 requirement decomposition이 가장 핵심적인 요소임을 입증했다.

How

Figure 1. VERISPECGEN traceable refinement workflow. Given a natural language problem description (e.g., “Find the most

• Atomic Requirement Decomposition (3.1): LLM decomposer가 자연어 문제 설명을 테스트 가능한 atomic requirement(AR)들로 분해.
• Requirement-targeted Test Generation (3.2): 각 AR에 대해 positive test, negative-output test, negative-input test를 생성하고, 참조 구현을 black-box oracle로 사용해 출력 레이블을 부여하며(코드 구조를 들여다보지 않음), 각 test와 이를 검증하는 AR를 연결하는 traceability map π를 구축.
• Specification Synthesis & Traceable Refinement (3.2 & 3.3): LLM이 AR들로부터 초기 Lean specification을 생성하고, Lean prover로 모든 test를 proposition으로 인스턴스화해 proof automation으로 검증. 검증 실패 시 traceability map을 통해 실패를 특정 AR에 귀속시켜, 전체 specification을 재작성하지 않고 영향받은 조항(clause)만 국소적으로 수정. 모든 test가 통과하고 adversarial testing에서 누락된 제약이 발견되지 않을 때까지 반복.
• Trajectory Distillation: Claude Sonnet 4.5로 TACO-verified 데이터셋에 대해 VeriSpecGen을 실행하여 requirement decomposition, traceability map, intermediate specification, localized repair를 포함한 구조화된 trajectory 343,827개를 supervised fine-tuning 데이터로 증류.

Originality

• 기존 intent-anchored specification synthesis 방법들이 coarse한 refinement 신호(type error, proof failure)에 의존하는 것과 달리, 자연어 요구사항을 atomic 단위로 분해하고 test-requirement traceability map을 통해 검증 실패를 특정 요구사항 수준으로 귀속시키는 최초의 접근법을 제시.
• clause-level의 국소적(localized) repair를 가능하게 하여 specification 전체 재작성 없이 targeted 수정을 수행하는 방식의 참신성.
• refinement trajectory 자체를 대규모 학습 데이터로 증류하여 inference-time 개선을 training-time 개선으로 전환하고, 이것이 spec synthesis뿐 아니라 코드 생성 및 일반 추론 능력으로도 전이됨을 보인 점.

Limitation & Further Study

• Lean이라는 특정 formal language와 proof automation에 의존하므로 다른 정형 언어나 검증 도구로의 일반화 가능성에 대한 추가 검증이 필요.
• 참조 구현(reference implementation)을 test oracle로 사용하는데, 이러한 구현이 항상 신뢰할 수 있는지, 혹은 참조 구현 자체의 결함이 있을 때의 영향에 대한 논의가 제한적일 수 있음.
• atomic requirement decomposition의 품질이 전체 파이프라인 성능에 결정적인데(ablation에서 가장 critical), 이 분해 단계 자체의 실패 모드나 자연어의 모호성이 매우 클 경우의 강건성에 대한 심층 분석이 더 필요.
• 343K 규모 데이터셋이 특정 모델(Claude Sonnet 4.5)의 trajectory로 생성되었기 때문에 이 모델의 편향이나 한계가 distillation된 데이터에 반영될 가능성.

Evaluation

총평: 자연어 요구사항 수준의 traceability를 통해 formal specification의 국소적 반복 수정을 가능케 한 실용적이고 참신한 프레임워크로, 강력한 실증 결과와 함께 훈련 데이터 증류를 통한 확장성까지 보여준 완성도 높은 연구이다.