{"id":"7e6249f0-21ee-400c-9e63-da6116da278f","arxiv_id":"2608.09277","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Joint program-and-proof planning improves LLM-backed verified code generation solve rates by 4.6 to 11.2 points across 12 benchmark-model settings.","lead":"P³ is an LLM agent workflow that writes the program and its Lean 4 proof from a single shared plan, instead of writing code first and proving it later. Across four frontier models and three benchmarks it reports higher solve rates and lower cost than program-then-proof baselines, and introduces a new repository-derived benchmark, Lean4Commit0.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Headline solve-rate claim rests on an unvalidated LLM judge for instruction compliance (Appendix E Phase 6); if that judge is lenient or method-biased, all 4.6–11.2 pp deltas in Table 2 are unsupported.","rationale":"I read the paper in good faith. The central claim is a comparative effectiveness result, and the paper has real strengths: Lean kernel acceptance is an objective check of the formal artifact; the win pattern is consistent across all 12 benchmark-model cells; the ablation isolates joint planning from implementation-only planning; plan-retention statistics and case studies add mechanistic support; and the Figshare release enables reproduction. The efficiency claims are secondary; the core claim is solve-rate superiority. The most load-bearing unsecured link is the instruction-compliance judge. The paper itself (Appendix E Phase 6) defines success as PASS-MECHANICAL and PASS-INSTRUCTION; the latter is produced by an LLM whose accuracy is never assessed. Because the Verina/AlgoVeri instructions are not formalized, this is a genuinely subjective component in the definition of 'solved' for every method. A noisy or biased judge affects every number in Table 2 and the ablation. Single-run noise alone is less threatening given the consistent 12-cell pattern, but systematic judge bias is not addressed by that consistency. This is exactly the reader's weakest assumption, so I agree. A human audit with blinded annotators is the decisive check. If the audit passes, I would accept the empirical claim as stated; if it fails, the solve-rate claim must be downgraded. Thus the reader's CONDITIONAL verdict is appropriate and I leave it unchanged.","tokens_in":19100,"tokens_out":4817,"duration_ms":48839,"concrete_test":"Sample roughly 120 solved-task traces, e.g., 10 per (benchmark, method) cell, and have two human experts blind to method independently judge instruction compliance from the final Lean code alone, without seeing plans, prompts, or method labels. Compute agreement between the lean-verifier-instruction verdict and the human majority (Cohen's kappa), then recompute Table 2 deltas using human-only labels. If kappa is high (≥0.8) and the human-audited P3-minus-stronger-baseline delta remains ≥4.6 pp in every cell, the concern is resolved. If kappa is low or deltas shrink materially, the headline claim needs qualification or additional validation.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The evaluation's solve criterion is not purely kernel-checked. Section 5.1 augments every Verina and AlgoVeri task with a natural-language algorithmic/complexity instruction, and Table 2 counts a task as solved only if the solution 'satisfies the instruction' and passes Lean. That satisfaction check is performed by 'lean-verifier-instruction', an LLM subagent described in Appendix E Phase 6, which reads the @start code...@end code region and judges whether the implementation meets the instruction's algorithmic intent. This judge is used for all methods, but its reliability is never measured: no human agreement study, no calibration, no error analysis, and each configuration is run once (Section 5.1, Appendix C). A lenient judge would count as solved formal-spec-satisfying implementations that violate the stated algorithm, inflating every solve rate. More concerning, leniency could be method-correlated: P3's skill restates the instruction verbatim in the plan and emits plan-documented code, which may systematically persuade the same LLM judge more than the baselines' outputs, even when both are instruction-compliant. Because the claimed gains are 4.6–11.2 pp (roughly 9–21 tasks on n=189), a judge bias of that magnitude would erase the headline result. Consistency across 12 cells does not rule this out, since the same judge pipeline is shared across all cells. The formal part of the criterion is solid; the informal part is not.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes P3, an LLM agentic workflow for verified code generation in Lean 4 that first produces a joint program-and-proof plan and then elaborates both artifacts under that plan, in contrast to the usual program-then-proof schedule. It also introduces Lean4Commit0, a repository-derived benchmark of 108 libraries with relational specifications, and evaluates P3 against plain and program-then-proof baselines on Verina, AlgoVeri, and Lean4Commit0 using four LLM backends. The reported headline result is that P3 achieves the highest solve rate in all 12 benchmark-model cells, with gains of 4.6--11.2 percentage points over the stronger baseline, and reduces cost and wall-clock time on a difficult subset. The formal part of the solve criterion is Lean kernel acceptance, but the solve rate additionally requires that the implementation satisfy a natural-language algorithmic instruction, a condition judged by an LLM subagent whose reliability is not validated.","tokens_in":19389,"tokens_out":2869,"duration_ms":32610,"significance":"If the central claim holds, the paper makes a useful conceptual contribution: it gives evidence that planning the program and proof together, rather than committing to code first, improves both effectiveness and efficiency in LLM-based verified code generation. The introduction of Lean4Commit0 is a genuine benchmark contribution, with a documented specification-quality pipeline, relational cross-API specifications, and repository-derived tasks that go beyond textbook single-function benchmarks. The evaluation is broad in coverage (three benchmarks, four backends, an ablation, and trace-level analysis), and the formal success signal is machine-checked by the Lean kernel, which is an objective check for the formal component. The main weakness is that the informal component of the solve criterion -- instruction compliance -- is assessed by an unvalidated LLM judge, and all configurations are run only once, so the magnitude and robustness of the reported gains are not yet established.","major_comments":[{"comment":"The solve-rate claim rests on an LLM judge whose reliability is never measured. A task is counted as solved only if the solution \"satisfies the instruction and passes Lean's checker\" (Section 5.1), and the instruction-compliance check is performed by the subagent lean-verifier-instruction, which reads the code region and judges whether it meets the algorithmic intent (Appendix E, Phase 6). No human agreement study, calibration, false-positive analysis, or error analysis is reported for this judge, and each configuration is run once. Since the claimed gains are 4.6--11.2 percentage points, which on Verina (n=189) is roughly 9--21 tasks, a judge bias or leniency of that size would erase the headline result. This concern is method-correlated rather than merely shared across cells: P3 restates the instruction verbatim in its plan and emits plan-documented code, which may systematically influence the same LLM judge even when the output is no more compliant than a baseline's. I would need a validation of this judge -- for example, an independent human annotation of instruction compliance on a stratified sample of accepted and rejected solutions, with reported agreement and a per-cell false-positive rate -- before the Table 2 deltas can be taken at face value.","section":"§5.1, Table 2, Appendix E Phase 6"},{"comment":"The statistical basis for the central claim is a single run per (task, model, method) configuration. The paper acknowledges this in Appendix C, but the acknowledgment does not address the fact that the reported gaps are small relative to the expected stochastic variance of LLM agents. For example, a 5.2-point gain on Verina corresponds to about 10 tasks out of 189; with a single run, the 95% binomial confidence interval for a single method's solve rate is already about ±7 points, so the difference between two methods is not statistically distinguishable on a per-cell basis. The consistency across all 12 cells is suggestive, but it does not replace variance estimation because all cells share the same pipeline and the same unvalidated judge. I recommend reporting confidence intervals over tasks (e.g., bootstrap or exact binomial intervals), and ideally running a repeated-seed experiment on a representative subset to estimate within-task stochasticity. Without this, the headline \"P3 attains the best solve rate on every cell\" should be weakened or supported with variance-aware analysis.","section":"§5.1, Appendix C, Table 2"},{"comment":"The efficiency comparison on the \"difficult subset\" is defined as the top 25% of tasks ranked by mean cost across the three methods (Section 5.2, Appendix J). This selection is not independent of the methods being compared: because P3 is cheaper on many tasks, the mean cost used for selection is pulled down by P3 itself, which can exclude tasks where P3 is expensive and include tasks where the baselines are expensive. This creates a selection bias that can inflate the reported cost and time reductions (up to 39.6% and 37.2%). The efficiency claim would be more convincing if the difficult subset were defined by a method-independent criterion -- for example, tasks that all methods fail to solve within a time limit, or tasks selected by a fixed feature such as length or formal-spec complexity -- or if the analysis were repeated on the full set with appropriate conditioning. As written, the efficiency result is confounded by the selection rule.","section":"§5.2, Appendix J, Table 5"}],"minor_comments":[{"comment":"Figure 1 is visually clear, but the caption would benefit from stating explicitly that the plan is produced before either the program or proof is elaborated; the current abstract already says this, so the figure caption is just a presentation issue.","section":"§1, Figure 1"},{"comment":"The quality score Quality(σ) = 0.5·Mutation + 0.5·Review is presented without a justification for the equal weighting; a brief sentence explaining why the two components are weighted equally would improve reproducibility and interpretability.","section":"§4.2, Table 1"},{"comment":"The phrase \"we augment each task with a natural-language instruction specifying the expected algorithmic strategy or asymptotic complexity\" would benefit from listing where these instructions are released and how they were authored; the Figshare link is given, but not an explicit pointer to the instruction files.","section":"§5.1"},{"comment":"The plan-retention analysis is informative, but the sentence \"retention is only a proxy for proof-burden prediction accuracy\" is important and could be moved earlier in the appendix to frame the numbers correctly.","section":"Appendix I"},{"comment":"The skill description says \"Self-review is not a gate\" and delegates the plan gate to lean_plan_verify or lean-verifier-plan, but the appendix does not describe how these plan-gate subagents are validated; a short note on their reliability would be useful given that the paper's core claim is about planning quality.","section":"Appendix E"}],"recommendation":"major_revision","confidential_remarks":"The paper is well within the scope of the journal and the conceptual idea is timely. My main concern is that the headline empirical claim depends on an unvalidated LLM judge and a single-run protocol; these are fixable with additional experiments and analysis, so I did not recommend rejection. I would also note that the related-work and baseline discussion cites several papers from the same group (Goedel-Code-Prover, AlgoVeri, Learning to Disprove); this is not inappropriate given the topic overlap, but the authors should ensure that independent comparisons are not crowded out."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What you should know: this is a useful paper on verified code generation with Lean. The core idea is classical — program and proof should be co-designed — but this is the first LLM-agent workflow that makes it work, and it shows consistent gains across all 12 benchmark-model cells. It also ships Lean4Commit0, a repository-derived benchmark with relational API specs, which the subfield genuinely needs. The formal half of the solve criterion is Lean kernel acceptance, so the programs really do meet the formal specs; the paper does not fake that part.\n\nThe empirical claim is a 4.6–11.2 point solve-rate improvement over the stronger baseline, plus cost and time reductions on the difficult subset. The ablation separating joint planning from implementation-only planning is well designed and supports the mechanism story. The authors also state their limitations honestly in Appendix C.\n\nThe real soft spot is the instruction-compliance judge. Because Verina and AlgoVeri don't impose complexity requirements, the authors add a natural-language algorithmic instruction and count a task solved only if the produced code also satisfies that instruction. That check is performed by an LLM subagent, \"lean-verifier-instruction\" (Appendix E Phase 6), and its reliability is never measured. If that judge is lenient, or lenient in a way that favors P3's plan-documented code, the headline deltas shrink or disappear. Consistency across cells doesn't rule this out because every method shares the same judge. This is fixable — measure judge agreement on a sample, replace it with a more formal check where possible, or report an error analysis — but it needs to be addressed before the numbers are taken at face value.\n\nSmaller concerns: each configuration ran once, so there's no variance or significance testing, and the gains on n=189, 77, and 108 could shift with a few task flips. The efficiency comparison selects the top 25% of tasks by mean cost, which is post-hoc, though the all-solved intersection table helps. These are minor to moderate.\n\nWho this is for: anyone working on LLM code generation or proof automation. The benchmark alone is a genuine contribution. I'd send it to a serious venue, with the requirement that the judge be validated and multi-seed runs be added. My recommendation: accept for peer review, with revision along those lines.","headline":"Solid empirical paper on joint program-and-proof planning for verified code generation, but the headline gains depend on an unmeasured LLM judge for instruction compliance; worth sending to review with a request to validate that judge.","tokens_in":19947,"tokens_out":3381,"would_cite":true,"duration_ms":31579,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper claims that a joint program-and-proof plan raises verified-code-generation solve rates by 4.6–11.2 percentage points across all tested models and benchmarks.","keywords":["verified code generation","Lean 4","LLM agents","program-and-proof planning","formal verification","relational specifications","benchmark construction"],"falsifier":"Select a random sample of accepted solutions on Verina and AlgoVeri, run each with size-doubled inputs, and compare the observed complexity against the natural-language instruction; if a substantial fraction of judge-approved solutions violate the stated complexity, the solve-rate gap is partly an artifact of the instruction judge rather than of planning.","tokens_in":94,"feed_emoji":"🧩","tokens_out":4557,"duration_ms":114537,"temperature":0.7,"pith_summary":"The paper targets verified code generation, where an LLM must output both a program and a machine-checked proof in Lean 4. It argues that the usual schedule—write the program first, prove it later—fails structurally, because a committed implementation may force a proof shape that was never planned, sending agents into expensive repair loops. P3 instead has the agent first settle a shared plan that fixes the program decomposition, the library lemmas it will use, and the proof obligations including any auxiliary invariant, and only then elaborate both artifacts against that plan. On Verina, AlgoVeri, and a new repository-derived benchmark, Lean4Commit0, P3 posts the highest solve rate in every benchmark-and-model cell, with gains of 4.6–11.2 points over the stronger baseline and 3.3–8.3 points over implementation-only planning, while cutting cost and time on hard tasks by up to roughly 40% and 37%.","feed_headline":"Plan code and proof together, beat write-then-prove by up to 11 points","feed_subtitle":"A shared program-and-proof plan beats write-then-prove across four LLMs and three Lean benchmarks.","key_machinery":"The load-bearing object is the shared plan, a small structured document with four commitments: the formal contract plus any algorithmic instruction; the program decomposition (recursion variable, branches, data representation, termination measure); the concrete library functions and lemmas; and the proof obligations (bridging predicate, induction or case structure, auxiliary lemma statements). It acts as a single point of retreat: elaboration-level failures are repaired in place under the plan, while plan-level failures trigger an explicit return to planning. The plan is lightweight because it is a sketch, not a Lean term, so the agent can compare alternative structural routes before either artifact is written.","core_discovery":"The central discovery is that proof structure is a selection criterion for program structure, not an afterthought. P3 introduces a two-stage agentic workflow: a planning stage proposes and validates a plan that pairs a program sketch with a proof sketch—fixing the recursion or case-split decomposition, the library functions, the bridging predicate, and the auxiliary lemmas—and an elaboration stage writes Lean code and proof scaffolds under that frozen plan, repairing locally when possible and retreating to replanning only when the plan itself cannot carry the proof. The listMax example shows why ordering matters: an accumulator-fold implementation is fine as code but forces proof of a universal fold invariant, while structural recursion lets the postcondition itself serve as the bridging predicate. The authors claim the plan makes the cost of such structural choices visible before any code is committed, and their experiments support that claim across four frontier LLM backends and three benchmarks.","pith_inferences":["If the same co-derivation discipline is ported to SMT-backed verifiers such as Dafny or Verus, the plan would pair loop invariants, decreases clauses, and ghost state with the program structure; the paper's own limitation section calls this transfer plausible but unverified.","The reliance on an LLM instruction judge means raw solve rates should be read as the conjunction of two checks; a direct comparison of the judge's verdicts against human judgments of algorithmic compliance would tighten the measurement.","A testable extension would vary the plan schema, such as omitting the bridging-predicate or library-support fields, and measure whether gains concentrate on tasks whose specifications share relational structure; the current ablation hints that implementation-only planning can hurt on such tasks.","The paper's single-run protocol means the reported gaps of 4–11 points could partly reflect sampling noise; repeated runs on a subset of tasks would bound that uncertainty."],"forward_implications":["If P3's claim holds, agents that plan code and proof jointly should dominate sequential pipelines on any benchmark where proof structure is sensitive to implementation choice.","The reported gains imply that planning overhead is small enough for joint planning to beat pure implementation planning on textbook tasks and to be essential on library-level relational tasks.","Lean4Commit0-style quality gating—reference satisfaction, mutation rejection, and LLM review—gives a floor for reading future solve rates on repository-derived tasks.","The cost and time reductions on difficult tasks imply that the plan-first workflow avoids most full-restart repairs.","Because Lean accepts only kernel-checked artifacts, every solved task carries a genuine machine-checked correctness guarantee relative to its shipped specification."],"supporting_citations":[{"why":"Supplies one of the benchmarks and defines the spec-code-proof task format on which P3 and the baselines are evaluated.","marker":"[7]"},{"why":"Supplies the classical-algorithms benchmark and is the source of the left-leaning red-black-tree deletion case study.","marker":"[15]"},{"why":"Commit0 is the source repository collection from which Lean4Commit0 extracts core APIs and relational specifications.","marker":"[22]"},{"why":"Lean 4 is the verifier and kernel that checks the final code and proof, defining what counts as a solved task.","marker":"[4]"},{"why":"Dijkstra's hand-in-hand development principle is the methodological basis for the joint planning schedule.","marker":"[14]"},{"why":"The Lean LSP MCP tooling provides the localized goals and diagnostics used during plan-guided elaboration and repair.","marker":"[26]"},{"why":"The Lean 4 Skills workflow pack defines the skill-based program-then-proof baseline SEQ used for comparison.","marker":"[27]"}],"fun_headline_variants":["Plan proof with program: up to 11-point verified-code gain","Joint program-proof planning beats write-then-prove by 11 points","P^3: plan code and proof together, cut costs by 40%","Proof-guided program planning improves verified code across LLMs","Verified code: shared program-proof plan lifts solve rates 4–11 pts"],"cache_read_input_tokens":22016,"weakest_assumption_plain":"Measured success depends on an LLM judge's verdict that the produced code follows natural-language algorithmic or complexity instructions; a lenient or noisy judge would inflate the reported solve-rate gains even though Lean's kernel objectively checks the formal proof.","fun_headline_variants_meta":{"raw":{"variants":["Plan proof with program: up to 11-point verified-code gain","Joint program-proof planning beats write-then-prove by 11 points","P^3: plan code and proof together, cut costs by 40%","Proof-guided program planning improves verified code across LLMs","Verified code: shared program-proof plan lifts solve rates 4–11 pts"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001302,"raw_usage":{"total_tokens":5368,"prompt_tokens":1062,"completion_tokens":4306,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":678,"completion_tokens_details":{"reasoning_tokens":4212}},"tokens_in":678,"tokens_out":4306,"duration_ms":32270,"temperature":1.0,"reasoning_tokens":4212,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T20:17:38.998436+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Select a random sample of accepted solutions on Verina and AlgoVeri, run each with size-doubled inputs, and compare the observed complexity against the natural-language instruction; if a substantial fraction of judge-approved solutions violate the stated complexity, the solve-rate gap is partly an artifact of the instruction judge rather than of planning.","supporting_citations":[{"cited_title":"Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover, 3","cited_arxiv_id":null,"evidence_quote":"The Lean LSP MCP tooling provides the localized goals and diagnostics used during plan-guided elaboration and repair."},{"cited_title":"Lean 4 Skills: Theorem proving skill and workflow pack for AI coding agents, October 2025","cited_arxiv_id":null,"evidence_quote":"The Lean 4 Skills workflow pack defines the skill-based program-then-proof baseline SEQ used for comparison."}],"review_version":1}