Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

• URL: http://arxiv.org/abs/2603.19239v1
• Date: Sat, 31 Jan 2026 07:14:57 GMT
• Title: Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
• Abstract summary: Gordian is a hybrid symbolic execution framework.<n>It generates lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments.<n>It improves coverage on average by 52-84% over traditional symbolic execution baselines.
• Score: 2.0890922389987683
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is a powerful program analysis technique, but its effectiveness is fundamentally limited by solver-hostile program fragments, complex numerical reasoning, and unbounded heap structures. Recent work proposed replacing constraint solvers with large language models (LLMs) to bypass these limitations, but such approaches struggle to analyze real-world codebases, where deep execution paths require globally consistent reasoning across many interacting constraints. We present Gordian, a hybrid symbolic execution framework that uses LLMs selectively to generate lightweight ghost code that aids an SMT solver in handling solver-hostile code fragments, while preserving its precise, global reasoning capability. In particular, we propose three types of ghost code: (1) inversion of difficult code fragments with iterative bidirectional constraint propagation, (2) modeling via solver-friendly surrogates while preserving relevant behavior, and (3) semantic partitioning of unbounded heap spaces. We implemented Gordian on top of the KLEE symbolic execution engine and evaluated it on synthetic "logic bombs" capturing distinct symbolic reasoning challenges, a popular mathematical library FDLibM, and three structured-input programs (libexpat, jq, and bc). Across all benchmarks, Gordian improves coverage on average by 52-84% over traditional symbolic execution baselines, and by 86-419% over LLM-based techniques, while reducing LLM token usage by an average of 90-96%. This highlights the practicality and effectiveness of this approach in real-world settings.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• RECON: An LLM-Enhanced Backward Constraint Analysis Framework [0.5424799109837065]
  In this paper, we present a novel large language model (LLM)-enhanced backward constraint analysis framework.<n>Our approach, titled RECON, performs backward path discovery from target method(s) to the application entry point(s), discovers method-level control-flow constraints, and leverages LLM reasoning to transform bytecode conditions into interpretable specifications.<n>Results demonstrate that our approach operates 5.8X faster than traditional symbolic execution, with a 100% success rate, while maintaining logical equivalence.
  arXiv  Detail & Related papers  (2026-06-09T00:09:50Z)
• EndoCoT: Scaling Endogenous Chain-of-Thought Reasoning in Diffusion Models [40.37673945173621]
  We propose Endogenous Chain-of-Thought (EndoCoT) as a novel framework to activate MLLMs' reasoning potential.<n>EndoCoT bridges latent thought states through an iterative thought guidance module, and then bridges these states to the DiT's denoising process.<n>Extensive evaluations across diverse benchmarks achieve an average accuracy of 92.1%, outperforming the strongest baseline by 8.3 percentage points.
  arXiv  Detail & Related papers  (2026-03-12T17:58:48Z)
• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  Inference-time compute has re-emerged as a practical way to improve LLM reasoning.<n>Most test-time scaling (TTS) algorithms rely on autoregressive decoding.<n>We propose Prism, an efficient TTS framework for dLLMs.
  arXiv  Detail & Related papers  (2026-02-02T09:14:51Z)
• Programming over Thinking: Efficient and Robust Multi-Constraint Planning [54.77940831026738]
  SCOPE is a framework that disentangles query-specific reasoning from generic code execution.<n>SCOPE achieves state-of-the-art performance while lowering cost and latency.
  arXiv  Detail & Related papers  (2026-01-14T02:58:07Z)
• Can Large Language Models Solve Path Constraints in Symbolic Execution? [32.45630887872447]
  We focus on investigating the possibility of adopting large language models (LLM) for path constraint solving.<n>We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification.<n>Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks.
  arXiv  Detail & Related papers  (2025-11-23T04:54:48Z)
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [7.658134651527103]
  Worst-case symbolic constraints analysis requires inferring the symbolic constraints that characterise worst-case program executions.<n>We show that even state-of-the-art large language models (LLMs) struggle when applied directly on this task.<n>We propose WARP, an innovative neurosymbolic approach that computes worst-case constraints on smaller concrete input sizes.
  arXiv  Detail & Related papers  (2025-06-09T19:33:30Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [30.938876549335067]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework.<n>A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic.<n> Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)
• Control Large Language Models via Divide and Conquer [94.48784966256463]
  This paper investigates controllable generation for large language models (LLMs) with prompt-based control, focusing on Lexically Constrained Generation (LCG) We evaluate the performance of LLMs on satisfying lexical constraints with prompt-based control, as well as their efficacy in downstream applications.
  arXiv  Detail & Related papers  (2024-10-06T21:20:06Z)
• Python Symbolic Execution with LLM-powered Code Generation [40.906079949304726]
  Symbolic execution is a key technology in software testing, which generates test cases by collecting symbolic path constraints. Symbolic execution has been proven helpful in generating high-coverage test cases, but its limitations prevent it from broader usage in software testing. We propose an agent, LLM-Sym, that automatically calls an SMT solver, Z3, to solve execution path constraints.
  arXiv  Detail & Related papers  (2024-09-14T02:43:20Z)
• Hierarchical Context Merging: Better Long Context Understanding for Pre-trained LLMs [61.40047491337793]
  We present Hierarchical cOntext MERging (HOMER), a new training-free scheme designed to overcome the limitations of large language models. HomeR uses a divide-and-conquer algorithm, dividing long inputs into manageable chunks. A token reduction technique precedes each merging, ensuring memory usage efficiency.
  arXiv  Detail & Related papers  (2024-04-16T06:34:08Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.