Vibe coding은 사용자가 대규모 언어 모델(LLMs)과의 자연어(NL) 상호작용을 통해 코드를 생성할 수 있게 함으로써 소프트웨어 개발을 민주화합니다. 그러나 생성된 코드는 사용자의 의도를 충실히 구현할 때만 신뢰할 수 있으며, 사용자가 이를 검증하는 과정은 어렵고 노동 집약적입니다. 기존의 검증 방법들은 프롬프트의 모호성과 모델의 오류 가능성으로 인해 어려움을 겪는 LLM 보조 자동 테스트에 의존하거나, 프롬프트 및 테스트 케이스와 같은 부분적인 소프트웨어 산출물에만 사용자를 참여시켜 코너 케이스(corner cases)와 프로그램 세부 사항을 간과할 수 있습니다. LLM 생성 코드에 대한 버그 연구에 착안하여, 우리는 실패의 원인이 종종 불충분하게 명시된 요구사항이나 미묘한 의미론적 편차에서 비롯되기 때문에 상세한 인간의 피드백이 필수적이라는 것을 발견했습니다. 본 논문은 모든 프로그래밍 수준의 사용자가 LLM 생성 코드의 검토/검증 프로세스에 쉽게 접근할 수 있도록 설계된 Human-in-the-loop 프레임워크인 검증 가능한 리터러트 프로그래밍(Verifiable Literate Programming, VLP)을 제시합니다. VLP의 핵심은 프롬프트와 코드 사이의 읽기 가능한 중간 계층으로서 모호하지 않은 NL 기반 문서를 제안하는 것입니다. 이 문서는 구체적인 프로그램 의미론(semantics)을 보여주며, 사용자가 잠재적인 의도-코드 불일치에 대해 피드백을 제공할 수 있게 합니다. VLP는 다음 세 가지 기술을 통해 인간이 참여하는 엔드 투 엔드(end-to-end) 수정 및 검증을 지원합니다: (i) 모호하지 않은 구문과 대부분 결정론적인 코드-문서 번역을 갖춘 NL 스타일의 리터러트 언어(literate language), (ii) 프롬프트와 문서 사이의 추적 링크(trace links)를 사용하여 사용자의 검토 노력을 의심스러운 문서 라인에 집중시키는 LLM 기반의 미세한 불일치 탐지, (iii) 사용자가 검증한 문서를 활용하여 API 사용 체크 및 형식적 속성(formal properties)을 도출하고, 이를 모델 체킹(model checking)을 통해 생성된 코드와 대조하여 검증하는 검증 모듈. 우리의 평가 결과에 따르면, VLP는 합리적인 사용자 노력으로 코드 pass@1 성능을 28.7%-73.2%에서 65.4%-93.5%로 향상시킵니다.