Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The Karp Dataset

Mason DiCicco, Eamon Worden, Conner Olsen, Nikhil Gangaram, Daniel Reichman, Neil Heffernan

TL;DR

The paper tackles assessing and improving the mathematical reasoning of large language models by introducing the Karp dataset, a collection of about 90 natural-language proofs of NP-hardness reductions sourced from literature. It provides a structured LaTeX-to-natural-language format with a consistent template and two evaluation sets (test and challenge), and reports results across Strawberry, Llama, and a fine-tuned LlamaReduce model. Key contributions include the dataset itself, a careful evaluation protocol with manual scoring, and evidence that prompt design and fine-tuning can boost performance on undergraduate-level reductions while remaining difficult for harder tasks. The work highlights both the potential and the challenges of automatic verification of formal reductions and suggests future directions toward machine-verifiable representations and broader datasets.

Abstract

Understanding the mathematical reasoning capabilities of Large Language Models (LLMs) is a central topic in the study of artificial intelligence. This new domain necessitates the creation of datasets of reasoning tasks for both training and benchmarking the performance of LLMs. To this end, we introduce the Karp dataset: The first dataset composed of detailed proofs of NP-completeness reductions. The reductions vary in difficulty, ranging from simple exercises of undergraduate courses to more challenging reductions from academic papers. We compare the performance of state-of-the-art models on this task and demonstrate the effect of fine-tuning with the Karp dataset on reasoning capacity.

The Karp Dataset

TL;DR

The paper tackles assessing and improving the mathematical reasoning of large language models by introducing the Karp dataset, a collection of about 90 natural-language proofs of NP-hardness reductions sourced from literature. It provides a structured LaTeX-to-natural-language format with a consistent template and two evaluation sets (test and challenge), and reports results across Strawberry, Llama, and a fine-tuned LlamaReduce model. Key contributions include the dataset itself, a careful evaluation protocol with manual scoring, and evidence that prompt design and fine-tuning can boost performance on undergraduate-level reductions while remaining difficult for harder tasks. The work highlights both the potential and the challenges of automatic verification of formal reductions and suggests future directions toward machine-verifiable representations and broader datasets.

Abstract

Understanding the mathematical reasoning capabilities of Large Language Models (LLMs) is a central topic in the study of artificial intelligence. This new domain necessitates the creation of datasets of reasoning tasks for both training and benchmarking the performance of LLMs. To this end, we introduce the Karp dataset: The first dataset composed of detailed proofs of NP-completeness reductions. The reductions vary in difficulty, ranging from simple exercises of undergraduate courses to more challenging reductions from academic papers. We compare the performance of state-of-the-art models on this task and demonstrate the effect of fine-tuning with the Karp dataset on reasoning capacity.
Paper Structure (30 sections, 1 theorem, 2 figures, 4 tables)

This paper contains 30 sections, 1 theorem, 2 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Related work
  3. Evaluating large language models on the Karp dataset
  4. The Karp dataset
  5. Formatting
  6. Omitted details
  7. Experiments
  8. Test set
  9. Prompts
  10. Scoring
  11. Models
  12. Results
  13. Example prompts and responses
  14. Prompt
  15. Response
  16. ...and 15 more sections

Key Result

Theorem 1

Problem X reduces to Problem Y

Figures (2)

  • Figure 1: Our reduction template (left) compared to MATH (middle) and GSM8k (right)
  • Figure 2: The distribution of lengths (i.e., number of characters) of reductions in the dataset. Most reductions have lengths between 1000 and 3000 characters. The minimum is 939, the maximum is 5789, and the mean is 2180.

Theorems & Definitions (2)

  • Theorem 1
  • proof