德克萨斯大学奥斯汀分校 发布 CLEVER 数据集, 应用在 程序合成、形式推理 领域

德克萨斯大学奥斯汀分校 本次发布的数据集 CLEVER, CLEVER是一个高质量的精选基准，包含161个编程任务，用于在Lean中生成端到端验证代码。每个问题都包括生成与保留的真实规范匹配的规范的任务，以及生成证明满足此规范的Lean实现的任务。与以前的基准不同，CLEVER避免了测试用例监督、LLM生成的注释以及可能泄露实现逻辑或允许空解决方案的规范。所有输出都使用Lean的类型检查器进行后验验证，以确保机器可检查的正确性。CLEVER用于评估基于最先进语言模型的几个少样本和代理方法。这些方法都难以实现完全验证，从而确立了它在程序合成和形式推理方面的挑战性前沿基准。我们的基准可以在GitHub和HuggingFace上找到。所有我们的评估代码也在线可用。

查看CLEVER

Dataset card 内容： 

Files and versions 内容： 

关于 德克萨斯大学奥斯汀分校 , 德克萨斯大学奥斯汀分校是美国德克萨斯州的一所公立研究型大学，位于德克萨斯州的首府奥斯汀市。该校是德克萨斯大学系统中的旗舰校园，也是美国最负盛名的大学之一，以其优秀的教育质量和研究水平著称。

关于 arXiv , arXiv 是一个免费分发服务和开放获取的学术文章档案库，涵盖了物理学、数学、计算机科学、定量生物学、定量金融、统计学、电气工程和系统科学以及经济学等领域。该网站上的材料并未经过 arXiv 的同行评审。