证明编码面试：形式化验证代码生成基准

我们介绍了形式化验证自动编程进度标准（FVAPPS），这是一个包含 4715 个样本的数据集，用于编写程序并证明其正确性，为目前规模最大的形式化验证基准，包括 1083 个经过精选和质量控制的样本。此前，APPS 提供了一个用于编程解谜的数据集和基准，可用 Python 完成并通过单元测试检查，这类单元测试在软件工程行业的技术评估中常见。基于最近在交互式定理证明中所采用的基准方法，我们将单元测试推广为 Lean 4 定理给定而无需证明（即使用 Lean 的“sorry”关键字）的形式。对于随机抽取的 100 个样本中的 406 个定理，Sonnet 正确证明了 30%，Gemini 正确证明了 18%。我们挑战机器学习和程序合成社区同时解决每个通用编程问题及其相关正确性规范。该基准可在 https://huggingface.co/datasets/quinn-dougherty/fvapps 获取。