$\forall$uto$\exists$val：LLM 在形式综合与解释任务中的自主评估
计算与语言
2024-07-23 v2 人工智能
摘要
本文提出了 utoval，一种用于扩展 LLM 在形式语法（如一阶逻辑、正则表达式等）翻译为自然语言（解释）或反之（编译）任务中评估的新方法，从而促进其在生成/解释程序逻辑和控制流等应用中的使用。这些领域现有的 LLM 评估方法需要耗费大量精力创建真值，而这会破坏训练集和测试集的分离。此外，此类数据集通常包含相对较少的手工编码测试用例，LLM 的准确性是基于这些用例确定的，因此不足以确定其生成输出的安全性或正确性。我们引入了一种新方法，利用上下文无关文法 (CFG) 即时生成分布外数据集，并使用形式验证器对 LLM 能力进行闭环测试，以保证 LLM 输出的正确性，无需任何人工干预。我们在 \url{https://github.com/AAIR-lab/auto-llm-assessment} 上以开源代码形式发布了我们的数据集和基准。我们还对几种 SOTA 闭源和开源 LLM 进行了评估，以展示这种范式的可行性和可扩展性。我们的实验表明，SOTA LLM 无法充分解决形式翻译任务。
引用
@article{arxiv.2403.18327,
title = {$\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks},
author = {Rushang Karia and Daniel Bramblett and Daksh Dobhal and Pulkit Verma and Siddharth Srivastava},
journal= {arXiv preprint arXiv:2403.18327},
year = {2024}
}