{"id":"6171faac-0e26-4a4d-94dc-c519d5e1a767","arxiv_id":"2504.21061","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Deepseek-R1 can usually distinguish intended behavior from buggy implementations when writing ACSL specs, and augmenting prompts with Frama-C tool outputs measurably changes the type and focus of generated annotations.","lead":"Researchers tested whether Deepseek-R1 can write formal C specifications (ACSL) that capture a programmer's intent even when the code contains bugs, and whether feeding outputs of symbolic analysis tools into the prompt changes the specs. They found the model often detects subtle bugs and that EVA reports shift specs toward safety preconditions, while PathCrawler examples lead to more abstract postconditions, with important caveats about evaluation quality.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper never checks whether the generated text is valid ACSL; Section 7 admits syntax problems were dropped. Without a parse/verification pass, 'specifications' and all derived claims are unvalidated.","rationale":"The reader's weakest_assumption is confirmation bias in the qualitative reading of chain-of-thought traces. I partially agree, but the logically prior soft spot is that the objects claimed to be ACSL specifications are never syntax/type checked. This is not an external-consensus disagreement; it is an internal evidentiary gap, acknowledged in Section 7. The duplicate Figs. 6 and 7 strengthen the concern: the displayed 'intent' output equals the 'implementation' output and actually encodes the buggy behavior, so the prompt-steering claim currently lacks even one clean displayed example. A Frama-C parse/verification pass across all outputs is a single, decisive test: parse failures would invalidate the quantitative counts and the label 'specifications'; successful parsing would leave the qualitative claims intact but still needing blinded trace coding. Thus the paper should remain CONDITIONAL until this check is run, and the duplicated figure should be corrected regardless.","tokens_in":23718,"tokens_out":5273,"duration_ms":55512,"concrete_test":"Run Frama-C's kernel parser and WP plugin on every generated annotated program across the three prompt sets plus the intent-suite outputs, and report parse/type error rates and well-formedness/provability status. If more than a small fraction (e.g., >5%) fail to parse, the quantitative counts and 'quality' claims in Section 4 and the 'specification' terminology in the central claim need re-scoping or correction; if parse rates are high, the qualitative claims remain to be evaluated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that Deepseek-R1 can be steered to generate ACSL specifications of intended behavior, and that symbolic-tool context changes those specifications. The load-bearing precondition is that the generated text blocks are in fact ACSL. The paper never runs Frama-C or any parser on any output: Section 3.3 explicitly disavows gold-standard/benchmark evaluation, and Section 7 says verification was abandoned because 'earlier LLMs struggled with syntactic correctness'. So the annotation counts in Fig. 8, the bug/intent claims in Sections 3.4-3.7, and the 'quality' comparisons in Section 4 all rest on unparsed, unverified text. This matters concretely: several displayed snippets are questionable ACSL (e.g., Fig. 13 encodes conditionals as integer arithmetic with (a >> 1 >= -4) + ..., which ACSL does not obviously admit), and Figs. 6 and 7 are byte-identical even though one is claimed to implement intent priority. If a parse/type pass were added and many outputs failed, the paper's specification-synthesis claims would be unsupported; if they mostly passed, the qualitative claims could still be assessed.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper investigates LLM-based synthesis of ACSL specifications for C programs using Deepseek-R1, pursuing two research directions. The first is the implementation-versus-intent problem: using a handcrafted 50-program dataset with buggy, anonymized, and combined variants, the authors qualitatively analyze Deepseek-R1's chain-of-thought to assess whether the model identifies program intent, notices injected bugs, and specifies intended rather than implemented behavior. The second direction combines the LLM with symbolic analysis by appending PathCrawler test-case outputs or EVA static-analysis reports to the prompt, and the authors report changes in annotation counts and qualitative changes in specification content. The paper concludes that Deepseek-R1 is resilient to the implementation-versus-intent problem and that neuro-symbolic prompting can steer specification synthesis toward more focused or safety-oriented annotations.","tokens_in":23858,"tokens_out":4139,"duration_ms":44839,"significance":"If the claims were fully supported, the paper would make a useful empirical contribution to LLM-based specification synthesis: it would demonstrate that a reasoning-focused LLM can separate intent from implementation and that symbolic tool output can influence the type and content of generated ACSL contracts. The qualitative observations about how the model uses supplied input/output examples, and the shift toward preconditions under EVA reports, are informative directions for neuro-symbolic tooling. The paper also makes the intent dataset public, which is a concrete asset for follow-up work. However, the significance is currently limited by the absence of any validation that the generated text is parseable ACSL, by a direct internal contradiction in the figures illustrating the intent-prioritization result, and by the lack of statistical support for the annotation-count claims. These issues affect the central claims, not just the presentation.","major_comments":[{"comment":"The paper never verifies that the generated text blocks are syntactically valid ACSL. Section 3.3 explicitly disavows gold-standard or benchmark evaluation, and Section 7 states that verification-based evaluation was abandoned because earlier LLMs struggled with syntactic correctness, yet all annotation counts and all bug/intent qualitative claims treat the raw model output as ACSL annotations. This is load-bearing: if a substantial fraction of outputs do not parse, the counts in Fig. 8 and the bug-and-intent findings in Sections 3.4–3.7 are counting arbitrary text rather than specifications. The authors should run a Frama-C kernel parse/type pass on all outputs and report pass rates per experimental condition. The risk is concrete: the displayed annotation in Fig. 13, `ensures \\result == ((a >> 1 >= -4) + ...)`, uses arithmetic over predicates and is not obviously well-formed ACSL.","section":"§3.3, §7"},{"comment":"The specification shown in Fig. 7 (captioned as generated when intent is prioritized) is byte-for-byte identical to the specification in Fig. 6 (captioned as generated when implementation is prioritized). This directly contradicts the text's claim that the revised prompt produced specifications that \"more closely aligned with the intended functionality.\" Since the implementation-versus-intent distinction is a central contribution, the displayed evidence must be corrected to show the actual intent-prioritized output, or the claim must be revised.","section":"§3.7, Figs. 6–7"},{"comment":"The abstract and Section 3.6 state that the model was \"almost always\" able to identify bugs, but Table 1 aggregates to 110/150 overall (73%), with notably lower rates in the Famous categories (9/30 and 14/30). A 73% overall rate, and 30% on the Famous subset, does not support \"almost always.\" The authors should report per-category rates in the text and qualify the claim accordingly, since the category dependence is itself an important finding.","section":"§3.6, Table 1"},{"comment":"The annotation-count results are presented as the quantitative support for the claim that symbolic context changes the quantity and type of generated specifications, but Fig. 8 is reported without error bars, confidence intervals, or any statistical test. With three generations per program and paired experimental conditions, the authors should report per-condition variability or perform a paired comparison before making statements such as \"EVA led to an increase in preconditions\" or \"approximately 20% increase in annotation counts.\"","section":"§4.4, Fig. 8"},{"comment":"The authors acknowledge that the qualitative analysis could be subject to confirmation bias. Since the bug-notice and intent-inference rates in Section 3 are derived from the authors' own reading of Deepseek-R1's reasoning traces, the paper needs a more disciplined protocol to make those rates credible: for example, independent coding by multiple annotators with inter-rater agreement, or release of the annotated traces alongside the dataset. Without this, the central qualitative claims rest on self-assessment by the same researchers who designed the bugs and defined the intended behavior.","section":"§6.1"}],"minor_comments":[{"comment":"The tool name is inconsistently rendered as \"EV A\" with an extra space in many places; please use \"EVA\" consistently.","section":"Throughout"},{"comment":"Section 4.1 says the PathCrawler suite contains 55 programs, while Section 6.2 says the total dataset consisted of approximately 50 programs; please clarify the actual number used in the experiments.","section":"§4.1 vs. §6.2"},{"comment":"In the submitted text, Section 4.4 references \"Fig. 8 on page 15\" but the figure content itself appears to be missing or placeholder-only; please ensure the actual annotated-count figure is included.","section":"Fig. 8"},{"comment":"Table 1 uses a category called \"Unique\" that is not introduced in the dataset description in Section 3.1; please define this category or remove it.","section":"§3.1, Table 1"},{"comment":"There are numerous typos, including \"Descrbe,\" \"annoations,\" \"Patchcrawler,\" \"pr ec ond iti ons,\" \"thostyle=csse,\" and \"EVA T unnel-vision\"; a careful proofreading pass is needed.","section":"Various"},{"comment":"The term \"high quality examples\" is defined only after the results are presented, as examples that cover all paths with multiple inputs per path; please state this criterion before the qualitative analysis so the reader can assess the claim.","section":"§4.6.3"}],"recommendation":"major_revision","confidential_remarks":"The core idea is timely and the qualitative observations are often insightful, but the manuscript currently treats unparsed LLM text as ACSL specifications, and the intent-prioritization demonstration is contradicted by the identical figures. Both issues are fixable within the scope of a revision: run a Frama-C parse pass, replace the incorrect figures, and add basic statistics for the count data. I would also encourage the editor to ask for the full generation outputs as supplementary material, since the paper's evidence is largely qualitative and trace-based."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThis one is worth reading for the observations, but I would not trust the framing as stated. The paper extends the authors' prior work from GPT-4 to Deepseek-R1 with a larger intent dataset and a much closer look at chain-of-thought reasoning. The qualitative findings are genuinely interesting: PathCrawler examples shift the model toward more abstract postconditions, EVA reports push it into precondition-heavy safety specs, and the \"EVA tunnel vision\" is a real failure mode worth naming. The small-numbers-of-test-cases discussion also makes a practical point about when symbolic context helps.\n\nWhat I cannot get past is that the authors never run a parser or verifier on the generated text. Section 7 admits they abandoned verification early because earlier LLMs produced syntactically broken annotations, and Section 3.3 explicitly declines gold-standard evaluation. That means \"specifications\" in this paper are unvalidated text blocks. I checked one of their own examples: Fig. 13 encodes a postcondition as arithmetic over comparisons, which is not ACSL. Some of the counts in Fig. 8 may be counting text that Frama-C would reject. This is a load-bearing gap, not a minor one.\n\nThe duplicate pair is worse. Figs. 6 and 7 are meant to show implementation-prioritized versus intent-prioritized specifications, but the two figures are byte-identical. The surrounding narrative says the prompt changed the output; the figure says otherwise. At minimum this is a copy-paste error that must be fixed; as published it undercuts the paper's central example.\n\nAlso, Table 1 gives an overall bug-notice rate of 110/150, 73%, which does not support \"almost always\" in the abstract. And the intent-ground-truth judgment is self-assessed by the authors, who injected the bugs and also admit confirmation bias from their previous results. The 3/200 \"intent not identified\" figure rests entirely on their reading of the traces.\n\nThat said, the paper is honest about these limitations, and the underlying questions are real. The reasoning-trace analysis is more careful than most in this area. If the authors add a syntax/verification pass, fix the duplicated figures, soften the \"almost always\" claim, and report counts with error bars, the qualitative story would be publishable.\n\nI would not desk-reject this. It deserves a serious referee, but with major revisions required. I would not cite it in its current form.","headline":"Interesting qualitative observations about steering LLM-generated formal specs, but the paper never checks whether the generated text is valid ACSL, and its two central figures appear identical.","tokens_in":24465,"tokens_out":2923,"would_cite":false,"duration_ms":30143,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Deepseek-R1, a reasoning LLM, can write ACSL specifications that capture a program's intended behavior rather than its buggy implementation—and adding output from symbolic tools like PathCrawler and EVA measurably steers the annotations…","keywords":["specification synthesis","ACSL","Deepseek-R1","large language models","neuro-symbolic methods","Frama-C","PathCrawler","EVA"],"falsifier":"Run the same prompt suite with the injected bugs concealed from the evaluators: have annotators who do not know the ground truth classify each reasoning trace for bug detection and inferred intent, and run every generated ACSL annotation through a parser and verifier against a reference intent specification; if blind bug-notice rates fall far below the reported counts, or if most annotations fail syntax or proof, the central claim is contradicted.","tokens_in":23440,"feed_emoji":"📜","tokens_out":5776,"duration_ms":56501,"temperature":0.7,"pith_summary":"Specification synthesis normally risks learning the bugs along with the code: a specification generated from a faulty implementation can formalize the fault instead of revealing it. This paper tries to establish that a reasoning large language model, Deepseek-R1, is largely immune to that failure: given C code and asked for ACSL contracts, the model inferred programmer intent in nearly every trial, including trials with deliberately injected bugs and anonymized function names. It also tries to show that the user can choose which contract to get—implementation or intent—by wording the prompt, and that appending output from symbolic tools (PathCrawler test cases or EVA static-analysis alarms) measurably steers the number and kind of annotations generated. If these claims hold, formal specification becomes a more practical activity: the LLM supplies flexibility and expressive postconditions, while symbolic tools supply precision and safety constraints. The paper's evidence is qualitative, based on reading the model's reasoning traces rather than on verifying the generated ACSL.","feed_headline":"Reasoning LLM recovers program intent from buggy C code","feed_subtitle":"Adding symbolic-analysis output to the prompt steers Deepseek-R1 toward fewer, sharper specifications.","key_machinery":"The mechanism that carries the argument is an observable reasoning trace: Deepseek-R1 emits a detailed chain of thought before its answer, and the paper treats that trace as evidence of which bugs the model noticed, what intent it inferred, and whether it chose implementation or intent. Around this, the experimental apparatus consists of a 50-program C suite (intent_tests) with Basic, Famous, Mirror, and Unique categories, transformed into buggy, anonymized, and buggy-anonymized variants; and three prompt conditions on a separate 55-program PathCrawler suite: baseline, baseline plus PathCrawler input/output pairs, and baseline plus EVA alarm reports. The prompts forbid loop invariants and restrict generation to function contracts, so the comparison focuses on ACSL preconditions, postconditions, and assigns clauses.","core_discovery":"The central claim, stated on the paper's own terms, is that neuro-symbolic prompting makes LLM-based specification synthesis viable for intent-sensitive contracts. Deepseek-R1 was nearly always able to identify intent: across nearly 600 generations it failed only three times, all in programs that were both buggy and anonymized, where the bug made the code resemble a different coherent program. It noticed most injected bugs (47/60 in Basic, 28/30 in Mirror, 26/30 in Unique, but only 9/30 in Famous), and in every trace where a bug was found the model explicitly consulted the prompt to decide whether to specify the implementation or the intended behavior; a simple prompt addition shifted it to intent. On the neuro-symbolic side, including symbolic analysis reduced total annotations but changed their focus: PathCrawler input/output pairs led to more abstract, case-structured postconditions, while EVA alarms were translated into preconditions that avoid runtime errors, sometimes to the point of tunnel vision that neglected the program's functional essence.","pith_inferences":["A natural test the paper leaves open: verify the generated ACSL with Frama-C/WP; if a large share fails parsing or proof, the intent-inference claim might survive but the practical synthesis claim would need qualifiers.","The chain-of-thought dependence suggests the same pipeline on a non-reasoning or silent model would be far harder to steer and to evaluate; this is testable by ablating the reasoning output.","The EVA tunnel-vision result implies symbolic context acts as an attention magnet; combining multiple symbolic sources (e.g., EVA alarms plus PathCrawler examples) is a plausible way to get both safety preconditions and meaningful postconditions in one contract.","PathCrawler's minimal-path-coverage test selection is designed for testing, not specification synthesis; the paper's BugKPath failure suggests an adapted example-selection criterion—multiple varied examples per path—could materially improve synthesis, which is a concrete next experiment."],"forward_implications":["Generated specifications can expose bugs instead of encoding them, provided the prompt tells the model to target intended behavior.","Users gain a control knob: prompt wording chooses implementation-conformant or intent-conformant contracts, and the choice of symbolic tool (PathCrawler vs EVA) shifts annotations toward postconditions or safety preconditions.","A raw EVA report can be dropped into a prompt with no custom translation, suggesting LLMs can absorb heterogeneous formal-tool outputs without integration code.","PathCrawler-style examples change the model's reasoning: it traces the examples instead of inventing its own, freeing attention for generalization—so the quality and coverage of test cases directly shapes specification quality.","Because EVA reports can dominate the model's attention, a workflow that wants both safety and functional content may need to combine tool outputs or explicitly rebalance the prompt."],"supporting_citations":[{"why":"The prior GPT-4 experiment this study extends and reproduces; it supplies the baseline findings and prompt designs.","marker":"[12]"},{"why":"Introduces PathCrawler, the concolic test generator whose input/output pairs are appended to the LLM prompt.","marker":"[34]"},{"why":"Describes EVA's abstract-interpretation value analysis, whose alarm reports are appended to the LLM prompt.","marker":"[6]"},{"why":"Introduces the Frama-C ecosystem that hosts ACSL, PathCrawler, and EVA.","marker":"[18]"},{"why":"Defines ACSL, the specification language in which all generated annotations are written.","marker":"[3]"},{"why":"Establishes few-shot learning, the prompting technique used to provide ACSL examples to the model.","marker":"[7]"},{"why":"Chain-of-thought prompting, which reasoning models like Deepseek-R1 perform by default and whose traces the paper analyzes.","marker":"[30]"}],"fun_headline_variants":["LLM plus symbolic tools turn buggy C into intent specs","Deepseek-R1 specs code intent, even with injected bugs","Symbolic hints steer LLM to sharper, intent-based contracts","Neuro-symbolic prompt makes LLM specify what code means","Pathcrawler and EVA prompts fix LLM spec focus"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that reading Deepseek-R1's reasoning traces is a reliable, unbiased measure of which bugs it noticed and what intent it inferred, even though the people who injected the bugs and defined the intended behavior also judged the traces; the paper itself flags confirmation bias from prior work.","fun_headline_variants_meta":{"raw":{"variants":["LLM plus symbolic tools turn buggy C into intent specs","Deepseek-R1 specs code intent, even with injected bugs","Symbolic hints steer LLM to sharper, intent-based contracts","Neuro-symbolic prompt makes LLM specify what code means","Pathcrawler and EVA prompts fix LLM spec focus"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000254,"raw_usage":{"total_tokens":1559,"prompt_tokens":927,"completion_tokens":632,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":543,"completion_tokens_details":{"reasoning_tokens":545}},"tokens_in":543,"tokens_out":632,"duration_ms":6344,"temperature":1.0,"reasoning_tokens":545,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T05:24:57.036172+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the same prompt suite with the injected bugs concealed from the evaluators: have annotators who do not know the ground truth classify each reasoning trace for bug detection and inferred intent, and run every generated ACSL annotation through a parser and verifier against a reference intent specification; if blind bug-notice rates fall far below the reported counts, or if most annotations fail syntax or proof, the central claim is contradicted.","supporting_citations":[{"cited_title":"In: International Confer- ence on Integrated Formal Methods","cited_arxiv_id":null,"evidence_quote":"The prior GPT-4 experiment this study extends and reproduces; it supplies the baseline findings and prompt designs."},{"cited_title":"In: European Dependable Computing Conference","cited_arxiv_id":null,"evidence_quote":"Introduces PathCrawler, the concolic test generator whose input/output pairs are appended to the LLM prompt."},{"cited_title":"CEA-LIST, Saclay, France, Tech","cited_arxiv_id":null,"evidence_quote":"Defines ACSL, the specification language in which all generated annotations are written."}],"review_version":1}