Python Symbolic Execution with LLM-powered Code Generation

• URL: http://arxiv.org/abs/2409.09271v1
• Date: Sat, 14 Sep 2024 02:43:20 GMT
• Title: Python Symbolic Execution with LLM-powered Code Generation
• Authors: Wenhan Wang, Kaibo Liu, An Ran Chen, Ge Li, Zhi Jin, Gang Huang, Lei Ma,
• Abstract summary: 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.
• Score: 40.906079949304726
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution is a key technology in software testing, which generates test cases by collecting symbolic path constraints and then solving constraints with SMT solvers. Symbolic execution has been proven helpful in generating high-coverage test cases, but its limitations, e.g., the difficulties in solving path constraints, prevent it from broader usage in software testing. Moreover, symbolic execution has encountered many difficulties when applied to dynamically typed languages like Python, because it is extremely challenging to translate the flexible Python grammar into rigid solvers. To overcome the main challenges of applying symbolic execution in Python, we proposed an LLM-empowered agent, LLM-Sym, that automatically calls an SMT solver, Z3, to solve execution path constraints. Based on an introductory-level symbolic execution engine, our LLM agent can extend it to supporting programs with complex data type `list'. The core contribution of LLM-Sym is translating complex Python path constraints into Z3 code. To enable accurate path-to-Z3 translation, we design a multiple-step code generation pipeline including type inference, retrieval and self-refine. Our experiments demonstrate that LLM-Sym is capable of solving path constraints on Leetcode problems with complicated control flows and list data structures, which is impossible for the backbone symbolic execution engine. Our approach paves the way for the combination of the generation ability of LLMs with the reasoning ability of symbolic solvers, and opens up new opportunities in LLM-augmented test case generation.

Related papers

• 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)
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [11.612762531670212]
  Large language models (LLMs) have been successfully applied to a variety of coding tasks, including code generation, completion, and repair.<n>This paper investigates the capacity of LLMs to reason about worst-case executions in programs through symbolic constraints analysis.
  arXiv  Detail & Related papers  (2025-06-09T19:33:30Z)
• "Don't Do That!": Guiding Embodied Systems through Large Language Model-based Constraint Generation [40.61171036032532]
  Large language models (LLMs) have spurred interest in robotic navigation that incorporates complex constraints from natural language into the planning problem.<n>In this paper, we propose a constraint generation framework that uses LLMs to translate constraints into Python functions.<n>We show that these LLM-generated functions accurately describe even complex mathematical constraints, and apply them to point cloud representations with traditional search algorithms.
  arXiv  Detail & Related papers  (2025-06-04T22:47:53Z)
• Capturing Sparks of Abstraction for the ARC Challenge [0.10878040851637999]
  Even commercial Large Language Models (LLMs) struggle to 'understand' many of the problems. We demonstrate that 'Sparks of Abstraction' can be extracted from the LLM output. Both the arc-dsl-llm DSL framework and the Gemini LLM-generated data are made Open Source.
  arXiv  Detail & Related papers  (2024-11-17T23:40:00Z)
• Combining LLM Code Generation with Formal Specifications and Reactive Program Synthesis [0.7580487359358722]
  Large Language Models (LLMs) struggle with accuracy and are unsuitable for high-risk applications. We introduce a solution that divides the code generation into two parts; one to be handled by an LLM and one to be handled by formal methods-based program synthesis.
  arXiv  Detail & Related papers  (2024-09-18T15:59:06Z)
• Can Language Models Pretend Solvers? Logic Code Simulation with LLMs [3.802945676202634]
  Transformer-based large language models (LLMs) have demonstrated significant potential in addressing logic problems. This study delves into a novel aspect, namely logic code simulation, which forces LLMs to emulate logical solvers in predicting the results of logical programs.
  arXiv  Detail & Related papers  (2024-03-24T11:27:16Z)
• If LLM Is the Wizard, Then Code Is the Wand: A Survey on How Code Empowers Large Language Models to Serve as Intelligent Agents [81.60906807941188]
  Large language models (LLMs) are trained on a combination of natural language and formal language (code) Code translates high-level goals into executable steps, featuring standard syntax, logical consistency, abstraction, and modularity.
  arXiv  Detail & Related papers  (2024-01-01T16:51:20Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• LPML: LLM-Prompting Markup Language for Mathematical Reasoning [8.995617701116142]
  We propose a novel framework that integrates the Chain-of-Thought (CoT) method with an external tool (Python REPL) Our approach enables LLMs to write the markup language and perform advanced mathematical reasoning using only zero-shot prompting.
  arXiv  Detail & Related papers  (2023-09-21T02:46:20Z)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, Logic-LM, which integrates LLMs with symbolic solvers to improve logical problem-solving.
  arXiv  Detail & Related papers  (2023-05-20T22:25:38Z)
• Low-code LLM: Graphical User Interface over Large Language Models [115.08718239772107]
  This paper introduces a novel human-LLM interaction framework, Low-code LLM. It incorporates six types of simple low-code visual programming interactions to achieve more controllable and stable responses. We highlight three advantages of the low-code LLM: user-friendly interaction, controllable generation, and wide applicability.
  arXiv  Detail & Related papers  (2023-04-17T09:27:40Z)
• PAL: Program-aided Language Models [112.94785609781503]
  We present Program-Aided Language models (PaL) to understand natural language problems. PaL offloads the solution step to a programmatic runtime such as a Python interpreter. We set new state-of-the-art results in all 12 benchmarks.
  arXiv  Detail & Related papers  (2022-11-18T18:56:13Z)

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.