arXiv:2505.02735v1 宣布类型: 新 摘要: 正式数学推理仍然是人工智能的重大挑战，现有基准存在的范围和规模限制阻碍了这一进展。为解决这一问题，我们提出了FormalMATH，这是一个大规模的Lean4基准，包含5,560个形式验证问题，涵盖了从高中奥林匹克挑战到本科生水平的定理，横跨多样化的领域（例如代数、应用数学、微积分、数论和离散数学）。为缓解手动形式化过程中的低效性，我们引入了一种新颖的人工智能辅助形式化流水线，该流水线结合了以下内容：（1）专门的大语言模型（LLMs）用于陈述形式化，（2）多LLM语义验证，以及（3）基于否定的反证筛选策略，使用现成的基于LLM的证明器。这种方法通过在手动验证前保留72.09%的陈述来减少专家注释成本，同时确保原自然语言问题的忠实性。我们对最先进的基于LLM的定理证明器的评价揭示了显著的局限性：即使是最强大的模型在实际采样预算下的成功率也只有16.46%，显示出明显的领域偏差（例如，在代数方面表现出色但在微积分方面失败），并且过分依赖简化自动化策略。值得注意的是，在链式推理场景中，我们发现自然语言解题指南与证明成功率之间存在一种反直觉的负相关关系，这表明人类编写的非正式推理在形式推理环境中引入了噪声而非清晰性。我们认为FormalMATH为形式数学推理提供了稳健的基准。