Validation is a central activity when developing formal specifications. Similarly to coding, a possible validation technique is to define upfront test cases or scenarios that a future specification should satisfy or not. Unfortunately, specifying such test cases is burdensome and error prone, which could cause users to skip this validation task. This paper reports the results of an empirical evaluation of using pre-trained large language models (LLMs) to automate the generation of test cases from natural language requirements. In particular, we focus on test cases for structural requirements of simple domain models formalized in the Alloy specification language. Our evaluation focuses on the state-of-the-art GPT-5 model, but results from other closed- and open-source LLMs are also reported. The results show that, in this context, GPT-5 is already quite effective at generating positive (and negative) test cases that are syntactically correct and that satisfy (or not) the given requirement, and that can detect many wrong specifications written by humans.

翻译：验证是开发形式化规约的核心活动。与编码类似，一种可行的验证技术是预先定义测试用例或场景，这些用例或场景应当（或不应当）被未来的规约所满足。然而，指定此类测试用例既繁琐又容易出错，可能导致用户跳过这一验证任务。本文报告了一项实证评估的结果，该评估旨在利用预训练大语言模型（LLM）从自然语言需求自动生成测试用例。我们特别关注针对简单领域模型的结构性需求所生成的测试用例，这些模型使用Alloy规约语言进行形式化描述。评估主要聚焦于当前最先进的GPT-5模型，同时也报告了其他闭源与开源LLM的结果。结果表明，在此背景下，GPT-5已能较为有效地生成语法正确、满足（或不满足）给定需求的正向（与负向）测试用例，并能检测出许多由人工编写的错误规约。