Hybrid Approach Combines LLM Ghost Code with Symbolic Execution to Handle Complex Program Analysis

Symbolic execution, a technique that analyzes programs by exploring multiple execution paths simultaneously, has long struggled with certain types of code that confound traditional constraint solvers. A new framework called Gordian attempts to overcome these limitations by strategically deploying large language models to generate lightweight helper code—called "ghost code"—that makes hard problems easier for solvers to crack.

The Challenge#

Symbolic execution works well for many program analysis tasks, but hits a wall when dealing with fragments that are particularly hostile to automated solvers, complex numerical computations that are hard to reason about formally, and dynamically allocated memory structures with unclear bounds. Recent proposals to replace solvers with LLMs outright sidestep these limitations but introduce new ones: they struggle to maintain logical consistency across deeply nested execution paths in real codebases where many constraints interact.

The Gordian Solution#

Rather than replacing solvers, Gordian keeps them as the primary reasoning engine while using LLMs judiciously. The framework generates three categories of helper code to smooth the solver's path:

• Inversion of difficult fragments using iterative constraint propagation in both directions
• Surrogate modeling that replaces complex operations with solver-friendly approximations while preserving behavioral correctness
• Semantic partitioning of unbounded heap structures to make memory reasoning tractable

The team integrated Gordian into KLEE, an existing symbolic execution engine, and tested it against synthetic benchmarks designed to expose symbolic reasoning challenges, the FDLibM mathematical library, and real-world programs including libexpat, jq, bc, and libyaml.

Results#

Across test cases, Gordian achieved 28.5–115.2% coverage improvement over traditional symbolic execution and 74.1–189.8% over pure LLM approaches. Notably, the hybrid method reduced LLM token consumption by 91–96% on average, making the approach practical for real deployments.

The work demonstrates that carefully orchestrated collaboration between solvers and language models—rather than wholesale replacement—offers a path forward for program analysis at scale.