测试大模型能否准确推断程序语义，发现其在复杂循环上表现差。
Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference
- 构建新基准FormalBench，评估模型生成精确形式化规范的能力。
- 简单控制流下表现良好，复杂循环中成功率不足30%。
- 提出自修复提示，使成功率达提升25%，适合验证工具开发者参考。
大型语言模型（LLMs）在自动化编程任务中应用日益广泛，但其对程序语义的推理能力尚未得到充分研究。本文提出FormalBench，一个全面的基准，用于评估LLMs在程序语义推理方面的能力，特别是通过合成形式化程序规范来辅助验证程序正确性。该任务需对所有可能的程序执行路径进行综合推理，并生成符合形式语法与语义的精确表达式。利用此基准，我们评估了LLMs生成一致且完整规范的能力。结果表明，当面对简单控制流时，模型表现良好；但在复杂结构，尤其是循环结构中仍存在显著困难，即便使用高级提示策略亦然。此外，模型对语义保持但结构变化的转换缺乏鲁棒性。我们还识别出常见失败模式，并设计自修复提示，使成功率提升25%。
原文摘要 · Abstract (English)
Large Language Models (LLMs) are increasingly being used to automate programming tasks. Yet, LLMs' capabilities in reasoning about program semantics are still inadequately studied, leaving significant potential for further exploration. This paper introduces FormalBench, a comprehensive benchmark designed to evaluate LLMs' reasoning abilities on program semantics, particularly via the task of synthesizing formal program specifications to assist verifying program correctness. This task requires both comprehensive reasoning over all possible program executions and the generation of precise, syntactically correct expressions that adhere to formal syntax and semantics. Using this benchmark, we evaluated the ability of LLMs in synthesizing consistent and complete specifications. Our findings show that LLMs perform well with simple control flows but struggle with more complex structures, especially loops, even with advanced prompting. Additionally, LLMs exhibit limited robustness against semantic-preserving transformations. We also highlight common failure patterns and design self-repair prompts, improving success rates by 25%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。