# Formalizing Natural Language Intent into Program Specifications via Large Language Models

**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/arxiv-id/2310.01831v1/

## Key points

- Informal natural language in software development provides valuable insights but may not always align with the actual implementation
- Large Language Models (LLMs) can translate natural language intent into programmatically checkable assertions
- LLM4nl2post transforms informal descriptions into formal method postconditions for identifying incorrect code
- Generated postconditions are accurate, correct, and capable of discriminating faulty code
- LLM4nl2post successfully identified 70 real-world bugs from Defects4J across different programming languages
- LLM4nl2post captures abstract functional relationships between input and output procedures effectively
- Efforts have been made to address limitations such as data leakage concerns and model stability issues for transparency in findings

## Summary

, , , , 

In the realm of software development, informal natural language often provides valuable insights into a program's intent through code comments and function documentation. However, the alignment between this natural language description and the actual implementation of a program is not always guaranteed. This misalignment can lead to challenges in fault localization, debugging, and overall code trustworthiness. Large Language Models (LLMs) have emerged as a potential solution to translate natural language intent into programmatically checkable assertions. A new approach, LLM4nl2post, leverages LLMs to transform informal natural language descriptions into formal method postconditions expressed as program assertions. By introducing and validating metrics to measure the correctness and discriminative power of generated postconditions, researchers have demonstrated that LLM4nl2post can generate accurate specifications that effectively identify incorrect code. Furthermore, qualitative and quantitative assessments have shown that these postconditions are generally correct and capable of discriminating faulty code. Moreover, the study has highlighted the practical utility of LLM4nl2post by successfully identifying 70 real-world historical bugs from Defects4J. The experiment showcases the versatility of this technique across different programming languages such as Python and Java. While machine learning-based approaches for specification generation have shown promise in various applications, including test oracle synthesis and unit test generation, LLM4nl2post stands out for its ability to capture abstract functional relationships between input and output procedures. Despite potential limitations such as data leakage concerns related to training datasets like EvalPlus and Defects4J, efforts have been made to ensure the replicability of the study results. By addressing stability issues with models accessed via OpenAI web APIs and providing access to generated artifacts, researchers aim to enhance transparency in their findings. Overall, the study underscores the significance of formalizing natural language intent into program specifications using cutting-edge technologies like Large Language Models for improved software development practices.