FRETish

新指南促进自然语言需求形式化的一致性

研究人员提出了一个名为“通过形式化实现一致性”的新指南，用于将自然语言需求翻译成形式语言。该原则表明，从自然语言到形式语言的不同形式化级别应保持相似的逻辑结构。该方法特别适用于在可由形式化工具验证的推理任务中使用大型语言模型（LLMs），其中结构化自然语言充当中间层。论文分析了NASA的形式化需求获取工具（FRET），并提供了一种从FRETish到MTL的替代自动化翻译，通过模型检查证明其等价性，并展示了支持新翻译的发现。