# Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?

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

## Key facts

- Cited by 57 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 58 references that are in the map.
- First posted on arXiv 3 Oct 2023.

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

- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Emergent Abilities of Large Language Models](https://mlsanity.com/paper/2206.07682/) (2022)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [CodeGen: An Open Large Language Model for Code with Multi-Turn Program Synthesis](https://mlsanity.com/paper/2203.13474/) (2022)
- [The Stack: 3 TB of permissively licensed source code](https://mlsanity.com/paper/2211.15533/) (2022)
- [Can language models learn from explanations in context?](https://mlsanity.com/paper/2204.02329/) (2022)
- [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 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)
- [CLN2INV: Learning Loop Invariants with Continuous Logic Networks](https://mlsanity.com/paper/1909.11542/) (2019)
- [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)
- [Towards Generating Functionally Correct Code Edits from Natural Language Issue Descriptions](https://mlsanity.com/paper/2304.03816/) (2023)
- [EvoSpex: An Evolutionary Algorithm for Learning Postconditions](https://mlsanity.com/paper/2102.13569/) (2021)

## Built on by (most cited first, 30 of 57)

- [SpecRover: Code Intent Extraction via LLMs](https://mlsanity.com/paper/2408.02232/) (2024)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification](https://mlsanity.com/paper/2412.14063/) (2024)
- [Agent READMEs: An Empirical Study of Context Files for Agentic Coding](https://mlsanity.com/paper/2511.12884/) (2025)
- [Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages](https://mlsanity.com/paper/2406.09757/) (2024)
- [LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations](https://mlsanity.com/paper/2407.02514/) (2024)
- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification](https://mlsanity.com/paper/2410.19940/) (2024)
- [Hallucination to Consensus: Multi-Agent LLMs for End-to-End JUnit Test Generation](https://mlsanity.com/paper/2506.02943/) (2025)
- [Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents](https://mlsanity.com/paper/2603.17150/) (2026)
- [Towards Formal Verification of LLM-Generated Code from Natural Language Prompts](https://mlsanity.com/paper/2507.13290/) (2025)
- [On the Effectiveness of Large Language Models in Writing Alloy Formulas](https://mlsanity.com/paper/2502.15441/) (2025)
- [Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?](https://mlsanity.com/paper/2510.12702/) (2025)
- [Agentic Verification of Software Systems](https://mlsanity.com/paper/2511.17330/) (2025)
- [Curiosity by Design: An LLM-based Coding Assistant Asking Clarification Questions](https://mlsanity.com/paper/2507.21285/) (2025)
- [Nexus: Execution-Grounded Multi-Agent Test Oracle Synthesis](https://mlsanity.com/paper/2510.26423/) (2025)
- [QuadSentinel: Sequent Safety for Machine-Checkable Control in Multi-agent Systems](https://mlsanity.com/paper/2512.16279/) (2025)
- [CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation](https://mlsanity.com/paper/2604.12268/) (2026)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learning](https://mlsanity.com/paper/2408.09237/) (2024)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)
- [Program Skeletons for Automated Program Translation](https://mlsanity.com/paper/2504.07483/) (2025)
- [Generative transformations and patterns in LLM-native approaches for software verification and falsification](https://mlsanity.com/paper/2404.09384/) (2024)
- [Effective LLM Code Refinement via Property-Oriented and Structurally Minimal Feedback](https://mlsanity.com/paper/2506.18315/) (2025)
- [ReqInOne: A Large Language Model-Based Agent for Software Requirements Specification Generation](https://mlsanity.com/paper/2508.09648/) (2025)
- [Large Language Models for Software Testing: A Research Roadmap](https://mlsanity.com/paper/2509.25043/) (2025)
- [SpecMind: Cognitively Inspired, Interactive Multi-Turn Framework for Postcondition Inference](https://mlsanity.com/paper/2602.20610/) (2026)
- [Automated Lemma Discovery in Agentic Program Verification](https://mlsanity.com/paper/2603.22114/) (2026)
- [Spec-Harness: Assessing and Guiding LLM-Synthesized Formal Specifications Beyond Verifiability](https://mlsanity.com/paper/2604.00280/) (2026)

## Abstract (arXiv)

Informal natural language that describes code functionality, such as code comments or function documentation, may contain substantial information about a programs intent. However, there is typically no guarantee that a programs implementation and natural language documentation are aligned. In the case of a conflict, leveraging information in code-adjacent natural language has the potential to enhance fault localization, debugging, and code trustworthiness. In practice, however, this information is often underutilized due to the inherent ambiguity of natural language which makes natural language intent challenging to check programmatically. The emergent abilities of Large Language Models (LLMs) have the potential to facilitate the translation of natural language intent to programmatically checkable assertions. However, it is unclear if LLMs can correctly translate informal natural language specifications into formal specifications that match programmer intent. Additionally, it is unclear if such translation could be useful in practice. In this paper, we describe nl2postcond, the problem of leveraging LLMs for transforming informal natural language to formal method postconditions, expressed as program assertions. We introduce and validate metrics to measure and compare different nl2postcond approaches, using the correctness and discriminative power of generated postconditions. We then use qualitative and quantitative methods to assess the quality of nl2postcond postconditions, finding that they are generally correct and able to discriminate incorrect code. Finally, we find that nl2postcond via LLMs has the potential to be helpful in practice; nl2postcond generated postconditions were able to catch 64 real-world historical bugs from Defects4J.