Clever

该数据集是一个高质量、精心筛选的基准，包含了161个问题，旨在推动_Lean_编程语言中的端到端验证代码生成。每个问题都要求生成一个规范说明以及一个满足该规范的_Lean_实现，并通过_Lean_的类型检查器来验证输出结果。此外，该基准设计避免了测试用例的监督，确保输出结果是事后验证的，从而使其成为程序合成和形式推理领域的挑战性前沿基准。任务内容为端到端的验证代码生成。