Pith. sign in

REVIEW 3 major objections 5 minor 81 references

Breaking the Myth: Can Small Models Infer Postconditions Too?

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

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

Pith's one-line read A 7-billion-parameter model, fine-tuned on 1,500 examples, writes Java postconditions as accurately as GPT-4o.

desk verdict A 7B model fine-tuned on 1.5K reasoning triples reportedly matches GPT-4o on postcondition generation, but the missing train/test disjointness analysis makes the headline claim unverifiable as written. read the letter →

arxiv 2507.10182 v1 pith:3GOEO24M submitted 2025-07-14 cs.SE cs.AI

Gehao Zhang , Zhenting Wang , Juan Zhai This is my paper
classification cs.SEcs.AI
keywords postconditiongenerationformalspecificationssupervisedfine-tuningsmalllanguagemodelsreasoningtracesDefects4JcodeLLMsJava
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

This paper tries to establish that a 7-billion-parameter code model, fine-tuned on roughly 1,500 prompt–reasoning–postcondition triples, can generate formal postconditions from natural-language comments as reliably as far larger models. The authors build a curated dataset from quality-filtered public code repositories, supervise the model to produce a structured specification (imports, pre-state ghost variables, post-state ghost variables, and a condition), and evaluate by injecting the generated assertions into fixed and buggy versions of real Java methods from Defects4J. On the benchmark, the fine-tuned 7B model reaches 43.0% semantic correctness at top-1, close to GPT-4o's 44.0%, and surpasses the 32B open-source models on most metrics. If this holds, teams that cannot host or pay for massive proprietary models could still get high-quality, verifiable specifications locally.

What carries the argument

The load-bearing mechanism is supervised fine-tuning on a dataset of prompt/reasoning/postcondition triples, where each prompt is a structured YAML bundle containing repository-level context, class-level context, the target method signature with its NL description, and task instructions, and each output pairs a step-by-step reasoning trace with a four-part specification: import statements, pre-ghost variables capturing pre-call state, post-ghost variables capturing values after the call, and the condition itself. The reasoning traces let the model self-correct during inference, the pre-ghost and post-ghost variables make stateful postconditions expressible, and injection into the instrumented method with a runtime check enables automated validation against the test suite. Together these components let a 7B model generate specifications that compile, hold on fixed code, and fail on buggy code.

What would settle it

Check the released training set for overlap with Defects4J: extract the method signatures and bodies of the 1,134 evaluated methods and search for them or near-duplicates in the training repositories; if any match is found, the headline comparison to GPT-4o is invalidated. Alternatively, run the fine-tuned model on a fresh, held-out set of methods from repositories never used in training and compare Sem@1.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central discovery is that task-specific supervised fine-tuning, with explicit reasoning traces in the training data, unlocks postcondition-inference ability in a small model that the same model without fine-tuning does not have. The fine-tuned model improves semantic correctness from the base model's 12.5% to 43.0% at top-1, matches GPT-4o on semantic correctness and bug distinguishing (11.0% vs. 11.8%), and beats Qwen2.5-Coder-32B and DeepSeek-R1-Distill-32B on most metrics despite using 1.5K training examples versus 800K for DeepSeek-R1-Distill. The paper claims this shows reasoning traces, not model scale, are the main ingredient that makes postcondition generation work.

Load-bearing premise

The whole comparison collapses if any of the 1,134 Defects4J evaluation methods, or code close to them, appeared in the 1,500 training triples, because the paper does not enumerate its training repositories or demonstrate that they exclude Defects4J projects.

Editorial extensions

If this is right

  • A 7B model fine-tuned on about 1.5K examples is a viable local alternative to GPT-4o for postcondition generation, with comparable semantic correctness and bug-finding rate.
  • Omitting reasoning traces from training data cuts semantic-correctness gains dramatically across tested repositories, so reasoning supervision is a key component of the result.
  • Longer reasoning traces do not monotonically improve quality; semantic correctness peaks at intermediate reasoning length and drops for the longest traces.
  • The structured prompt with repository and class context alone improves GPT-4's semantic correctness, so context is a separate contributor beyond model size.
  • Task-specific fine-tuning can bring the benefits of reasoning-oriented training to small models for formal specification tasks, without test-time scaling.
  • If the training and evaluation corpora are truly disjoint, the result reframes the cost-quality tradeoff: for narrow, verifiable tasks, data quality and reasoning supervision may matter more than parameter count.

Reading between the lines

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

  • The same pipeline, which works from NL comments, signatures, and class skeletons, could be shifted earlier in the development cycle to produce postconditions before implementation, a direction the paper mentions as formal specification-driven development.
  • The observed reasoning-length trend suggests a cheap inference-time lever: sampling several reasoning traces and selecting by length could tune semantic correctness without retraining, though the paper does not propose this.
  • The method's dependence on well-documented Java repositories and test suites means transfer to less documented languages or codebases may need new data curation, an open question the paper acknowledges.
  • If the disjointness of training and evaluation corpora is confirmed, the result reframes the cost-quality tradeoff: for narrow, verifiable tasks, data quality and reasoning supervision may matter more than parameter count.
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. The paper proposes a supervised fine-tuning approach for generating Java postconditions from natural-language method descriptions together with class- and repository-level context. The authors construct a training set of roughly 1,500 prompt/reasoning/postcondition triples: DeepSeek-R1 generates candidate specifications and reasoning traces, which are then validated by test-suite injection and manual review. They fine-tune Qwen2.5-Coder-7B-Instruct and evaluate on Defects4J v2.0.0 by injecting generated postconditions into fixed and buggy versions and measuring syntax correctness (Syn@k), semantic correctness (Sem@k), and bug-distinguishing rate (rBugD). The headline result is that the 7B model reaches Sem@1=43.0%, Sem@5=72.3%, Syn@1=72.3%, and rBugD=11.0%, matching or exceeding GPT-4o and surpassing larger open models, despite using only 1.5K training examples.

Significance. If the empirical claims are valid, this is a valuable practical result: a 7B model that can produce compilable, semantically correct, bug-distinguishing postconditions at a fraction of the inference cost of GPT-4o-class models. The injection-based evaluation is a genuine strength, because the metrics are machine-checked against actual compilation and test execution on real and buggy Defects4J versions, rather than judged by an LLM or human preference. The release of code and data would support reproducibility. The main caveat is that the entire comparison rests on the assumption that the 1.5K training triples do not overlap with Defects4J; the manuscript does not currently demonstrate this, so the headline numbers cannot yet be fully credited.

major comments (3)
  1. [§4.2 and §6] The central empirical claim is not interpretable without a demonstrated train/eval disjointness guarantee. The Quality Filter selects public GitHub repositories, but the paper never enumerates them, and Defects4J v2.0.0 projects are themselves public GitHub repositories. If any training triple was derived from a Defects4J method, or even from nearby code in the same class or repository, the model could memorize the postcondition or the context needed to reconstruct it, inflating Sem@1, Syn@1, and rBugD. Section 6 says membership inference attacks and prompt checks were used to address leakage, but no results of those checks are shown, and the cited reference [11] is titled 'Do Membership Inference Attacks Work on Large Language Models?' and reports largely negative findings, so it cannot serve as evidence of clean data. Please provide the full list of training repositories, a file- and method-level overlap analysis with Defects4J, and a concrete description of the leakage checks actually performed.
  2. [§5.1.4 and Table 1] The number of evaluation units is internally inconsistent. The text says Defects4J has 835 bugs and that 1,134 tasks were obtained, and that 11,340 postconditions per approach are generated. Table 1, however, reports rBugD denominators of 726 (and 525 for the asterisked baselines), not 835 or 1,134. Please clarify how 835 bugs become 726 bugs, how tasks map to bugs for rBugD, and why the denominator differs from the number of tasks used for Sem@k and Syn@k. Without this clarification, the headline rBugD comparison is not reproducible.
  3. [§5.2 and Table 1] Direct comparisons of rBugD across rows with different denominators are not controlled. The table reports GPT-4* and StarChat* on 525 bugs while all other models are reported on 726 bugs, and the text draws comparative conclusions such as 'our model performs better than DeepSeek-R1-Distill on each metric' and achieves 'comparable rBugD = 11.0%.' Although the footnote discloses the 525/726 difference, the comparison should be limited to the same bug subset or accompanied by a matched-subset analysis; otherwise the ranking could be an artifact of the different evaluation sets.
minor comments (5)
  1. [§7 and Table 1] The conclusion states that training used 'only a few hundred training examples,' while the introduction, abstract, and Table 1 state 1.5K examples; please reconcile this factual discrepancy.
  2. [§4.4 and §5.1.3] The training specifications and reasoning traces were produced by DeepSeek-R1, so the comparison against DeepSeek-R1-Distill-32B is partly a student/teacher distillation comparison; this should be stated explicitly in the experimental setup so readers do not misinterpret the result as a fully independent small-model capability.
  3. [§4.5] The manual validation stage should report quantitative details such as the number of specifications rejected or revised and the inter-rater agreement among the four experts; currently the reader cannot assess the curation cost or reliability.
  4. [Figure 5 and §5.3] The text refers to 'Qwen2.5-Coder-7B-SFT' without specifying whether this variant is trained on the same 1.5K examples with the reasoning traces removed; please state this explicitly.
  5. [Throughout] There are several typos and formatting errors, including 'Specificatin' in the Section 2.1 heading, 'astest-time scaling' in Section 2.2, 'leverage' in Section 4.4, and 'close-sourced' in Section 6; a copyedit pass is needed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claim is an empirical comparison against the external Defects4J benchmark; the unresolved train/eval overlap is a validity threat, not a circular reduction.

full rationale

The paper's derivation chain is empirical rather than formal. Training data are constructed in Sections 4.2-4.5 from public GitHub repositories, and evaluation uses Defects4J v2.0.0 (Section 5.1.1); the model's outputs are judged by compiling and running tests on fixed and buggy versions (Eqs. 1-3), which are external to the fine-tuning objective defined in Section 4.6. No equation in the paper defines a predicted quantity in terms of a fitted input: the 1.5K training triples are not used to compute Sem@k, Syn@k, or rBugD, and the fine-tuning loss does not contain evaluation metrics. The comparison against GPT-4o, Qwen2.5-Coder-32B, and DeepSeek-R1-Distill-32B is an external benchmark, not a self-citation chain; the authors' own prior work is cited only as general background and is not load-bearing. The only concern that approaches circularity is training/evaluation contamination: Section 6 asserts membership-inference and prompt checks but does not enumerate training repositories or demonstrate that Defects4J methods are absent from the 1,500 triples. Had a Defects4J method appeared in training, the reported gains could be memorization renamed as prediction; however, the paper provides no quoted evidence of such an overlap, and the absence of a leakage audit is a correctness or validity risk, not a demonstrated reduction of the result to its own inputs. Under the hard rule requiring an exhibited reduction, no circular step can be claimed, so the circularity score is 0.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

No mathematical derivation is present. The ledger captures the empirical assumptions behind the evaluation. The most load-bearing item is the disjointness assumption, because Defects4J projects are public Java repositories and the training corpus is drawn from public GitHub.

free parameters (4)
  • learning_rate = 1e-5
    Chosen SFT hyperparameter; not fitted to evaluation data, but the headline results depend on training settings.
  • weight_decay = 1e-4
    Regularization hyperparameter selected by hand; standard for fine-tuning.
  • training_examples = ~1,500
    Data budget selected by the authors; central to the claim that small data suffices.
  • generation_attempts = 10
    Ten samples per task are used to compute top-k and bug-distinguishing metrics; an evaluation choice, not a fitted model parameter.
assumptions (4)
  • domain assumption Public GitHub repositories with good documentation and tests are a sound source of training specifications.
    Quality Filter selects on documentation and test coverage (Section 4.2); this assumes coverage and comments faithfully encode intended behavior.
  • domain assumption Automated test pass/fail and human expert review establish correctness of training specifications.
    Specification Validator (Section 4.5) treats test failures as specification errors and human review as ground truth.
  • domain assumption Compilation and test outcomes are valid proxies for semantic correctness of generated postconditions.
    Metrics in Section 5.1.4 define correctness as compiling and passing all tests; an incomplete test suite could mark weak or wrong postconditions as correct.
  • ad hoc to paper Training and evaluation data are disjoint.
    Needed for the evaluation to be a genuine out-of-distribution test; the paper asserts leakage checks in Section 6 but supplies no repository list or proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Breaking the Myth: Can Small Models Infer Postconditions Too?." pith.science (2026). https://pith.science/paper/3GOEO24M

@misc{pith2026250710182,
  author       = {Pith},
  title        = {Pith review of: Breaking the Myth: Can Small Models Infer Postconditions Too?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3GOEO24M}},
  note         = {Machine review of arXiv:2507.10182}
}
abstract

Formal specifications are essential for ensuring software correctness, yet manually writing them is tedious and error-prone. Large Language Models (LLMs) have shown promise in generating such specifications from natural language intents, but the giant model size and high computational demands raise a fundamental question: Do we really need large models for this task? In this paper, we show that a small, fine-tuned language model can achieve high-quality postcondition generation with much lower computational costs. We construct a specialized dataset of prompts, reasoning logs, and postconditions, then supervise the fine-tuning of a $7$B-parameter code model. Our approach tackles real-world repository dependencies and preserves pre-state information, allowing for expressive and accurate specifications. We evaluate the model on a benchmark of real-world Java bugs (Defects4J) and compare against both proprietary giants (e.g., GPT-4o) and open-source large models. Empirical results demonstrate that our compact model matches or outperforms significantly larger counterparts in syntax correctness, semantic correctness, and bug-distinguishing capability. These findings highlight that targeted fine-tuning on a modest dataset can enable small models to achieve results formerly seen only in massive, resource-heavy LLMs, offering a practical and efficient path for the real-world adoption of automated specification generation.

Figures

Figures reproduced from arXiv: 2507.10182 by the authors.

Figure 1
Figure 1. Excerpts from the model’s reasoning trace for the [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Overall Workflow. Note that, different from some previous works [31] that rely on a runnable environment, including the code implementation and test cases, our work generates formal specifications purely from compo￾nents that can be defined at the early stage of the software design, i.e., NL documents, signatures of classes and methods, and field defi￾nitions. This means this trained model is satisfied to be integra… view at source ↗
Figure 3
Figure 3. LLM Prompt Example. necessary dependencies and structural relationships. Given a repos￾itory, the Prompt Builder first extracts all class-level code skeletons, excluding implementation details, using abstract syntax tree parser [49]. These extracted skeletons are stored as a codebase for retrieval. For each method, the Prompt Builder concatenates the signatures of the method itself and its associated class to form a… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: Reasoning, Postcondition, and Injection Example. [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: Comparison of Sem@1 among initial Qwen model, non-reasoning SFT model from Qwen2.5-Coder-7B, and ours, in which "Qwen2.5-Coder-7B-SFT" and "ours" use the same number of training data. 39.7% on Sem@1 and 67.3% on Syn@1. In contrast, our fine-tuned 7B model surpasses the…
Figure 6
Figure 6. Figure 6: Trend of average tokens and Sem@1 while the rank of reasoning context length increased, from rank 1 shortest to 10 longest. fine-tuning yields limited improvements for most projects. For ex￾ample, on Chart, the Sem@1 increased from 8.7% to 12.3% and on Cli, the number …
Figure 7
Figure 7. Figure 7: An example of long reasoning [PITH_FULL_IMAGE:figures/full_fig_p009_7.png]
Figure 8
Figure 8. Figure 8: An example of GPT-4 generating post-condition with [PITH_FULL_IMAGE:figures/full_fig_p010_8.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

81 extracted references · 55 canonical work pages

  1. [11]

    Michael Duan, Anshuman Suri, Niloofar Mireshghallah, Sewon Min, Weijia Shi, Luke Zettlemoyer, Yulia Tsvetkov, Yejin Choi, David Evans, and Hannaneh Hajishirzi. 2024. Do Membership Inference Attacks Work on Large Language Models? arXiv preprint arXiv: 2402.07841 (2024)

    arXiv 2024

  2. [1]

    Alibaba. 2023. Qwen2.5-Coder: Open-Source Code LLMs. (2023)

    2023

  3. [2]

    Zachary Ankner, Mansheej Paul, Brandon Cui, Jonathan D Chang, and Prithvi- raj Ammanabrolu. 2024. Critique-out-loud reward models. arXiv preprint arXiv:2408.11791 (2024)

    arXiv 2024

  4. [3]

    Angello Astorga, Siwakorn Srisakaokul, Xusheng Xiao, and Tao Xie. 2018. PreInfer: Automatic Inference of Preconditions via Symbolic Analysis. In2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 678–689

    work page 2018

  5. [4]

    Osbert Bastani, Saswat Anand, and Alex Aiken. 2015. Specification inference using context-free language reachability. InACM SIGPLAN Notices. ACM, 553–566

    work page 2015

  6. [5]

    Arianna Blasi, Alberto Goffi, Konstantin Kuznetsov, Alessandra Gorla, Michael D Ernst, Mauro Pezzè, and Sergio Delgado Castellanos. 2018. Translating code comments to procedure specifications, In Proceedings of the 27th ACM SIGSOFT Breaking the Myth: Can Small Models Infer Postconditions Too? Conference acronym ’XX, June 03–05, 2018, Woodstock, NY Interna...

    work page 2018

  7. [6]

    Junjie Chen, Yanwei Bai, Dan Hao, Lingming Zhang, Lu Zhang, Bing Xie, and Hong Mei. 2016. Supporting oracle construction via static analysis. 2016 31st IEEE/ACM International Conference on Automated Software Engineering (ASE) (2016), 178–189. https://api.semanticscholar.org/CorpusID:472942

    work page 2016

  8. [7]

    Sehyun Choi, Tianqing Fang, Zhaowei Wang, and Yangqiu Song. 2023. KCTS: knowledge-constrained tree search decoding with token-level hallucination detection. arXiv preprint arXiv:2310.09044 (2023)

    arXiv 2023

Show all 81 references
  1. [8]

    Matthias Cosler, Christopher Hahn, Daniel Mendoza, Frederik Schmitt, and Caroline Trippel. 2023. nl2spec: Interactively translating unstructured natural language to temporal logics with large language models. In International Conference on Computer Aided Verification. Springer...

    2023

  2. [9]

    Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado

  3. [10]

    Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. 2013. Automatic inference of necessary preconditions. In International Workshop on Verification, Model Checking, and Abstract Interpretation. Springer, 128–148

    2013

  4. [12]

    Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, and Shuvendu K Lahiri

  5. [13]

    Michael D Ernst, Jake Cockrell, William G Griswold, and David Notkin. 2001. Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27, 2 (2001), 99–123

    2001

  6. [14]

    Ernst, Jeff H

    Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. 2007. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69 (2007), 35–45. https://api.semanticscholar.org/CorpusID:17620776

    2007

  7. [15]

    Rustan M

    Cormac Flanagan and K. Rustan M. Leino. 2001. Houdini, an Annotation Assistant for ESC/Java. In FME. https://api.semanticscholar.org/CorpusID:1534849

    2001

  8. [16]

    Francesco Fuggitti and Tathagata Chakraborti. 2023. NL2LTL–a python package for converting natural language (NL) instructions to linear temporal logic (LTL) for- mulas. InProceedings of the AAAI Conference on Artificial Intelligence. 16428–16430

    2023

  9. [17]

    Alberto Goffi, Alessandra Gorla, Michael D Ernst, and Mauro Pezzè. 2016. Automatic generation of oracles for exceptional behaviors. InProceedings of the 25th International Symposium on Software Testing and Analysis. ACM, 213–224

    2016

  10. [18]

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al . 2025. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948 (2025)

    2025 arXiv

  11. [19]

    Sudheendra Hangal and Monica S. Lam. 2002. Tracking down software bugs using automatic anomaly detection. Proceedings of the 24th Inter- national Conference on Software Engineering. ICSE 2002 (2002), 291–301. https://api.semanticscholar.org/CorpusID:11004588

    2002

  12. [20]

    Johannes Henkel, Christoph Reichenbach, and Amer Diwan. 2008. Developing and debugging algebraic specifications for Java classes. ACM Transactions on Software Engineering and Methodology (TOSEM) 17, 3 (2008), 1–37

    2008

  13. [21]

    Aaron Hurst, Adam Lerer, Adam P Goucher, Adam Perelman, Aditya Ramesh, Aidan Clark, AJ Ostrow, Akila Welihinda, Alan Hayes, Alec Radford, et al. 2024. Gpt-4o system card. arXiv preprint arXiv:2410.21276 (2024)

    2024 arXiv

  14. [22]

    Nan Jiang, Thibaud Lutellier, Yiling Lou, Lin Tan, Dan Goldwasser, and Xiangyu Zhang. 2023. Knod: Domain knowledge distilled tree decoder for automated program repair. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 1251–1263

    2023

  15. [23]

    James A Jones, Mary Jean Harrold, and John Stasko. 2002. Visualization of test information to assist fault localization. In Proceedings of the 24th International Conference on Software Engineering. ICSE 2002. IEEE, 467–477

    2002

  16. [24]

    René Just, Darioush Jalali, and Michael D Ernst. 2014. Defects4J: A database of existing faults to enable controlled testing studies for Java programs. InProceedings of the 2014 international symposium on software testing and analysis. 437–440

    2014

  17. [25]

    Jens U Kreber and Christopher Hahn. 2021. Generating symbolic reasoning problems with transformer gans. arXiv preprint arXiv:2110.10054 (2021)

    2021 arXiv

  18. [26]

    Axel van Lamsweerde. 2000. Formal specification: a roadmap. InProceedings of the Conference on the Future of Software Engineering. 147–159

    2000

  19. [27]

    Andreas Leitner, Ilinca Ciupa, Manuel Oriol, Bertrand Meyer, and Arno Fiva

  20. [28]

    Raymond Li, Loubna Ben Allal, Yangtian Zi, Niklas Muennighoff, Denis Kocetkov, Chenghao Mou, Marc Marone, Christopher Akiki, Jia Li, Jenny Chim, et al. 2023. Starcoder: may the source be with you!arXiv preprint arXiv:2305.06161 (2023)

    2023 arXiv

  21. [29]

    Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. 2023. Let’s ver- ify step by step. InThe Twelfth International Conference on Learning Representations

    2023

  22. [30]

    In Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

    Contract driven development= test driven development-writing test cases. In Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering. ACM, 425–434

  23. [31]

    Lezhi Ma, Shangqing Liu, Yi Li, Xiaofei Xie, and Lei Bu. 2024. Specgen: Automated generation of formal program specifications via large language models. arXiv preprint arXiv:2401.08807 (2024)

    2024 arXiv

  24. [32]

    Bertrand Meyer, Ilinca Ciupa, Andreas Leitner, and Lisa Ling Liu. 2007. Automatic testing of object-oriented software. InInternational Conference on Current Trends in Theory and Practice of Computer Science. Springer, 114–129

    2007

  25. [33]

    Jiacheng Liu, Andrew Cohen, Ramakanth Pasunuru, Yejin Choi, Hannaneh Hajishirzi, and Asli Celikyilmaz. 2023. Don’t throw away your value model! Generating more preferable text with Value-Guided Monte-Carlo Tree Search decoding. arXiv preprint arXiv:2309.15028 (2023)

    2023 arXiv

  26. [34]

    Niklas Muennighoff, Zitong Yang, Weijia Shi, Xiang Lisa Li, Li Fei-Fei, Hannaneh Hajishirzi, Luke Zettlemoyer, Percy Liang, Emmanuel Candès, and Tatsunori Hashimoto. 2025. s1: Simple test-time scaling. arXiv preprint arXiv:2501.19393 (2025)

    2025 arXiv

  27. [35]

    Hoan Anh Nguyen, Robert Dyer, Tien N Nguyen, and Hridesh Rajan. 2014. Mining preconditions of APIs in large-scale code corpus. InProceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. ACM, 166–177

    2014

  28. [36]

    Facundo Molina, Renzo Degiovanni, Pablo Ponzio, Germán Regis, Nazareno Aguirre, and Marcelo Fabian Frias. 2019. Training Binary Classifiers as Data Struc- ture Invariants. 2019 IEEE/ACM 41st International Conference on Software Engineer- ing (ICSE) (2019), 759–770. https://api...

    2019

  29. [37]

    OpenAI. 2024. Learning to reason with LLMs. https://openai.com/index/learning- to-reason-with-llms/

    2024

  30. [38]

    Jiayi Pan, Glen Chou, and Dmitry Berenson. 2023. Data-efficient learning of natural language to linear temporal logic translators for robot task specification. In 2023 IEEE International Conference on Robotics and Automation (ICRA). IEEE, 11554–11561

    2023

  31. [39]

    Jeremy W Nimmer and Michael D Ernst. 2002. Automatic generation of program specifications. ACM SIGSOFT Software Engineering Notes 27, 4 (2002), 229–239

    2002

  32. [40]

    Hung Phan, Hoan Anh Nguyen, Tien N Nguyen, and Hridesh Rajan. 2017. Statistical learning for inference between implementations and documentation. In Proceedings of the 39th International Conference on Software Engineering: New Ideas and Emerging Results Track. IEEE Press, 27–30

    2017

  33. [41]

    Murali Krishna Ramanathan, Ananth Grama, and Suresh Jagannathan. 2007. Static specification inference using predicate mining. InACM SIGPLAN Notices. ACM, 123–134

    2007

  34. [42]

    Rahul Pandita, Xusheng Xiao, Hao Zhong, Tao Xie, Stephen Oney, and Amit Paradkar. 2012. Inferring method specifications from natural language API descriptions, In Proceedings of the 34th International Conference on Software Engineering. 2012 34th International Conference on So...

    2012

  35. [43]

    Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Sekhar Jana. 2019. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. ArXiv abs/1909.11542 (2019). https://api.semanticscholar.org/CorpusID:202749930

    2019 arXiv

  36. [44]

    Mohamed Nassim Seghir and Daniel Kroening. 2013. Counterexample-guided pre- condition inference. InEuropean Symposium on Programming. Springer, 451–471

    2013

  37. [45]

    Richard Rutledge, Sheryl Duggins, Dan Lo, and Frank Tsui. 2014. Formal specification-driven development. InProceedings of the International Conference on Software Engineering Research and Practice (SERP) . The Steering Committee of The World Congress in Computer Science, Compu...

    2014

  38. [46]

    Naik, and Le Song

    Xujie Si, Aaditya Naik, Hanjun Dai, M. Naik, and Le Song. 2020. Code2Inv: A Deep Learning Framework for Program Verification.Computer Aided Verification 12225 (2020), 151–164. https://api.semanticscholar.org/CorpusID:211027794

    2020

  39. [47]

    Charlie Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. 2024. Scaling llm test-time compute optimally can be more effective than scaling model parameters. arXiv preprint arXiv:2408.03314 (2024)

    2024 arXiv

  40. [48]

    Fink, and Marco Pistoia

    Sharon Shoham, Eran Yahav, Stephen J. Fink, and Marco Pistoia

  41. [49]

    IEEE Transactions on Software Engineering 34 (2007), 651–666

    Static Specification Mining Using Automata-Based Abstrac- tions. IEEE Transactions on Software Engineering 34 (2007), 651–666. https://api.semanticscholar.org/CorpusID:2483401

    2007

  42. [50]

    Lin Tan, Ding Yuan, Gopal Krishna, and Yuanyuan Zhou. 2007. /* iComment: Bugs or bad comments?*. InACM SIGOPS Operating Systems Review. ACM, 145–158

    2007

  43. [51]

    Lin Tan, Yuanyuan Zhou, and Yoann Padioleau. 2011. aComment: mining annotations from comments and code to detect interrupt related concurrency bugs, In Software Engineering (ICSE), 2011 33rd International Conference on. 2011 33rd International Conference on Software Engineerin...

    2011

  44. [52]

    Colin Frank Snook. 2001. Exploring the barriers to formal specification . Ph. D. Dissertation. University of Southampton

    2001

  45. [53]

    Weisong Sun, Chunrong Fang, Yun Miao, Yudu You, Mengzhe Yuan, Yuchen Chen, Quanjun Zhang, An Guo, Xiang Chen, Yang Liu, et al. 2023. Abstract syntax tree for programming language understanding and representation: How far are we? arXiv preprint arXiv:2312.00413 (2023)

    2023 arXiv

  46. [54]

    Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park, and Flavio Lerda. 2003. Model checking programs. Automated software engineering 10, 2 (2003), 203–232

    2003

  47. [55]

    Hendryx, Summer Yue, and Hugh Zhang

    Evan Z Wang, Federico Cassano, Catherine Wu, Yunfeng Bai, William Song, Vaskar Nath, Ziwen Han, Sean M. Hendryx, Summer Yue, and Hugh Zhang

  48. [56]

    Shin Hwei Tan, Darko Marinov, Lin Tan, and Gary T Leavens. 2012. @tcomment: Testing javadoc comments to detect comment-code inconsistencies, In Software Testing, Verification and Validation (ICST), 2012 IEEE Fifth International Confer- ence on. 2012 IEEE Fifth International Co...

    2012

  49. [57]

    Niki Vazou, Eric L Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon Peyton- Jones. 2014. Refinement types for Haskell. In ACM SIGPLAN Notices . ACM, 269–282

    2014

  50. [58]

    Sean Welleck, Amanda Bertsch, Matthew Finlayson, Hailey Schoelkopf, Alex Xie, Graham Neubig, Ilia Kulikov, and Zaid Harchaoui. 2024. From decoding to meta-generation: Inference-time algorithms for large language models. arXiv preprint arXiv:2406.16838 (2024)

    2024 arXiv

  51. [59]

    Yangzhen Wu, Zhiqing Sun, Shanda Li, Sean Welleck, and Yiming Yang. 2024. An empirical analysis of compute-optimal inference for problem-solving with language models. (2024)

    2024

  52. [60]

    Yangzhen Wu, Zhiqing Sun, Shanda Li, Sean Welleck, and Yiming Yang. 2024. Inference scaling laws: An empirical analysis of compute-optimal inference for problem-solving with language models. arXiv preprint arXiv:2408.00724 (2024)

    2024 arXiv

  53. [61]

    Peiyi Wang, Lei Li, Zhihong Shao, RX Xu, Damai Dai, Yifei Li, Deli Chen, Yu Wu, and Zhifang Sui. 2023. Math-shepherd: Verify and reinforce llms step-by-step without human annotations. arXiv preprint arXiv:2312.08935 (2023)

    2023 arXiv

  54. [62]

    Weishi Wang, Yue Wang, Shafiq Joty, and Steven CH Hoi. 2023. Rap-gen: Retrieval-augmented patch generation with codet5 for automatic program repair. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engin...

    2023

  55. [63]

    Yuxi Xie, Kenji Kawaguchi, Yiran Zhao, James Xu Zhao, Min-Yen Kan, Junxian He, and Michael Xie. 2023. Self-evaluation guided beam search for reasoning. Advances in Neural Information Processing Systems 36 (2023), 41618–41650

    2023

  56. [64]

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data.arXiv preprint arXiv:2405.14333 (2024)

    2024 arXiv

  57. [65]

    Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2024. Leandojo: Theorem proving with retrieval-augmented language models.Advances in Neural Information Processing Systems 36 (2024)

    2024

  58. [66]

    Danning Xie, Yitong Li, Mijung Kim, Hung Viet Pham, Lin Tan, Xiangyu Zhang, and Michael W Godfrey. 2022. DocTer: documentation-guided fuzzing for testing deep learning API functions. InProceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis...

    2022

  59. [67]

    Danning Xie, Byungwoo Yoo, Nan Jiang, Mijung Kim, Lin Tan, Xiangyu Zhang, and Judy S Lee. 2023. Impact of large language models on generating software specifications. arXiv preprint arXiv:2306.03324 (2023)

    2023 arXiv

  60. [68]

    He Ye and Martin Monperrus. 2024. Iter: Iterative neural repair for multi-location patches. In Proceedings of the 46th IEEE/ACM International Conference on Software Engineering. 1–13

    2024

  61. [69]

    Andreas Zeller and Ralf Hildebrandt. 2002. Simplifying and isolating failure- inducing input. IEEE Transactions on software engineering 28, 2 (2002), 183–200

    2002

  62. [70]

    Juan Zhai, Yu Shi, Minxue Pan, Guian Zhou, Yongxiang Liu, Chunrong Fang, Shiqing Ma, Lin Tan, and Xiangyu Zhang. 2020. C2S: translating natural language comments to formal program specifications. InProceedings of the 28th ACM Joint Meeting on European Software Engineering Conf...

    2020

  63. [71]

    Ling Yang, Zhaochen Yu, Bin Cui, and Mengdi Wang. 2025. ReasonFlux: Hierarchical LLM Reasoning via Scaling Thought Templates. arXiv preprint arXiv:2502.06772 (2025)

    2025 arXiv

  64. [72]

    Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2023. Harnessing the power of large language models for natural language to first-order logic translation. arXiv preprint arXiv:2305.15541 (2023)

    2023 arXiv

  65. [73]

    Kunhao Zheng, Juliette Decugis, Jonas Gehring, Taco Cohen, benjamin ne- grevergne, and Gabriel Synnaeve. 2025. What Makes Large Language Models Reason in (Multi-Turn) Code Generation?. InThe Thirteenth International Confer- ence on Learning Representations. https://openreview....

    2025

  66. [74]

    Hao Zhong, Lu Zhang, Tao Xie, and Hong Mei. 2009. Inferring resource specifications from natural language API documentation. In Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering. IEEE Computer Society, 307–318

    2009

  67. [75]

    Andy Zhou, Kai Yan, Michal Shlapentokh-Rothman, Haohan Wang, and Yu-Xiong Wang. 2023. Language agent tree search unifies reasoning acting and planning in language models. arXiv preprint arXiv:2310.04406 (2023)

    2023 arXiv

  68. [76]

    Shun Zhang, Zhenfang Chen, Yikang Shen, Mingyu Ding, Joshua B Tenenbaum, and Chuang Gan. 2023. Planning with large language models for code generation. arXiv preprint arXiv:2303.05510 (2023)

    2023 arXiv

  69. [77]

    Shiyu Zhang, Juan Zhai, Bu Lei, Wang Linzhang, and Xuandong Li. 2020. Auto- mated geration of LTL Specifications For Smart Home IoT Using Natural Language. In 2020 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE

    2020

  70. [81]

    Yu Zhou, Ruihang Gu, Taolue Chen, Zhiqiu Huang, Sebastiano Panichella, and Harald Gall. 2017. Analyzing APIs documentation and code to detect directive defects. In 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). IEEE, 27–37

    2017

  71. [2007]

    Bouncer: Securing software by blocking bad input.ACM SIGOPS Operating Systems Review 41, 6 (2007), 117–130

    2007

  72. [2024]

    Can large language models transform natural language intent into formal method postconditions? Proceedings of the ACM on Software Engineering 1, FSE (2024), 1889–1912

    2024

  73. [2025]

    In The Thirteenth International Conference on Learning Representations

    Planning in Natural Language Improves LLM Search for Code Gener- ation. In The Thirteenth International Conference on Learning Representations . https://openreview.net/forum?id=48WAZhwHHw

Pith tools

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