# Breaking the Myth: Can Small Models Infer Postconditions Too?

arXiv: https://arxiv.org/abs/2507.10182 · HTML: https://mlsanity.com/paper/2507.10182/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 7 of its 71 references that are in the map.
- First posted on arXiv 14 Jul 2025.

## Builds on (most cited first, 7 of 7)

- [Self-Evaluation Guided Beam Search for Reasoning](https://mlsanity.com/paper/2305.00633/) (2023)
- [Planning In Natural Language Improves LLM Search For Code Generation](https://mlsanity.com/paper/2409.03733/) (2024)
- [ReasonFlux: Hierarchical LLM Reasoning via Scaling Thought Templates](https://mlsanity.com/paper/2502.06772/) (2025)
- [Don't throw away your value model! Generating more preferable text with Value-Guided Monte-Carlo Tree Search decoding](https://mlsanity.com/paper/2309.15028/) (2023)
- [KCTS: Knowledge-Constrained Tree Search Decoding with Token-Level Hallucination Detection](https://mlsanity.com/paper/2310.09044/) (2023)
- [What Makes Large Language Models Reason in (Multi-Turn) Code Generation?](https://mlsanity.com/paper/2410.08105/) (2024)
- [Generating Symbolic Reasoning Problems with Transformer GANs](https://mlsanity.com/paper/2110.10054/) (2021)

## Built on by (most cited first, 1 of 1)

- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)

## Abstract (arXiv)

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 7B-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.