arXiv:2502.05714v1 类型: cross 摘要: 我们引入了形式化验证自动化编程进展标准，或FVAPPS，这是一个包含4715个样本的基准，用于编写程序并证明其正确性，这是最大的形式化验证基准，其中包括1083个经过精心选编和质量控制的样本。在此之前，APPS为编程谜题提供了一个基准和数据集，这些谜题需用Python完成，并通过单元测试进行检查，类似于软件工程行业中技术评估中所见的类型。在近期在交互定理证明基准方法的基础上，我们将单元测试推广到Lean 4定理中（即，使用Lean的"sorry"关键字）。在随机选取的100个样本中的406个定理上，Sonnet正确地证明了30%，Gemini正确地证明了18%。我们向机器学习和程序合成社区挑战，解决每个通用编程问题及其相关的正确性规范。基准数据集可在https://huggingface.co/datasets/quinn-dougherty/fvapps获取。