{"id":"117f5d93-ffd4-47b5-826b-da17f1f4b5ae","arxiv_id":"2507.12443","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"LLM-based incremental config synthesis needs user disambiguation of insertion placement; Clarify uses differential questions and binary search to resolve it.","lead":"This paper argues that LLM-based network configuration synthesis fails when inserting a new rule into an existing route-map or ACL, because overlapping rules make the correct placement ambiguous. The authors propose Clarify, a tool that asks the user targeted differential questions to disambiguate placement, and they show it works on a small synthetic network.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Section 4's formal conditions do not characterize single-insertion intents: the non-strict inequality in condition 3 allows one existing rule to be both old and new for different inputs, so the binary-search disambiguation algorithm rests on an unproven uniformity assumption.","rationale":"The reader's weakest_assumption targets the same load-bearing point: the binary-search algorithm assumes user intents are representable by a single inserted rule satisfying the Section 4 conditions. My stress-test sharpens this into a concrete internal flaw: as written, condition 3 does not even guarantee single-insertion representability, because equality permits one original rule to be split between old and new behavior. This is not merely an unrealistic user intent; it is a gap in the formal argument. The paper's evaluation is also too narrow to cover the binary-search algorithm, since the prototype is described as supporting only top/bottom insertion and the workload is synthetic. These issues do not refute the paper's motivating observation that overlap-based ambiguity exists, nor the general idea of interactive disambiguation, but they mean the central algorithm's correctness and scope are not established. A conditional accept remains the right verdict: the direction is plausible and the measurements are useful, but the formal model and evaluation must be repaired or broadened before the contribution is fully supported.","tokens_in":9672,"tokens_out":9943,"duration_ms":134309,"concrete_test":"Construct the two-rule counterexample from Section 4: S=[A,B], S* matches inputs handled by A, and define M' so one A-handled input remains on A while another A-handled input switches to S*. Check that this M' satisfies all three published conditions yet has no single insertion point. If the authors accept the counterexample, the formal characterization and the binary-search guarantee need repair, e.g., by adding a uniformity condition (M(r)=M(r') implies M'(r)=M'(r')) and using a strict ordering in condition 3. A follow-up empirical check would then measure, on real configuration changelogs, how often desired final behaviors satisfy the corrected conditions.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central algorithm's correctness depends on the three conditions in Section 4. As written, condition 3 is: for all r, r' matched by S*, if M'(r)=M(r) and M'(r')=S*, then M(r) <= M(r'). The non-strict <= allows the same original rule to appear on both sides: take S=[A,B], let S* match inputs that A handles, and define M' so one such input keeps A while another is handled by S*. Then M(r)=M(r')=A, so the condition is satisfied, but no single insertion point realizes M': inserting before A makes both inputs use S*, inserting after A keeps both on A. Thus the three conditions are insufficient to ensure that the intended semantics can be implemented by inserting one rule. The binary-search procedure assumes a uniform cut through the original rule list, but the paper never proves that real operator intents satisfy that uniformity property; the Section 5 workload is synthetic and small, and Section 2.2 states the prototype only supports top/bottom insertion, so the binary-search path is not actually exercised in the evaluation. The paper's central claim that Clarify resolves insertion ambiguity therefore rests on an unverified and formally incomplete model of user intent.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper argues that LLM-based incremental synthesis of network configuration stanzas (route-maps and ACLs) faces a distinct problem beyond hallucination: even when an LLM correctly generates a stanza in isolation, the stanza's placement in an existing ordered list of rules is ambiguous because rules frequently overlap in header space. The paper offers overlap statistics from a cloud provider and a campus network, formalizes the disambiguation problem in Section 4, and proposes Clarify, a prototype that verifies LLM-generated stanzas and asks users differential behavioral questions to determine insertion placement. The evaluation is a small synthetic three-router topology, and the authors explicitly describe the work as a toy demonstration in Section 7.","tokens_in":9896,"tokens_out":7457,"duration_ms":92869,"significance":"If the central claim holds, the paper identifies a real and underexplored bottleneck in LLM-based configuration synthesis and provides a reasonable starting point for addressing it. The strengths are the clear problem statement, the use of real-network overlap measurements, the crisp (though currently flawed) formal model, and the candid acknowledgment of limitations. However, the formalization in Section 4 has a correctness gap, and the evaluation in Section 5 does not exercise the proposed binary-search algorithm; as written, the evidence is not yet sufficient to support the claim that Clarify resolves insertion ambiguity in general.","major_comments":[{"comment":"The non-strict inequality in condition 3 is insufficient to guarantee that a single insertion point can realize the intended semantics M'. Consider S=[A,B] and let S* match exactly the inputs that A matches. Define M' so that one such input is handled by A (kept) and another is handled by S* (new). Then conditions 1 and 2 hold, and condition 3 holds because M(r)=M(r')=A for the two inputs, so M(r)<=M(r') is true. Yet no insertion point realizes M': inserting S* before A makes both inputs use S*, while inserting after A keeps both on A. The condition should use strict inequality (M(r)<M(r')) or an additional constraint preventing the same original rule from appearing on both sides; with strict inequality the condition does characterize realizable single-insertion semantics. This is load-bearing because the binary-search correctness argument and the claim that Clarify resolves ambiguity both rest on this characterization.","section":null},{"comment":"The evaluation does not validate the Section 4 algorithm. Section 2.2 states that the prototype only supports inserting a stanza at the top or bottom of the initial route-map, so the 17 reported disambiguation choices (5, 6, and 6 for routers M, R1, R2) exercise only the two-location special case, not the general binary search over arbitrary insertion positions described in Section 4. In addition, the evaluation has no baseline comparison (e.g., LLM-only insertion without disambiguation, random insertion, or human expert placement), and Section 7 concedes the experiment is a toy demonstration. The central claim that Clarify resolves insertion ambiguity therefore goes beyond what the current evidence supports.","section":null},{"comment":"The overlap measurements are presented without error analysis, confidence intervals, or a precise statement of what an 'overlap count' counts (number of overlapping pairs? number of rules involved?). For route-maps, the overlap definition deliberately ignores actions and is an upper bound on behavioral ambiguity, so the reported 140/800 route-maps with overlaps do not directly establish that insertion ambiguities would occur in practice. For campus ACLs, the fraction with conflicting overlaps drops from 37.7% to 18.6% when proper-subset matches are excluded, and the cloud ACL numbers do not provide the corresponding breakdown. The connection from overlap frequency to actual disambiguation need is asserted rather than measured, for instance by simulating realistic incremental updates over the measured configurations.","section":null}],"minor_comments":[{"comment":"There are several typographical errors, including 'LLLLM' instead of 'LLM', 'to to produce' instead of 'to produce', and 'preferen ce' in the example route-map.","section":null},{"comment":"The Related Work text contains 'os then filled' instead of 'is then filled', and reference [19] appears to have incorrect author formatting ('Sean Welleck Pranjal Aggarwal, Bryan Parno').","section":null},{"comment":"The notation in condition 3 should make explicit that M(r) and M(r') are compared by their order in the original list S, and that the consequent uses M(r'), the original rule handling r', not the new rule S*; the surrounding prose can be read either way.","section":null},{"comment":"The caption could state the totals (33 LLM calls and 17 disambiguation choices) to make the scale of the evaluation immediately clear.","section":null}],"recommendation":"major_revision","confidential_remarks":"The authors are appropriately honest about the toy-demonstration scope, and the formalization issue in Section 4 is fixable by tightening condition 3. The main risk is that the paper's framing claims more than the evaluation and the current formal model deliver; a revision should either strengthen both or explicitly narrow the claim to the two-location prototype. This is a reasonable workshop-style contribution but needs the formal repair and a more faithful evaluation before it should appear as a full paper."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper does two genuinely useful things: it documents that overlapping rules in real ACLs and route-maps are common (69/237 cloud ACLs, 140/800 route-maps), and it frames a clean subproblem — where to insert a synthesized stanza — rather than expecting an LLM to produce a whole policy at once. The disambiguator idea, using differential examples to elicit intent, is sensible, and the workflow is clearly described. Credit is due for the overlap measurements; I haven't seen those quantified before.\n\nThe soft spot is in Section 4. The three conditions meant to characterize when a user's intended semantics M' can be implemented by inserting a single rule S* are not sufficient. Condition 3 uses non-strict <= and allows the same original rule to appear on both sides. Concretely: if S* matches two inputs that were both handled by rule A, and the user wants one to stay on A and the other to move to S*, then condition 3 is satisfied (A <= A), but no insertion point realizes that behavior — inserting before A moves both, inserting after A keeps both. The real requirement is that the set of original rules shadowed by S* forms a suffix of the matched rules, which condition 3 neither states nor implies. I don't think this is a nitpick: the binary-search disambiguation algorithm rests on exactly this uniformity assumption, and the paper doesn't argue that real operator intents have that shape. The evaluation doesn't help because the prototype only supports top/bottom insertion (Section 2.2), so the binary-search path is never exercised.\n\nThe other limitations are the ones the authors themselves flag: a three-router synthetic topology, 14 LLM calls, no baseline, no artifacts. Those would be acceptable for a vision paper if the core algorithm were solid, but right now the formal foundation is the weakest part.\n\nThe paper is worth engaging with seriously — the problem is real and the overlap data deserve attention — but the central algorithm needs a corrected correctness argument and at least one evaluation that actually exercises the disambiguator beyond top/bottom insertion. I'd send it to review as a conditional accept, not a rejection.","headline":"Real problem and useful overlap data, but the formal conditions in Section 4 don't actually guarantee a single insertion point, and the binary-search disambiguator is never exercised in the evaluation.","tokens_in":10436,"tokens_out":3214,"would_cite":true,"duration_ms":36187,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"LLM-generated route-map and ACL updates are often ambiguous because overlapping rules make insertion order underdetermined; Clarify resolves this by asking users targeted differential behavioral questions.","keywords":["LLM-based configuration synthesis","disambiguation","route-map","access control list","network verification","incremental synthesis","rule overlap","user intent"],"falsifier":"Run Clarify on a corpus of real production route-map and ACL change requests. If a substantial fraction of requests cannot be expressed as a single inserted rule satisfying the three conditions, or if operators presented with the generated differential examples frequently pick an option that does not match their stated intent, the central claim that disambiguation-by-binary-search resolves the problem would be refuted.","tokens_in":9465,"feed_emoji":"🧭","tokens_out":5107,"duration_ms":53160,"temperature":0.7,"pith_summary":"The paper argues that the main remaining obstacle to LLM-based network configuration synthesis is not hallucination but ambiguity: when a newly generated route-map or ACL stanza is inserted into an existing ordered list, overlapping rules mean the right insertion point cannot be inferred from the natural-language intent. It claims this ambiguity is common in practice, citing measurements of route-maps and ACLs with dozens and even hundreds of overlapping rules in cloud and campus networks. To address it, the paper proposes Clarify, which first has the LLM synthesize a config stanza in isolation, then asks the user targeted differential behavioral questions, using binary search over candidate insertion points. On a small synthetic workload, Clarify successfully synthesizes and verifies all router configurations incrementally. The intended takeaway is that disambiguation is a necessary component of LLM-based config synthesis, and the same idea transfers to any code update where insertion order matters.","feed_headline":"Network config synthesis needs disambiguation, not just better LLMs","feed_subtitle":"Overlapping ACL and route-map rules make insertion order unknowable; Clarify resolves it with differential examples.","key_machinery":"The Disambiguator is the load-bearing component. Given a verified new stanza and an existing ordered configuration, it determines possible insertion positions by comparing behaviors of candidate configurations, generating differential behavioral examples—concrete input routes or packets that are treated differently depending on where the stanza is placed—and asking the user which behavior matches their intent. Because the user's intended update is assumed to be expressible as a single inserted rule satisfying the three conditions, the problem reduces to locating one insertion point in an ordered list of interacting rules, and binary search over the candidate rules yields the answer with a logarithmic number of user queries. Verification of the stanza in isolation is done with existing ACL and route-map analysis methods before insertion, so disambiguation only has to resolve ordering, not the stanza's own correctness.","core_discovery":"The central claim is that incremental synthesis of routing policies and access-control lists with LLMs fails unless the system disambiguates where a newly generated stanza belongs, because route-maps and ACLs are ordered rule lists whose rules often overlap in header space. The paper formalizes a single-rule update as one new rule $S^*$ inserted into an existing list $S$, with the intended semantics $M'$ satisfying three conditions: every input is either handled as before or by the new rule; inputs handled by the new rule must match it; and there is a single insertion point consistent with the intended behavior. Given these conditions, the Disambiguator collects the rules that potentially interact with $S^*$, shows the user a differential example between two candidate insertion positions, and uses binary search to locate the correct position with a logarithmic number of questions. The paper's measurements of 237 ACLs (69 with overlaps, one with over 100 overlapping rule pairs) and 800 route-maps (140 with overlaps) support the premise that ambiguity is a practical problem, and the synthetic evaluation on a three-router topology shows the workflow can produce verified configurations end to end.","pith_inferences":["A natural extension would be to test Clarify against real operator change requests from production networks, since the paper's evaluation is limited to a small synthetic topology; that test would reveal whether real intents satisfy the single-rule conditions.","The disambiguator's interface could be made harder to misread by presenting multiple differential examples at once, because a single example may not isolate the dimension of intent the user cares about; this is a usability question the paper leaves open.","The binary-search approach could be adapted to other ordered structures beyond route-maps and ACLs, such as firewall rule sets or compiler optimization passes, wherever overlapping match conditions make insertion order consequential."],"forward_implications":["If disambiguation is accepted as necessary, LLM-based config synthesis tools should include an interactive clarification phase rather than emitting a single config from a prompt.","The binary-search disambiguation algorithm means the number of user questions grows only logarithmically with the number of interacting rules, so even configs with hundreds of overlaps remain practical to clarify.","The same disambiguation step is needed for manual configuration updates, not just LLM-generated stanzas, because the insertion-order ambiguity exists independent of the generator.","The approach generalizes to other program updates where the new code is correct in isolation but its placement in an existing program determines global behavior."],"supporting_citations":[{"why":"Establishes the baseline LLM-with-verification synthesis workflow that Clarify builds on by adding incremental stanza generation and a disambiguation step.","marker":"[18]"},{"why":"Provides the Lightyear topology and global-to-local policy decomposition used to construct the synthetic evaluation network.","marker":"[26]"},{"why":"Supplies evidence that LLM-proposed resolutions of ambiguous intent are often judged incorrect, motivating the need for explicit disambiguation.","marker":"[15]"},{"why":"Shows LLMs behave inconsistently under ambiguous prompts, supporting the claim that user intent cannot be reliably inferred from the prompt alone.","marker":"[22]"},{"why":"Documents a real network outage caused by a small configuration error, giving practical stakes to the ambiguity problem.","marker":"[17]"}],"fun_headline_variants":["LLM config synthesis fails without disambiguation","Overlapping ACLs require user intent elicitation","Clarify: Disambiguator for LLM network config synthesis","Disambiguation is the missing piece in LLM config synthesis"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing assumption is that every intended update can be represented as a single new rule that either leaves each route's handling unchanged or hands it to the new rule, with one insertion point that realizes the intended behavior, and that users can reliably choose the correct option from the differential examples.","fun_headline_variants_meta":{"raw":{"variants":["LLM config synthesis fails without disambiguation","Overlapping ACLs require user intent elicitation","Clarify: Disambiguator for LLM network config synthesis","Disambiguation is the missing piece in LLM config synthesis"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000691,"raw_usage":{"total_tokens":3113,"prompt_tokens":916,"completion_tokens":2197,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":532,"completion_tokens_details":{"reasoning_tokens":2133}},"tokens_in":532,"tokens_out":2197,"duration_ms":16907,"temperature":1.0,"reasoning_tokens":2133,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T16:45:06.792181+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Clarify on a corpus of real production route-map and ACL change requests. If a substantial fraction of requests cannot be expressed as a single inserted rule satisfying the three conditions, or if operators presented with the generated differential examples frequently pick an option that does not match their stated intent, the central claim that disambiguation-by-binary-search resolves the problem would be refuted.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Documents a real network outage caused by a small configuration error, giving practical stakes to the ambiguity problem."}],"review_version":1}