January 01, 1970
Vibe coding democratizes software development by allowing users to generate code via natural-language (NL) interaction with large language models (LLMs). However, the code is reliable only when it faithfully implements the user’s intent, which is difficult and labor-intensive for users to validate, especially for non-programmers. Existing validation methods either rely on LLM-assisted automated testing, which suffers from prompt ambiguity and model fallibility, or involve users only in partial software artifacts such as prompts and test cases, which may overlook corner cases and program details. Motivated by a bug study of LLM-generated code, we find that detailed human feedback is essential, as the failures often stem from underspecified requirements or subtle semantic deviations, and thus cannot be resolved through automated or coarse-grained checking alone.
This paper presents verifiable literate programming (VLP), a human-in-the-loop framework designed to make the review/validation process of LLM-generated code accessible to users at all programming levels. At its core, VLP proposes unambiguous NL-based documentation as a readable intermediate layer between prompts and code. The documentation demonstrates concrete program semantics and enables users to provide feedback on potential intent-code mismatches. It supports human-involved, end-to-end repair and validation via three techniques: (i) an NL-style literate language with unambiguous syntax and mostly deterministic code-to-documentation translation, (ii) LLM-based fine-grained mismatch detection that uses trace links between prompts and documentation to focus users’ review effort on suspicious documentation lines, and (iii) a verification module that leverages user-validated documentation to derive API-usage checks and formal properties, which are then verified against the generated code using model checking. Our evaluation shows that VLP improves code pass@1 from 28.7%–73.2% to 65.4%–93.5% with reasonable user effort.
Vibe coding democratizes software development by shifting much of programming from manual code writing to natural-language (NL) interaction with large language models (LLMs). As a result, recent reports estimate that 63% of vibe-coding users are non-programmers [1], [2]. However, LLM-generated code is useful and trustworthy only when it faithfully implements the user’s intended behavior. Ensuring intent-code alignment is difficult because LLMs can hallucinate during generation, while users, especially non-programmers, often face many lines of generated code without knowing whether the program actually behaves as intended. This concern is reflected in recent developer surveys, which report that LLM-generated code remains unreliable [3]–[5] and that 96% of developers do not fully trust the functional correctness of AI-generated code [6]. Therefore, validating LLM-generated code has become an urgent problem for vibe coding.
This need has motivated a large body of work on automated testing and verification for LLM-generated code. One line of work utilizes LLM reasoning to generate tests or formal properties from the original NL prompt, or to directly judge program correctness [7]–[19]. However, these methods suffer from the ambiguity of the original prompt and the fallibility of LLM-generated validation artifacts. Tests may miss important paths, formal properties tend to overlook key requirements, and LLM-based judges can misjudge correctness [20]–[23]. Thus, validation that depends solely on LLM reasoning cannot provide a fully reliable basis for LLM-generated code.
Recognizing these limits, recent work has begun to involve users in specific stages of the vibe coding workflow to align code with user intent. Clarification-based methods ask users to resolve ambiguous prompts before code generation [24]–[29], while test-driven interaction methods use user feedback on generated test cases to partially formalize intent [10], [30]–[32]. These methods can expose ambiguities or concrete program failures, but they involve users only through partial software artifacts. Prompt clarification cannot catch errors introduced during code generation, and test cases cover only sampled behaviors, potentially missing subtle deviations and corner cases [20], [21]. Test-case-based code validation can also be hard for data-science and domain-specific programs, where outputs are often statistical, data-dependent, and difficult to judge from input/output examples alone [33], [34].
Ideally, an effective validation workflow should help users find and repair more intent-code mismatches with minimal effort. To understand what failures in LLM-generated code should be exposed to users and how to effectively interact with users, we conduct a bug study on BigCodeBench-Hard [35] using DeepSeek V4 Flash [36] and Claude Opus 4.7 [37]. We find that most failures stem from underspecified prompts or subtle semantic deviations, necessitating fine-grained user judgment beyond automated checking. In addition, 81.7%–83.3% of the studied failures can be expressed as concrete intent-level behavior in NL. These observations and literate programming [38] together motivate our key idea of verifiable literate programming (VLP). As illustrated in 1 (b), VLP introduces NL-based program description (called documentation) as a faithful and readable intermediate layer between user intent and generated code. The layer is literate because it exposes the concrete semantics of LLM-generated code in a form that users can read without programming-language knowledge. It is verifiable because the documentation is linked to the code through (mostly) bidirectionally deterministic code-to-documentation translation. Once validated by users, it can be translated into formally verifiable properties and deterministic code aligning with user intent.
To realize this idea, VLP targets three connected design goals. First, documentation must be faithful and unambiguous: if the documentation is merely a lossy LLM-generated summary or comment [39], [40], subtle deviations and underspecified behaviors in the generated code may disappear before users can inspect them. Second, validation must be low-effort: even faithful documentation is impractical if users must review it line by line, so VLP should guide users to snippets most likely to require intent validation. Third, validated documentation must lead to reliable code: without translating validated or repaired documentation into reliable code, users would still need to reason about whether the code aligns with the documentation and whether programming-language-specific issues exist, such as API usage and syntax.
VLP realizes these goals through three components. First, it introduces an NL-style literate language (4.2) that uses syntax-directed translation to turn generated code into structured, human-readable descriptions. Meanwhile, it preserves the control flow, data flow, and assertion-based properties. Second, VLP provides misalignment hints through implementation-relevant traceability and taxonomy-based mismatch detection. The trace links are built between implementation-relevant sentences or formulas in the prompts and the documentation. Given these linked sentences and their surrounding context, LLMs can more accurately flag intent-documentation mismatches. Then, VLP highlights suspicious documentation snippets for user feedback (4.3). Third, it derives API checks and formal properties from the validated documentation and verifies them against the generated code with bounded model checking [41]. We encourage users to focus on intent-level decisions and let VLP automatically handle Python-specific details (4.4).
We build a VLP prototype. Our evaluation on QuantCodeEval [34] and BigCodeBench [35] examines whether VLP helps users effectively identify intent-code mismatches in LLM-generated code and improves code correctness. The results show that VLP improves pass@1 from 28.7%–73.2% to 65.4%–93.5%, significantly outperforming the original generated code and three state-of-the-art (SOTA) human-in-the-loop code generation methods: ClarifyGPT [24], TiCoder [32], and PInG [40]. Our user study further shows that VLP achieves higher user experience and provides better tradeoff between user validation time and code correctness. In summary, we make the following contributions.
We conduct a systematic bug study of LLM-generated code on BigCodeBench-Hard. Our study shows that most failures can be reviewed by users as intent-level misalignments through an NL representation of program semantics.
We propose verifiable literate programming, a human-in-the-loop validation framework for LLM-generated code. VLP first translates generated code into faithful, readable, and fine-grained literate documentation; then uses trace-link-guided LLM analysis to find likely intent-documentation mismatches for user validation and repair; and finally uses the validated documentation to derive verifiable properties and API usage checks for verifying the generated code.
We evaluate VLP on two coding benchmarks and show that it helps users validate and repair LLM-generated code more effectively (i.e., higher pass rate) than SOTA human-in-the-loop code generation and validation methods.
Literate programming [38] was introduced with the philosophy that programs should be written for humans to read, not only for machines to execute. Instead of organizing a program solely around compiler requirements, literate programming asks programmers to present the program in an order and form that explain the underlying ideas to human readers. As shown in 1 (a), in the original literate programming system, a programmer interleaves explanatory text with code. The WEAVE processor then produces readable documentation, while the TANGLE processor produces executable code. Although literate programming is not widely adopted today, its core idea has had broad influence. Modern computational notebooks, such as Jupyter notebooks [42], continue this idea by placing explanations, code, and results in the same document.
Although VLP, shown in 1 (b), is inspired by the readable documentation layer of literate programming, the two differ in several aspects. First, VLP’s documentation is derived from the code in a mostly deterministic and unambiguous way, rendering it more faithful to the code semantics than the free-form explanatory prose used in conventional literate programming. More importantly, literate programming uses NL primarily to support human comprehension. In contrast, VLP uses NL as part of a review and validation process. It assesses whether generated code implements user intent and helps identify underspecified requirements in the prompt as well as deviations in the code.
Beyond improving program readability for human review, formal verification tools also play an important role in ensuring code correctness. When part of the intended behavior can be expressed as explicit formal properties, bounded model checking (BMC) [41], [43] can automatically check whether a program satisfies those properties over all feasible executions up to a given bound. If a symbolic execution path reaches a violation state, the checker returns a concrete counterexample, including the input and the execution path that break the property. Otherwise, within the bounded search space explored by the checker, the property holds for all feasible executions.
Compared with unit testing, BMC provides stronger assurance. Unit tests exercise only selected concrete inputs, whereas BMC reasons over symbolic inputs and systematically explores feasible execution paths. Although BMC does not prove correctness beyond the chosen bound, it is often more automatic and lightweight than full deductive verification while providing stronger guarantees than ordinary testing.
At the same time, though formal tools can verify code with respect to a given property, they do not determine whether that property faithfully reflects the user’s intent. In particular, they cannot by themselves identify underspecification in the original prompt or detect cases where the code satisfies the written property while still subtly deviating from user intent.
We conduct a bug study to figure out what failures in LLM-generated code should be exposed to users and how to interact with users. Specifically, Python is chosen as the programming language for our study and system implementation because of its widespread use. We find that failures frequently arise from underspecified requirements or subtle semantic deviations and therefore cannot be resolved by automated or coarse-grained checking alone. Detailed NL documentation and concrete validation questions about short documentation snippets for users can expose these deviations, allowing users to confirm the intended behavior. Our observations motivate VLP’s documentation-based user interface that (i) enables users to validate program semantics in NL and (ii) provides precise guidance for user feedback.
Specifically, we focus on BigCodeBench-Hard Instruct mode [35], which contains complex instructions and diverse library usage. We prompt Claude Opus 4.7 and DeepSeek V4 Flash (temperature=0.2). To investigate the opportunity of NL-based documentation, we further translate each generated program into NL documentation using the approach introduced in 4.2. Across 148 tasks, each with approximately five tests, we collect about 200 bugs from each model [36], [37]. For each bug, two experienced programmers independently inspect the task description, test cases, error message, generated code, and corresponding documentation, and label whether the bug is reviewable in the documentation. Disagreements are resolved through discussion.
Most failures are reviewable at the intent level in NL and not solvable via automated checking. We first examine whether failures in the generated code can be exposed by translating code behavior into NL descriptions (documentation). We consider a bug documentation-reviewable if its incorrect behavior can be recognized from the documentation, without requiring users to inspect Python-specific details such as syntax, package imports, complex data types, or library usage. As shown in 2 (Logic-Related), most studied bugs are documentation-visible: 156 out of 191 bugs for DeepSeek and 169 out of 203 bugs for Opus. This result suggests that documentation can expose a large fraction of failures at the intent level. Moreover, 85.9%–90.5% of documentation-visible bugs are easy for users to judge because the incorrect behavior can be identified from the problematic documentation line and a few surrounding lines, without reading the full documentation.
Failures require fine-grained review of underspecification and subtle semantic deviations. Generated code usually follows the overall prompt, but many reviewable failures come from underspecified or subtle details. Prompt underspecification is the largest source, accounting for 43.6%–46.7% of reviewable bugs. Across these cases, the LLM makes plausible choices according to its assumptions rather than confirmed user intent. For example, an LLM may filter records that the user expects to keep, or silently return a fallback value instead of reporting an error. The remaining reviewable failures often involve missing steps, redundant steps, wrong execution flow, wrong actions or operations, and wrong operand values. Overall, we observe that many reviewable failures are subtle. Concretely, the generated code mostly follows the prompt, but it instantiates a slightly different intent that requires fine-grained review and validation.
Intent-level documentation cannot support reviewing Python-specific failures. As shown in 2 (Python-Specific), failures that are not documentation-reviewable typically result from programming-language-level bugs that are difficult to express as user-facing intent, such as API selection, argument meanings, return-value handling, and side effects. API calls are a typical case. Documentation can record the callee, arguments, and return target, but judging whether they implement the intended action often requires library knowledge. These failures are difficult to validate through documentation alone, especially for non-programmers with limited library knowledge or programming expertise.
The observations above motivate the central idea of VLP: using NL-based documentation as a faithful and readable intermediate layer between user intent and generated code. For users, this layer exposes the concrete semantics of LLM-generated code in a form they can review even without programming-language knowledge. For reliable code generation, VLP turns confirmed user intent into program repair targets and verifiable properties. Based on this idea, VLP has three design goals.
First, the code-to-documentation translation must be faithful and unambiguous enough to demonstrate subtle deviations and underspecified behaviors in LLM-generated code. It should never use ambiguous NL sentence structures that confuse users or lose important program semantics, including control flow, data flow, and assertion-based properties.
Second, VLP should minimize user effort in documentation review. Though many failures can be exposed, users cannot be expected to review the entire documentation. Instead, an efficient framework should present users suspicious documentation snippets and provide precise surrounding context.
Finally, after multi-turn user review and repair, the validated documentation should help turn user-confirmed intent into reliable Python code. In vibe coding, users should not be responsible for checking Python-specific details or low-level implementations of complex algorithms, as these details are hard to verify manually. Fortunately, the documentation retains assertions and concrete NL descriptions of API behaviors. Thus, VLP can use automated verification tools to check assertion-based properties and API usage against the generated code.
This section first presents the overall workflow of VLP (4.1) and then describes the design of three components that help users repair and validate LLM-generated code. (1) VLP introduces an NL-style language for the documentation called the literate language (4.2), which converts generated code into human-readable descriptions via syntax-directed translation. VLP also presents the documentation hierarchically, so users can keep the global overview while diving into local details. (2) VLP recovers trace links between the documentation and implementation-relevant sentences in the user prompt, allowing LLMs to identify potential mismatches more accurately by narrowing the search scope. The mismatch-detection prompt is guided by the bug taxonomy derived from our study. When a potential mismatch is detected, the LLM generates concrete validation questions about the intended behavior and presents them to users with the surrounding context (4.3). (3) VLP integrates automated tools to check API usage and algorithmic properties in the generated code against the validated documentation (4.4), which reduces the burden of manually reviewing complex algorithms and Python-specific implementation details.
As shown in 3, VLP consists of a code generation step followed by a multi-turn review-and-repair loop until the documentation is validated by the user. Then, the code will go through API check and assertion-based property verification.
Generation step. Given an NL prompt (), VLP first generates Python code, where the LLM is encouraged to generate assertion-based properties alongside the code (). Then, it applies Python-to-documentation translation ().
Mismatch detection for guiding user review and validation. After the documentation is constructed, VLP analyzes documentation-intent alignment (). It decomposes the prompt and the documentation into fine-grained alignment units and recovers trace links between them. Based on the linked pairs, VLP uses an LLM to detect and potential intent-documentation mismatches in a fine-grained manner. These problematic documentation snippets are highlighted in the user interface with related validation questions and evidence from the prompt, which turns a long documentation review into a focused set of intent-level validations. If the user revises a highlighted snippet, VLP patches the Python code accordingly () and updates the corresponding documentation lines ().
Complementary verification after user validation. After the documentation is validated, VLP checks the remaining details that are better handled by automated formal verification methods. It uses bounded model checking () for two complementary tasks: (i) Python-specific checking for library calls and related implementation details, and (ii) property checking stated as NL assertions in the documentation. If verification fails, VLP feeds the failure examples back into the repair loop. The workflow terminates once the Python code passes verification or the maximum repair count is reached.
5pt
>
cp0.17 >
cp0.40 >
cp0.37
Categories & Purpose & Example
Declarations and type signatures & Introduce functions, custom types, fields, inputs, and outputs in a form close to English. & There is a calculate_score function, whose input is a decimal named raw_val, whose output is a decimal
Core expressions and data access & Express arithmetic, Boolean logic, etc. Prefer keeping symbolic representations as users are familiar. & today_score = basic_score + correct_answers[date, person_id] / 2
Programming-style function calls & Support precise function invocation inside expressions, including recursion and method calls. & recursive_calc(n - 1) + recursive_calc(n - 2) + 1
Natural-language-style operations & Describe workflow steps and API-like operations as verb phrases, optionally with parameters and returns. & Normalize input_values with scale = 2.0 then return to normalized
Conditionals and predicate formulas & Encode branching logic using either comparison expressions or restricted natural-language predicates. & If (volatility_index exceeds threshold by 10 percent) and (min_score > 50), is_valid =
true
Loops and iteration & Express both conventional loops and natural-language iteration over collections. & For each document in document_collection, extract keywords from document and append to kw_list
Properties assertions (Hoare logic style [44]) & State preconditions and postconditions for verification inside formally declared
functions. & At this point, assume that unsorted_score_list.length > 0
To translate generated code into literate-language documentation, first, we design grammar and conversion rules to support (mostly) deterministic translation for validation-relevant code snippets. Second, we encourage the code-generation LLM to summarize complex algorithm implementations by extracting their properties, so users can simply review high-level behavior and automated checks can subsequently verify low-level details. Third, we organize the documentation into a hierarchical structure when showing it to users, preserving a global overview while enabling rapid comprehension of the local context.
At the language level, we define the literate language with an NL-style LALR(1) grammar, a parser-friendly grammar with an unambiguous parse structure. This keeps the documentation readable to users while remaining precise enough to review. In this paper, we use English in the literate language and study 200 NL-program pairs, together with prior NL-programming literature [45], [46], to analyze how people express programming-language semantics in English. Nevertheless, VLP can be extended to other natural languages by building dedicated LALR(1) lexers and parsers.
Syntax-directed python-to-documentation translation. For major Python syntax rules, we propose corresponding translation rules in the literate-language grammar. As shown in ¿tbl:tab:lfl-grammar-categories?, these rules follow Python’s key syntactic categories, including declarations, expressions, function calls, conditionals, loops, and assertions. During runtime, after an LLM-generated Python program is parsed into a syntax tree, VLP performs a syntax-directed translation. It traverses the tree and emits literate-language snippets following the corresponding translation rules. During translation, several hierarchical Python syntax-tree nodes often need to be linearized into one literate-language sentence. We therefore carefully design the literate-language syntax so that such sentences read naturally while still preserving the nested grammatical structure needed for LALR(1) parsing. Specifically, step in 3 illustrates how a complex Python statement is translated by fixed rules into a literate-language sentence step by step on the tree.
Ideally, the translation would be fully deterministic even though Python syntax supports flexible parts such as variable names and expressions. In most cases, this is possible because the translation rules directly carry Python variable names, expressions, and conditions into the corresponding documentation without decimating readability. However, some flexible parts cannot be handled by syntax-directed translation alone. Simply copying these Python snippets would make the documentation hard to read, yet their forms are too flexible for us to exhaustively define fixed rules that translate them into understandable literate-language descriptions. API calls are a typical case. The converter can parse the callee, arguments, and return target, but the API name often needs to be explained as a clearer action, such as creating a dataframe or computing a distance matrix. Likewise, lambda expressions and higher-order expressions may encode sorting keys, filtering rules, or data transformations. A fixed translation rule would either stay too close to raw Python or miss the behavior users need to validate. VLP therefore statically analyzes syntax trees and marks these snippets as python_level blocks. For each python_level block, the LLM generates a short verb phrase using its pretrained knowledge and available docstrings. Meanwhile, for determinism, translation rules still fix the surrounding control flows, input arguments, and return assignment.
Property support in documentation. Reviewing every implementation step of a complex algorithm can make user validation difficult. Therefore, VLP encourages the Python-generation LLM to abstract algorithms into compact properties. We use assertion-based Hoare-logic-style properties: a precondition specifies what must hold before function execution, a postcondition specifies what must hold after the function returns, and an invariant specifies what must remain true during execution. For example, a sorting function can be documented by requiring the output to be ordered and to contain the same elements as the input, rather than describing each implementation step. Such properties serve as a shared interface between users and verification tools. In VLP, users validate whether the properties reflect their intent, while automated verifiers leverage bounded model checking to verify the code.
Hierarchical documentation display for focused review. After translating Python code into documentation (step in 3) and generating validation questions (step ), VLP presents them in a hierarchical view as the user interface. The goal is to avoid making users read the full documentation while still preserving the surrounding program context needed to judge a potential documentation-intent mismatch. Specifically, documentation lines are grouped into collapsible blocks using function calls and classes as boundaries. For recursive function calls and class references, the same function or class is expanded to depth at most two. When a validation question generated in 4.3 highlights a suspicious documentation snippet, the user interface proactively opens the relevant block and nearby context. Thus, users only have to review and validate a small portion of the documentation.
After VLP constructs the documentation, users will validate whether its behavior matches their intent. A full documentation view is insufficient for complex programming tasks, as users do not know which parts of the long documentation deserve more attention. To narrow the scope, as illustrated in step of 3, VLP conducts fine-grained misalignment detection based on implementation-relevant trace links between documentation and prompts, and then presents found mismatches and corresponding validation questions via the user interface.
Implementation-relevant traceability link recovery. VLP detects mismatches by comparing linked pairs of prompt-side and documentation-side link units. Each unit covers a single action, a condition, a function signature, or a formula, including constants and literals. For example, a sentence in the prompt describing how invalid inputs should be handled should be linked to the code snippets that implements the check and corner-case handling. Such fine-grained links have two benefits. First, they allow the LLM to focus on a specific bug type and a small snippet in each detection step, following the general principle of decomposing complex tasks into focused subproblems [47], [48]. Second, the narrow scope makes the detected mismatches easier for users to review.
| Scope | Mismatch type | LLM check criterion | Validation question | |||||
|---|---|---|---|---|---|---|---|---|
| prompt unit | Missing steps | A prompt-side unit has no linked documentation unit. The LLM checks whether the behavior is truly required but missing. | Whether the prompt unit should be implemented. | |||||
| doc unit | Redundant steps | A documentation-side unit has no prompt support. The LLM checks whether it is truly redundant behavior or a reasonable enhancement. | Whether the extra program behavior is intended. | |||||
| ambiguous unit | ||||||||
| lacking domain knowledge | The prompt does not fully determine the implementation choice, or the behavior depends on domain-specific conventions. | Corresponding clarification questions. | ||||||
| with API use | Wrong action/operation | For python_level blocks that invoke APIs, VLP retrieves API docstrings and semantically similar alternatives. The LLM checks whether the current API behavior matches the intended operation. | Which operation or documented API behavior is intended. | |||||
| with API use | Wrong operand/value | The API-level action is correct, but parameters, operands, exception behavior, or boundary cases differ from the prompt. | The intended details or edge-case behavior. | |||||
| Other linked pair | ||||||||
| Wrong operand/value | The documentation simplifies or misinterprets the required operation. For example, the prompt asks to combine \(A\) and \(B\) without specifying the formula, while the documentation instantiates it as \((A+B)/2\). | The intended operation, operand, or property. | ||||||
| Function-level flow | Wrong execution flow | The prompt-side control-flow sketch and documentation-side execution flow disagree on conditions, loops, or ordering. | When or in what order the behavior should occur. |
3pt
We regard this as a traceability-link recovery (TLR) problem [49] with an implementation-relevance filter, which we refer to as implementation-relevant TLR. Our design is motivated by the observation that complex coding prompts often contain implementation-irrelevant noise, such as explanatory sentences and background information. Thus, instead of treating all prompt sentences as link candidates, VLP identifies the behaviors and constraints that a correct implementation must realize and builds link units around them. Specifically, the prompt side and the documentation side are selected and decomposed differently. For documentation, where program structure is available, VLP uses syntax trees to identify candidate link units such as verb-phrase statements, conditions, properties, formulas, and basic blocks. These units expose the concrete actions and conditions expressed by the implementation.
On the prompt side, VLP uses an LLM to decompose the prompt into hierarchical link units. Each unit exposes one implementable behavior or constraint, while preserving its text from the original prompt. When a sentence specifies multiple behaviors, VLP further splits it into smaller clauses. Unlike flat sentence-level linking, this hierarchy lets VLP keep each link unit concrete while retaining the logical context needed to interpret it. This design serves two purposes. First, it helps VLP handle long prompts without collapsing fine-grained requirements into coarse summaries. Instead of asking the LLM to produce a single global summary, VLP first identifies coarse implementable behavior regions and then recursively decomposes each region into more detailed child units. The recursion stops once the relevant text span reaches a manageable size for the LLM to output extracted sentences from the original prompt rather than free-form summaries. Second, the hierarchy preserves logical relations among prompt-side units. When one unit specifies the condition under which another behavior should occur, such as an error condition followed by a required message, the behavior unit is recorded as a child of the condition unit. The hierarchy retains the condition/context in which each behavior should be implemented.
Given the prompt-side and documentation-side candidate units, VLP retrieves the top-\(k\) documentation candidates for each prompt unit based on semantic similarity, where \(k=3\) in our evaluation. Following recent LLM-assisted TLR work [50], an LLM-based judge then confirms or rejects each candidate link using the two units and their surrounding context. Using LLM-assisted TLR allows the recovered links to reflect relevant program behavior rather than superficial textual similarity.
Fine-grained misalignment detection. After recovering trace links, VLP uses an LLM to check both linked prompt-documentation pairs and unlinked units for potential mismatches. Guided by the logic-related bug taxonomy in 2, VLP considers seven mismatch types. 1 summarizes the fine-grained detection criteria for each type.
We additionally introduce the way to detecting underspecification for linked pairs with API use, which is not illustrated by the table. For a linked pair whose documentation-side unit invokes an API-based python_level block, VLP retrieves the API docstring and top three semantically similar alternatives from an incrementally extended API knowledge base. If the retrieved APIs suggest multiple plausible behaviors or edge-case handling, but the
prompt-side unit does not specify which one is intended, VLP treats the case as API-level prompt underspecification and asks the user for clarification.
Documentation enables users to validate intent-level behavior, but low-level concerns such as Python-specific API requirements and the correctness of algorithms are better handled automatically. To this end, VLP integrates two complementary verifiers: an API verifier for Python-specific API usage, and a bounded model checker for postconditions and invariants stated in the validated documentation.
Python-specific API verifier. User validation helps ensure that the selected APIs match the intended functionality, but users, especially non-programmers, may still be unfamiliar with Python-specific API requirements, such as stateful APIs, argument and return-value constraints, and initialization and cleanup. Thus, VLP checks API-level requirements automatically with an LLM in the code repair process.
Bounded model checking for properties. During constrained Python generation, VLP emits verifiable properties, including preconditions, postconditions, and invariants, as executable assertions. After users validate these properties in the documentation, VLP checks the corresponding functions with bounded model checking. Concretely, we use CrossHair [51] to symbolically explore program executions and search for inputs that violate the validated assertions. When CrossHair finds a counterexample, VLP feeds the failing input and violated assertion back to the LLM for subsequent program repair.
Our evaluation answers the following research questions: (i) Does VLP generate more correct programs than LLM-only generation and prior human-in-the-loop code generation frameworks (5.2)? (ii) How accurately does VLP localize intent-documentation mismatches (5.4)? (iii) How much does VLP affect user satisfaction during repair and validation (5.4)? (iv) What additional cost does VLP introduce (5.5)? (v) How much do the API knowledge base and implementation-relevant TLR contribute to VLP’s effectiveness (5.6)?
Implementation and evaluated LLMs. We implement VLP using LangGraph [52] and NLTK [53]. We evaluate it with GPT-5.4 [54] and DeepSeek V4 Flash [36] by calling the official APIs with default decoding parameters.
Benchmark selection. We evaluate VLP on two complementary LLM-for-code benchmarks. (1) We use BigCodeBench-Instruct [35] (BCB) to evaluate LLM-generated code on tasks with diverse API calls and complex instructions. (2) We use QuantCodeEval [34] (QCE), a finance paper-to-code benchmark, to evaluate domain-specific and extremely complex code generation tasks.
Metrics. We evaluate VLP from four perspectives: end-to-end code correctness, guidance quality, user experience, and cost efficiency. For end-to-end code correctness, we report pass@1 [55] using benchmark-provided tests and property checkers. Pass@1 measures whether a single generated implementation passes all required checks. For guidance quality, we measure the precision of VLP‘s mismatch detection (recall is already represented by pass@1), defined as the fraction of suspicious documentation snippets reported by VLP that correspond to ground-truth intent-documentation mismatches. For user experience, we demonstrate code review and validation time and users’ self-reported experience in the user study. Finally, for cost efficiency, we report the average token usage and dollar cost per programming task.
Baselines. We compare VLP against four baselines. Default Code directly prompts the LLM to generate code without user review, clarification, or validation. We also compare against three open-source SOTA human-in-the-loop code generation frameworks, covering pre-generation clarification, comment-based validation, and test-driven interaction. ClarifyGPT [24] is a strong pre-generation intent clarification baseline. PInG [40] is a comment-based human-in-the-loop framework that interleaves code generation, comments, and user feedback through editable comments, and is reported to outperform Copilot. We include it to test whether ordinary editable comments are sufficient, or whether VLP’s documentation, guidance, and verifiers provide additional benefits. TiCoder [32] is a test-based intent clarification framework that uses generated tests and user feedback on the tests to infer user intent and refine code. We include it to compare documentation-based validation against test-driven interaction.
| BCB-21 | BCB-254 | BCB-344 | BCB-389 | BCB-493 | BCB-597 | QCE-T01 | QCE-T24 | |
|---|---|---|---|---|---|---|---|---|
| P1 | VLP | TiCo | PInG | Clari | VLP | TiCo | PInG | Clari |
| L1 | VLP | TiCo | PInG | Clari | VLP | TiCo | PInG | Clari |
| P2 | Clari | VLP | TiCo | PInG | Clari | VLP | TiCo | PInG |
| L2 | Clari | VLP | TiCo | PInG | Clari | VLP | TiCo | PInG |
| P3 | PInG | Clari | VLP | TiCo | PInG | Clari | VLP | TiCo |
| L3 | PInG | Clari | VLP | TiCo | PInG | Clari | VLP | TiCo |
| P4 | TiCo | PInG | Clari | VLP | TiCo | PInG | Clari | VLP |
| L4 | TiCo | PInG | Clari | VLP | TiCo | PInG | Clari | VLP |
2.0pt
| Method | Simulator input following the papers | Allowed simulator output | |||
|---|---|---|---|---|---|
| VLP | Validation questions and highlighted documentation (rather than the code). | Answer only the validation questions. The simulator may fix the highlighted statements according to the validation hints, but cannot touch unrelated documentation parts. | |||
| ClarifyGPT | Clarification questions generated from the ambiguous requirements [24]. | Answer only the asked clarification according to the intended behavior. The simulator cannot provide unsolicited bug fixes or compare the full code with the reference. | |||
| PInG | NL comments and the binary PASS/FAIL execution results [40]. | Review only the shown comments. The simulator may confirm or edit each comment line, but cannot perform code-level review. | |||
| TiCoder | Five candidate tests generated by TiCoder with five candidate code implementations [32]. | Return the expected pass/fail outputs of the golden reference code given the input test cases, which follows TiCoder’s open-source Github repository. |
3.2pt
Since our evaluation involves 30 finance papers and 1,140 general programming tasks, conducting the entire evaluation with real users would be prohibitively costly. We therefore combine real user feedback with an LLM-based user simulator for large-scale evaluation, following prior interactive code-generation work [24], [32]. The consistency analysis between simulated and real users is in 5.3.
LLM-based user simulation. As shown in 3, the simulator is provided with oracle context which represents the full vibe coding user intent. The oracle context includes the benchmark prompt and golden reference implementation, so that the user simulator’s feedback is grounded in the intended behavior. This oracle context is available only to the simulator, not to the evaluated framework during code generation or repair. The simulator can only respond to questions posed by VLP, ClarifyGPT, and TiCoder, and update PInG’s comments via their original interaction interface for fair comparison. Moreover, it cannot reveal unrelated code defects proactively.
Real user study. We conduct a real-user study on a selected subset to compare VLP with prior human-in-the-loop methods. We recruit 10 participants, reserving 2 for pilot testing to refine task selection, user interfaces, and instructions, and using the remaining 8 in the main study. We sample 8 tasks from the benchmarks, including 2 QCE and 6 BCB tasks that are unsolved by the initial code. Before the study, participants provided informed consent and completed a pre-study questionnaire on their background. For each human-in-the-loop method, we implement a user interface following the paper. The model used in the real-user study is GPT-5.4.
We assign tasks and methods to participants according to three criteria, as shown in 2. First, each selected task is evaluated with all four human-in-the-loop methods, so method comparison is not confounded by task difficulty. Second, each participant sees only one method for the same task, avoiding carryover effects from answering the same task multiple times. Third, each method on each task is assigned to one programmer and one non-programmer participant, reducing confounding from participant expertise. Each participant will respond through the dedicated user interface.
| Method | H-correctness | S-correctness | H-scope | S-scope |
|---|---|---|---|---|
| VLP | 0.72 | 0.69 | 0.87 | 0.81 |
| ClarifyGPT | 0.64 | 0.80 | 0.96 | 0.93 |
| PInG | 0.87 | 0.64 | 1 (all in scope by design) | 1 |
2.2pt
Overall pass rate and analysis. 4 and 5 show that VLP consistently improves pass@1 under both LLM-simulated feedback and real user
feedback. On BCB, VLP achieves the strongest results for both models, substantially outperforming other baselines. We attribute this advantage to our fine-grained mismatch detection through the linked documentation and
prompts. Moreover, VLP exposes concrete implementation inconsistencies in the validation questions to users, and therefore eventually results in more actionable repair commands. Nevertheless, VLP still fails on 6.5%–33.8% of BCB tasks. Besides LLM inherent randomness, the remaining BCB failures are often caused by totally unstated operations that the prompts never mention. For example, in BCB-306, the prompt asks to
remove all JavaScript files whose names contain jquery and record the removed files in jquery_removal.log; it never specifies that the implementation should use Python’s logging module or call logging.info.
Nevertheless, the BCB checker expects such a call, making this hidden requirement difficult for VLP to detect. Other failures arise when the correct feedback is not correctly applied by the repair LLM since it requires
coordinated edits across scattered code snippets.
On QCE, VLP also improves the code generated by both models, especially for DeepSeek. However, it does not achieve full correctness because QCE tasks require substantial quantitative finance knowledge, such as reasoning about time-window alignment and look-ahead bias. VLP is not designed to detect inconsistencies beyond the LLM’s knowledge and prompt. Furthermore, even when such inconsistencies are identified and the user provides the correct feedback, the repair model may still fail to implement the required changes, especially for DeepSeek. Overall, these results suggest that VLP is most effective when missing requirements or semantic deviations can be grounded in the program or prompt, while its remaining limitations stem primarily from the underlying model’s domain knowledge and code repair capability.
Because simulator feedback affects the final pass@1, we examine whether it approximates real human feedback. Note that TiCoder is excluded because users only need to accept or reject test cases without any NL interaction. We use blind rubric-based adjudication, which is inspired by LLM-as-a-judge work that validates model-based outputs against human judgments [56], [57]. For each task used in both LLM-simulated and real-user settings, we collect all question/comment-feedback pairs, anonymize them, and then ask three independent human adjudicators to score each response along two dimensions: (i) feedback correctness measures whether the response is relevant and accurate with respect to the query or comment line (2: correct; 1: relevant but misleading; 0: irrelevant) and (ii) scope compliance measures whether the response stays within the queried line (2: no leakage; 1: minor extra detail; 0: excessive cross-scope feedback).
We measure simulator-human consistency on each rubric dimension \(d \in \{\text{correctness}, \text{scope}\}\), corresponding to feedback correctness and scope compliance. Let \(N\) be the number of questions/comments generated by GPT-5.4, and let each question/comment have one simulator response and \(J\) real-user responses. For question/comment \(i\), we denote the simulator response as \(s_i\) and the \(j\)-th real-user response as \(h_{ij}\). For each response, we aggregate scores from independent adjudicators by majority vote, using the median score to break ties; \(\hat{r}_d(x)\) denotes the resulting adjudicated score of response \(x\) on dimension \(d\). We then compare the simulator score with the average human score:
\[\mathrm{\small SimCons}_{d} = 1-\frac{1}{N}\sum_{i=1}^{N} \frac{\left|\hat{r}_d(s_i)-\frac{1}{J}\sum_{j=1}^{J}\hat{r}_d(h_{ij})\right|}{2}.\]
We also report average leave-one-out human-human consistency for reference. The overall results in 4 show that simulator feedback is reasonably aligned with human feedback. Scope compliance is a bit less consistent for VLP, because fixing a bug may go beyond the scope of the documentation line directly associated with the question/comment.
In this section, we evaluate user validation burden and question usefulness. On BCB, VLP asks 8.79 questions per task on average with GPT-5.4 and 2.87 with DeepSeek V4 Flash, corresponding to 0.223 and 0.098 questions per line of code. On QCE, it asks 86.07 and 11.63 questions per task, with corresponding question-to-code-line ratios of 0.264 and 0.053. Among these questions, after review, 55.1% and 64.1% of cases on QCE and BCB require code modifications for DeepSeek, respectively, compared with 55.2% and 66.3% for GPT. Since GPT poses more questions, with a code-correcting question rate similar to DeepSeek, the simulated user plus GPT can cover more intent mismatches. Compared with ClarifyGPT (0.015-0.164 questions per line) and PInG, VLP generally achieves a higher review-trigger rate than ClarifyGPT while eliciting substantially more user feedback, yet it requires far less review effort than PInG’s line-by-line comment review. Finally, question quality varies across LLMs used for detection, suggesting that the misalignment-detection prompt may require model-specific calibration.
After finishing a programming task, the participant answered 5 survey questions for the used method, with scores ranging from 1 (low) to 5 (high). The questions measure helpfulness for finding code issues, low labor intensity, understanding of the generated code, confidence in using the code beyond simple tests, and overall satisfaction. Higher scores indicate better user experience for all metrics. 5 shows that VLP achieves the highest scores in helpfulness for mismatch detection, code understanding, and confidence in using the code, while maintaining a lower labor-intensity than PInG and TiCoder. These results suggest that guided validation over code-derived documentation helps users validate LLM-generated code with a better balance between correctness and effort.
6 and 5 show the token cost and user pass@1 over time of each method, respectively. On BCB, VLP uses 27.3K tokens per task on average with GPT-5.4 and 32.1K with DeepSeek V4 Flash; on QCE, it uses 291.1K and 337.2K tokens, respectively. When we use DeepSeek and VLP to approach GPT’s performance on complex tasks such as QCE, although 7.66\(\times\) more tokens are used, the cost efficiency is still 2.33\(\times\)–6.99\(\times\) higher. In the real-user study, VLP slows users down more noticeably on short coding tasks, especially when using GPT, which asks more questions. However, for some more complex BCB and all QCE tasks used in real user study, where the code is longer, VLP almost lies on the Pareto frontier when considering both pass rate and user response time. It achieves higher correctness than faster methods and lower user time than methods with comparable correctness.
We conduct an ablation study on BCB-Hard to measure the contribution of the API knowledge base and implementation-relevant TLR. With GPT-5.4, removing the API knowledge base decreases pass@1 from 91.9% to 85.1%, while removing TLR decreases pass@1 to 72.3%. With DeepSeek V4 Flash, the two ablations both reduce pass@1 from 66.2% to 58.8%. These drops show that both components are important.
First, although LLMs may have been trained on open-source dataset, data leakage is unlikely to substantially affect our results because VLP validates and repairs errors that remain in LLM-generated programs rather than reproducing benchmark solutions. Moreover, QuantCodeEval [34], released in May 2026, is unlikely to have appeared in model training data. Second, due to the cost of large-scale user studies, we combine a real-user study with an LLM-based user simulator. We improve simulation fidelity with clarifying questions and ground-truth test cases, and observe close agreement between simulated and real-user feedback (5.3). Finally, we do not evaluate the faithfulness of the documentation separately because most of it is enforced by a deterministic, syntax-directed translation. For API calls that require LLM-assisted translation, the LLM is provided with API documentation and constrained by our syntax, while the exact control flow, arguments, return targets, and data dependencies are preserved.
Validating/verifying LLM-generated code. Existing approaches to validating/verifying LLM-generated code mainly fall into two groups. The first detects likely errors using probabilistic methods, such as LLM-generated tests [7], [9], LLM judges, task-specific rules, risk prediction based on LLM internal states, calibration, or metamorphic testing [58]–[61]. They can reveal failures, but cannot guarantee correctness.
The second group uses certificate-based verification, where generated code or specifications are checked by formal tools. These methods rely on expert-written or LLM-generated properties [19], [62]–[68], verifier-guided refinement [13], or runtime checks with expert knowledge [69]. Their key bottleneck is certificate quality: current LLMs often fail to produce properties that are both verifiable and complete enough to exclude incorrect behaviors [18], [70], [71].
Human-in-the-loop for vibe coding. Human-in-the-loop techniques have been explored to make AI-assisted programming more controllable. Prior work studies developer interactions with coding assistants [72]–[74], elicits intent through intermediate feedback [75], and updates generated code using runtime feedback or interactive model decisions [76]–[78]. However, these systems mostly expose code snippets, tests, or runtime results to users. VLP instead asks users to validate a human-readable NL representation of program semantics before verifying the code implementation.
Ambiguous or contradictory prompts can substantially degrade code correctness even when models still generate plausible code [79]. Existing work reduces underspecification mainly through pre-generation clarification or specification-oriented prompting [24], [27], [32], [80]. In contrast, VLP traces fine-grained links between the prompt and generated code, enabling iterative discovery of subtle mismatches.
We present VLP, a human-in-the-loop framework that introduces an unambiguous literate documentation layer to bridge prompts and LLM-generated code. By enabling fine-grained misalignment detection, targeted user feedback, and automated verification over user-validated semantics, VLP improves code correctness with user validation effort, demonstrating that structured and user-friendly human-LLM collaboration is more effective than purely automated validation.