Pith. sign in

REVIEW 5 major objections 3 minor 1 cited by

The Karp Dataset

T0 review · 5 major / 3 minor · reviewed 2026-08-10 · deepseek-v4-flash

Pith's one-line read The Karp dataset introduces the first collection of 90 detailed NP-completeness reduction proofs, and early results show that current LLMs are far from mastering the task.

desk verdict Genuinely new dataset idea, but the artifact is unreleased and has concrete bugs; deserves review with major revision. read the letter →

arxiv 2501.14705 v1 pith:TCJ7R5XB submitted 2025-01-24 cs.LG cs.CL

classification cs.LGcs.CL MSC 68Q1768T50
keywords NP-completenessreductionsLLMreasoningmathematicalbenchmarkfine-tuningnaturallanguageproofscomputationalcomplexityKarpdataset
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper introduces the Karp dataset, which it says is the first collection of detailed natural-language proofs of NP-completeness reductions. The dataset contains 90 reductions, sourced from textbooks, classic papers, and Karp's original 21 problems, formatted in a structured template that pairs a mapping with a correctness proof. The authors argue that constructing reductions is a high-level reasoning task well suited to exposing the strengths and limits of large language models, and they report initial results: fine-tuning Llama 70B-Instruct on the dataset lifts its score on an eight-problem test set from 0.875 to 1.25 out of 2, while OpenAI's Strawberry model scores 1.5 on that set and 0.875 on a harder challenge set. A sympathetic reader should care because the dataset opens a new, harder benchmark category for mathematical reasoning in LLMs, beyond arithmetic word problems.

What carries the argument

The load-bearing artifact is the dataset itself: 90 reductions, each written in a strict template that states the source and target decision problems, defines a mapping, and proves correctness in both directions using natural language, with polynomial-time computability and NP-membership verification deliberately omitted. The template is designed to make the proofs machine-readable enough for LLMs while staying in natural language. Fine-tuning uses QLoRA on the Llama 70B-Instruct base model, and evaluation relies on a human expert scoring each generated reduction 0, 1, or 2.

What would settle it

Audit all 90 proofs with an independent verifier, such as a team of complexity theorists or an automated checker like the Karp language. If a substantial fraction of the reductions contains uncorrectable errors, or if independent experts score the same model responses very differently from the single graduate student scorer, the benchmark's model rankings and fine-tuning conclusions would be called into question.

Watch

Extended reading notes

Core claim

The central claim is that the Karp dataset is a viable resource for training and benchmarking LLMs on NP-completeness reductions, and that existing models are far from mastering the task. On the paper's small human-scored test set, the best model scores 1.5 of 2, and on a more challenging held-out set the best score drops to 0.875, with fine-tuning providing only a modest boost. The paper concludes that reductions remain a difficult reasoning task for current LLMs, that fine-tuning is helpful for easier reductions, and that prompt engineering (as embodied by Strawberry) seems to matter more for the easier test-set problems.

Load-bearing premise

The whole benchmark stands on the accuracy and correctness of the 90 hand-written reductions, but the full dataset is not released in the paper and no external audit, formal verification, or inter-annotator check is provided.

Editorial extensions

If this is right

  • The dataset gives the community a new benchmark for LLM reasoning at the undergraduate-to-graduate theoretical CS level, distinct from arithmetic word problems.
  • Fine-tuning on this dataset transfers to improved performance on held-out homework-level reductions, suggesting the dataset is useful for instruction tuning.
  • Hard challenge-set reductions remain largely unsolved, indicating clear headroom for better models and methods.
  • The structured template could serve as a scaffold for automatic verification of natural-language proofs of reductions.
  • The low scores on challenge-set reductions suggest that reasoning about reductions requires capabilities beyond current chain-of-thought prompting.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the dataset deliberately omits polynomial-time computability and NP-membership proofs, it cannot, as released, certify full NP-completeness proofs; a verification chain would need to recover those pieces.
  • The full dataset is not publicly released and correctness rests on the authors' own proofs, so independent replication and error auditing are the natural next step; automated checkers like the Karp language could provide that audit.
  • The dataset could be extended beyond decision problems to hardness-of-approximation reductions, which the authors explicitly name as future work, potentially bridging complexity theory and optimization.
  • The small human-scored test sets, each with eight problems and a single scorer, limit the benchmark's statistical power; a larger pool with multiple annotators would give more reliable model rankings.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 3 minor

Summary. The paper introduces the Karp dataset, claimed to be the first dataset of detailed NP-completeness reductions, comprising 90 natural-language proofs organized in a structured LaTeX template. It evaluates three LLMs — OpenAI's Strawberry, Llama 70B-Instruct, and a fine-tuned variant called LlamaReduce — on two small hand-scored sets of eight reductions each, reporting fine-tuning gains on the test set and uniformly low performance on a more challenging set. The paper also reports MATH and MGSM accuracies for the fine-tuned model. The central contribution is the dataset itself, but the dataset is not released, several of the paper's technical claims about its contents are internally inconsistent, and the experimental evidence is based on a small, single-annotator evaluation.

Significance. If the dataset were released, verified, and the inconsistencies resolved, it would fill a genuine gap in LLM reasoning benchmarks: existing math datasets are mostly numerical or symbolic, while NP-completeness reductions require constructing multi-step proofs with both algorithmic and logical components. The structured template, the example prompts, and the detailed scoring of model responses are useful elements for future benchmark design. The experimental comparison, though small-scale, provides a reasonable initial baseline and highlights that current frontier models still struggle with reduction problems. However, the scientific value currently hinges on the correctness and availability of the 90 reductions, neither of which is established in the manuscript.

major comments (5)
  1. [Section 2 (Dataset availability)] The full dataset is withheld ('We will share the full dataset with interested researchers upon request'), so the 90 reductions—the paper's central artifact—cannot be inspected, checked, or used by other researchers. No external audit, formal verification, or complete release is provided. This makes the benchmark's ground truth unreviewable and the central claim unverifiable.
  2. [Section 2, 'Omitted details'] The paper explicitly states that every proof omits polynomial-time computability of the reduction and polynomial-time verification of NP membership, and that the authors only 'maintain' that these conditions hold. Consequently, the entries are not complete NP-completeness proofs as claimed in the abstract; they are equivalence proofs between decision problems. The abstract and dataset description should be revised to reflect this limitation, or the missing steps should be added.
  3. [Appendix D, Theorem 7] The reduction 'Hamiltonian Path to Bounded-Degree Spanning Tree' branches on an integer k that is not part of the Hamiltonian Path input ('If k = 2, let G' = G; if k > 2 ...'). As written, the reduction is not a function from Hamiltonian Path instances to Bounded-Degree Spanning Tree instances, because k is undefined. This is a load-bearing flaw: it appears in the paper's own example of dataset content and indicates that at least one dataset entry is ill-posed.
  4. [Table 2 vs. Appendix A] The test set reported in Table 2 does not match the test set listed in Appendix A. Table 2 includes '3Coloring to Planar 3Coloring', '3SAT to NAE4SAT', and 'Hamiltonian Path to K-SpanningTree', whereas Appendix A lists 'Independent Set to Undirected Feedback Set', 'Clique to Dense Subgraph', 'Unweighted Max Bisection to Weighted Bisection Width', and 'Hamiltonian Cycle to Hamiltonian Path'. These are different problem sets, so the reported average scores cannot be reconstructed from the paper.
  5. [Section 3 (Scoring and experimental evidence)] The experiments rely on a single human expert scoring 8 problems per set on a 0–2 scale. With only 8 items, the reported differences (e.g., 0.875 vs. 1.25 on the test set) are sensitive to a single score change, and no inter-annotator agreement or error analysis is provided. This limits the strength of the fine-tuning comparison and the benchmark's reliability for model ranking.
minor comments (3)
  1. [Figure 2 and Section 2] Figure 2's caption states the mean reduction length is 2180 characters, while Section 2 says the average length is approximately 2000 characters; please reconcile these numbers.
  2. [Section 4, Balanced Biclique score] The score explanation for the Clique-to-Balanced-Biclique response says 'take G = K3,3 and the construction fails'; this example is unclear, since K3,3 is bipartite and the reduction's input is an arbitrary graph, and the failure of the 'misaligned' biclique is not demonstrated for K3,3.
  3. [References] Some references have inconsistent metadata: the Azerbayev et al. entry lists both '2021' and '2023', and the Hendrycks et al. MMLU citation appears both as [2020] in the text and as arXiv 2009.03300; please standardize.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; the dataset construction and held-out evaluations are self-contained.

full rationale

The paper's central contribution is a dataset of 90 NP-hardness reductions and a comparison of LLM performance on held-out problem sets. No derivation or quantitative claim in the paper is defined in terms of its own output. The fine-tuning experiment uses a held-out test set: 'In the second row, LlamaReduce has been fine-tuned on the entire Karp dataset, while in the first row, the test set is held out during training' (Section 3, Table 1 caption), so the reported improvement is not a fitted parameter renamed as a prediction. The challenge set was constructed separately as 'an additional list of eight more challenging reductions that did not belong to the original dataset,' and all scoring is performed by a human expert according to a 0-2 rubric, not by a model trained on the benchmark itself. The paper does contain an explicit limitation in Section 2: 'In all of our proofs, we omit a key concept needed to establish NP-completeness: Polynomial-time computability and verification.' This affects whether the dataset entries are complete NP-completeness proofs, but it is a correctness and completeness concern, not circularity, since the admitted omission does not presuppose the benchmark conclusion. Similarly, the ill-defined k in Appendix D, Theorem 7 and the inconsistency between Appendix A and Table 2 are internal-consistency issues, not instances of a claim reducing to its own inputs. There are no load-bearing self-citations of the 'uniqueness theorem' style, no ansatz smuggled in through citation, and no renaming of a known empirical pattern as a new derivation. The central benchmark claims have independent content and would stand or fall on dataset quality and evaluation methodology rather than on circular reasoning.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new mathematical entities or fitted parameters. Its claims rest on the unverified accuracy of the dataset and the reliability of the small human-scored benchmark, neither of which is independently checkable from the preprint.

assumptions (3)
  • domain assumption The 90 reductions in the dataset are accurate and correctly formatted.
    Section 2 states the dataset contains detailed proofs sourced from literature, but the dataset is not released and no verification method is described. Since the dataset is the central artifact, all claims depend on this assumption.
  • domain assumption The human expert scoring on the 8-problem test and challenge sets is reliable and consistent.
    Section 3 states all models are manually evaluated by a graduate student, with scores 0, 1, or 2, but no inter-annotator agreement or repeated scoring is reported.
  • domain assumption The fine-tuning setup described in Appendix B is sufficient to reproduce LlamaReduce's behavior.
    The paper reports training on 1 A100 GPU for 10 epochs with QLoRA and a learning rate, but does not provide code or the exact data split, so the fine-tuned model cannot be independently reproduced.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Karp Dataset." pith.science (2026). https://pith.science/paper/TCJ7R5XB

@misc{pith2026250114705,
  author       = {Pith},
  title        = {Pith review of: The Karp Dataset},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TCJ7R5XB}},
  note         = {Machine review of arXiv:2501.14705}
}
read the original 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.

Figures

Figures reproduced from arXiv: 2501.14705 by the authors.

Figure 1
Figure 1. Our reduction template (left) compared to MATH (middle) and GSM8k (right) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. The distribution of lengths (i.e., number of characters) of reductions in the dataset. Most [PITH_FULL_IMAGE:figures/full_fig_p018_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A SAT-based Approach for Specification, Analysis, and Justification of Reductions between NP-complete Problems

    cs.LO 2025-11 accept novelty 6.0 of 10

    A URSA/SAT workflow specifies NP problems as certificate checkers and verifies NP-reductions for all instances up to a chosen size, covering full correctness in some cases and soundness in others.

Reference graph

Works this paper leans on

31 extracted references · 16 canonical work pages · cited by 1 Pith paper

  1. [1]

    Gpt-4 technical report

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023

  2. [2]

    Np-hardness of euclidean sum-of-squares clustering

    Daniel Aloise, Amit Deshpande, Pierre Hansen, and Preyas Popat. Np-hardness of euclidean sum-of-squares clustering. Machine learning, 75: 0 245--248, 2009

  3. [3]

    Mathqa: Towards interpretable math word problem solving with operation-based formalisms

    Aida Amini, Saadia Gabriel, Peter Lin, Rik Koncel-Kedziorski, Yejin Choi, and Hannaneh Hajishirzi. Mathqa: Towards interpretable math word problem solving with operation-based formalisms. arXiv preprint arXiv:1905.13319, 2019

  4. [4]

    Proof verification and the hardness of approximation problems

    Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy. Proof verification and the hardness of approximation problems. Journal of the ACM (JACM), 45 0 (3): 0 501--555, 1998

  5. [5]

    Complexity and approximation: Combinatorial optimization problems and their approximability properties

    Giorgio Ausiello, Pierluigi Crescenzi, Giorgio Gambosi, Viggo Kann, Alberto Marchetti-Spaccamela, and Marco Protasi. Complexity and approximation: Combinatorial optimization problems and their approximability properties. Springer Science & Business Media, 2012

  6. [6]

    Llemma: An open language model for mathematics.(2023)

    Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, MD Santos, Stephen McAleer, Albert Q Jiang, Jia Deng, Stella Biderman, and Sean Welleck. Llemma: An open language model for mathematics.(2023). arXiv preprint arXiv:2310.10631, 2021

  7. [7]

    Proving theorems with computers

    Kevin Buzzard. Proving theorems with computers. Notices of the American Mathematical Society, 67 0 (11): 0 1791--1799, 2020

  8. [8]

    Induced matchings

    Kathie Cameron. Induced matchings. Discrete Applied Mathematics, 24 0 (1-3): 0 97--102, 1989

Show all 31 references
  1. [9]

    Training verifiers to solve math word problems, 2021

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems, 2021. URL https://arxiv. org/abs/2110.14168, 2021

  2. [10]

    Automatic evaluation of reductions between np-complete problems

    Carles Creus, Pau Fern \'a ndez, and Guillem Godoy. Automatic evaluation of reductions between np-complete problems. In International Conference on Theory and Applications of Satisfiability Testing, pages 415--421. Springer, 2014

  3. [11]

    Algorithms

    Sanjoy Dasgupta, Christos H Papadimitriou, and Umesh Vazirani. Algorithms. McGraw-Hill, Inc., 2006

  4. [12]

    Qlora: Efficient finetuning of quantized llms

    Tim Dettmers, Artidoro Pagnoni, Ari Holtzman, and Luke Zettlemoyer. Qlora: Efficient finetuning of quantized llms. Advances in Neural Information Processing Systems, 36, 2024

  5. [13]

    The pcp theorem by gap amplification

    Irit Dinur. The pcp theorem by gap amplification. Journal of the ACM (JACM), 54 0 (3): 0 12--es, 2007

  6. [14]

    Interactive proofs and the hardness of approximating cliques

    Uriel Feige, Shafi Goldwasser, L \'a szl \'o Lov \'a sz, Shmuel Safra, and Mario Szegedy. Interactive proofs and the hardness of approximating cliques. Journal of the ACM (JACM), 43 0 (2): 0 268--292, 1996

  7. [15]

    On the parameterized complexity of cutting a few vertices from a graph

    Fedor V Fomin, Petr A Golovach, and Janne H Korhonen. On the parameterized complexity of cutting a few vertices from a graph. In Mathematical Foundations of Computer Science 2013: 38th International Symposium, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. Proceedings...

  8. [16]

    Computers and intractability, volume 174

    Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979

  9. [17]

    Some simplified np-complete problems

    Michael R Garey, David S Johnson, and Larry Stockmeyer. Some simplified np-complete problems. In Proceedings of the sixth annual ACM symposium on Theory of computing, pages 47--63, 1974

  10. [18]

    Some np-complete geometric problems

    Michael R Garey, Ronald L Graham, and David S Johnson. Some np-complete geometric problems. In Proceedings of the eighth annual ACM symposium on Theory of computing, pages 10--22, 1976

  11. [19]

    Measuring massive multitask language understanding

    Dan Hendrycks, Collin Burns, Steven Basart, Andy Zou, Mantas Mazeika, Dawn Song, and Jacob Steinhardt. Measuring massive multitask language understanding. arXiv preprint arXiv:2009.03300, 2020

  12. [20]

    Measuring mathematical problem solving with the math dataset

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021

  13. [21]

    Reducibility among combinatorial problems

    Richard M Karp. Reducibility among combinatorial problems. Springer, 2010

  14. [22]

    Hypertree proof search for neural theorem proving

    Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aur \'e lien Rodriguez, and Timoth \'e e Lacroix. Hypertree proof search for neural theorem proving. URL https://arxiv. org/abs/2205.11491, 2022

  15. [23]

    Decoupled weight decay regularization

    I Loshchilov. Decoupled weight decay regularization. arXiv preprint arXiv:1711.05101, 2017

  16. [24]

    Computational complexity

    Christos H Papadimitriou. Computational complexity. Addison Wesley, 1994

  17. [25]

    Formal mathematics statement curriculum learning

    Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022

  18. [26]

    Language models are multilingual chain-of-thought reasoners

    Freda Shi, Mirac Suzgun, Markus Freitag, Xuezhi Wang, Suraj Srivats, Soroush Vosoughi, Hyung Won Chung, Yi Tay, Sebastian Ruder, Denny Zhou, et al. Language models are multilingual chain-of-thought reasoners. arXiv preprint arXiv:2210.03057, 2022

  19. [27]

    A promising path towards autoformalization and general artificial intelligence

    Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics: 13th International Conference, CICM 2020, Bertinoro, Italy, July 26--31, 2020, Proceedings 13, pages 3--20. Springer, 2020

  20. [28]

    Proofwriter: Generating implications, proofs, and abductive statements over natural language

    Oyvind Tafjord, Bhavana Dalvi Mishra, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. arXiv preprint arXiv:2012.13048, 2020

  21. [29]

    Llama: Open and efficient foundation language models

    Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timoth \'e e Lacroix, Baptiste Rozi \`e re, Naman Goyal, Eric Hambro, Faisal Azhar, et al. Llama: Open and efficient foundation language models. arXiv preprint arXiv:2302.13971, 2023

  22. [30]

    The clrs algorithmic reasoning benchmark

    Petar Veli c kovi \'c , Adri \`a Puigdom \`e nech Badia, David Budden, Razvan Pascanu, Andrea Banino, Misha Dashevskiy, Raia Hadsell, and Charles Blundell. The clrs algorithmic reasoning benchmark. In International Conference on Machine Learning, pages 22084--22102. PMLR, 2022

  23. [31]

    Karp: a language for np reductions

    Chenhao Zhang, Jason D Hartline, and Christos Dimoulas. Karp: a language for np reductions. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 762--776, 2022

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.