The Karp Dataset

Authors: mason  dicicco
eamon  worden
conner  olsen
nikhil  gangaram
daniel  reichman
neil  heffernan
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-24 20:16:11

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.

Main paper: 
 introduction: 
 Perhaps the concept receiving the most attention in theoretical computer science is that of a reduction. Loosely speaking, a reduction between decision problems A and B is a mapping f such that: If x is an input to A, then f (x) is an input to B, and the answer to x is "yes" if and only if the answer to f (x) is "yes." Efficiently computable reductions can be used to leverage algorithms that solve B in order to solve A. Furthermore, efficient reductions can establish hardness results: if A is believed to be intractable, and A reduces to B efficiently, then B is intractable as well, since an efficient algorithm for B can be used to solve A. This simple observation is at the core of the theory of NP-completeness, which is the topic of thousands of papers and an influential monograph Garey and Johnson [1979] .Our goal is to study the capabilities of Large Language Models (LLMs) and their potential to influence formal mathematics. To that end, we built a new dataset of 90 NP-hardness proofs (reductions) to be used for evaluation and training of language models. We are not aware of the study of LLMs for proving new NP-hardness results (by constructing reductions) or reproving and verifying known results. We believe that aiming language models at reductions in particular has great potential to benefit our understanding of their reasoning capabilities and applicability to formal mathematics. This is because:• Finding a reduction between two problems is a high-level reasoning task. Imbuing LLMs with the ability to construct reductions could lead to improved reasoning capabilities. • It is feasible to construct dozens of examples of reductions that are theoretically interesting, go beyond symbolic manipulations to prove mathematical identities, and have a short (several paragraphs) proof using natural language. The existence of short yet difficult-to-find proofs hints that such proofs can be found automatically with reasonable computing resources (e.g., memory, training time). • Such datasets are challenging to construct in other mathematical domains. Current datasets of mathematical problems (e.g., Hendrycks et al. [2021] ) that are used to evaluate math capabilities of large language models generally focus on a single numerical or symbolic outcome.There has been extensive recent research directed toward using generative AI, neural networks, and Interactive Theorem Provers (ITP) in pushing the boundaries of mathematics [Azerbayev et al., 2021 , Buzzard, 2020 , Hendrycks et al., 2021 , Lample et al., 2022 , Polu et al., 2022 , Szegedy, 2020] including proving new theorems as well as reproving known theorems. To our knowledge, they do not include proofs of NP completeness using reductions. Very few works seem to have studied automatically constructing reductions toward establishing NP-completeness results. One of the more advanced datasets similar to ours is The CLRS Algorithmic Reasoning Benchmark of Veličković et al. [2022] , which predicts the trajectories of various algorithms using an algorithmic model but explicitly avoids NP-Hard problems. Motivated by the education domain, Creus et al. [2014] study the problem of testing the correctness of reductions using SAT-solvers and designated programming language REDNP to establish NP-completeness. One bottleneck noted in proof verification using SAT solvers is the large size of SAT formulas obtained in the process of verification. Recently, Zhang et al. [2022] introduced Karp, a language for programming and testing reductions, motivated by the educational domain as well. Karp is a Racket-esque framework that can be used to define computational problems as well as reductions between them. In addition to providing a systematic way to construct reductions, Karp automatically tests the correctness of reductions. The Karp dataset contains significantly fewer solved questions compared to most math datasets. It does not use generative AI to find reductions and their proofs.Related datasets such as MATH [Hendrycks et al., 2020] , MathQA [Amini et al., 2019] , GSM8K [Cobbe et al., 2021] , MGSM [Shi et al., 2022] , ProofWriter [Tafjord et al., 2020] and others have offered new ways to evaluate the mathematical reasoning and proof generation capabilities of language models. The MATH dataset consists of challenging problems taken from high school math competitions, testing a model's elementary problem-solving skills across various domains of mathematics. The GSM8K and MGSM (multilingual GSM8K) datasets focus on grade-school math problems, assessing the model's ability to perform arithmetic reasoning and handle multi-step calculations. ProofWriter evaluates a model's proficiency in generating natural language proofs for elementary logical inference tasks, emphasizing multi-hop reasoning. While these datasets are instrumental in testing general mathematical and logical reasoning, they are completely disjoint from the task of constructing reductions for NP-completeness proofs. Reductions in computational complexity involve a unique blend of algorithmic thinking, formal proof techniques, and an understanding of computational problems' intrinsic properties. This gap highlights the need for specialized resources.Datasets such as MATH and MGSM are valuable because they allow for standardized comparison of the capabilities of language models, but LLMs now excel at scoring highly on them. For instance, GPT-4o [Achiam et al., 2023] scores over 90% on GSM8K, 75% on the MATH dataset, and around 86% on MMLU (Massive Multitask Language Understanding) [Hendrycks et al., 2020] . While impressive, there are concerns that LLMs have been overfit on the testing datasets due to their availability on the internet. Moreover, achieving a high level of performance on GSM8K, which consists of grade-school math problems, only indicates that LLMs are comparable to highly skilledTheorem 1. Problem X reduces to Problem Y Proof. Assume we have an algorithm A solving Y. Then, we can execute the following algorithm to solve X:Given input x to X, construct inputs to Y as follows. y = . . . Output the result of A on y.It remains to prove that x is "yes" if and only if y is "yes" =⇒ : Suppose x is "yes". • • • ⇐= : Suppose y is "yes". eighth graders. As more advanced LLMs such as Strawberry (also known as o1) are released, researchers will be aiming towards matching the problem-solving capacity of undergraduate or even PhD level students. This necessitates datasets of complex higher-education-level questions such as reductions. 
the karp dataset: 
 Our dataset consists of detailed natural language descriptions of dozens of reductions establishing NP-hardness proofs. These proofs are significantly more involved and labor-intensive to generate relative to math problems with a numerical answer [Hendrycks et al., 2021] or a sequence of computational steps as a solution [Cobbe et al., 2021] . Every reduction in the dataset is sourced from well-known literature such as Garey and Johnson [1979] , Papadimitriou [1994] , Dasgupta et al. [2006] . The dataset also contains natural language versions of Karp's 21 original NP-complete problems [Karp, 2010] . Other sources include academic papers Garey et al. [1974 Garey et al. [ , 1976]] , Fomin et al. [2013] , Aloise et al. [2009] and dedicated surveys of NP-completeness Ausiello et al. [2012] and the references therein.Many proofs of NP-completeness in the literature compress proofs of claims that are somewhat tedious to prove formally, and it has been observed that some proofs contain inaccuracies [Zhang et al., 2022] . In our proofs, we attempted to avoid including unproven claims, emphasizing clarity at the cost of verbosity. Such proofs also often rely on diagrams, which we convert to natural language for LLM comprehension. As a result, the proofs in our dataset are somewhat longer than proofs in other datasets, altogether spanning over 170 pages. We avoided including problems with highly complex proofs that require more than two pages. The reductions in the dataset have lengths between 1000 and 6000 characters and have an average length of approximately 2000 characters. The distribution of lengths is depicted in Figure 2 . Some examples of reductions can be found in Appendix D, and the full lists of problems and reductions can be found in Tables 5 and 6 , respectively. We will share the full dataset with interested researchers upon request.Formatting The dataset consists of reductions (in the form of L A T E X-typeset theorems) between computational problems whose definitions are also provided. Reductions in the dataset adhere to a highly structured template: A precise definition of the mapping followed by a proof of correctness (See Figure 1 ). The language is fairly expository and instructive: While all the content of a formal proof is present, we frequently include conceptual justification of non-trivial logical steps.Omitted details In all of our proofs, we omit a key concept needed to establish NP-completeness: Polynomial-time computability and verification. For example, in a proper NP-completeness proof, the mapping from one decision problem to another must be possible to implement efficiently1 , otherwise the reduction is vacuous (e.g., if exponential time is allowed, then one could just brute-force the answer to the original problem.) Efficiency of a reduction is often easy (but tedious) to prove, and we maintain that this holds true for all problems in our dataset. Hence, we choose to mask these details. Question: Does the paper discuss the limitations of the work performed by the authors? Answer: [Yes] Justification: We discuss the limitations of the dataset in Section 2 Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.• The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
experiments: 
 In contrast to computations and formal logical deductions, natural-language mathematical proofs resist straightforward automatic verification. Due to this limitation, all models are manually evaluated on a small, fixed test set by a human expert (a graduate student in theoretical computer science).We initially evaluated our models on a randomly chosen set of 8 reductions from the dataset, at the level of undergraduate homework assignments (test set). After our initial evaluation, Strawberry was released and achieved significantly better results on the test set. To gain a better understanding of the capabilities of Strawberry, we constructed an additional list of eight more challenging reductions (challenge set) that did not belong to the original dataset.Prompts Models are evaluated on their responses to a highly structured prompt, which asks for a reduction between two decision problems. The prompt provides a L A T E X template for the reduction, which matches the format of the dataset, states the two problems and any necessary definitions, and asks for a detailed reduction. Full examples of prompts can be found in Appendix E.Scoring Completed reductions receive a score of 0, 1, or 2, where 0 represents a completely incorrect answer, 1 reflects a construction that contains significant yet fixable flaws, and 2 indicates a fully or nearly correct reduction with only minor errors. If the response contains superficial bugs (such as L A T E X-compilation errors), we repair these and proceed with normal scoring.We compare the performance of OpenAI's recent Strawberry model, the Llama70B-Instruct base model [Touvron et al., 2023] as well as our fine-tuned Llama70B-Instruct model, which we call LlamaReduce. The fine-tuning method we used is described in Appendix B.Strawberry achieves impressive averages of 1.5 on the test set, and 0.875 on the challenge set. Interestingly, Strawberry even gave a more compact version of a current well-known reduction in the challenge set (See Appendix E). This outperforms the base Llama model, which scores 0.875 on the test set and 0.375 on the challenge set. The only problem that Llama answered correctly from the challenge set was NAE4SAT to Set Splitting, whose difficulty is relatively low. LlamaReduce clearly benefited from fine-tuning on the Karp dataset, as it was able to score 1.25 and 0.5 on the test and challenge sets respectively. The complete breakdown of scores is compiled in Tables 2 and 3 in Appendix C.These preliminary findings, especially the low scores achieved on the challenge set, suggest that reductions are a challenging task for LLMs, leaving room for potential improvement. For easier reductions (such as those in the test set), fine-tuning was beneficial in improving performance. The impressive performance of Strawberry provides additional evidence that prompt engineering has a significant effect on problem-solving capacity, particularly on problems from the test set (at the level of homework questions from an undergraduate course covering NP-completeness). Both prompt engineering and fine-tuning appear to be less effective for improving performance for the harder reductions such as those in the challenge dataset.We also evaluate LlamaReduce on the MATH and MGSM datasets. Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof? Answer: [NA] Justification: We have no theoeretical results per se, but the reductions in the dataset constitute theoretical results and indeed all have full proofs. 
conclusion: 
 We have constructed the Karp dataset consisting of reductions establishing NP-completeness. Future work could examine extending the dataset with additional reductions (e.g., reductions establishing hardness of approximation of NP-hard optimization problems Arora et al. [1998] , Feige et al. [1996] , Dinur [2007] ). Using the Karp dataset as well as generative AI more broadly to discover new reductions and simplify known NP-completeness proofs is an exciting future direction.The lack of automatic verification for natural language proofs of NP-completeness is a bottleneck in creating a larger dataset. In our experiments, language models failed to judge the correctness of reductions. We suspect that a transformation from natural language to more structured representations (e.g., code, formal math, the Karp language) is a required step to allow automatic verification. Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?Answer: [Yes] Justification: We describe our experimental setup in Appendix B, and the dataset and code for fine-tuning and inference are available upon request Guidelines:• The answer NA means that the paper does not include experiments.• If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not. • If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable. • Depending on the contribution, reproducibility can be accomplished in various ways.For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed. • While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. (d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results. • The experimental setting should be presented in the core of the paper to a level of detail that is necessary to appreciate the results and make sense of them. • The full details can be provided either with the code, in appendix, or as supplemental material. 
experiment statistical significance: 
 Question: Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments? Answer: [NA] Justification: Results of statistical significance were unfortunately too expensive since proofs must be carefully verified manually by a human. This is discussed in Section 3 Guidelines:• The answer NA means that the paper does not include experiments.• The authors should answer "Yes" if the results are accompanied by error bars, confidence intervals, or statistical significance tests, at least for the experiments that support the main claims of the paper. • The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).• The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.) • The assumptions made should be given (e.g., Normally distributed errors).• It should be clear whether the error bar is the standard deviation or the standard error of the mean. Justification:Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [NA] Justification: The Karp dataset is merely a compilation of publicly available and well known materialGuidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.• Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)? Answer: [NA] Justification: The dataset poses no risk for misuse and is not publicly available Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort. 12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected? Answer: [Yes] Justification: The literature from which reductions were sourced is cited Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. 
 
 Appendix: We fine-tuned Llama 70B-Instruct using Unsloth. For training, we utilized the AdamW optimizer Loshchilov [2017] and QLora Dettmers et al. [2024] with 4-bit precision to reduce memory consumption. The learning rate was set to 2 × 10 -5 , following a linear scheduler with 10 warmup steps. We applied weight decay of 0.01 to prevent overfitting. The model was trained with a batch size of 8 per device. We used 16-bit floating point precision and random seed 0. LlamaReduce was trained on 1 A100 GPU until the loss converged on a validation set at 10 epochs. All models, fine-tuned or not, were inferenced with a temperature of 0.This section contains tables of results that were omitted due to space constraints. This section contains the reductions 3SAT to Independent Set as well as Hamiltonian Path to Bounded-Degree Spanning Tree as they appear in the dataset.Definition 1. A 3-CNF is a Boolean formula equal to an AND of clauses, where each clause is an OR of exactly 3 literals (i.e., variables or their negations). A 3-CNF is satisfiable if there exists an assignment of variables to true (1) or false (0) such that the entire formula evaluates to true. Problem 1 (3SAT).• Input: (X, C), whereX = {x 1 , • • • , x n } is a set of variables and C = {C 1 , • • • , C m }is a set of clauses containing exactly 3 literals derived from X (i.e., x i or ¬x i ).• Output:1 There exists an assignment (of variables in X)satisfying ϕ = C 1 ∧ • • • ∧ C m . 0 OtherwiseDefinition 2. Given an undirected graph G = (V, E), a subset of vertices S ⊆ V is an independent set if no two nodes are joined by an edge:∀u, v ∈ S : (u, v) / ∈ E.Problem 2 (Independent Set).• Input: (G, k) where-G = (V, E) is an undirected graph -k is a positive integer • Output: 1 G has an independent set of size k 0 otherwiseTheorem 2. 3SAT reduces to Independent SetProof. Assume we have an algorithm A solving Independent Set. Then, we can execute the following algorithm to solve 3SAT:Reduction Given inputs (X, C) to 3SAT, construct inputs to Independent Set (G, k) as follows:1. For each clause C i = (a i ∨ b i ∨ c i ), create a "cluster" of vertices a i , b i , c i in V , and connect them in a triangle by adding edges (a i , b i ), (b i , c i ), (c i , a i ) to E. 2. Additionally, connect every two vertices corresponding to complementary literals (i.e. there is an edge between every x i and ¬x i ). Output the result of A on (G, k), where k = |C|.To establish correctness, it remains to prove that ϕ is satisfiable ⇐⇒ G has an independent set of size k.=⇒ : Let T be an assignment of variables satisfying ϕ. In particular, each clause C i contains at least one true literal. Construct a set I which contains one such true literal from each clause. We now claim that I corresponds to an independent set in G of size k: It contains one vertex (literal) from each of the k clauses, and no pair of vertices in I are adjacent since there is only one vertex per cluster and vertices corresponding to complementary literals (i.e. x and ¬x) cannot both be in I since that would be an impossible assignment; x and ¬x cannot simultaneously be true. ⇐= : Let I be an independent set of size k in G. Note that I cannot contain two vertices in the same cluster. Hence, I contains one vertex in each cluster of G and does not contain vertices corresponding to complementary literals (i.e. x i and ¬x i ). Thus, it is possible to assign every literal (vertex) in I to be true simultaneously, which constitutes a satisfying assignment for ϕ.Hamiltonian Path to Bounded-Degree Spanning Tree Definition 3. Given an undirected graph G = (V, E), a Hamiltonian path is a simple path in G that visits each vertex in V exactly once.• Input: An undirected graph G = (V, E).• Output:1 G has a Hamiltonian path. 0 Otherwise. Definition 4. Given an undirected graph G = (V, E) and a positive integer k, a degree-k spanning tree of G is a subgraph T of G such that:• T is connected;• T is acyclic;• T spans all the vertices of G (i.e., includes all vertices in V );• The maximum degree of any vertex in T is at most k. Problem 4 (Bounded-Degree Spanning Tree).• Input: An undirected graph G = (V, E) and a positive integer k.• Output:1 G has a degree-k spanning tree 0 Otherwise Theorem 3. Hamiltonian Path reduces to Bounded-Degree Spanning Tree.Proof. Assume we have an algorithm A solving Bounded-Degree Spanning Tree. Then, we can execute the following algorithm to solve Hamiltonian Path:Reduction: Given an instance G = (V, E) of Hamiltonian Path, we construct an instance (G ′ , k) of Bounded-Degree Spanning Tree as follows:•If k = 2, let G ′ = G. • If k > 2: -Let V ′ = V ∪ {v 1 , v 2 , . . . , v k-2 | v ∈ V } -Let E ′ = E ∪ {(v, v i ) | v ∈ V, 1 ≤ i ≤ k -2}Output the result of A on (G ′ , k).We claim that G has a Hamiltonian path ⇐⇒ G ′ has a degree-k spanning tree. This clearly holds for k = 2 as a degree-2 spanning tree is exactly a Hamiltonian path; a tree with maximum degree 2 is a path, and spanning G is equivalent to visiting every vertex. We now show the reduction holds for all k > 2: =⇒ : Suppose G has a Hamiltonian path P . We can construct a degree-k spanning tree T ′ of G ′ by taking P and adding all the new edges (v, v i ) for each v ∈ V . This tree spans all vertices of G ′ , is acyclic, and has maximum degree k (2 from the original path plus k -2 new edges). ⇐= : Conversely, suppose G ′ has a degree-k spanning tree T ′ . All the new vertices v i must be leaves in T ′ as they have degree 1. If we remove these leaves and their incident edges (k -2 per vertex of G) from T ′ , we obtain a spanning tree T of G with maximum degree 2, which must be a Hamiltonian path.This section contains the prompts and responses from the Strawberry model on the Independent Set to Induced Matching and Clique to Balanced Bi-clique reductions. For the sake of readability, the L A T E Xsnippets in the prompts have been made renderable.You are a bot designed to write NP-Hardness reductions. You must use the following LaTeX template to write the reduction: Theorem 4. Problem Independent_Set reduces to Problem Induced_Matching Proof. Assume we have an algorithm A solving Problem Induced_Matching. Then, we can execute the following algorithm to solve Problem Independent_Set:Reduction Given inputs x 1 , • • • to Problem Independent_Set, construct an instance of Problem Induced_Matching as follows.•y 1 = • • • Output the result of A on y 1 , • • • .To establish correctness, it remains to prove thatx 1 , • • • contains a foo of size k ⇐⇒ y 1 , • • • contains a bar of size k ′ . =⇒ : Suppose x 1 , • • • contains a foo of size k. • • • Thus, y 1 , • • • contains a bar of size k ′ . ⇐= : Suppose y 1 , • • • contains a bar of size k ′ . • • • Thus, x 1 , • • • contains a foo of size k. • • • .Definition 5. Given an undirected graph G = (V, E), a subset of vertices S ⊆ V is an independent set if no two nodes are joined by an edge:∀u, v ∈ S : (u, v) / ∈ E.Problem 5 (Independent Set).• Input: (G, k) where-G = (V, E) is an undirected graph -k is a positive integer • Output:1 G has an independent set of size k 0 otherwise Definition 6. Given an undirected graph G = (V, E), a subset of edges M ⊆ E is an induced matching if no two edges in M are incident to the same vertex. Problem 6 (Induced Matching).• Input: (G, k) where -G = (V, E) is an undirected graph k is a positive integer• Output: 1 G has an induced matching of size k 0 otherwise Write a proof that Induced_Matching is NP-hard by reducing from Independent_Set.Proof. Assume we have an algorithm A solving Problem Induced Matching. Then, we can execute the following algorithm to solve Problem Independent Set:Reduction Given inputs (G, k) to Problem Independent Set, construct an instance of Problem Induced Matching as follows.• For each vertex v ∈ V (G), create two vertices u v and w v in G ′ , and add an edge (u v , w v ). • For every edge (v i , v j ) ∈ E(G), add edges between all pairs of vertices from {u vi , w vi } and {u vj , w vj }. Specifically, add edges:-(u vi , u vj ) -(u vi , w vj ) -(w vi , u vj ) -(w vi , w vj ) Set k ′ = k. Output the result of A on (G ′ , k ′ ).To establish correctness, it remains to prove that G contains an independent set of size k ⇐⇒ G ′ contains an induced matching of size k ′ .=⇒ : Suppose G contains an independent set S ⊆ V (G) of size k. Consider the set of edgesM = {(u v , w v ) | v ∈ S} in G ′ .• Since S is an independent set in G, there are no edges between any pair of vertices v i , v j ∈ S. • Therefore, by construction, there are no edges between any pair of edges (u vi , w vi ) and (u vj , w vj ) in G ′ for v i , v j ∈ S. • Additionally, since each edge in M shares no common vertices with others in M , M is a matching in G ′ .• There are also no edges connecting the endpoints of different edges in M (due to the absence of connections between their vertices), so M is an induced matching in G ′ .Thus, G ′ contains an induced matching of size k ′ .⇐= : Suppose G ′ contains an induced matching M of size k ′ = k. Let S = {v ∈ V (G) | (u v , w v ) ∈ M }.• Since M is a matching in G ′ , no two edges in M share a common vertex.• Since M is an induced matching, there are no edges between the endpoints of different edges in M . • By construction, if there were an edge (v i , v j ) ∈ E(G) between any two vertices v i , v j ∈ S, then in G ′ , there would be edges between the endpoints of (u vi , w vi ) and (u vj , w vj ), violating the induced matching property. • Therefore, there are no edges between any pair of vertices in S in G.Thus, S is an independent set of size k in G.Therefore, G contains an independent set of size k if and only if G ′ contains an induced matching of size k ′ . Score This construction does indeed resemble the well-known reduction from Cameron [1989] .The key difference is that Strawberry constructs a clique on the four vertices {u vi , w vi , u vj , w vj } for each edge (v i , v j ) ∈ E, whereas [Cameron, 1989 ] constructs a larger gadget, where the four edges between the u's and w's are replaced with disjoint paths of length 8. Interestingly, a short argument shows that a slight modification of Strawberry's construction does produce a valid reduction. The main point is that G ′ may contain a matching which contains some "vertical" or "diagonal" edges (i.e., edges not of the form (u v , w v )). However, it is possible to swap these edges with the desired type of edge, which completes the proof. As a result, this response receives a 1.You are a bot designed to write NP-Hardness reductions. You must use the following LaTeX template to write the reduction: Theorem 6. Problem Clique reduces to Problem Balanced_Biclique Proof. Assume we have an algorithm A solving Problem Balanced_Biclique. Then, we can execute the following algorithm to solve Problem Clique:Reduction Given inputs x 1 , • • • to Problem Clique, construct an instance of Problem Balanced_Biclique as follows.•y 1 = • • • Output the result of A on y 1 , • • • .To establish correctness, it remains to prove thatx 1 , • • • contains a foo of size k ⇐⇒ y 1 , • • • contains a bar of size k ′ . =⇒ : Suppose x 1 , • • • contains a foo of size k. • • • Thus, y 1 , • • • contains a bar of size k ′ . ⇐= : Suppose y 1 , • • • contains a bar of size k ′ . • • • Thus, x 1 , • • • contains a foo of size k. • • • .Definition 7. Given a undirected graph G = (V, E), a subset of the vertices S ⊆ V is a clique if pair of vertices in S is adjacent:∀u ̸ = v ∈ S, (u, v) ∈ EProblem 7 (Clique). The Clique Problem, given a graph G and an integer k, is to decide whether or not G contains a clique of size k.• Input: (G, k) where G = (V, E) is an undirected graph and k is a positive integer.• Output:1 G contains a clique of size at least k. 0 Otherwise Definition 8. A balanced bipartite graph is a bipartite graph in which both sides have the same cardinality; the bipartition (A, B) satisfies|A| = |B|. Given a balanced bipartite graph G = (V, E) with bipartition (A, B), a subset C ⊂ V is a balanced biclique if it is a complete bipartite graph satisfying |A ∩ C| = |B ∩ C|.Problem 8 (Balanced Biclique). The Balanced Biclique Problem, given a balanced bipartite graph G and an integer k, is to decide whether or not G contains a balanced biclique of size k.• Input: (G, k) where G = (V, E) is a balanced bipartite graph and k is a positive integer.• Output:1 G contains a balanced biclique of size at least k. 0 Otherwise Write a proof that Balanced_Biclique is NP-hard by reducing from Clique.Theorem 7. Problem Clique reduces to Problem Balanced_Biclique.Proof. Assume we have an algorithm A solving Problem Balanced_Biclique. Then, we can execute the following algorithm to solve Problem Clique:Reduction Given inputs (G, k) to Problem Clique, construct an instance of Problem Balanced_Biclique as follows.• Construct a balanced bipartite graph G ′ = (V ′ , E ′ ) with bipartition (A, B) where:-A = V , the vertex set of G. -B = V ′ , a copy of the vertex set V (i.e., for each v ∈ V , there is a corresponding v ′ ∈ B). -For each edge (u, v) ∈ E, include edges (u, v ′ ) and (v, u ′ ) in E ′ , where u ∈ A, v ′ ∈ B, v ∈ A, and u ′ ∈ B. • Set k ′ = k.Output the result of A on (G ′ , k ′ ). Justification: We introduce the Karp dataset and perform preliminary experiments which includes a comparison of language models and fine-tuning Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper.• The answer NA means that the paper does not include theoretical results.• All the theorems, formulas, and proofs in the paper should be numbered and crossreferenced.• All assumptions should be clearly stated or referenced in the statement of any theorems.• The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition. • Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material. • Theorems and Lemmas that the proof relies upon should be properly referenced.Here, "efficiently" means "in polynomial time", with respect to the size of the input 



Reviews: review: title: title: review for "The Karp Dataset"
main_review: main_review: Pros:
1. The Karp Dataset is specifically designed to test LLMs on NP-completeness reductions, a challenging task that requires deep mathematical reasoning rather than simple arithmetic or symbolic manipulation. This focus enables a better assessment of an LLM’s ability to handle complex problem-solving tasks, which is a step forward in benchmarking advanced mathematical capabilities.
2. Unlike other math-focused datasets that concentrate on numerical solutions, the Karp Dataset provides a series of reductions involving NP-hard problems. This allows for evaluating and training LLMs in a domain not widely explored by other datasets, helping to fill a gap in the types of problems used for AI evaluation. Such reasoning processes are more advanced and valuable to test.

Cons:
1. While the dataset provides a unique challenge, its focus on NP-completeness may limit its applicability for general mathematical reasoning evaluation. The problems proposed in this paper are very interesting yet still far away from the major scope of math. Yet, this is still a very meaning attempt.
2. The main concern is that this method is hard to extend; it seems that it is not easy to extend such dataset and a small amount of data may results in bias or false statistical significance.
title: title: Review for the Karp Dataset
main_review: main_review: Summary:
The paper introduces the Karp dataset, a structured collection of NP-completeness reductions with varying difficulty designed to test the reasoning ability of language models. 

Pros:
- The dataset fills a gap by focusing on reductions, which are not covered by existing math datasets.
- It provides a benchmark for evaluating language models on complex tasks where they currently struggle. Evaluation results show that the dataset can differentiate between models (it would be nice to add more models, e.g., Gemini/Claude).
- Fine-tuning experiments with the dataset show improvements, suggesting the training split could enhance reasoning capabilities of language models.

Cons/Comments:
- On evaluation, manual verification of results can not scale well for larger experiments, which limits the practicality of the evaluation (since grad students in theoretical computer science are becoming scarce these days). This scalability is likely the biggest concern. It would be helpful for the authors to add more discussions on potential strategies to automate this verification process (beyond a formal system, can llm-as-a-judge approach be compared here?) — it should help future researchers to use the dataset more efficiently.
- On fine-tuning LLMs with Karp, it would strengthen the paper if the authors included evaluations on more math or downstream tasks, or providing recipes on mixed dataset training (in Table 4, it looks like that finetuning with Karp can hurt the performance of multilingual GSM8K?). This would give a broader view of how the knowledge contained in dataset improves overall reasoning ability.

Overall, I believe the contribution of this work on the construction of the new dataset is sufficient as an workshop paper.
title: title: Significant Contribution to the Field
main_review: main_review: This study presents the creative dataset, which contains detailed proofs of NP-completeness reductions. It serves as a valuable resource for the study and analysis of these complex problems, representing a significant contribution to the field of computational complexity.

The paper's strengths lie in its innovative approach and rigorous experimental design, demonstrating a high level of precision in validating the dataset's effectiveness. However, the study has a few limitations: the range of experiments is somewhat limited, and the validation dataset is relatively small, which could impact the robustness of the results.

Overall, despite these limitations, the paper makes a novel and meaningful contribution to the field, paving the way for further research on NP-completeness and related topics.
title: title: New dataset of detailed proofs of NP-completeness reductions in natural language, with limitations for LLM evaluation
main_review: main_review: Summary: 
The paper introduces a new dataset composed of detailed proofs of NP-completeness reductions in natural language.

Strengths:
- This dataset is innovative and appears to be high-quality.

Opportunities for improvements:
- I'm skeptical about the dataset’s utility as a benchmark. As the authors mentioned, testing models on this dataset requires human evaluation, which restricted their tests to only 8 problems. Would it be possible to augment the dataset with formalizations using the Karp programming language, so that models can be tested with an automated verification tool?
- The rating system (0, 1, 2) is somewhat unclear and it might be more intuitive to use a percentage-based system. The paper would also benefit from a clearer description of the dataset, for example by indicating the number of total samples in the dataset, the average length of the proofs, the distribution of the lengths, etc.

Final remark: 
The paper introduces a high-quality dataset with potential applications in training/finetuning LLMs. However, due to concerns about its current use for LLM evaluation (reliance on human evaluation), I opt for a rating of 6.
title: title: The paper presents a novel Karp dataset for NP-completeness reductions, but its experimental results require more clarity and thorough evaluation.
main_review: main_review: The paper presents the Karp dataset, an important contribution for assessing LLMs on NP-completeness reductions, addressing a critical gap in benchmarking reasoning tasks. The dataset spans simple to complex reductions, enabling robust evaluations. The comparison of state-of-the-art models and the impact of fine-tuning on reasoning performance is a valuable addition. However, the paper could improve by providing a clearer discussion on evaluation metrics and a more detailed error analysis.