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 LLM4nl2post, the problem 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 LLM4nl2post approaches, using the correctness and
discriminative power of generated postconditions. We then perform qualitative
and quantitative methods to assess the quality of LLM4nl2post postconditions,
finding that they are generally correct and able to discriminate incorrect
code. Finally, we find that LLM4nl2post via LLMs has the potential to be
helpful in practice; specifications generated from natural language were able
to catch 70 real-world historical bugs from Defects4J.

使用 LLM4nl2post 将非正式自然语言转化为形式化方法的后置条件，并通过验证度量在质量和生成的后置条件的可区分性方面进行比较。结果显示，这些后置条件通常是正确的且能够区分错误的代码，并且通过 LLMs 进行 LLM4nl2post 有潜力在实践中发挥重要作用，在 Defects4J 中成功捕获了 70 个真实世界历史 BUG。