arXiv:2502.00855v1 宣告类型: 新 摘要: 正式定理证明的大语言模型（LLMs）已成为一个重要的研究焦点。目前，这些LLMs的证明能力主要通过在miniF2F等数据集上的证明通过率进行评估。然而，这种方法忽略了定理的不同重要性，导致未能突出LLMs之间的实际性能差异，且评估成本较高。本研究提出了一种基于心理测量的定理证明评估方法，该方法包含两个主要组成部分：数据集注释和自适应评估。首先，我们提出了一种度量计算方法，通过注释数据集中的难度和区分度度量来标注数据集。具体来说，我们为miniF2F数据集中的每个定理进行了注释，并根据LLMs的表现将其分为不同难度级别，从而得到了增强的数据集：miniF2F-Graded。实验结果显示，miniF2F-Graded中的难度分级更好地反映了LLMs感知到的定理难度。其次，我们设计了一种自适应评估方法，根据标注的度量和LLMs的实际表现动态选择最合适的定理进行测试。我们将该方法应用于10个LLMs的评估。结果显示，我们的方法细腻地突出了LLMs之间的性能差异，并通过仅使用数据集中的23%的定理减少了评估成本。