{"id":"4dff43db-913a-47f8-94d9-dd54a4a76bec","arxiv_id":"2607.03963","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"Separating LLM fact filtering from Lean 4 obligation discharge improves vulnerability-detection F1 in all fifteen CWE×backend settings, especially doubling recall on double-free.","lead":"LeanGuard stops LLMs from casually declaring memory-safety bugs safe by making them only filter AST facts, while Lean 4 checks whether each dangerous operation has a real guard. It raises F1 on five CWE classes against pure models and full-repo coding agents.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"The F1 gains rest on hand-built per-CWE pairing and adjudication that are not independently validated against classical static analyzers, so the role-separation claim is only partially stress-tested.","rationale":"The reader correctly flags the hand-built per-CWE extraction, entailments, pairing, and adjudication matrix as the weakest assumption and rates correctness risk medium. That is the load-bearing point: the empirical claim is comparative and holds inside the declared scope, but the causal attribution to “premature-discharge separation” is under-supported without an independent static baseline. The paper already positions itself as an exploratory prototype (§VI), so the concern does not force REJECT; it keeps the verdict CONDITIONAL and simply makes the external-validity caveat more precise. No circularity or internal inconsistency is present; the Lean kernel checks only the already-paired model, which is honest. A single classical-analyzer comparison on the two lifecycle classes would settle whether the role split, rather than the custom rules, is doing the work.","tokens_in":22660,"tokens_out":604,"duration_ms":5619,"concrete_test":"On the CWE-415 and CWE-416 subsets, run Infer (or CodeQL with standard UAF/double-free queries) under the same function-level isolation used by LeanGuard; compute F1 of Infer alone and of LeanGuard with its Stage-3/6 rules replaced by Infer’s open obligations. If LeanGuard’s F1 advantage over the pure-LLM/agent baselines shrinks by >0.10 or disappears, the gains are largely rule-driven rather than role-separation-driven.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The strongest claim is that LeanGuard improves F1 in all fifteen settings by separating neural fact filtering from symbolic obligation discharge. That separation is only as trustworthy as Stage 3 auto-pairing (Table II) and Stage 6 adjudication (Table III and class variants). Both are hand-specified per CWE: dominance/scope rules, Force-Keep via γ, noise/high-risk lexicons, and the asymmetric matrix that can override V_LLM when Q_Lean is strong. The paper never shows that these rules recover the same open obligations a mature analyzer (Infer, CodeQL, Coverity) would flag on the same 801 functions, nor that they avoid inventing obligations the classical tools correctly dismiss. Ablations (Table V) remove AST or the translator but never replace the hand rules with an independent static baseline. External validity (§VI) already concedes the per-class specification is intrinsic and non-general; without that missing comparison, the reported recall doubling on CWE-415/416 could be an artifact of the custom rules rather than of the neural/symbolic role split itself.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","summary":"The paper presents LeanGuard, a neuro-symbolic vulnerability detector that separates roles: an LLM acts only as a constrained semantic filter over AST-extracted candidate facts, while a Lean 4 kernel discharges (or leaves open) safety obligations over a compiled Verification Model M=⟨E,P,O⟩. Unproved obligations in the necessarily partial function-level model are fused with neural evidence via an asymmetric, quality-graded adjudicator. Instantiated on five memory-safety CWE classes and three backends (pure LLM, Codex, Claude Code, all on DeepSeek-V4-Pro), LeanGuard improves F1 over the corresponding baseline in all fifteen settings, with the largest gains on lifecycle classes (CWE-415/416), where recall roughly doubles. Ablations, three-run stability with paired t-tests, and cost are reported; external validity explicitly limits the claim to hand-specified per-CWE pipelines.","tokens_in":23016,"tokens_out":986,"duration_ms":13880,"significance":"If the results hold under broader scrutiny, the paper offers a concrete, auditable alternative to unconstrained LLM vulnerability detection: demoting the model from obligation-discharger to fact editor, and routing discharge through a kernel-checked structural model. Strengths include the machine-checked Lean 4 path, constrained JSON fact-editing schema, deterministic auto-pairing, explicit evidence grades, and an evaluation that covers pure and full-repository agentic backends with stability and cost reporting. The diagnosis of premature obligation discharge is useful for the community. The work is positioned as an exploratory prototype rather than a general detector, which is appropriate given the per-class specifications.","major_comments":[{"comment":"The central thesis is that F1 gains come from separating neural fact filtering from symbolic obligation discharge. Tables II and III (and class variants) encode hand-built auto-pairing, Force-Keep via γ, noise/high-risk lexicons, and an asymmetric adjudication matrix. Ablations (Table V) remove AST extraction or the deterministic translator, but never replace these hand rules with an independent classical static analyzer (e.g., Infer, CodeQL, Coverity) on the same 801 functions. Without that comparison, the large recall gains on CWE-415/416 (Table IV: e.g., Claude Code CWE-415 Rec 0.21→0.41) could be driven primarily by the custom pairing/adjudication rules rather than by the neural/symbolic role split. A head-to-head on open obligations, or an ablation that freezes the symbolic rules and varies only the neural filter, is needed to support the causal claim in the abstract and §I.","section":null},{"comment":"Stage 6 grades Q_Lean using the same CWE-specific high-risk lexicons that assign γ=High in Stage 1 and protect facts via Force-Keep (Eq. 2). When Q_Lean=strong, the adjudication matrix (Table III, Row 1) can override a neural SAFE verdict. This coupling means the symbolic 'strong' grade is not fully independent evidence; it re-weights sinks already privileged by the extractor. The paper should either (a) show that Q_Lean remains predictive when graded with a lexicon disjoint from Stage 1, or (b) report sensitivity of final F1 to the strong/weak/noisy thresholds so readers can assess circular reinforcement.","section":null},{"comment":"CWE-125 and CWE-415 are single runs (§V-E, Table IV), while significance tests (Table VII) cover only the three-run subset. The abstract and §I still highlight CWE-415 recall doubling as a headline result. Either extend the multi-run protocol to CWE-415 (and ideally CWE-125) or qualify the strongest claims so they rest only on the statistically tested cells (6/9 with p<0.05).","section":null},{"comment":"External validity (§VI) correctly states that the target CWE must be fixed in advance and that per-class specifications are intrinsic. The evaluation, however, never measures mis-routing or multi-CWE interference: every sample is scored under its ground-truth CWE pipeline. For a framework whose practical use would require knowing or predicting the class, the paper should report at least a small cross-class stress test (run CWE-416 samples under the CWE-476 pipeline, etc.) or make the 'oracle class' assumption explicit in the RQ1 claims.","section":null}],"minor_comments":[],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The thing to know is that this is a clean, usable diagnosis of why pure LLM vulnerability detectors fail (premature discharge of safety obligations) plus a working pipeline that actually enforces the fix: the model only edits AST candidates; Lean 4 decides whether a guard covers an obligation; an adjudicator fuses the two when the model is partial. That inversion relative to the usual LLM-proposes-proof loop is the new piece.\n\nWhat they do well: end-to-end implementation on five CWEs, same DeepSeek-V4-Pro backend for everyone, consistent F1 lifts in all fifteen settings (biggest on lifecycle classes—CWE-415 recall roughly doubles), ablations that show the deterministic translator and AST stage matter, three-run stability with paired tests on a subset, and cost numbers. The running UAF example is honest about where agents invent “safe” stories. Circularity is low; the claim is comparative F1, not a fitted identity. Shipping Lean-checked claims is real engineering credit.\n\nSoft spots, in proportion: the stress-test note is right that Stage-3 auto-pairing and Stage-6 adjudication are hand-specified per CWE (lexicons, Force-Keep, asymmetric matrix). Without a head-to-head against Infer/CodeQL/Coverity on the same 801 functions, you cannot fully separate “role split works” from “our custom rules recover more sinks.” External validity already says the per-class specs are intrinsic and non-general; CWE-125/415 are single runs. Those are real limits, not fatal ones—the paper does not hide them, and the ablations still show the pipeline pieces move the needle.\n\nThis is for people building LLM+static or LLM+prover security tools who care about obligation discipline more than another agent harness. Math and data look solid inside the declared scope; citations cover the right prior (IRIS, QLPro, APOLLO, etc.). I would send it to peer review. Engage if you work on neuro-symbolic SE or memory-safety tooling; the role-separation idea is worth citing even if you later replace the hand rules.","headline":"LeanGuard’s real contribution is the role split—LLM as constrained fact editor, Lean as obligation checker—and the F1 gains are real within that design, even if the hand-built per-CWE rules leave the “why” only partly stress-tested.","tokens_in":23637,"tokens_out":543,"would_cite":true,"duration_ms":5585,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"LLMs declare code safe by discharging obligations with fluent justifications rather than proofs; LeanGuard separates interpretation from discharge and recovers the missed defects.","keywords":["neuro-symbolic","vulnerability detection","Lean 4","large language models","memory safety","CWE","obligation discharge","static analysis"],"falsifier":"On the same five CWE datasets and three backends, a pure LLM or full-repository agent that still discharges obligations by fluent justification alone matches or exceeds LeanGuard’s F1 and recall, especially the roughly doubled recall on CWE-415.","tokens_in":23543,"feed_emoji":"🛡️","tokens_out":870,"duration_ms":16877,"temperature":0.7,"pith_summary":"Large language models can produce plausible reasons why a pointer use looks safe, yet those reasons are not proofs, so real memory-safety bugs still slip through. The paper traces this failure to premature discharge of safety obligations: the same component that reads the code is also allowed to close the obligation as soon as it can phrase a justification. LeanGuard assigns the two acts to different sides. An LLM is restricted to filtering candidate facts taken from the abstract syntax tree; it may keep or prune facts but never decides that an obligation is met. Surviving facts are compiled into a Lean 4 model in which every dangerous operation must be matched by a guard that structurally covers it; without such a guard the obligation stays open. Because a function usually lacks full context, an evidence-aware adjudicator then weighs the symbolic and neural signals by quality. Instantiated on five CWE classes and three backends, the division of labor raises F1 in every setting and roughly doubles recall on double-free bugs.","feed_headline":"LeanGuard doubles recall on double-free bugs","feed_subtitle":"LLM only filters AST facts; Lean keeps obligations open until a guard covers them","key_machinery":"The unified Verification Model M = ⟨E, P, O⟩ (entities, protections, obligations) together with the structural discharge relation that requires a type-compatible protection to cover each obligation; Lean 4 accepts a claim only under kernel-checked proof, so unproved obligations remain open instead of being argued away.","core_discovery":"The core unreliability of LLM-based vulnerability detection is premature discharge of safety obligations. The remedy is a strict separation of roles: the neural side only interprets and filters AST-derived candidate facts, while a Lean 4 symbolic side holds every dangerous operation open unless a type-compatible guard structurally covers it; an evidence-aware adjudicator then fuses the two partial verdicts by quality rather than letting either side decide alone.","pith_inferences":["The same premature-discharge pattern likely appears in other high-stakes LLM tasks that mix interpretation with obligation checking, such as policy compliance or protocol verification.","Automatic induction of the per-CWE pairing and adjudication rules from labeled examples would remove the main barrier to broader deployment.","Adding whole-program interprocedural context to the same role separation could close remaining false negatives on callee-mediated invalidations."],"forward_implications":["Even agents given full repository access still systematically under-flag lifecycle bugs; structural obligation checking is required to recover them.","Constraining the LLM to edit a fixed AST candidate list prevents both invention of nonexistent guards and deletion of real sinks.","Partial, function-level symbolic models can still improve detection when residual unproved claims are graded by quality rather than treated as final verdicts.","The same division of labor can be extended to further memory-safety CWE classes once per-class extraction and pairing rules are supplied."],"fun_headline_variants":["LeanGuard holds safety obligations open until Lean proves a guard","LLM filters AST facts; Lean never discharges unguarded risks alone","Neuro-symbolic split: LLM prunes facts, Lean requires covering guards","LeanGuard stops premature discharge of memory-safety obligations","LLM interprets only; Lean keeps null-free and UAF obligations open"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"The hand-written, per-CWE extraction rules, pairing strategies, and adjudication matrix correctly turn partial function-level AST facts into trustworthy open or closed obligations even though the symbolic model is incomplete and the target class must be fixed in advance.","fun_headline_variants_meta":{"raw":{"variants":["LeanGuard holds safety obligations open until Lean proves a guard","LLM filters AST facts; Lean never discharges unguarded risks alone","Neuro-symbolic split: LLM prunes facts, Lean requires covering guards","LeanGuard stops premature discharge of memory-safety obligations","LLM interprets only; Lean keeps null-free and UAF obligations open"]},"model":"grok-4.5","effort":"low","cost_usd":0.00324,"raw_usage":{"total_tokens":1184,"prompt_tokens":870,"num_sources_used":0,"completion_tokens":71,"cost_in_usd_ticks":32400000,"prompt_tokens_details":{"text_tokens":870,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":243,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":870,"tokens_out":71,"duration_ms":2774,"temperature":1.0,"reasoning_tokens":243,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-11T22:41:58.903343+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"On the same five CWE datasets and three backends, a pure LLM or full-repository agent that still discharges obligations by fluent justification alone matches or exceeds LeanGuard’s F1 and recall, especially the roughly doubled recall on CWE-415.","supporting_citations":[],"review_version":1}