REVIEW 5 cited by
Python Symbolic Execution with LLM-powered Code Generation
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original 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.
Forward citations
Cited by 5 Pith papers
-
Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming
VLP adds an NL documentation layer with trace-linked mismatch detection and derived formal checks to make human validation of LLM code feasible, lifting pass@1 from 28.7-73.2% to 65.4-93.5%.
-
ConcoLixir: Reactive LLM Discovery Oracles for Python Concolic Testing
ConcoLixir uses a reactive LLM oracle to improve line coverage in Python concolic testing by 8.6 to 17 percentage points on synthetic, real-world, and library targets.
-
Can Large Language Models Reason About Complex Execution Paths? An Empirical Study on Python
State-of-the-art LLMs solve over 60% of complex Python path constraints in test generation, but their path classification is unreliable, especially for infeasible paths.
-
Can LLMs Replace Humans During Code Chunking?
LLM-generated partitions of legacy code yield documentation that LLM judges rate as up to 20% more factual and up to 10% more useful than documentation based on human expert partitions.
-
A Neuro-Symbolic Framework for Accountability in Public-Sector AI
A framework combining legal ontology, rule extraction, and solver reasoning verifies whether AI explanations for CalFresh eligibility align with statutory constraints.
Discussion (0). Sign in to comment.