Pith. sign in

REVIEW 4 major objections 49 references

LLMs declare code safe by discharging obligations with fluent justifications rather than proofs; LeanGuard separates interpretation from discharge and recovers the missed defects.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-11 22:41 UTC pith:DKT4C2XU

load-bearing objection 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. the 4 major comments →

arxiv 2607.03963 v1 pith:DKT4C2XU submitted 2026-07-04 cs.SE

Neuro-Symbolic Reasoning for Vulnerability Detection

Yanjie Zhao , Hongjie Chen , Li Lu , Zhou Yang , Xiao Cheng , Haoyu Wang This is my paper
classification cs.SE
keywords neuro-symbolicvulnerability detectionLean 4large language modelsmemory safetyCWEobligation dischargestatic analysis
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

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.

Core claim

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.

What carries the argument

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.

Load-bearing premise

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.

What would settle it

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.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • 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.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 0 minor

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.

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 (4)
  1. 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.
  2. 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.
  3. 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).
  4. 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.

Circularity Check

0 steps flagged

No significant circularity: F1 gains are empirical measurements against external CVE labels and independent baselines, not quantities forced by construction from fitted inputs or self-citation.

full rationale

LeanGuard's central claim is an empirical F1 improvement over pure-LLM and agentic baselines on 801 labeled functions drawn from PrimeVul/ReposVul/R2Vul. The pipeline (AST extraction, constrained LLM fact editing, deterministic auto-pairing, Lean 4 kernel discharge, evidence-aware adjudication) is an engineered architecture, not a first-principles derivation that reduces a predicted quantity to its own inputs. Hand-built per-CWE pairing rules (Table II), risk lexicons for γ/Force-Keep, and the asymmetric adjudication matrix (Table III) are design choices that define system behavior; they do not fit a free parameter to a subset of the evaluation metric and then re-report that metric as a prediction. Lean kernel outcomes are machine-checked over the compiled model, which is independent evidence of structural consistency of the encoded claims, not a self-citation uniqueness theorem. Ablations and multi-run statistics further treat the method as an external system under test. Concerns that the custom rules are uncompared to Infer/CodeQL/Coverity are external-validity and correctness risks, not circularity under the stated patterns. No self-definitional loop, fitted-input-as-prediction, load-bearing self-citation uniqueness claim, or renaming of a known result as a forced derivation is present.

Axiom & Free-Parameter Ledger

3 free parameters · 4 axioms · 2 invented entities

The empirical claim rests on engineering axioms about what counts as an entity/protection/obligation per CWE, high-recall AST extraction, constrained LLM edits, deterministic pairing, and a hand-designed adjudicator for partial models—not on free physical constants. Invented structure is the unified Verification Model and quality grades that mediate incomplete context.

free parameters (3)
  • Syntactic confidence tag γ ∈ {High, Low}
    Assigned via CWE-specific risk lexicons after Stage 1; High forces Force-Keep and feeds strong symbolic grade. Lexicon membership is hand-curated, not learned from the evaluation metric.
  • Adjudication matrix cells (VLean, QLean, VLLM, QLLM, |O|)
    Table III (and class variants) encode when structural evidence overrides neural SAFE and when noisy unproved claims are downgraded. Matrix design is author-chosen and load-bearing for final labels.
  • Single refinement round triggers
    Conflict-driven and empty-model retry conditions (Stage 5) are fixed heuristics that can change which facts reach Lean.
axioms (4)
  • domain assumption Memory-safety detection for the five CWEs can be cast as obligation discharge under a shared model M=⟨E,P,O⟩ with class-specific ≺safe and ⊢CWE.
    Stated in §IV-A and Table I; enables one Lean kernel for heterogeneous weaknesses.
  • domain assumption Stage-1 AST/regex extraction is over-approximate and high-recall enough that false negatives there are the main unrecoverable failure mode.
    §IV-B; justifies Force-Keep and treating missing context conservatively rather than as safety.
  • ad hoc to paper An unproved obligation in a partial function-level model is not yet a defect and must be fused with neural evidence quality.
    Core design of Stage 6; without it VLean would be the final label and false positives would dominate incomplete context.
  • standard math Lean 4 kernel acceptance of discharged claims is a trustworthy structural check over the compiled model (not over raw C).
    §IV-E; standard trust in the Lean kernel for the encoded propositions only.
invented entities (2)
  • Verification Model M=⟨E, P, O⟩ with claims c=⟨o, Po⟩ no independent evidence
    purpose: Unify five CWE classes into one kernel-checkable obligation/protection interface.
    Introduced in §IV-A; independent of any single prior analyzer’s IR.
  • Evidence grades QLean ∈ {strong, weak, noisy, none} and QLLM ∈ {strong, weak, none} no independent evidence
    purpose: Mediate partial symbolic models and neural bias in the final adjudicator.
    §IV-G; grades are defined by paper-specific noise/high-risk lexicons.

pith-pipeline@v1.1.0-grok45 · 26768 in / 3191 out tokens · 31043 ms · 2026-07-11T22:41:58.903343+00:00 · methodology

0 comments
read the original abstract

Ask a large language model (LLM) whether a pointer dereference is safe, and it can often produce a plausible justification for ``yes''. The difficulty is that a fluent justification is not a proof. This gap is precisely where automated vulnerability detection lives: deciding, for a given operation in source code, whether a memory safety defect such as a null dereference, use-after-free, or double free can actually occur. We trace the unreliability of LLM-based vulnerability detection to a mechanism, the premature discharge of safety obligations, and argue that the remedy is not better prompting but a separation of roles: the component that interprets the code must not also be the one that decides a safety obligation is met. In this paper, we present LeanGuard, a neuro-symbolic framework that assigns each act to the side equipped for it. On the neural side, an LLM serves strictly as a semantic filter over candidate facts extracted from the abstract syntax tree (AST): it prunes spurious facts and keeps the real ones, but never discharges an obligation or decides the verdict on its own. On the symbolic side, the surviving facts are compiled into a verification model in Lean 4 (a formal proof assistant whose kernel accepts a conclusion only when it is formally proved), where every dangerous operation must be matched by a guard that provably covers it in scope; absent such a guard, the obligation stays open rather than being argued away. Because a function rarely arrives with full context, this symbolic model is necessarily partial: an unproved obligation is not yet a defect. An evidence-aware adjudicator therefore weighs the symbolic and neural verdicts by the quality of each. We instantiate the framework on five CWE classes to ask how far this division of labor can be pushed.

Figures

Figures reproduced from arXiv: 2607.03963 by Haoyu Wang, Hongjie Chen, Li Lu, Xiao Cheng, Yanjie Zhao, Zhou Yang.

Figure 1
Figure 1. Figure 1: Overview of the LEANGUARD framework. • E is the set of Entities, the components whose safety￾relevant state is tracked (e.g., pointer variables, allocated buffer objects). Every protection and obligation is bound to one such entity through an evaluation function ent(·). • P is the set of Protections, the explicit program operations or state guards that establish safety properties (e.g., nullity validation,… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references · 12 linked inside Pith

  1. [1]

    Qlpro: Automated code vulnerability discovery via LLM and static code analysis integration,

    “Qlpro: Automated code vulnerability discovery via LLM and static code analysis integration,”CoRR, vol. abs/2506.23644, 2025, withdrawn. [Online]. Available: https://doi.org/10.48550/arXiv.2506.23644

    Pith/arXiv arXiv doi:10.48550/arxiv.2506.23644 2025

  2. [2]

    SecVulEval: Benchmarking LLMs for Real-world C/C++ Vulnerability Detection,

    M. B. U. Ahmed, N. S. Harzevili, J. Shin, H. V . Pham, and S. Wang, “SecVulEval: Benchmarking LLMs for Real-world C/C++ Vulnerability Detection,” 2025. [Online]. Available: https://arxiv.org/abs/2505.19828

    Pith/arXiv arXiv 2025

  3. [3]

    Claude code: Agentic coding assistant,

    Anthropic, “Claude code: Agentic coding assistant,” https://docs. anthropic.com/en/claude-code, 2026, iDE-integrated autonomous coding agent built on Claude large language models

    2026

  4. [4]

    Claude Mythos,

    Anthropic, “Claude Mythos,” https://www.anthropic.com/claude/mythos, 2026

    2026

  5. [5]

    A few billion lines of code later: using static analysis to find bugs in the real world,

    A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Gros, A. Kamsky, S. McPeak, and D. R. Engler, “A few billion lines of code later: using static analysis to find bugs in the real world,” Commun. ACM, vol. 53, no. 2, pp. 66–75, 2010. [Online]. Available: https://doi.org/10.1145/1646353.1646374

    doi:10.1145/1646353.1646374 2010

  6. [6]

    CVEfixes: Automated Collection of Vulnerabilities and Their Fixes from Open-source Software,

    G. P. Bhandari, A. Naseer, and L. Moonen, “CVEfixes: Automated Collection of Vulnerabilities and Their Fixes from Open-source Software,”CoRR, vol. abs/2107.08760, 2021. [Online]. Available: https://arxiv.org/abs/2107.08760

    Pith/arXiv arXiv 2021

  7. [7]

    A benchmark for vericoding: formally verified program synthesis,

    S. Bursuc, T. Ehrenborg, S. Lin, L. Astefanoaei, I. E. Chiosa, J. Kukovec, A. Singh, O. Butterley, A. Bizid, Q. Dougherty, M. Zhao, M. Tan, and M. Tegmark, “A benchmark for vericoding: formally verified program synthesis,”CoRR, vol. abs/2509.22908, 2025. [Online]. Available: https://doi.org/10.48550/arXiv.2509.22908

    doi:10.48550/arxiv.2509.22908 2025

  8. [8]

    DiverseVul: A New Vulnerable Source Code Dataset for Deep Learning Based Vulnerability Detection,

    Y . Chen, Z. Ding, X. Chen, and D. A. Wagner, “DiverseVul: A New Vulnerable Source Code Dataset for Deep Learning Based Vulnerability Detection,”CoRR, vol. abs/2304.00409, 2023. [Online]. Available: https://doi.org/10.48550/arXiv.2304.00409

    Pith/arXiv arXiv doi:10.48550/arxiv.2304.00409 2023

  9. [9]

    Training verifiers to solve math word problems,

    K. Cobbe, V . Kosaraju, M. Bavarian, M. Chen, H. Jun, L. Kaiser, M. Plappert, J. Tworek, J. Hilton, R. Nakano, C. Hesse, and J. Schulman, “Training verifiers to solve math word problems,”CoRR, vol. abs/2110.14168, 2021. [Online]. Available: https://arxiv.org/abs/ 2110.14168

    Pith/arXiv arXiv 2021

  10. [10]

    Linux kernel vulnerability statistics for 2024,

    CVE Details, “Linux kernel vulnerability statistics for 2024,” https://www.cvedetails.com/vulnerability-list/vendor id-33/product id-47/year-2024/Linux-Linux-Kernel.html, 2024, accessed: 2026-06- 30

    2024

  11. [11]

    Deepseek-v4: Towards highly efficient million- token context intelligence,

    DeepSeek-AI, “Deepseek-v4: Towards highly efficient million- token context intelligence,” https://huggingface.co/deepseek-ai/ DeepSeek-V4-Pro, 2026

    2026

  12. [12]

    Neural networks and the chomsky hierarchy,

    G. Del ´etang, A. Ruoss, J. Grau-Moya, T. Genewein, L. K. Wenliang, E. Catt, C. Cundy, M. Hutter, S. Legg, J. Veness, and P. A. Ortega, “Neural networks and the chomsky hierarchy,” inThe Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net, 2023. [Online]. Available: https://openreview.net...

    2023

  13. [13]

    Vulnerability Detection with Code Language Models: How Far Are We?

    Y . Ding, Y . Fu, O. Ibrahim, C. Sitawarin, X. Chen, B. Alomair, D. A. Wagner, B. Ray, and Y . Chen, “Vulnerability Detection with Code Language Models: How Far Are We?”CoRR, vol. abs/2403.18624,

    Pith/arXiv arXiv

  14. [14]

    Available: https://doi.org/10.48550/arXiv.2403.18624

    [Online]. Available: https://doi.org/10.48550/arXiv.2403.18624

    Pith/arXiv arXiv doi:10.48550/arxiv.2403.18624

  15. [15]

    A C/C++ Code Vulnerability Dataset with Code Changes and CVE Summaries,

    J. Fan, Y . Li, S. Wang, and T. N. Nguyen, “A C/C++ Code Vulnerability Dataset with Code Changes and CVE Summaries,” inMSR ’20: 17th International Conference on Mining Software Repositories, Seoul, Republic of Korea, 29-30 June, 2020, S. Kim, G. Gousios, S. Nadi, and J. Hejderup, Eds. ACM, 2020, pp. 508–512. [Online]. Available: https://doi.org/10.1145/33...

    doi:10.1145/3379597.3387501 2020

  16. [16]

    Codebert: A pre-trained model for programming and natural languages,

    Z. Feng, D. Guo, D. Tang, N. Duan, X. Feng, M. Gong, L. Shou, B. Qin, T. Liu, D. Jiang, and M. Zhou, “Codebert: A pre-trained model for programming and natural languages,” inFindings of the Association for Computational Linguistics: EMNLP 2020, Online Event, 16-20 November 2020, ser. Findings of ACL, T. Cohn, Y . He, and Y . Liu, Eds., vol. EMNLP 2020. As...

    doi:10.18653/v1/2020.findings-emnlp.139 2020

  17. [17]

    Codeql: Semantic code analysis engine for security vul- nerability detection,

    GitHub, Inc., “Codeql: Semantic code analysis engine for security vul- nerability detection,” https://codeql.github.com/, 2026, accessed: 2026- 06-26, Relational static analysis tool supporting C/CWE vulnerability checking

    2026

  18. [18]

    From Naptime to Big Sleep: Using large language models to catch vulnerabilities in real-world code,

    Google Project Zero, “From Naptime to Big Sleep: Using large language models to catch vulnerabilities in real-world code,” https://projectzero. google/2024/10/from-naptime-to-big-sleep.html, 2024

    2024

  19. [19]

    Deepseek-coder: When the large language model meets programming - the rise of code intelligence,

    D. Guo, Q. Zhu, D. Yang, Z. Xie, K. Dong, W. Zhang, G. Chen, X. Bi, Y . Wu, Y . K. Li, F. Luo, Y . Xiong, and W. Liang, “Deepseek-coder: When the large language model meets programming - the rise of code intelligence,”CoRR, vol. abs/2401.14196, 2024. [Online]. Available: https://doi.org/10.48550/arXiv.2401.14196

    Pith/arXiv arXiv doi:10.48550/arxiv.2401.14196 2024

  20. [20]

    Large language models for software engineering: A systematic literature review,

    X. Hou, Y . Zhao, Y . Liu, Z. Yang, K. Wang, L. Li, X. Luo, D. Lo, J. Grundy, and H. Wang, “Large language models for software engineering: A systematic literature review,”ACM Trans. Softw. Eng. Methodol., vol. 33, no. 8, Dec. 2024. [Online]. Available: https://doi.org/10.1145/3695988

    doi:10.1145/3695988 2024

  21. [21]

    Fact-aligned and template-constrained static analyzer rule enhancement with llms,

    Z. Jiang, M. Wen, G. Wen, and H. Jin, “Fact-aligned and template-constrained static analyzer rule enhancement with llms,” in 40th IEEE/ACM International Conference on Automated Software Engineering, ASE 2025, Seoul, Korea, Republic of, November 16-20, 2025. IEEE, 2025, pp. 1642–1654. [Online]. Available: https://doi.org/10.1109/ASE63991.2025.00138

    doi:10.1109/ase63991.2025.00138 2025

  22. [22]

    Detecting false alarms from automatic static analysis tools: How far are we?

    H. J. Kang, K. L. Aw, and D. Lo, “Detecting false alarms from automatic static analysis tools: How far are we?” in44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022. ACM, 2022, pp. 698–709. [Online]. Available: https://doi.org/10.1145/3510003.3510214

    doi:10.1145/3510003.3510214 2022

  23. [23]

    seL4: formal verification of an os kernel

    G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. A. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood, “seL4: formal verification of an os kernel.” inProceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, J. N. Matthews a...

    doi:10.1145/1629575.1629596 2009

  24. [24]

    Formal verification of a realistic compiler,

    X. Leroy, “Formal verification of a realistic compiler,”Commun. ACM, vol. 52, no. 7, pp. 107–115, 2009. [Online]. Available: https://doi.org/10.1145/1538788.1538814

    doi:10.1145/1538788.1538814 2009

  25. [25]

    CleanVul: Automatic Function-level Vulnerability Detection in Code Commits Using LLM Heuristics,

    Y . Li, T. Zhang, R. Widyasari, Y . N. Tun, H. H. Nguyen, T. Bui, I. C. Irsan, Y . Cheng, X. Lan, H. W. Ang, F. Liauw, M. Weyssow, H. J. Kang, E. L. Ouh, L. K. Shar, and D. Lo, “CleanVul: Automatic Function-level Vulnerability Detection in Code Commits Using LLM Heuristics,”CoRR, vol. abs/2411.17274, 2024. [Online]. Available: https://doi.org/10.48550/arX...

    Pith/arXiv arXiv doi:10.48550/arxiv.2411.17274 2024

  26. [26]

    IRIS: llm-assisted static analysis for detecting security vulnerabilities,

    Z. Li, S. Dutta, and M. Naik, “IRIS: llm-assisted static analysis for detecting security vulnerabilities,” inThe Thirteenth International Conference on Learning Representations, ICLR 2025, Singapore, April 24-28, 2025. OpenReview.net, 2025. [Online]. Available: https://openreview.net/forum?id=9LdJDU7E91

    2025

  27. [27]

    Cppcheck: Static analysis tool for c/c++,

    D. Marjam ¨aki and C. Developers, “Cppcheck: Static analysis tool for c/c++,” https://cppcheck.sourceforge.io/, 2026, accessed: 2026-06-26, Open-source static analyzer detecting undefined behavior, memory flaws and CWE vulnerabilities

    2026

  28. [28]

    Tree-sitter: An incremental parsing system for programming tools,

    Max Brunsfeld et al., “Tree-sitter: An incremental parsing system for programming tools,” https://tree-sitter.github.io/tree-sitter/, 2024, ac- cessed: 2026-06-26

    2024

  29. [29]

    Infer: A static analyzer for Java, C, C++, and Objective-C,

    Meta, “Infer: A static analyzer for Java, C, C++, and Objective-C,” https://fbinfer.com/, 2026

    2026

  30. [30]

    The lean 4 theorem prover and programming language,

    L. d. Moura and S. Ullrich, “The lean 4 theorem prover and programming language,” inAutomated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Berlin, Heidelberg: Springer- Verlag, 2021, p. 625–635. [Online]. Available: https://doi.org/10.1007/ 978-3-030-79876-5 37

    2021

  31. [31]

    Vulnerability search results: Linux Kernel and CWE-476 (NULL pointer dereference),

    National Vulnerability Database, “Vulnerability search results: Linux Kernel and CWE-476 (NULL pointer dereference),” https://nvd.nist.gov/vuln/search/results?form type=Advanced&cpe vendor=cpe%3A2.3%3Ao%3Alinux&cpe product=cpe%3A2.3% 3Ao%3Alinux%3Alinux kernel&cwe id=CWE-476, 2024, accessed: 2026-06-30

    2024

  32. [32]

    Introducing codex,

    OpenAI, “Introducing codex,” https://openai.com/research/codex, 2021, accessed: 2026-06-25

    2021

  33. [33]

    APOLLO: Automated LLM and lean collaboration for advanced formal reasoning,

    A. Ospanov, F. Farnia, and R. Yousefzadeh, “APOLLO: Automated LLM and lean collaboration for advanced formal reasoning,” inThe Thirty-ninth Annual Conference on Neural Information Processing Systems, 2026. [Online]. Available: https://openreview.net/forum?id= fxDCgOruk0

    2026

  34. [34]

    Battles with false positives in static analysis of javascript web applications in the wild,

    J. Park, I. Lim, and S. Ryu, “Battles with false positives in static analysis of javascript web applications in the wild,” inProceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016 - Companion Volume, L. K. Dillon, W. Visser, and L. A. Williams, Eds. ACM, 2016, pp. 61–70. [Online]. Available: h...

    doi:10.1145/2889160.2889227 2016

  35. [35]

    Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,

    Z. Z. Ren, Z. Shao, J. Song, H. Xin, H. Wang, W. Zhao, L. Zhang, Z. Fu, Q. Zhu, D. Yang, Z. F. Wu, Z. Gou, S. Ma, H. Tang, Y . Liu, W. Gao, D. Guo, and C. Ruan, “Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition,”CoRR, vol. abs/2504.21801, 2025. [Online]. Available: https://doi.org/10.48550/ar...

    Pith/arXiv arXiv doi:10.48550/arxiv.2504.21801 2025

  36. [36]

    Sakana Fugu: One model to command them all,

    Sakana AI, “Sakana Fugu: One model to command them all,” https: //sakana.ai/fugu-release/, 2026

    2026

  37. [37]

    Coverity static analysis,

    Synopsys, “Coverity static analysis,” https://www.synopsys.com/ software-integrity/security-testing/static-analysis-sast.html, 2026

    2026

  38. [38]

    Common weakness enumeration (cwe),

    The MITRE Corporation, “Common weakness enumeration (cwe),” https://cwe.mitre.org/, 2024, accessed: 2026-06-26, Community- developed taxonomy of software security weaknesses

    2024

  39. [39]

    2025 cwe top 25 most dangerous software weaknesses,

    ——, “2025 cwe top 25 most dangerous software weaknesses,” https: //cwe.mitre.org/top25/archive/2025/2025 cwe top25, 2025

    2025

  40. [40]

    Cve metrics: Published cve records statistics,

    ——, “Cve metrics: Published cve records statistics,” https://www.cve. org/about/Metrics, 2026

    2026

  41. [41]

    Cwe-416: Use after free,

    ——, “Cwe-416: Use after free,” https://cwe.mitre.org/data/definitions/ 416.html, 2026, accessed: 2026-06-25, Common Weakness Enumeration (CWE)

    2026

  42. [42]

    LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks,

    S. Ullah, M. Han, S. Pujar, H. Pearce, A. K. Coskun, and G. Stringhini, “LLMs Cannot Reliably Identify and Reason About Security Vulnerabilities (Yet?): A Comprehensive Evaluation, Framework, and Benchmarks,” inIEEE Symposium on Security and Privacy, SP 2024, San Francisco, CA, USA, May 19-23, 2024. IEEE, 2024, pp. 862–880. [Online]. Available: https://do...

    doi:10.1109/sp54263.2024.00210 2024

  43. [43]

    Beyond notations: Hygienic macro expansion for theorem proving languages,

    S. Ullrich and L. de Moura, “Beyond notations: Hygienic macro expansion for theorem proving languages,”Log. Methods Comput. Sci., vol. 18, no. 2, 2022. [Online]. Available: https://doi.org/10.46298/ lmcs-18(2:1)2022

    2022

  44. [44]

    ReposVul: A Repository-level High-quality Vulnerability Dataset,

    X. Wang, R. Hu, C. Gao, X. Wen, Y . Chen, and Q. Liao, “ReposVul: A Repository-level High-quality Vulnerability Dataset,” inProceedings of the 2024 IEEE/ACM 46th International Conference on Software Engineering: Companion Proceedings, ICSE Companion 2024, Lisbon, Portugal, April 14-20, 2024. ACM, 2024, pp. 472–483. [Online]. Available: https://doi.org/10....

    doi:10.1145/3639478.3647634 2024

  45. [45]

    R2Vul: Learning to Reason about Software Vulnerabilities with Reinforcement Learning and Structured Reasoning Distillation,

    M. Weyssow, C. Yang, J. Chen, Y . Li, H. Huang, R. Widyasari, H. W. Ang, F. Liauw, E. L. Ouh, L. K. Shar, and D. Lo, “R2Vul: Learning to Reason about Software Vulnerabilities with Reinforcement Learning and Structured Reasoning Distillation,”CoRR, vol. abs/2504.04699,

    Pith/arXiv arXiv

  46. [46]

    Available: https://doi.org/10.48550/arXiv.2504.04699

    [Online]. Available: https://doi.org/10.48550/arXiv.2504.04699

    Pith/arXiv arXiv doi:10.48550/arxiv.2504.04699

  47. [47]

    Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,

    H. Xin, Z. Z. Ren, J. Song, Z. Shao, W. Zhao, H. Wang, B. Liu, L. Zhang, X. Lu, Q. Du, W. Gao, H. Zhang, Q. Zhu, D. Yang, Z. Gou, Z. F. Wu, F. Luo, and C. Ruan, “Deepseek-prover-v1.5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search,” in The Thirteenth International Conference on Learning Representations, ICLR 202...

    2025

  48. [48]

    Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving,

    R. Xin, C. Xi, J. Yang, F. Chen, H. Wu, X. Xiao, Y . Sun, S. Zheng, and M. Ding, “Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving,” inProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2025, Vienna, Austria, July 27 - August 1, 2025, W. Che, J. Nabende, E...

    doi:10.18653/v1/2025.acl-long.1565 2025

  49. [49]

    Large language models for cyber security: A systematic literature review,

    H. Xu, S. Wang, N. Li, K. Wang, Y . Zhao, K. Chen, T. Yu, Y . Liu, and H. Wang, “Large language models for cyber security: A systematic literature review,”ACM Trans. Softw. Eng. Methodol., Sep. 2025, just Accepted. [Online]. Available: https://doi.org/10.1145/3769676

    doi:10.1145/3769676 2025