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 →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
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.
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
- 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.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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)
- [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.
- [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.
- [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.
- [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.
- [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)
- [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.
- [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.
- [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
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
assumptions (3)
- domain assumption The 90 reductions in the dataset are accurate and correctly formatted.
- domain assumption The human expert scoring on the 8-problem test and challenge sets is reliable and consistent.
- domain assumption The fine-tuning setup described in Appendix B is sufficient to reproduce LlamaReduce's behavior.
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
Forward citations
Cited by 1 Pith paper
-
A SAT-based Approach for Specification, Analysis, and Justification of Reductions between NP-complete Problems
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
-
[1]
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
arXiv 2023
-
[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
2009
-
[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
arXiv 1905
-
[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
work page 1998
-
[5]
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
work page 2012
-
[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
arXiv 2023
-
[7]
Proving theorems with computers
Kevin Buzzard. Proving theorems with computers. Notices of the American Mathematical Society, 67 0 (11): 0 1791--1799, 2020
work page 2020
-
[8]
Kathie Cameron. Induced matchings. Discrete Applied Mathematics, 24 0 (1-3): 0 97--102, 1989
work page 1989
Show all 31 references
-
[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
2021 arXiv
-
[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
2014
-
[11]
Algorithms
Sanjoy Dasgupta, Christos H Papadimitriou, and Umesh Vazirani. Algorithms. McGraw-Hill, Inc., 2006
2006
-
[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
2024
-
[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
2007
-
[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
1996
-
[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...
2013
-
[16]
Computers and intractability, volume 174
Michael R Garey and David S Johnson. Computers and intractability, volume 174. freeman San Francisco, 1979
1979
-
[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
1974
-
[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
1976
-
[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
2009 arXiv
-
[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
2021 arXiv
-
[21]
Reducibility among combinatorial problems
Richard M Karp. Reducibility among combinatorial problems. Springer, 2010
2010
-
[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
2022 arXiv
-
[23]
Decoupled weight decay regularization
I Loshchilov. Decoupled weight decay regularization. arXiv preprint arXiv:1711.05101, 2017
2017 arXiv
-
[24]
Computational complexity
Christos H Papadimitriou. Computational complexity. Addison Wesley, 1994
1994
-
[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
2022 arXiv
-
[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
-
[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
2020
-
[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
2012 arXiv
-
[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
2023 arXiv
-
[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
2022
-
[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
2022
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.