SymLift: Neural Semantic Lifting for Compile-Free Vulnerability Detection in Context-Incomplete Code Fragments

What it claims

SymLift detects vulnerabilities in C functions that cannot be compiled on their own. The authors' motivating case is code generated by an LLM or a function pulled out of a larger repository. A fine-tuned LLM does not predict a vulnerability label. Instead it writes a restricted LLVM-like IR. Explicit Soufflé Datalog rules then make every vulnerability judgment, so each finding links to supporting facts, a matched rule and a derivation trace. The paper was posted to arXiv on 25 October 2026 by authors from Peking University, NTU, Nanjing University and others.

The paper calls the problem it targets the "compilation gap." On Juliet, cutting complete programs down to function-level fragments drops the Clang compilation success rate from 100% to 12.00%. SymLift's analysis completion rate falls by only 1.17 percentage points in the same setting.

How it works

flowchart LR
  F[Target function] --> Q{Project sources?}
  Q -- yes --> C[Tree-sitter call graph, d=3, max 50 fns]
  Q -- no --> T[Target only]
  C --> L[Neural lifter: LLVM-like IR]
  T --> L
  L --> P[Deterministic parser: Base Facts, DefUse, ArrayAccess...]
  P --> D[Soufflé Datalog rules]
  D --> R[Findings + derivation traces]

• Context selection. When project sources exist, Tree-sitter builds direct-call edges only to unique project-local definitions. It keeps functions within 3 call edges, up to 50 including the target. Indirect, library and ambiguous calls add no edges. Each function is lifted separately, the facts are analyzed together, and findings that appear only in auxiliary functions are dropped.
• Inference without a compiler. Inference uses no Clang and no reference IR. Missing context is left out, not made up. Facts are extracted even when llvm-as would reject the IR.
• Fine-tuning stage 1 (structural fidelity). Training pairs C functions with Clang-generated IR. Token cross-entropy is combined with a policy-gradient term. Four outputs are sampled per input and get a reward of +1 if both llvm-as and the custom parser accept them, otherwise −1. The advantage is the reward minus the mean reward of the other three samples, clipped to [−2, 2]. The total loss is L_CE + 0.1·L_struct.
• Fine-tuning stage 2 (vulnerability-oriented). This stage trains on the FormAI training subset plus matched non-vulnerable functions. Augmentation uses variable renaming, reordering of independent statements and equivalent source rewrites.
• Rule families. The rules cover buffer overflow, memory leak, null pointer, division by zero, missing array check and resource leak. A rule can fire when there is evidence of an operation and no safety condition can be derived. One example is missing_bounds_check, which fires when CompleteBoundsGuard is absent.

Evidence

• FormAI, SymLift-Qwen-7B. The model reaches 87.83% overall relation-level IoU, 96.85% control-flow IoU and 94.41% Target-F1. That Target-F1 is 24.08 points above the strongest direct-LLM baseline, Gemini-3.5-Flash.
• MegaVul, six vulnerability families. Micro-averaged precision is 98.24% and micro-averaged Target-F1 is 91.66%.
• IR versus direct fact generation. The paper says Table VII compares the IR route against generating facts directly. That table is not in the fetched text.

How to use it

The authors publish the implementation and experimental data at https://figshare.com/s/cda7af5b537730fd7ab3. The page gives no install commands, weights licence or hardware figures. The evaluated configuration is Qwen-7B fine-tuned in the two stages described above.

Limits

• The authors say the IR layer does not remove uncertainty from neural lifting. It makes the reconstructed relations inspectable.
• Analysis completion does not establish semantic equivalence with the source. The structural reward checks validity and parser compatibility, not correctness.
• Datalog can only reason over relations the lifter actually recovers.
• Findings are local. The motivating example flags a missing lower bound without establishing that it is reachable from callers.
• The stage-2 training data comes from FormAI, which is also an evaluation benchmark.
• The fetched text stops partway through the training-data description, which mentions 12,980 items. The limitations, threats-to-validity and full results sections are not included.