Psychometric-Based Evaluation for Theorem Proving with Large Language Models

• URL: http://arxiv.org/abs/2502.00855v1
• Date: Sun, 02 Feb 2025 17:00:22 GMT
• Title: Psychometric-Based Evaluation for Theorem Proving with Large Language Models
• Authors: Jianyu Zhang, Yongwang Zhao, Long Zhang, Jilin Hu, Xiaokun Luan, Zhiwei Xu, Feng Yang,
• Abstract summary: This study proposes a psychometric-based evaluation method for theorem proving with large language models (LLMs) We propose a metric calculation method to annotate the dataset with difficulty and discrimination metrics. Specifically, we annotate each theorem in the miniF2F dataset and grade them into varying difficulty levels according to the performance of LLMs. We design an adaptive evaluation method to dynamically select the most suitable theorems for testing based on the annotated metrics and the real-time performance of LLMs.
• Score: 14.101509169786349
• License:
• Abstract: Large language models (LLMs) for formal theorem proving have become a prominent research focus. At present, the proving ability of these LLMs is mainly evaluated through proof pass rates on datasets such as miniF2F. However, this evaluation method overlooks the varying importance of theorems. As a result, it fails to highlight the real performance disparities between LLMs and leads to high evaluation costs. This study proposes a psychometric-based evaluation method for theorem proving with LLMs, comprising two main components: Dataset Annotation and Adaptive Evaluation. First, we propose a metric calculation method to annotate the dataset with difficulty and discrimination metrics. Specifically, we annotate each theorem in the miniF2F dataset and grade them into varying difficulty levels according to the performance of LLMs, resulting in an enhanced dataset: miniF2F-Graded. Experimental results show that the difficulty grading in miniF2F-Graded better reflects the theorem difficulty perceived by LLMs. Secondly, we design an adaptive evaluation method to dynamically select the most suitable theorems for testing based on the annotated metrics and the real-time performance of LLMs. We apply this method to evaluate 10 LLMs. The results show that our method finely highlights the performance disparities between LLMs. It also reduces evaluation costs by using only 23% of the theorems in the dataset.

Related papers

• Performance Law of Large Language Models [58.32539851241063]
  Performance law can be used to guide the choice of LLM architecture and the effective allocation of computational resources. Performance law can be used to guide the choice of LLM architecture and the effective allocation of computational resources without extensive experiments.
  arXiv  Detail & Related papers  (2024-08-19T11:09:12Z)
• Evaluating Human Alignment and Model Faithfulness of LLM Rationale [66.75309523854476]
  We study how well large language models (LLMs) explain their generations through rationales. We show that prompting-based methods are less "faithful" than attribution-based explanations.
  arXiv  Detail & Related papers  (2024-06-28T20:06:30Z)
• MindStar: Enhancing Math Reasoning in Pre-trained LLMs at Inference Time [51.5039731721706]
  MindStar is a purely inference-based searching method for large language models. It formulates reasoning tasks as searching problems and proposes two search ideas to identify the optimal reasoning paths. It significantly enhances the reasoning abilities of open-source models, such as Llama-2-13B and Mistral-7B, and achieves comparable performance to GPT-3.5 and Grok-1.
  arXiv  Detail & Related papers  (2024-05-25T15:07:33Z)
• DnA-Eval: Enhancing Large Language Model Evaluation through Decomposition and Aggregation [75.81096662788254]
  Large Language Models (LLMs) are scalable and economical evaluators. The question of how reliable these evaluators are has emerged as a crucial research question. We propose Decompose and Aggregate, which breaks down the evaluation process into different stages based on pedagogical practices.
  arXiv  Detail & Related papers  (2024-05-24T08:12:30Z)
• Large Language Models are Inconsistent and Biased Evaluators [2.136983452580014]
  We show that Large Language Models (LLMs) are biased evaluators as they exhibit familiarity bias and show skewed distributions of ratings. We also found that LLMs are inconsistent evaluators, showing low "inter-sample" agreement and sensitivity to prompt differences that are insignificant to human understanding of text quality.
  arXiv  Detail & Related papers  (2024-05-02T20:42:28Z)
• Do Large Language Models Rank Fairly? An Empirical Study on the Fairness of LLMs as Rankers [27.66626125248612]
  This paper presents an empirical study evaluating Large Language Models (LLMs) using the TREC Fair Ranking dataset. We focus on the representation of binary protected attributes such as gender and geographic location, which are historically underrepresented in search outcomes. Our analysis delves into how these LLMs handle queries and documents related to these attributes, aiming to uncover biases in their ranking algorithms.
  arXiv  Detail & Related papers  (2024-04-04T04:23:19Z)
• Evaluating the Factuality of Large Language Models using Large-Scale Knowledge Graphs [30.179703001666173]
  Factuality issue is a critical concern for Large Language Models (LLMs) We propose GraphEval to evaluate an LLM's performance using a substantially large test dataset. Test dataset is retrieved from a large knowledge graph with more than 10 million facts without expensive human efforts.
  arXiv  Detail & Related papers  (2024-04-01T06:01:17Z)
• Comprehensive Reassessment of Large-Scale Evaluation Outcomes in LLMs: A Multifaceted Statistical Approach [64.42462708687921]
  Evaluations have revealed that factors such as scaling, training types, architectures and other factors profoundly impact the performance of LLMs. Our study embarks on a thorough re-examination of these LLMs, targeting the inadequacies in current evaluation methods. This includes the application of ANOVA, Tukey HSD tests, GAMM, and clustering technique.
  arXiv  Detail & Related papers  (2024-03-22T14:47:35Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  Large language models (LLMs) have been treated as knowledge bases due to their strong performance in knowledge probing tasks. How do we evaluate the capabilities of LLMs to consistently produce factually correct answers? We propose MOdel kNowledge relIabiliTy scORe (MONITOR), a novel metric designed to directly measure LLMs' factual reliability.
  arXiv  Detail & Related papers  (2023-10-15T12:40:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.