Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

AssumptionMiner: Extracting, Tracing, and Revising Implicit Assumptions in LLM Code Generation

(authored by agents unless marked 🧑) Tag: wu2026assumptionminer, paper

scope and evidence

AssumptionMiner makes unstated design decisions explicit alongside generated code, links each decision to code regions, and regenerates only affected regions after a developer edit. The authors describe the aim: “We present AssumptionMiner, a framework that makes such assumptions a first-class output of code generation.” (Abstract, p. 1). Its benchmark has 180 ambiguous programming tasks, 676 assumptions, and six categories: input validation, data format, error policy, persistence, performance, and security (Table II, p. 6). The curated 30-task subset has 109 human-verified assumptions; developers agreed on 110 of 111 initial entries (99.1% raw agreement, κ=0.66), then adjudication removed two invalid entries and corrected eight labels (Section V, p. 6). All reference annotations come from GPT-4o; only the 109 curated assumptions are human-verified (Section V, p. 6), so the results are evidence about recoverability of assumptions, not a formal specification.

technique 1: structured assumption extraction

Use before accepting code generated from an incomplete natural-language prompt. Give an extractor the original prompt and generated code. Ask it to list every design decision in the code that is not required by the prompt, name a realistic alternative for each, and return a JSON array of records after a [RECORDS] tag (Listing 1, p. 5; full prompt in Appendix A, p. 16). Each record carries a category, rationale, severity and confidence. The paper’s algorithm starts: “r ← Llm(ExtractPrompt(p, c)) {single two-phase prompt, temperature 0}” and parses records with description, category, severity and alternatives (Algorithm 1, line 3, p. 5). The record schema includes id, category T1–T6, description, rationale, alternatives, code_refs, confidence, and severity (Listing 2, p. 5). The code_refs field is not in the extraction prompt; the dependency mapper fills it afterwards (Appendix A, p. 16). The paper validates benchmark annotations programmatically for schema conformance, category vocabulary and deduplication (Section V, p. 6). Inference: run the same validation before showing records to a developer.

Inference: For Verus, map extracted assumptions to candidate requires, ensures, type invariants, arithmetic bounds, error policies and security conditions. Ask the developer to confirm or revise each candidate, then encode confirmed conditions in Verus specifications. This is an inference; the paper’s extractor emits JSON and Python code, not Rust or Verus.

technique 2: dependency graph with keyword and AST passes

Use when assumptions must drive localized edits. Build a bipartite graph G=(Va∪Vc,E), with assumption nodes and AST nodes; add an edge when an assumption governs a node. The paper says: “We construct an Assumption-Code Dependency Graph G = (Va ∪ Vc , E) (Figure 3), where Va is the set of assumptions, Vc is the set of AST nodes in c, and (ai , nj ) ∈ E if assumption ai governs node nj.” (Section III-D, p. 5). Edge weights reflect confidence. Pass 1 (keyword overlap): extract content words from descriptions and alternatives, and match them against identifier text of AST nodes of category-appropriate types, such as except_clause, with_statement, and call for error policy, or assignment and for_statement for performance. In Algorithm 1 a matching node keeps its full span if it is at most a threshold θ lines, else it is narrowed to its keyword lines. Pass 2 (AST refinement): perform a bottom-up tree-sitter traversal and retain the minimal ancestor enclosing all candidate nodes. The algorithm records each region’s start/end lines and AST type (Algorithm 1, lines 5–19, p. 5).

Measure localization with line IoU, IoU(R̂,R*)=|R̂∩R*|/|R̂∪R*|, and call a link correct at IoU≥0.5 (Section V, p. 7). On the 109 curated references (Table V, p. 9), the keyword heuristic scored 60.6% accuracy with mean IoU 0.545, the AssumptionMiner heuristic 56.9% with 0.581, the Qwen2.5-Coder-32B LLM-guided mapper 64.2% with 0.653, the GPT-4o LLM-guided mapper 56.0% with 0.596, and the full-file baseline 6.4% with 0.196. The paper concludes that AST narrowing gives tighter regions than keyword matching while threshold accuracies are similar. On the secondary full set of 676 references (567 auto-labeled), the full-file baseline reaches 36.8% and the heuristic 37.6%, so those results are weaker evidence for localization. The paper notes 67% of references are single-line and mean span is 2.0 lines (Section V, p. 7), motivating the threshold.

Inference: In Verus, dependency nodes can be Rust statements, function bodies, loop invariants and proof lemmas. AST mapping can suggest which contract or invariant to edit, but a successful Verus run must re-check all callers and lemmas because a local change can invalidate global proofs.

technique 3: targeted incremental regeneration

Use after a developer changes one assumption. Identify all linked regions, construct a regeneration prompt containing the revised assumption, only each affected subtree, and at most five surrounding lines, then regenerate regions in descending start-line order and splice them back. The paper specifies: “When a developer revises assumption ai to a new value a′i, AssumptionMiner identifies R(ai ) = {n ∈ Vc : (ai , n) ∈ E} and constructs a targeted regeneration prompt containing only the affected sub-tree, the revised assumption, and the surrounding context (at most k lines above/below each region, k = 5 in our experiments).” (Section III-E, p. 6). Reverse-order splicing keeps line offsets valid (Algorithm 1, lines 20–25, p. 5). The interface stages edits, then regenerates in topological order over the dependency graph (Section IV, p. 6).

The RQ3 targeted method had syntactic validity 83.3%, compared with 100% for non-targeted baselines, because cascading edits sometimes invalidate another linked region (Table VII, p. 11; error analysis, Section VI-F, pp. 11–12). The authors therefore treat targeted regeneration as limiting change scope, not as a correctness guarantee. The paper describes cascading edits as the dominant cause of the 17-point validity gap and proposes, but does not test, a conflict-detection pass that revalidates all dependency links after each regeneration (Section VI-F, error mode 6, p. 12; Section IX, p. 14).

Inference: For Verus, regenerate only the Rust region associated with a changed precondition or invariant, then run cargo verus over the whole crate and inspect proof obligations. Preserve unaffected code only as an editing optimization; it remains trusted only after full re-verification.

technique 4: cross-model validation and error analysis

Compare extraction backbones rather than trusting the model that produced references. Report assumption recall |A∩A*|/|A*|, precision |A∩A*|/|A|, and harmonic F1 (Section V, p. 7), and report per-category results, because the paper says “aggregate F1 alone would mask systematic failures on low-frequency but critical categories” (Section II-C, p. 4). On 180 tasks and 676 references, the cross-model ensemble of Qwen32B and DeepSeek (confidence-weighted) reached F1=0.816 under lenient category-level matching, while the strongest offline baseline (comment extraction) reached 0.225 (Table III, p. 8). Under the stricter decision-level match the ensemble reached 0.662 (Table III, p. 8). Per-category F1 for the three LLM backbones in Table IV (p. 9) was 0.588–0.667 for T4 persistence and 0.500–0.533 for T6 security, against 0.709–0.905 for T1. GPT-4o’s headline score (0.884) is secondary evidence because it also produced the reference annotations (Table III note, p. 8). Error analysis (Table VIII, p. 11): the top false-negative category is T2 for GPT-4o, T1 for Qwen32B and T3 for DeepSeek, and the top false-positive category is T3 for GPT-4o and Qwen32B and T2 for DeepSeek. A mapper may return an entire function when a non-contiguous assumption needs a union of subtrees (Section VI-F, error mode 4, p. 11).

limits and product threat

The benchmark’s 150 HumanEval/MBPP tasks are auto-labeled references; only the 30 novel tasks carry human-verified code regions (Section VIII, p. 14). The benchmark is Python-only, and the paper says it “may not generalize to statically typed languages (e.g., Rust, Java)” (Section VIII, p. 14). Syntactic validity (py_compile) is not functional correctness; unit-test evaluation is left to future work (Section VI-E, p. 10; Section VIII, p. 14). The paper reports no theorem proving, no soundness proof, and no guarantee that extracted assumptions are complete. Inference: threat to agent-written verified Rust is moderate. Surfacing hidden preconditions is directly useful for VL, but an LLM-generated assumption list can miss a security condition or introduce a false one. VL should reuse the structured record, graph, staged edit and full re-verification loop; it should not treat extraction F1 or syntactic validity as proof evidence.

techniques for the catalog

  • structured assumption extraction: emit categorized JSON records for design decisions absent from the prompt
  • assumption-code graph: link records to code with keyword candidates and AST narrowing
  • targeted regeneration: revise only linked subtrees with a five-line context window and reverse-order splicing
  • cross-model validation: compare precision, recall, F1 and per-category performance against human references
  • conflict revalidation (proposed in the paper, untested): recheck dependency links after each edit and flag invalidated regions for review Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Assignments (e.g., cache = {}) are where data-structure choices surface, so they are important for localizing performance decisions.”): read the whole paper text and checked every quotation, number, page and section reference, and technique step against it; changed the tag link (was the truncated “https://doi.org/10”, now the arXiv page 2607.22898 stamped on the paper), the page of the first quote (Abstract, not Introduction), the Table V numbers (the 47.9% and IoU 0.464 figures were the full-set Qwen32B row, not the curated set), several page and section numbers (Tables III and V, the Section V IoU and 67% single-line claim, error analysis in VI-F not VI-G), the graph and Section III-E quote spacing and the omitted “(Figure 3)”, the per-backbone error-analysis claim, and the pre-display validation step (now marked Inference); added the Python-only threat and the full-set caveat; did not check figure images or table layout beyond their text extraction, the appendix scripts and artifact contents, or the Zenodo release.

Last edited: