# SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 12 of its 62 references that are in the map.
- First posted on arXiv 24 Feb 2026.

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

- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [RLEF: Grounding Code LLMs in Execution Feedback with Reinforcement Learning](https://mlsanity.com/paper/2410.02089/) (2024)
- [Unit Test Case Generation with Transformers and Focal Context](https://mlsanity.com/paper/2009.05617/) (2020)
- [TOGA: A Neural Method for Test Oracle Generation](https://mlsanity.com/paper/2109.09262/) (2021)
- [Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?](https://mlsanity.com/paper/2310.01831/) (2023)
- [Interactive Code Generation via Test-Driven User-Intent Formalization](https://mlsanity.com/paper/2208.05950/) (2022)
- [CoverUp: Effective High Coverage Test Generation for Python](https://mlsanity.com/paper/2403.16218/) (2024)
- [Can Large Language Models Write Good Property-Based Tests?](https://mlsanity.com/paper/2307.04346/) (2023)
- [Generating Accurate Assert Statements for Unit Test Cases using Pretrained Transformers](https://mlsanity.com/paper/2009.05634/) (2020)
- [Using Transfer Learning for Code-Related Tasks](https://mlsanity.com/paper/2206.08574/) (2022)
- [Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)](https://mlsanity.com/paper/2003.07959/) (2020)
- [Learning Invariants using Decision Trees](https://mlsanity.com/paper/1501.04725/) (2015)

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

- [Teaching Code LLMs to Reason with Intermediate Formal Specifications](https://mlsanity.com/paper/2607.04232/) (2026)
- [Multi-Large Language Model Orchestrated Severity Assessment of Clinical Records (MOSAIC)](https://mlsanity.com/paper/2607.05032/) (2026)

## Abstract (arXiv)

Specifications are vital for ensuring program correctness, yet writing them manually remains challenging and time-intensive. Recent large language model (LLM)-based methods have shown successes in generating specifications such as postconditions, but existing single-pass prompting often yields inaccurate results. In this paper, we present SpecMind, a novel framework for postcondition generation that treats LLMs as interactive and exploratory reasoners rather than one-shot generators. SpecMind employs feedback-driven multi-turn prompting approaches, enabling the model to iteratively refine candidate postconditions by incorporating implicit and explicit correctness feedback, while autonomously deciding when to stop. This process fosters deeper code comprehension and improves alignment with true program behavior via exploratory attempts. Our empirical evaluation shows that SpecMind significantly outperforms state-of-the-art approaches in both accuracy and completeness of generated postconditions.