P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation

• URL: http://arxiv.org/abs/2608.09277v1
• Date: Mon, 10 Aug 2026 08:33:18 GMT
• Title: P$^{3}$: Joint Program-and-Proof Planning for Verified Code Generation
• Abstract summary: Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification.<n>We observe that this sequential pipeline can be both ineffective and inefficient in practice.<n>Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose $P3$.
• Score: 19.3449645807529
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verified code generation asks a large language model (LLM) to generate both an executable program and a machine-checkable proof that the program meets a formal specification, promising software that is correct by construction. The de facto workflow decouples the two halves of the problem: first synthesize a program, then attempt to prove it correct. We observe that this sequential pipeline can be both ineffective and inefficient in practice. A program generated without anticipating its proof can be subtly incorrect or structurally difficult to verify, forcing the LLM into brittle repair loops that alternate between patching the code and patching the proof. Inspired by Dijkstra's view that a program and its correctness argument should be developed hand in hand, we propose $P^3$, an LLM-based agentic workflow that first derives a unified program-and-proof plan from the specification, then elaborates the implementation and proof scaffold under this shared plan. To evaluate verified code generation in realistic settings, we further introduce Lean4Commit0, a repository-derived, library-level benchmark built by extracting core APIs from real-world software repositories and translating their requirements, including relational specifications across APIs, into Lean tasks. Using four frontier LLM backends, we evaluate $P^3$ on Verina, AlgoVeri, and our Lean4Commit0 benchmark, where it achieves the highest solve rate in every benchmark--model setting. Compared with the stronger baseline, it improves solve rates by 4.6--11.2 percentage points and reduces per-task API cost by up to roughly 40\% and wall-clock time by up to roughly 37\% on the difficult subset of each benchmark. A targeted ablation further shows gains of 3.3--8.3 points over implementation-only planning, isolating the benefit of planning the program and proof jointly.

Related papers

• Inferring Code Correctness from Specification [0.0]
  Large language models (LLMs) have become integral to modern software development, enabling automated code generation at scale.<n>We propose TRAILS (Targeted Reasoning Agreement via Inputs and Specifications), an approach that grounds LLM reasoning with concrete (input, output) pairs.<n>We evaluate TRAILS on two datasets, LiveCodeBench and CoCoClaNeL, across three LLMs (Qwen3Coder-30B, Devstral-Small-24B, and Olmo3.1-Instruct), comparing against HoarePrompt and a Zero-Shot Chain-of-Thought baseline.
  arXiv  Detail & Related papers  (2026-05-28T12:04:51Z)
• SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
  We introduce SCDBench, a dataset and benchmark methodology for smart contract decompilation.<n>The dataset contains 600 real-world Solidity contracts with paired bytecode inputs, ground-truth source code, and replayable semantic checkpoints.<n>We evaluate Claude Opus 4.7, GPT-5.3-Codex, and GLM-5 in a zero-shot decompilation setting, including GLM-5 variants with and without extended reasoning.
  arXiv  Detail & Related papers  (2026-05-27T20:08:47Z)
• SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
  We introduce a neuro-symbolic, scenario-based framework that bridges the gap between high-level program intent and the rigid syntactic constraints of pointer arithmetic and manual memory management.<n>We evaluate it on 59 real-world and algorithmic subjects, where it outperforms the vanilla prompt generation baseline by 31.36% in line coverage, 26.01% in branch coverage, and 20.78% in mutation score, matching or exceeding the symbolic execution tool KLEE.
  arXiv  Detail & Related papers  (2026-02-18T18:09:03Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• 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)
• Evaluating and Achieving Controllable Code Completion in Code LLM [89.64782747840225]
  We present the first instruction-guided code completion benchmark, Controllable Code Completion Benchmark (C3-Bench)<n>We reveal substantial gaps in instruction-following capabilities between open-source and advanced proprietary models during code completion tasks.<n>The resulting model, Qwen2.5-Coder-C3, achieves state-of-the-art performance on C3-Bench.
  arXiv  Detail & Related papers  (2026-01-22T11:40:04Z)
• 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)
• The 4/$δ$ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee [5.345468714252351]
  This work bridges the gap by developing an LLM-Verifier Convergence Theorem.<n>We model the interaction between the LLM and the verifier as a discrete-time Markov Chain.<n>We stress-tested this prediction in an extensive empirical campaign comprising more than 90,000 trials.
  arXiv  Detail & Related papers  (2025-11-30T22:19:09Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGE decomposes verification into three interconnected domains: Code, Specifications, and Proofs.<n>We show that this approach substantially improves both accuracy and efficiency beyond standard error feedback methods.
  arXiv  Detail & Related papers  (2025-11-26T06:39:19Z)
• Learning to Reason via Program Generation, Emulation, and Search [33.11955431589091]
  Program synthesis with language models (LMs) has unlocked a large set of reasoning abilities. Not all reasoning tasks are easily expressible as code, e.g. tasks involving commonsense reasoning, moral decision-making, and sarcasm understanding. We propose Code Generation and Emulated EXecution (CoGEX) to extend an LM's program synthesis skills to such tasks.
  arXiv  Detail & Related papers  (2024-05-25T19:40:50Z)
• LeTI: Learning to Generate from Textual Interactions [60.425769582343506]
  We explore LMs' potential to learn from textual interactions (LETI) that not only check their correctness with binary labels but also pinpoint and explain errors in their outputs through textual feedback. Our focus is the code generation task, where the model produces code based on natural language instructions. LETI iteratively fine-tunes the model, using the objective LM, on a concatenation of natural language instructions, LM-generated programs, and textual feedback.
  arXiv  Detail & Related papers  (2023-05-17T15:53:31Z)

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.