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

**Authors:** Madeline Endres, Sarah Fakhoury, Saikat Chakraborty, Shuvendu K. Lahiri  
**arXiv:** [2310.01831](https://arxiv.org/abs/2310.01831)  
**Date:** 2023-10-03  
**Summary page:** https://www.summarizepaper.com/en/paper/2310.01831v2/

## Key points

- Informal natural language specifications are crucial in modern software development for documenting code functionality.
- Weak association between natural language intent and code implementation often leads to software bugs.
- Translating informal natural language descriptions into formal specifications can help detect bugs early on and enhance trust in AI-generated code.
- Large Language Models (LLMs) like GPT-4 have shown promising abilities to synthesize high-quality code from natural language intent.
- nl2postcond is a novel approach that leverages LLMs to transform informal natural language into formal method postconditions expressed as program assertions.
- Results show that nl2postcond postconditions are generally correct and effective at identifying incorrect code, with the potential to catch real-world bugs from Defects4J.
- Using LLMs for translating natural language intent into formal specifications opens up new possibilities for improving software quality and trustworthiness in AI-assisted programming.

## Summary

In modern software development, informal natural language specifications play a crucial role in documenting code functionality. Studies have shown their prevalence in GitHub repositories and popular projects. However, the weak association between natural language intent and code implementation often leads to software bugs. This issue is further compounded in AI-assisted programming where code is generated from natural language descriptions without a reliable way to ensure accuracy. To address this challenge, translating informal natural language descriptions into formal specifications could help detect bugs early on and enhance trust in AI-generated code. Current approaches to translating natural language into formal specifications are limited by heuristics and structured input requirements, often tailored to specific programming languages. Large Language Models (LLMs) have emerged as a promising solution due to their ability to synthesize high-quality code from natural language intent. Despite not being explicitly trained for this task, larger models like GPT-4 have shown "emergent abilities" to excel in diverse tasks beyond their training data. This paper introduces nl2postcond, a novel approach that leverages LLMs to transform informal natural language into formal method postconditions expressed as program assertions. The study validates metrics for measuring different nl2postcond approaches based on correctness and discriminative power of generated postconditions. Results show that nl2postcond postconditions are generally correct and effective at identifying incorrect code, with the potential to catch real-world bugs from Defects4J. By exploring the use of LLMs for translating natural language intent into formal specifications, this research opens up new possibilities for improving software quality and trustworthiness in AI-assisted programming. The findings suggest that nl2postcond via LLMs has practical utility in enhancing fault localization, debugging processes, and overall code reliability.