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

What it is

SymLift (arXiv 2610.34431v1, 25 October 2026, Peking University with collaborators) is a neuro-symbolic vulnerability detector for C functions that cannot be compiled on their own. A fine-tuned LLM does not predict vulnerability labels. It only rewrites the function as a constrained LLVM-like IR. A deterministic parser and Souffle Datalog rules then make the findings. The authors say the implementation and data are on figshare (https://figshare.com/s/cda7af5b537730fd7ab3).

How it works

The pipeline has three stages.

1. Lifting. The target function is the unit of analysis. With project sources, Tree-sitter adds direct callees and callers within 3 call edges, up to 50 functions including the target. Indirect, ambiguous or library calls add no edges. Without project sources, only the target is used. Missing context is omitted, not invented.
2. Parsing. A deterministic parser validates the IR and turns supported operations into Base Facts (alloc, call, br_cond, icmp and others). It derives relations such as DefUse, Reachable, CallEdge and ArrayAccess. Inference does not require llvm-as to accept the IR.
3. Rules. Explicit Datalog rules cover buffer overflow, memory leak, null pointer, division by zero, missing array check and resource leak. Each finding links to its supporting facts, the matched rule and a derivation trace.

Training has two stages. Structural-fidelity fine-tuning uses C-to-Clang-IR pairs. It adds a policy-gradient reward (+1 if both llvm-as and the custom parser accept the output, -1 otherwise), with weight α = 0.1 on four samples per input. Vulnerability-oriented fine-tuning then uses the FormAI training subset with matched non-vulnerable functions and semantics-preserving augmentation.

The paper's example is a function with idx < count but no idx >= 0 check before ctx->entries[idx]. The rule emits missing_bounds_check because CompleteBoundsGuard cannot be derived.

flowchart LR
  A[C fragment] --> B[Fine-tuned LLM lifts to IR]
  B --> C{Parser accepts ops?}
  C -->|yes| D[Base Facts]
  C -->|no| E[Unsupported ops dropped or incomplete]
  D --> F[Datalog rules]
  F --> G[Finding + derivation trace]

Results

• Juliet reduced to function-level fragments: Clang compilation success falls from 100% to 12.00%. SymLift's analysis completion falls by only 1.17 points.
• FormAI, SymLift-Qwen-7B: control-flow IoU 96.85%, overall relation IoU 87.83%, Target-F1 94.41%. That is 24.08 points above the strongest direct-LLM baseline, listed as Gemini-3.5-Flash.
• MegaVul, six vulnerability families: micro precision 98.24%, micro Target-F1 91.66%.

Caveats

• Analysis completion is not semantic equivalence. The IR reward checks only that the IR is well-formed, not that it matches the source.
• The IR layer does not remove lifting uncertainty. It only makes the reconstructed relations inspectable. Datalog can reason only over the relations it receives.
• Determinism holds for fixed facts and rules. The LLM lifting step is still probabilistic.
• The detection numbers come after fine-tuning on FormAI, with Target-F1 as the metric. The fetched text is cut off before the baselines, the Table VII comparison with direct fact generation, and the limitations and threats-to-validity sections. I could not check those.
• The reachability of the flagged example across real calling contexts is not established.