Stakeholders often describe system requirements using natural language which
are then converted to formal syntax by a domain-expert leading to increased
design costs. This paper assesses the capabilities of Large Language Models
(LLMs) in converting between natural language descriptions and formal
specifications. Existing work has evaluated the capabilities of LLMs in
generating formal syntax such as source code but such experiments are typically
hand-crafted and use problems that are likely to be in the training set of
LLMs, and often require human-annotated datasets. We propose an approach that
can use two copies of an LLM in conjunction with an off-the-shelf verifier to
automatically evaluate its translation abilities without any additional human
input. Our approach generates formal syntax using language grammars to
automatically generate a dataset. We conduct an empirical evaluation to measure
the accuracy of this translation task and show that SOTA LLMs cannot adequately
solve this task, limiting their current utility in the design of complex
systems.

利用大型语言模型 (LLMs) 将自然语言描述转换为形式化规范的能力进行了评估，提出了一种使用两个 LLMs 与现成验证程序结合的方法来自动评估其翻译能力，结果显示目前最先进的 LLMs 无法充分解决这个任务，限制了它们在复杂系统设计中的实用性。

LLM 能够正式对话吗？自动评估 LLM 在翻译和解释正式规范中的表现

Can LLMs Converse Formally? Automatically Assessing LLMs in Translating  and Interpreting Formal Specifications

Large language models (LLMs) like ChatGPT and GPT-4 have exhibited remarkable
abilities on a wide range of natural language processing (NLP) tasks, including
various machine translation abilities accomplished during chat. However, these
models are only accessible through restricted APIs, which creates barriers to
new research and advancements in the field. Therefore, we propose the
$\mathbf{ParroT}$ framework to enhance and regulate the translation abilities
during chat based on open-sourced LLMs (i.e., LLaMA-7b) and human written
translation and evaluation data. Specifically, ParroT reformulates translation
data into the instruction-following style, and introduces a "Hint" field for
incorporating extra requirements to regulate the translation process.
Accordingly, we propose three instruction types for finetuning ParroT models,
including translation instruction, contrastive instruction, and error-guided
instruction. Experiments on two Flores subsets and WMT22 test sets suggest that
translation instruction improves the translation performance of vanilla LLMs
significantly while error-guided instruction can lead to a further improvement,
which demonstrates the importance of learning from low-quality translations
annotated by human. Meanwhile, the ParroT models can also preserve the ability
on general tasks with the Alpaca multi-task dataset involved in finetuning.
Codes: this https URL

提出了基于开源 LLMS（LLaMA-7b）和人工翻译评估数据的 ParroT 框架，该框架通过重新规划翻译数据到遵循指令的风格，并引入 “提示” 字段，以调节翻译过程。通过 Finetuning ParroT 模型的三种指令类型，包括翻译指令、对比指令和误差引导指令，实验结果显示翻译指令可以显着提高香草 LLMS 的翻译性能，而误差引导指令则进一步改善了翻译性能，并展示了从人工注释的低质量翻译中学习的重要性。同时，ParroT 模型也可以通过包含多任务数据集 Alpaca 的精调任务中保持其对通用任务的能力。