Can Large Language Models Solve Path Constraints in Symbolic Execution?

• URL: http://arxiv.org/abs/2511.18288v1
• Date: Sun, 23 Nov 2025 04:54:48 GMT
• Title: Can Large Language Models Solve Path Constraints in Symbolic Execution?
• Abstract summary: 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.
• Score: 32.45630887872447
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is an important software analysis technique which benefits downstream tasks such as software testing and debugging. However, several limitations hinder symbolic execution from application on real-world software. One of the limitations is the inability to solve diverse execution path constraints: traditional symbolic execution based on SMT solvers is difficult to handle execution paths with complex data structures or external API calls. In this paper, we focus on investigating the possibility of adopting large language models (LLM) for path constraint solving instead of traditional solver-based techniques in symbolic execution. We conduct an empirical study to evaluate the ability of LLMs in two types of path constraint solving: generating test inputs to facilitate an execution path, and determining whether a given execution path can be satisfied without triggering any bugs. We build new evaluation pipelines and benchmarks for two tasks: test case generation and path classification, which include data sources from both competition-level programs and real-world repositories. Our experiment results show that state-of-the-art LLMs are able to solve path constraints in both generation and classification tasks, with 60% of generated test cases that accurately cover the given execution path. Moreover, LLMs are capable of improving test coverage by covering execution paths in real-world repositories where traditional symbolic execution tools cannot be applied. These findings highlight the possibility of extending symbolic execution techniques with LLMs in the future to improve the ability and generalizability of symbolic execution.

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)
• PeakBench: Benchmarking Resource-Aware Tool Invocation in LLM Agents [79.28372522980153]
  PeakBench is a benchmark of executable multi-tool dependency annotations and measured resource profiles.<n>We show that strong logical planning does not reliably translate into safe or efficient execution under resource constraints.<n>PeakBench is a useful testbed for diagnosing resource-aware agent behavior.
  arXiv  Detail & Related papers  (2026-08-25T12:56:08Z)
• RepoReasoner: Evaluating Repository-Level Code Reasoning Ability of Long-Context Language Models [54.53236295237077]
  We introduce RepoReasoner, a benchmark for evaluating repository-level code reasoning.<n> Output Prediction measures fine-grained, stateful execution reasoning across files.<n>Call Chain Prediction evaluates high-level architectural dependency understanding under noisy context.
  arXiv  Detail & Related papers  (2026-07-28T17:12:41Z)
• 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)
• Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code [2.0890922389987683]
  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.
  arXiv  Detail & Related papers  (2026-01-31T07:14:57Z)
• Environment-Aware Code Generation: How far are We? [52.69113158357018]
  It is unclear whether large language models (LLMs) can reliably generate executable code tailored to a user's specific environment.<n>We present the first systematic study of Environment-Aware Code Generation (EACG), where generated code must be functionally correct and directly executable under arbitrary software configurations.<n>Our results show that current LLMs struggle with environment-specific code generation, while our adaptations improve environment compatibility and executability.
  arXiv  Detail & Related papers  (2026-01-18T04:58:15Z)
• Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
  Large Language Models (LLMs) have evolved from simple text generators into complex software systems that integrate retrieval augmentation, tool invocation, and multi-turn interactions.<n>Their inherent non-determinism, dynamism, and context dependence pose fundamental challenges for quality assurance.<n>This paper decomposes LLM applications into a three-layer architecture: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, and textbftextitLLM Inference Core.
  arXiv  Detail & Related papers  (2025-08-28T13:00:28Z)
• Symbolic Execution in Practice: A Survey of Applications in Vulnerability, Malware, Firmware, and Protocol Analysis [3.1844358655583846]
  Symbolic execution is a powerful program analysis technique that allows for the systematic exploration of all program paths.<n>This paper introduces a systematic taxonomy of strategies to enable symbolic execution on complex software systems.<n>We survey applications of symbolic executions in several domains such as vulnerability analysis, malware analysis, firmware re-hosting, and network protocol analysis.
  arXiv  Detail & Related papers  (2025-08-08T18:43:45Z)
• Generating and Understanding Tests via Path-Aware Symbolic Execution with LLMs [8.828992823055]
  PALM is a test generation system that combines symbolic path enumeration with LLM-assisted test generation.<n>Palm helps users better understand path coverage and identify which paths are actually exercised by PALM-generated tests.
  arXiv  Detail & Related papers  (2025-06-24T03:46:16Z)
• Beyond Next Token Probabilities: Learnable, Fast Detection of Hallucinations and Data Contamination on LLM Output Distributions [60.43398881149664]
  We introduce LOS-Net, a lightweight attention-based architecture trained on an efficient encoding of the LLM Output Signature.<n>It achieves superior performance across diverse benchmarks and LLMs, while maintaining extremely low detection latency.
  arXiv  Detail & Related papers  (2025-03-18T09:04:37Z)
• Test Wars: A Comparative Study of SBST, Symbolic Execution, and LLM-Based Approaches to Unit Test Generation [11.037212298533069]
  Large Language Models (LLMs) have opened up new opportunities to generate tests automatically.<n>This paper studies automatic test generation approaches based on three tools: EvoSuite for SBST, Kex for symbolic execution, and TestSpark for LLM-based test generation.<n>Our results show that while LLM-based test generation is promising, it falls behind traditional methods in terms of coverage.
  arXiv  Detail & Related papers  (2025-01-17T13:48:32Z)
• Test-driven Software Experimentation with LASSO: an LLM Prompt Benchmarking Example [1.4685355149711299]
  Test-Driven Software Experiments ( TDSEs) involve the execution of software subjects and the observation and analysis of their "de facto" run-time behavior.<n>We present a general-purpose analysis platform called LASSO that provides a minimal set of domain-specific languages and data structures to conduct TDSEs.
  arXiv  Detail & Related papers  (2024-10-11T15:32:48Z)
• 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)
• DOCE: Finding the Sweet Spot for Execution-Based Code Generation [69.5305729627198]
  We propose a comprehensive framework that includes candidate generation, $n$-best reranking, minimum Bayes risk (MBR) decoding, and self-ging as the core components. Our findings highlight the importance of execution-based methods and the difference gap between execution-based and execution-free methods.
  arXiv  Detail & Related papers  (2024-08-25T07:10:36Z)
• Can Long-Context Language Models Subsume Retrieval, RAG, SQL, and More? [54.667202878390526]
  Long-context language models (LCLMs) have the potential to revolutionize our approach to tasks traditionally reliant on external tools like retrieval systems or databases. We introduce LOFT, a benchmark of real-world tasks requiring context up to millions of tokens designed to evaluate LCLMs' performance on in-context retrieval and reasoning. Our findings reveal LCLMs' surprising ability to rival state-of-the-art retrieval and RAG systems, despite never having been explicitly trained for these tasks.
  arXiv  Detail & Related papers  (2024-06-19T00:28:58Z)

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.