{"id":"dc3751a6-a0d1-4613-a6fa-296b3cae3b24","arxiv_id":"2606.00669","paper_version":1,"verdict":"UNVERDICTED","confidence":"LOW","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":1,"one_line_summary":"NeuroLog is a build-free neuro-symbolic pipeline that extracts facts via LLM, composes them in Datalog, filters with SMT, and synthesizes crashes to rediscover CVEs and find new memory-safety bugs in libraries like libarchive and curl.","lead":"NeuroLog uses an LLM to pull typed dataflow facts from individual C/C++ functions, then Datalog rules and SMT solving to find cross-function issues without needing a build. A smart generalist might read it for a practical example of mixing language models with formal tools to make vulnerability hunting more repeatable and less dependent on full compilation setups.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.3","headline":"LLM fact extraction may omit or hallucinate critical dataflow details that Datalog then composes unchecked","rationale":"The reader's weakest assumption matches the load-bearing point exactly. With only abstract-level information the low-confidence UNVERDICTED verdict is appropriate; the absence of fact-extraction validation is the clearest internal risk to the pipeline's soundness. No other assumption (SMT filtering, crash synthesis, no-build claim) is more fragile once the fact base is accepted.","tokens_in":1965,"tokens_out":327,"duration_ms":10953,"concrete_test":"For the curl 8.3.0 function(s) containing CVE-2023-38545, manually extract ground-truth typed dataflow facts (variables, types, flows, aliases); compare against the exact LLM facts used by the paper; compute precision and recall. If recall < 80% on critical flows, the end-to-end claim weakens.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim requires that per-function LLM facts are sufficiently accurate and complete for Soufflé rules to produce correct cross-function results that Z3 then filters. The pipeline has no independent oracle or quantitative audit of the fact base (precision/recall on typed dataflow, aliasing, or range facts) against manual ground truth on the evaluated code (curl, libarchive, stb, etc.). If extraction errors occur on the CVE functions, the reported ASan-confirmed findings could be the result of fortunate LLM outputs rather than reliable composition. The abstract and described method provide no such measurement.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.3","summary":"The paper presents NeuroLog, a build-free neuro-symbolic pipeline for C/C++ vulnerability discovery. An LLM extracts typed dataflow facts one function at a time; Soufflé Datalog rules compose them into cross-function findings; Z3 filters infeasible paths and emits SAT models; runtime range invariants from a handful of corpus seeds are folded in; and a second LLM agent synthesizes candidate crashing inputs that are validated by an ASan harness. The paper reports end-to-end rediscovery of eight CVE-class issues (including the CVSS-9.8 CVE-2023-38545 in curl 8.3.0) plus five memory-safety bugs on libarchive HEAD (four previously unreported), with upstream filings and merges.","tokens_in":2115,"tokens_out":609,"duration_ms":17426,"significance":"If the per-function LLM facts prove sufficiently accurate and complete, the approach offers a practical, auditable alternative to heavyweight static analyzers by avoiding build requirements while retaining symbolic composition and SMT filtering. The concrete ASan-confirmed rediscoveries, new bug reports with rapid upstream acknowledgment, and crash-synthesis examples (e.g., 102-byte stb_vorbis input) demonstrate end-to-end utility and provide falsifiable artifacts. The explicit separation of LLM fact extraction from Datalog/SMT reasoning is a strength that supports auditability.","major_comments":[{"comment":"The central claim that LLM-derived facts are accurate and complete enough for correct Datalog composition and Z3 filtering rests on an unverified assumption. No precision, recall, or error-rate measurements are reported for the typed dataflow, aliasing, or range facts extracted by the LLM against manual ground truth on the evaluated codebases (stb, curl, libarchive, libxml2, FFmpeg slice). Without such an oracle or quantitative audit of the fact base, the reported ASan-confirmed findings could result from fortunate LLM outputs rather than reliable pipeline behavior (abstract; pipeline description).","section":"Methodology / Evaluation"},{"comment":"The evaluation does not address the risk of post-hoc selection of libraries, functions, or corpus seeds. The abstract reports successes on a small set of named libraries but provides no counts of false positives, total queries attempted, or failure cases, making it difficult to assess the pipeline's overall reliability or generalizability.","section":"Abstract / Results"}],"minor_comments":[{"comment":"The description of the LLM prompt engineering, model choice, and temperature settings is minimal; expanding this would aid reproducibility of the fact-extraction step.","section":"Methodology"},{"comment":"Figure or table summarizing the exact Datalog rules and the Z3 encoding of the SAT models would clarify how the composition and filtering steps operate on the LLM facts.","section":"Pipeline description"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":{"model":"grok-4.3","summary":"We thank the referee for the constructive feedback emphasizing the need for quantitative validation of the LLM fact base and a more complete picture of evaluation outcomes. We address each major comment below and commit to revisions that directly respond to the concerns raised.","responses":[{"response":"We agree that the absence of precision/recall metrics against manual ground truth leaves the reliability of the fact-extraction step less quantified than ideal. The manuscript's primary validation is end-to-end: ASan-confirmed rediscovery of eight CVEs (including CVE-2023-38545) plus five new bugs with upstream acceptance. This provides evidence that the composed facts were sufficient for the reported outcomes, but does not directly measure per-fact accuracy. In revision we will add an appendix containing a manual audit on a stratified sample of functions drawn from the evaluated codebases, reporting precision and recall for dataflow, aliasing, and range facts. This will be performed by the authors on a held-out subset and presented with inter-annotator agreement notes.","revision_made":"yes","referee_comment":"[Methodology / Evaluation] The central claim that LLM-derived facts are accurate and complete enough for correct Datalog composition and Z3 filtering rests on an unverified assumption. No precision, recall, or error-rate measurements are reported for the typed dataflow, aliasing, or range facts extracted by the LLM against manual ground truth on the evaluated codebases (stb, curl, libarchive, libxml2, FFmpeg slice). Without such an oracle or quantitative audit of the fact base, the reported ASan-confirmed findings could result from fortunate LLM outputs rather than reliable pipeline behavior (abstract; pipeline description)."},{"response":"The libraries were chosen a priori as widely used open-source projects containing documented CVEs suitable for rediscovery experiments; the libarchive results were obtained on HEAD without prior knowledge of the specific bugs. Nevertheless, the manuscript reports only successful cases and omits aggregate statistics. We will revise the evaluation section to report: (i) total functions analyzed per library, (ii) total Datalog queries issued, (iii) number of findings before and after Z3 filtering, (iv) observed false-positive patterns (e.g., over-approximated aliasing), and (v) a brief discussion of failure modes encountered during development. These additions will be placed in the main evaluation section rather than an appendix.","revision_made":"yes","referee_comment":"[Abstract / Results] The evaluation does not address the risk of post-hoc selection of libraries, functions, or corpus seeds. The abstract reports successes on a small set of named libraries but provides no counts of false positives, total queries attempted, or failure cases, making it difficult to assess the pipeline's overall reliability or generalizability."}],"tokens_in":1715,"tokens_out":594,"duration_ms":18706,"standing_objections":[]},"desk_editor":{"model":"grok-4.3","letter":"NeuroLog's main result is an end-to-end run that re-finds eight CVE-class issues, including the CVSS-9.8 curl SOCKS5 overflow, plus five memory-safety bugs on libarchive HEAD (four new), all ASan-confirmed and some already fixed upstream. The pipeline skips the build step by letting an LLM pull typed dataflow facts per function, letting Souffle compose them across functions, Z3 filter with SMT, and a second LLM turn the surviving SAT model into a crashing input script. Runtime seeds from a few corpus runs add cheap range invariants.\n\nWhat is actually new is the LLM fact base, the no-build operation, and treating the SAT model as input to crash synthesis rather than a binary answer. The concrete library outcomes and quick upstream response on the cpio use-after-free show the pipeline can produce usable artifacts.\n\nThe soft spot is the missing audit on the LLM extraction step. The abstract gives extraction time and cost but no precision or recall numbers for the typed facts, aliasing, or ranges against ground truth on the evaluated functions. Without that measurement, the successes could rest on fortunate LLM outputs on the chosen seeds rather than reliable composition. The stress-test concern lands.\n\nThis is for readers working on practical security tooling who want build-free static analysis with auditable steps. Someone in program analysis or vulnerability discovery would get value from the library case studies and the way the pieces close the loop to a crash script.\n\nI would send it for peer review. The reported findings are specific enough to justify referee time even if the fact-base validation needs to be added.","headline":"NeuroLog reports concrete ASan-confirmed bugs from curl and libarchive via an LLM-Datalog-SMT no-build pipeline, but provides no quantitative check on LLM fact accuracy.","tokens_in":2648,"tokens_out":409,"would_cite":false,"duration_ms":17212,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.3","headline":"An LLM extracts per-function dataflow facts that Datalog composes and SMT filters to rediscover CVEs and synthesize crashes without building the code.","keywords":["vulnerability discovery","neuro-symbolic analysis","LLM fact extraction","Datalog composition","SMT filtering","crash synthesis","build-free analysis","C/C++ security"],"falsifier":"A case in which the LLM misses or invents a dataflow fact for a known vulnerability, causing the Datalog rules and SMT pass to produce either a false negative or an invalid finding that survives filtering.","tokens_in":2844,"feed_emoji":"🔍","tokens_out":797,"duration_ms":20208,"temperature":0.7,"pith_summary":"The paper presents NeuroLog as a build-free pipeline that lets an LLM pull typed dataflow facts from individual C/C++ functions one at a time. A Souffle Datalog mesh then links those facts into cross-function findings, Z3 SMT removes infeasible ones while producing SAT models, and a second LLM turns the models into Python programs that generate candidate inputs tested under AddressSanitizer. Runtime range invariants from a few corpus seeds are folded in to tighten the constraints at low cost. This layered approach matters because pure static tools demand compilable builds while standalone LLMs lose track of dataflow and invent details. The method rediscovers eight CVE-class issues including the CVSS-9.8 CVE-2023-38545 and reports five memory-safety bugs in libarchive HEAD, several of which received upstream fixes.","feed_headline":"LLM-Datalog-SMT pipeline rediscovers eight CVEs without builds","feed_subtitle":"Facts extracted per function are composed into findings, filtered by SMT, and turned into crashing inputs, finding new bugs in libarchive.","key_machinery":"The LLM-derived fact base composed by Souffle Datalog rules and refined by Z3 SMT solvers, with SAT models serving as direct input to LLM-based crash synthesis.","core_discovery":"NeuroLog assigns an LLM the task of extracting typed dataflow facts one function at a time from source code, uses a Datalog rule mesh to compose those facts into cross-function findings, applies Z3 to filter infeasible ones and emit SAT models, incorporates runtime invariants from seeds, and has a second LLM synthesize crashing inputs from the models. This end-to-end process rediscovers eight CVE-class issues including CVE-2023-38545 and surfaces five memory-safety bugs in libarchive HEAD, with several fixes merged upstream.","pith_inferences":["If fact extraction scales reliably to larger modules, the method could open static analysis to projects that resist standard builds.","SAT models produced as artifacts could supply high-quality seeds to fuzzers instead of relying solely on mutation.","Adding more classes of runtime evidence beyond range invariants might further reduce the SMT search space on complex codebases."],"forward_implications":["Static findings become concrete crashing inputs after a small number of LLM iterations that emit Python programs, as shown with a 102-byte stb_vorbis crash.","A handful of runtime seeds can eliminate a measurable fraction of the feasible set, such as 13.2 percent for the FFmpeg demuxer.","The pipeline operates on real libraries including curl 8.3.0 and libarchive HEAD without requiring any build step.","Extraction cost stays low, around 37 seconds and $0.005 on stb, while still surfacing actionable memory-safety issues that reach upstream acknowledgment in hours."],"fun_headline_variants":["LLM-Datalog-SMT pipeline finds eight CVEs without builds","NeuroLog composes LLM facts into eight CVE findings via SMT","Build-free NeuroLog rediscovers CVEs using datalog and SMT","Datalog and SMT filter LLM facts to rediscover eight CVEs"],"cache_read_input_tokens":64,"weakest_assumption_plain":"The LLM extracts accurate typed dataflow facts one function at a time that are complete enough for the Datalog rules to compose into correct cross-function findings without missing or inventing critical details.","fun_headline_variants_meta":{"raw":{"variants":["LLM-Datalog-SMT pipeline finds eight CVEs without builds","NeuroLog composes LLM facts into eight CVE findings via SMT","Build-free NeuroLog rediscovers CVEs using datalog and SMT","Datalog and SMT filter LLM facts to rediscover eight CVEs"]},"model":"grok-4.3","cost_usd":0.009993,"raw_usage":{"total_tokens":4474,"prompt_tokens":900,"num_sources_used":0,"completion_tokens":72,"cost_in_usd_ticks":99928000,"prompt_tokens_details":{"text_tokens":900,"audio_tokens":0,"image_tokens":0,"cached_tokens":64},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":3502,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":900,"tokens_out":72,"duration_ms":22412,"temperature":1.0,"reasoning_tokens":3502,"cache_read_input_tokens":64,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-06-28T18:36:48.883442+00:00","model_set":{"reader":"grok-4.3"},"falsifier":"A case in which the LLM misses or invents a dataflow fact for a known vulnerability, causing the Datalog rules and SMT pass to produce either a false negative or an invalid finding that survives filtering.","supporting_citations":[],"review_version":1}