Pith. sign in

REVIEW 3 major objections 5 minor 1 cited by

Next Steps in LLM-Supported Java Verification

T0 review · 3 major / 5 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper claims that iterative prompting raises GPT-4O's JML annotation success rate, but KeY's current feedback does not significantly outperform plain resampling.

desk verdict Honest and underpowered: the feedback-vs-sampling comparison is a real but tentative negative result, and the paper says so itself. read the letter →

arxiv 2502.01573 v1 pith:VKATFW6S submitted 2025-02-03 cs.SE cs.AIcs.LGcs.LO

Samuel Teuber , Bernhard Beckert This is my paper · ORCID
classification cs.SEcs.AIcs.LGcs.LO
keywords LargeLanguageModelsProgramVerificationFormalSpecificationJavaJMLLoopInvariantsDeductiveKeY
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper asks whether an automated deductive verifier can steer an unreliable large language model toward correct specification annotations for Java code. Focusing on the auxiliary-specification use case—where a human supplies the top-level contract and the LLM fills in missing loop invariants or contracts for called methods—it compares two error-recovery strategies with GPT-4O and the KeY verifier: continuing the same conversation with verifier feedback, or restarting from scratch with a fresh sample. The central result is that both iterative strategies improve the success rate over a single attempt, but KeY's current feedback does not significantly beat plain sampling in success rate or token efficiency. On 27 invariant and 14 subcontract tasks, sampling and feedback reached similar median success by ten attempts, and sampling was cheaper per solved task because it avoids re-sending the whole conversation. The authors flag that the differences are not yet statistically significant and that a larger benchmark is needed, but the preliminary evidence matters because reliable annotation generation is the main bottleneck for scaling deductive verification.

What carries the argument

The load-bearing object is the verification-checked generation loop: an LLM produces a JML annotation draft for one missing gap, the KeY verifier tries to prove the annotated program, and on failure the system either feeds the parser error or open proof-branch labels back into the same conversation (feedback) or discards the conversation and starts fresh (sampling). The comparison is quantified through token ratio, defined as tokens spent divided by the tokens in the initial input query. If $I$ is the initial token count, $O$ the LLM output per turn, and $R$ the feedback message size, then $n$ sampling iterations cost $n(I+O)$ tokens, while $n$ feedback iterations cost $n(I+O)+\frac{n(n-1)}{2}(O+R)$ tokens; that quadratic term is why sampling dominates on token efficiency. The paper also uses a mixed strategy that bounds the conversation length by restarting after a fixed number of feedback steps.

What would settle it

Run the same feedback-versus-sampling comparison on a larger JML benchmark, for example with 50 or more runs per task; if the median success curve of the feedback strategy rises visibly above the sampling min/max band at any step, the paper's central claim is refuted, while a curve that stays inside the band would confirm it.

Watch

Extended reading notes

Core claim

On its own terms, the paper's discovery is that the verifier's role in this pipeline is currently closer to an oracle that filters candidate annotations than to a tutor whose feedback improves the next draft. Iterative error recovery, whether feedback-based or sampling-based, lifts GPT-4O's success rate well above a single generation attempt; by ten steps the median success rate on invariant synthesis reached roughly the same level for both strategies, and on subcontract synthesis sampling occasionally outperformed feedback. The paper identifies a structural reason for sampling's token advantage: each feedback turn re-inputs the entire conversation, so costs grow quadratically, while each fresh sample costs exactly one fixed input-output round. A mixed strategy that allowed five conversations with up to ten feedback steps each solved one more invariant and one more subcontract than 50 independent samples (24/27 vs. 23/27, and 8/14 vs. 7/14), but the authors explicitly caution that these results are not yet statistically significant.

Load-bearing premise

The conclusion that verifier feedback is no better than resampling rests on the assumption that the 27 invariant tasks and 14 subcontract tasks, with five runs per strategy, represent how GPT-4O and KeY behave generally; the paper itself says the results are not yet statistically significant.

Editorial extensions

If this is right

  • If these results hold on larger benchmarks, scaling should spend additional budget on more independent samples rather than on longer feedback conversations, because sampling gives comparable success at lower token cost.
  • A mixed approach—a few feedback turns per conversation, then a restart—is a cheap guard against the cases that feedback can find, since in these experiments it matched pure sampling and added one success in each task category.
  • The verifier's most valuable current contribution is checking candidate annotations for free; improving the information extracted from failed proofs (better labels, counterexamples, richer diagnostics) is the natural next step to make feedback actually steer the LLM.
  • Reliability at scale will require raising the per-attempt success probability, since subcontract synthesis still solves only about half the tasks in the current benchmark even after multiple attempts.
  • Because the approach is modular and sound, any future gain in first-attempt accuracy translates directly into larger programs with multiple annotation gaps becoming tractable.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A quantitative test the paper does not run is to measure the marginal success per token for each feedback turn and compare it with the marginal success per token of an extra sample; this would decide exactly when a conversation should be abandoned for a restart.
  • If the pattern generalizes, it suggests engineering effort should shift toward cheap pre-verification filters—syntax checks, testing, or fuzzing—that reject bad candidates before the expensive prover runs, so that the verifier acts as a final gate rather than a mid-conversation teacher.
  • The shaded overlap between feedback and sampling curves hints that task difficulty, not strategy, dominates the outcome; stratifying benchmarks by difficulty could reveal whether feedback helps on hard tasks even if it is neutral overall.
  • Given the mixed approach's slight edge, an adaptive policy that switches from feedback to sampling when a conversation stops making progress is a direct and safe extension, and it is compatible with the paper's context-window motivation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. This short paper studies error-recovery strategies for LLM-generated JML annotations in the KeY deductive verifier. It compares a feedback-based approach, which feeds KeY error messages and open proof-branch labels back to GPT-4O, against a sampling baseline that restarts generation from scratch without feedback. Using 27 invariant-synthesis tasks and 14 subcontract-synthesis tasks from the authors' prior work, the paper reports three main empirical claims: (i) iterative attempts, whether feedback- or sampling-based, increase per-task success rates relative to a single attempt; (ii) KeY feedback does not meaningfully improve success rate or token efficiency over sampling; and (iii) a mixed approach (5 feedback runs of up to 10 steps each) solves all benchmarks solved by 50 pure samples plus two additional tasks. The paper also derives an analytical token-cost model and provides full prompt texts in an appendix.

Significance. If the results held firmly, the paper would provide a useful baseline for the community on whether verifier feedback is worth its additional complexity in LLM-driven specification synthesis, and its sampling comparison would be a practical guide for tool builders. The paper has notable strengths: success is determined by an independent verifier (KeY), the token-efficiency analysis is analytically derived, the prompts are fully disclosed, and the limitations are stated explicitly rather than hidden. However, the central comparative claim currently rests on a small benchmark and only five runs per task, and the paper itself acknowledges the results are not statistically significant. As an early results paper it is thought-provoking, but the main conclusion that feedback does not improve over sampling is not yet supported by the data at the strength claimed.

major comments (3)
  1. [Section III, Figures 2–3 and Limitations] The claim that KeY feedback 'does not significantly improve' GPT-4O's success rate is load-bearing, but the experiment is underpowered: only 41 tasks and 5 runs per condition. With 5 runs, each per-task success rate is a multiple of 0.2, and the median curves in Figures 2 and 3 are therefore step functions that can move with a single task's seed. The paper's own Limitations paragraph states the shaded regions show results are 'not yet statistically significant.' A non-significant difference is not evidence that no effect exists; with this sample size and between-task variance, the data are consistent with feedback being substantially better or worse than sampling. Please provide a quantitative uncertainty analysis (e.g., exact confidence intervals for the 41 paired task outcomes, or a sign test at fixed step count) and either soften the Results wording to 'we found no statistically significant improvement' or state an effect-size bound that would support the stronger claim.
  2. [Section III, Table I] The mixed-approach gain over pure sampling is just two tasks across both categories, and the paper itself reports that the subcontract gain (a contract for copying a range of an array) was found in the first iteration, i.e., before any feedback was provided. That instance therefore provides no evidence that verifier feedback helps; it may simply reflect the luck of sampling within the first 5 attempts of the 5 feedback runs. The invariant gain (array reversal) was found at feedback step 8 in two of five runs, which is more informative, but a single task is too small a basis for a general claim. The text should present the mixed approach as an exploratory observation and explicitly separate gains attributable to feedback from gains that already occur on the initial generation.
  3. [Section III, benchmark description] The 41-task benchmark is taken entirely from the authors' prior work [3, Table 1], and this paper does not describe the task features beyond a broad statement that they cover 'a wide range of JML features.' Because the generalizability of the central comparison depends on the representativeness of this set, the manuscript should either reproduce or summarize the benchmark's construction and JML features, or explicitly restrict all conclusions to this particular benchmark. This is not a correctness error but a matter of evidentiary scope: the current wording invites readers to generalize beyond what the data can support.
minor comments (5)
  1. [Section III, Token Efficiency] The token-cost formula is correct, but the notation is slightly ambiguous: R is defined as 'each feedback response on our side,' yet the formula n(I+O)+n(n-1)/2*(O+R) assumes a feedback message is sent after every iteration except the first. Please clarify that R covers the verifier-side feedback token cost and that the formula applies to the feedback-based approach with a fresh feedback message each turn.
  2. [Section II, Listing 1] The example in Listing 1 shows a missing annotation for method g, but the expected annotation is not indicated. A one-line description of the desired contract (e.g., 'requires: nothing; ensures: \result == 2*x') would make the running example easier to follow.
  3. [Figures 2 and 3 captions] The captions state 'Successful Instances (GPT-4O)' but the y-axes show the fraction of tasks solved; please use 'success rate' in the captions for consistency with the text and the axes.
  4. [Section III, Mixed Approach] The sentence 'the mixed approach solves all benchmarks solved by sampling and two additional ones' is ambiguous because Table I reports 24/27 vs 23/27 for invariants and 8/14 vs 7/14 for subcontracts. Please state the overlap explicitly for each category (e.g., 'for invariants, the mixed approach solves the 23 tasks solved by pure sampling plus exactly one additional task').
  5. [Reference [3]] In the reference list, the title of [3] contains a typo: 'Progam' should be 'Program.'

Circularity Check

0 steps flagged · score 1.0 of 10

The central comparisons are validated by the external KeY verifier, so the paper's derivation chain is not circular; the only self-citation, reuse of the benchmark set from [3], is not load-bearing for the success-rate claims.

full rationale

The paper's headline claims are about whether iterative prompting, with or without KeY feedback, improves the rate at which GPT-4O produces JML annotations that KeY can prove. Success is determined by the KeY prover itself, which is an external, independent checker and not fitted or defined in terms of the LLM's output. No parameter is fitted to a subset of the data and then renamed as a prediction; the reported success rates are direct experimental outcomes on held-out prompt attempts. The benchmark tasks are reused from the authors' prior work [3, Table 1], which is a self-citation, but the prior work is not invoked as a uniqueness theorem or as evidence for the quantitative comparison; the current paper reruns the experiments with GPT-4O and compares fresh outcomes. The token-efficiency comparison is an analytic cost model based on conversation length, not a circular prediction. The paper even notes that one of the two additional successes of the mixed approach was found in the first iteration, before any feedback, which weakens the mixed approach's advantage but does not make the derivation circular. The paper's admitted lack of statistical significance in Section III is a statistical-power concern, explicitly acknowledged by the authors, and is not an instance of circular reasoning. Thus there is no circular step; the only minor self-citation is the reuse of the benchmark set, which is not load-bearing for the central empirical claim.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new entities and no fitted parameters in a derivation sense. Its conclusions rest on KeY's soundness, the representativeness of the small benchmark, and the independence of LLM samples in the restart condition; the hand-chosen experimental cutoffs are listed as free parameters.

free parameters (2)
  • Maximum attempts (steps/samples) = 10
    Chosen by hand; success-rate curves are truncated at this point, so the comparison is only valid up to 10 attempts.
  • Number of runs = 5
    Hand-chosen; the min/max/median bands in Figures 2 and 3 are over 5 runs, and the paper admits results are not statistically significant.
assumptions (3)
  • domain assumption KeY is a sound deductive verifier for JML
    Section II states that KeY deductively verifies Java programs against JML contracts; the conclusion that a verified auxiliary annotation implies the top-level specification assumes this soundness.
  • domain assumption The 27 invariant and 14 subcontract tasks in the benchmark are representative of real annotation tasks
    Section III and Limitations: the paper bases its quantitative claims on these instances and acknowledges that 'we require a larger set of representative instances to validate our hypotheses.'
  • domain assumption In the sampling condition, each restart yields an independent LLM response to the same prompt
    Section III describes restarting the probabilistic process from scratch; the token-efficiency and success-rate analysis treats samples as independent.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Next Steps in LLM-Supported Java Verification." pith.science (2026). https://pith.science/paper/VKATFW6S

@misc{pith2026250201573,
  author       = {Pith},
  title        = {Pith review of: Next Steps in LLM-Supported Java Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VKATFW6S}},
  note         = {Machine review of arXiv:2502.01573}
}
read the original abstract

Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable correctness guarantees for large-scale software systems. In comparison to other LLM tasks, the application field of deductive verification has the notable advantage of providing a rigorous toolset to check LLM-generated solutions. This short paper provides early results on how this rigorous toolset can be used to reliably elicit correct specification annotations from an unreliable LLM oracle.

Figures

Figures reproduced from arXiv: 2502.01573 by the authors.

Figure 1
Figure 1. Setup of our LLM integration for KeY: A partially JML-annotated [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 3
Figure 3. Increase of Success Rate for invariant (top) resp. subcontract (bottom) [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Do AI models help produce verified bug fixes?

    cs.SE 2025-07 conditional novelty 6.0 of 10

    Programmers with LLM access solved fewer formally verified debugging tasks than a no-AI control group, though complete novices and strong language experts gained some benefit.

Reference graph

Works this paper leans on

21 extracted references · 18 canonical work pages · cited by 1 Pith paper

  1. [1]

    (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice

    Ahrendt, W., Beckert, B. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Springer (2016)

    work page 2016

  2. [2]

    : Modular Verification of JML Contracts Using Bounded Model Checking

    Beckert, B., Kirsten, M., et al. : Modular Verification of JML Contracts Using Bounded Model Checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020, Rhodes, Greece, October 20-30, 2020, Proceedings, Part I. LNCS, vol. 12476, pp. 60–80. Springer, Heidelberg (2020). https://doi. org/10.1007/978-3-030-61362-4 4

    work page doi:10.1007/978-3-030-61362-4 2020

  3. [3]

    : Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification

    Beckert, B., Klamroth, J., et al. : Towards Combining the Cognitive Abilities of Large Language Models with the Rigor of Deductive Progam Verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, Crete, Greece, October 27-31, 2024, Proceedings, Part IV. LNCS, vol. 15222, pp. 242–257. Springer, Heidelberg (2024). https://doi.org/10.1007/978- 3-031-75387-9 15

    doi:10.1007/978- 2024

  4. [4]

    In: Larochelle, H., Ranzato, M

    Brown, T.B., Mann, B., et al.: Language Models are Few-Shot Learners. In: Larochelle, H., Ranzato, M. (eds.) Advances in Neural Informa- tion Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual (2020)

    work page 2020

  5. [5]

    : Ranking LLM-Generated Loop Invariants for Program Verification

    Chakraborty, S., Lahiri, S.K., et al. : Ranking LLM-Generated Loop Invariants for Program Verification. (2023). https://doi.org/10.18653/ V1/2023.FINDINGS-EMNLP.614

    work page 2023

  6. [6]

    In: Dubois, C., Giannakopoulou, D., M ´ery, D

    Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., M ´ery, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014. EPTCS, pp. 79–92 (2014). https://doi.org/10.4204/EPTCS.149.8

    work page doi:10.4204/eptcs.149.8 2014

  7. [7]

    In: AI for Math Workshop @ ICML 2024 (2024)

    Granberry, G., Ahrendt, W., Johansson, M.: Specify What? A Case-Study using GPT-4 and Formal Methods For Specification Synthesis. In: AI for Math Workshop @ ICML 2024 (2024). https://openreview.net/forum?id= ZRTcPkNl7v

    work page 2024

  8. [8]

    Greiner, S., B ¨uhlmann, N., et al. : Automated Generation of Code Con- tracts: Generative AI to the Rescue? In: Proceedings of the 23rd ACM SIGPLAN International Conference on Generative Programming: Con- cepts and Experiences. GPCE ’24, pp. 1–14. Association for Computing Machinery, Pasadena, CA, USA (2024). https://doi.org/10.1145/3689484. 3690738

    work page doi:10.1145/3689484 2024

Show all 21 references
  1. [9]

    (eds.) Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings

    Janßen, C., Richter, C., Wehrheim, H.: Can ChatGPT support software verification? In: Beyer, D., Cavalcanti, A. (eds.) Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings. LNCS, v...

    2024

  2. [10]

    : JML Reference Manual

    Leavens, G.T., Poll, E., et al. : JML Reference Manual . Draft revision

  3. [11]

    CoRR abs/2311.07948 (2023)

    Kamath, A., Senthilnathan, A., et al.: Finding Inductive Loop Invariants using Large Language Models. CoRR abs/2311.07948 (2023). arXiv: 2311.07948

    2023 arXiv

  4. [12]

    Journal of Systems and Software 211, 111972 (2024)

    Lathouwers, S., Huisman, M.: Survey of annotation generators for de- ductive verifiers. Journal of Systems and Software 211, 111972 (2024). https://doi.org/10.1016/j.jss.2024.111972

    2024

  5. [13]

    In: Ball, T., Zuck, L., Shankar, N

    Leino, K.R.M., Moskal, M.: Usable auto-active verification. In: Ball, T., Zuck, L., Shankar, N. (eds.) Usable Verification Workshop (2010). https: //fm.csl.sri.com/UV10

    2010

  6. [14]

    : Can Large Language Models Reason about Program Invariants? In: Krause, A., Brunskill, E

    Pei, K., Bieber, D., et al. : Can Large Language Models Reason about Program Invariants? In: Krause, A., Brunskill, E. (eds.) Proceedings of the 40th International Conference on Machine Learning. Proceedings of Machine Learning Research, pp. 27496–27520. PMLR (2023). https:// ...

    2023

  7. [15]

    In: Margaria, T., Steffen, B

    Platzer, A.: Intersymbolic AI - Interlinking Symbolic AI and Subsymbolic AI. In: Margaria, T., Steffen, B. (eds.) ISoLA 2024, Crete, Greece, Octo- ber 27-31, 2024, Proceedings, Part IV. LNCS, vol. 15222, pp. 162–180. Springer, Heidelberg (2024). https://doi.org/10.1007/978-3-0...

    2024 doi

  8. [16]

    In: Avni, G., Giacobbe, M

    Sun, C., Sheng, Y ., et al.: Clover: Closed-Loop Verifiable Code Genera- tion. In: Avni, G., Giacobbe, M. (eds.) AI Verification - First International Symposium, SAIV 2024, Montreal, QC, Canada, July 22-23, 2024, Pro- ceedings. LNCS, vol. 14846, pp. 134–155. Springer, Heidelbe...

    2024 doi

  9. [17]

    In: The Twelfth International Conference on Learning Representations (2024)

    Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating Large Language Models in Automated Program Verification. In: The Twelfth International Conference on Learning Representations (2024). https://openreview.net/ forum?id=Q3YaCghZNt

    2024

  10. [18]

    : Leveraging Large Language Models for Au- tomated Proof Synthesis in Rust

    Yao, J., Zhou, Z., et al. : Leveraging Large Language Models for Au- tomated Proof Synthesis in Rust. CoRR abs/2311.03739 (2023). arXiv: 2311.03739 APPENDIX A. LLM Prompts Below we provide examples for the prompts used to elicit specifications from the LLM

    2023 arXiv

  11. [20]

    (\" \"(\

    Invariant Generation: We invoke GPT with the follow- ing system message: You are an assistant for JML annotation . In the first message of this conversation , you are provided with a Java class with partial JML annotation . Additionally , you are provided with natural language...

  12. [21]

    loop_invariant \

    Submethod Contract Generation: We invoke GPT with the following system message: You are an assistant for JML annotation . In the first message of this conversation , you are provided with a Java class with partial JML annotation . Additionally , you are provided with natural l...

  13. [2344]

    http://www.eecs.ucf.edu/ ∼leavens/JML//OldReleases/ jmlrefman.pdf

    May 2013. http://www.eecs.ucf.edu/ ∼leavens/JML//OldReleases/ jmlrefman.pdf

    2013

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.