基于心理测量学的大语言模型定理证明评估
人工智能
2025-02-04 v1
摘要
用于形式化定理证明的大语言模型（LLMs）已成为一个突出的研究焦点。目前，这些LLMs的证明能力主要通过数据集（如miniF2F）上的证明通过率来评估。然而，这种评估方法忽略了定理的不同重要性。因此，它未能突出LLMs之间的真实性能差异，并导致高昂的评估成本。本研究提出了一种基于心理测量学的LLMs定理证明评估方法，包含两个主要组成部分：数据集标注和自适应评估。首先，我们提出了一种度量计算方法，用难度和区分度指标来标注数据集。具体来说，我们标注了miniF2F数据集中的每个定理，并根据LLMs的性能将其分级为不同的难度级别，从而生成了一个增强的数据集：miniF2F-Graded。实验结果表明，miniF2F-Graded中的难度分级更好地反映了LLMs感知到的定理难度。其次，我们设计了一种自适应评估方法，根据标注的指标和LLMs的实时性能，动态选择最合适的定理进行测试。我们应用此方法评估了10个LLMs。结果表明，我们的方法精细地突出了LLMs之间的性能差异。它还通过仅使用数据集中23%的定理降低了评估成本。
引用
@article{arxiv.2502.00855,
title = {Psychometric-Based Evaluation for Theorem Proving with Large Language Models},
author = {Jianyu Zhang and Yongwang Zhao and Long Zhang and Jilin Hu and Xiaokun Luan and Zhiwei Xu and Feng Yang},
journal= {arXiv preprint arXiv:2502.00855},
year = {2025}
}