CLEVER：一个经过精心策划的形式化验证代码生成基准

本文介绍了一个高质量的基准数据集CLEVER，包含161个问题，专注于验证代码生成的任务。与之前的基准不同，CLEVER避免了测试用例监督和生成的注释，确保所有输出通过Lean的类型检查器进行后验验证，以保证可机检查的正确性。研究表明，现有的少样本和自主方法在实现完全验证方面面临挑战，揭示了程序合成和形式推理的前沿难题。

本文介绍了高质量基准数据集CLEVER，包含161个专注于代码生成验证的问题。CLEVER避免了测试用例监督，确保输出通过Lean类型检查器验证，揭示了程序合成和形式推理的挑战。

CLEVER 代码生成 基准数据集 形式推理 验证
原文中文，约300字，阅读约需1分钟。发表于：。
阅读原文
分享给好友