{"id":"33623e8c-3b82-4a5a-968e-6d11cccdb094","arxiv_id":"2503.11657","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"KG-Prover shows that traversing a ProofWiki-derived knowledge graph at inference time improves LLM theorem-proving accuracy on miniF2F, ProofNet, and MUSTARDSAUCE without extra fine-tuning.","lead":"This paper introduces KG-Prover, a system that retrieves and traverses a knowledge graph of mathematical statements to give large language models extra context when generating proofs, which are then checked by the Lean theorem prover. Without fine-tuning, the extra context improves pass rates by a few to several points on theorem-proving benchmarks, though the evaluation uses weak baselines and small subsets.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The graph-scaling attribution is untested: §5.3/Fig. 3 conflate traversal depth with retry count r, and Table 1's caption permits beam search for KG-Prover while baselines are single-completion; no compute-matched control exists.","rationale":"The central claim requires that the knowledge graph's structure—nodes connected by ProofWiki hyperlinks, traversed iteratively—adds accuracy beyond what a generic LLM with enough retries or retrieved text would achieve. That condition is exactly what the paper never tests. The strongest evidence (Figure 3) confounds retries with depth because r is described as attempts in Section 5.3 and as traversal depth in the figure label; Table 1's caption allows beam search for KG-Prover but not for baselines; and Table 3 quantifies the 10x call gap. I did not find a contradiction in the Lean-verification pipeline itself, and the qualitative example in Appendix I shows a plausible mechanism, but qualitative examples do not separate the confound. The reader's CONDITIONAL verdict is therefore appropriate: the paper should be revised with the ablation above and with corrected figure labels and captions. The issue is not 'outside current consensus'; it is internal to the evaluation design. Notably, the Limitations section discusses embedding noise and autoformalization failures but never flags the compute-matching confound, which is the central threat to the title claim.","tokens_in":17875,"tokens_out":8984,"duration_ms":84602,"concrete_test":"Run a miniF2F-test ablation with Llama 3.1 8B that fully crosses retry count r ∈ {1,3,7} with graph depth d ∈ {1,3,7} (same autoformalizer, Lean verifier, and temperature), plus a sampling-only best-of-r control with no graph context and a flat-retrieval control with the same per-attempt token budget. If accuracy tracks r rather than d, or if best-of-r matches the deep-traversal curve, the graph-scaling claim fails; if accuracy rises with d at fixed r, the concern is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"KG-Prover's central claim is that graph traversal, not extra sampling or retries, drives the reported gains. The paper does not establish that. Section 5.3 defines r as 'multiple consecutive attempts' for failure correction, but Figure 3's x-axis is labeled 'Traversal Depth r' and the caption says accuracy increases with depth; thus the scaling curves are equally explained by 'more retries help' with no graph at all. The Table 1 caption adds that KG-Prover 'may additionally apply beam search' while Base and RAG generate a single completion per Lean retry, and Table 3 shows the beam configuration uses 30 LLM calls per problem versus 3 for baselines. No compute-matched baseline (e.g., best-of-N sampling from a flat retrieval corpus with the same call and token budget) is reported, so the 31.97% vs 20.49% miniF2F result and the 'up to 21%' headline can be produced by test-time compute alone. Appendix H.2's semantic-search description ('avoids exhaustive traversal') further clouds whether graph edges are used at all in the reported system. The framework is plausible and table-level trends are consistent, but the central attribution is not yet supported.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces KG-Prover, a training-free framework that augments general-purpose LLMs with a knowledge graph mined from ProofWiki for automated theorem proving. At inference time, KG-Prover embeds the problem statement, retrieves semantically similar nodes, generates an informal proof, autoformalizes it with DeepSeek-Prover-V1.5, and verifies it in Lean. If verification fails, the system traverses the graph to add neighboring nodes and retries, optionally using best-of-N selection or beam search. The authors evaluate on miniF2F, ProofNet, and MUSTARDSAUCE with six LLMs, and report consistent improvements over zero-shot baselines and a fixed top-5 RAG baseline, with the largest gains on miniF2F (e.g., Llama 3.1 8B at 31.97% vs. 20.49% baseline) and 52.9% for o4-mini with beam search. The central claim is that graph-based retrieval and traversal, scaled at test time, drive these gains.","tokens_in":18103,"tokens_out":5595,"duration_ms":58482,"significance":"If the central attribution were established, this would be a practically useful result: it shows that retrieval from an open mathematical corpus can improve general-purpose LLM theorem proving without finetuning, and the use of the external Lean verifier plus public benchmarks is a genuine strength. The paper is also transparent about token and API-call costs (Table 3), reports deterministic evaluations, and makes code available. However, the significance is currently limited by the absence of compute-matched controls: the reported gains conflate graph traversal with extra retries and beam search, so the title's claim that graph-based test-time compute is the driver is not yet supported. The framework is plausible and the direction of the effect is consistent with prior retrieval-augmented reasoning results, but the magnitude and attribution need stronger evidence.","major_comments":[{"comment":"The paper conflates graph traversal depth with the number of LLM attempts. Section 5.3 defines r as 'multiple consecutive attempts' for failure correction, while Figure 3 labels its x-axis 'Traversal Depth r'. Under this definition, any point at depth >3 in Figure 3 uses strictly more LLM calls than the Base and RAG baselines (which are fixed at r=3), so the accuracy-vs-depth curves are equally explained by 'more retries help' as by 'deeper graph traversal helps'. The reported scaling claim therefore requires compute-matched controls, e.g., best-of-N sampling from a flat top-k retrieval context with the same number of generations and tokens, and repeated generation at a fixed graph depth without new node injection.","section":"§5.3, Figure 3, §4.4"},{"comment":"The comparison in Table 1 is not compute-matched and the caption admits as much: Base and RAG generate a single completion per Lean retry, while 'KG-Prover may additionally apply beam search as detailed in §5.4'. Table 3 shows that the beam configuration uses r[n + w(w^s − 1)/(w − 1)] = 30 LLM calls per problem versus 3 for Base and RAG. Under this protocol the KG-Prover row includes extra test-time compute and search, so headline improvements such as 31.97% vs. 20.49% on miniF2F can be produced by compute alone. The authors should report the exact configuration used for every Table 1 row and include flat-context beam/best-of-N baselines with identical call and token budgets.","section":"§4.3, Table 1, Table 3"},{"comment":"No uncertainty quantification is provided. ProofNet has 186 problems, miniF2F 244, and MUSTARDSAUCE 250, so several reported differences of 1–2 percentage points (e.g., ProofNet Llama 3.1 8B: 4.30% vs. 3.76%; miniF2F o1-mini: 30.74% vs. 28.28%) are within plausible binomial noise. The paper should report confidence intervals or significance tests (e.g., McNemar or bootstrap) and, for nondeterministic settings, multiple seeds. Without this, the claim of 'consistent improvements ranging from 2–11%' is not warranted.","section":"§5.1, Table 1"},{"comment":"There is an internal inconsistency about whether graph edges are used at all. Section 3.2.1 defines traversal over the 1-hop neighbors V_d of the traversed set, but Appendix H.2 describes the semantic-search implementation as 'avoid[ing] exhaustive traversal' and incrementally adding 'the most similar nodes' to the prompt. If the reported rows are actually produced by flat semantic similarity rather than graph adjacency, the paper's central graph-based claim is untested. The authors should clarify which experimental rows use graph edges, and include an ablation that shuffles or randomizes node order within the same retrieved-context set.","section":"§3.2.1, Appendix H.2"},{"comment":"The six free parameters introduced in §4.4 (k, r, d, n, w, search depth) are tuned on the test benchmarks themselves: depth is varied in Figure 2, n is varied in Table 6, and the 'depth = 6' configuration in Table 2 is reported on miniF2F test. No validation-split protocol or fixed default configuration is described. This creates a risk that the reported 'best' numbers are selected from many configurations on the test set. A sensitivity analysis with a fixed default configuration and a hold-out validation protocol is needed before the reported gains can be taken at face value.","section":"§4.4, §5.2, Figure 2, Table 6"}],"minor_comments":[{"comment":"The baseline description says 'single-completion, single-retry budget' but then specifies 'on failure we repeat the same single-completion pipeline up to r=3 times'; the wording should be aligned with the actual r=3 budget.","section":"§4.3.1"},{"comment":"The notation for V_{d-1} is circular: 'V_{d-1} is defined as the set of v_j: ∃(a,b) ∈ E where a ∈ V_{d-1}'. Please define V_0 and the neighbor-expansion step with distinct index names.","section":"§3.2.1"},{"comment":"The pass@128 comparison is unclear: the table reports TheoremLlama at pass@128 (35.04%) and TheoremLlama + KG-Prover at 36.89%, but the number of proof attempts, tokens, and traversal budget for the KG-Prover row is not stated, so the comparison may not be budget-matched.","section":"Table 2"},{"comment":"The phrase 'on average performs on par better' is grammatically confusing; it should be rewritten to state whether the depth-1 configuration is better or equal to the non-scaling KG-Prover.","section":"§5.4"},{"comment":"The Limitations section contains an incomplete sentence ending 'different attention mechanisms or.' and the phrase 'disrupt of affect' should be 'disrupt or affect'.","section":"§7"},{"comment":"The reproducibility statement says the code is publicly available on GitHub but provides no URL, repository name, or commit hash; please include a link.","section":"§8"}],"recommendation":"major_revision","confidential_remarks":"The paper is a plausible empirical contribution, and the external Lean verification and public benchmarks are strengths. However, the central attribution claim is currently not supported because traversal depth, retry count, and beam search are conflated, and no compute-matched baselines are provided. I would ask the authors to add the missing controls and uncertainty quantification; this is a focused empirical fix rather than a request for a different scope."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick take: this is a modest, believable idea with a real verification setup, but the headline claim about graph-based scaling is not supported by the experiments as reported.\n\nThe genuinely new piece is the specific pipeline: a ProofWiki-derived knowledge graph, embedding-based retrieval, iterative neighbor expansion, an LLM judge for best-of-N and beam search, and informal-to-Lean verification. The graph itself (60k nodes, 300k edges) is a useful asset. Because correctness is checked by the external Lean verifier on public benchmarks, the successes in Tables 1 and 5 are real proofs, not self-assessed. The general direction that retrieved context helps LLM theorem proving is consistent with prior RAG work and the table-level trends are consistent across six models.\n\nThe soft spots are central, not cosmetic. Table 1's caption says KG-Prover \"may additionally apply beam search\" while Base and RAG generate a single completion per Lean retry. Table 3 shows that beam configuration uses 30 LLM calls per problem versus 3 for baselines. There is no compute-matched control, such as best-of-N sampling over a flat retrieval corpus with the same call and token budget. Figure 3's x-axis is labeled \"Traversal Depth r\" but Section 5.3 defines r as consecutive attempts, so the scaling curves are equally explained by \"more retries help\" without any graph. The semantic search description in Appendix H.2 (\"avoids exhaustive traversal\") makes it unclear whether graph edges are used at all in the reported system. There are also no error bars or significance tests, hyperparameters appear to be chosen on the test set, the abstract's \"up to 21%\" does not match Table 1, the traversal equation in Section 3.2.1 is garbled, and no GitHub link appears despite the reproducibility statement.\n\nNone of this kills the underlying idea. A revision with a compute-matched baseline, error bars, and a clean graph-versus-retries ablation would tell us whether the graph structure earns its complexity. As written, the quantitative claims run ahead of the evidence.\n\nThis paper is for researchers working on retrieval-augmented theorem proving or test-time compute scaling. They would get value from the system description and the failure analysis, but should not take the headline numbers at face value. It deserves a serious referee because the question is real and the verification setup is sound, but I would expect major revision before it is citable.","headline":"Plausible retrieval-helps result, but the graph-scaling attribution is not established without a compute-matched control.","tokens_in":18682,"tokens_out":2727,"would_cite":false,"duration_ms":28548,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"KG-Prover claims that injecting a knowledge graph mined from a curated mathematics compendium into off-the-shelf LLMs, and scaling traversal depth with best-of-N and beam search, raises theorem-proving accuracy by up to 21% on…","keywords":["automated theorem proving","knowledge graph","test-time compute scaling","retrieval-augmented generation","natural language proofs","Lean 4 verification","beam search","best-of-N sampling"],"falsifier":"Run a compute-matched control that spends the same 30 LLM calls per problem on best-of-N sampling or repeated chain-of-thought retries with no graph context; if that control matches or beats KG-Prover's 31.97% on miniF2F-test, the claim that the graph drives the gains would be refuted.","tokens_in":17607,"feed_emoji":"🧮","tokens_out":9970,"duration_ms":87675,"temperature":0.7,"pith_summary":"KG-Prover tries to establish that a general-purpose LLM can prove more theorems in natural language when, at inference time, it is given semantically retrieved and graph-expanded context from a large mathematical knowledge graph. The paper claims accuracy gains of up to 21% on miniF2F-test, consistent 2-11% improvements across ProofNet, miniF2F-test, and MUSTARDSAUCE, and further gains from scaling test-time compute via traversal depth, best-of-N sampling, and beam search. If true, this matters because it would mean substantial theorem-proving progress is available without finetuning on formal corpora: an off-the-shelf model, a curated concept graph, and a Lean verification loop may suffice. The framework separates proof generation from formalization, so the natural-language reasoning is judged by Lean rather than assumed correct.","feed_headline":"Knowledge graph lifts LLM theorem-proving accuracy by up to 21%","feed_subtitle":"KG-Prover feeds a 60,000-node math knowledge graph to off-the-shelf LLMs, beating baselines with no fine-tuning.","key_machinery":"The central object is the proof-knowledge graph $G=(V,E)$ built from a curated mathematics compendium, where each node is a definition, theorem, lemma, or corollary and hyperlinks between pages become edges. Given a proposition $P$, the system embeds $P$ and scores all nodes by cosine similarity $S=\\frac{v_P\\cdot v_i}{\\lVert v_P\\rVert_2\\lVert v_i\\rVert_2}$, uses the top-$k$ nodes as initial context, and if the proof fails Lean verification, expands to the top-$k$ 1-hop neighbors of already traversed nodes up to a depth $D$ with $r$ attempts. A judge-based best-of-$N$ selection and beam-search refinement scale the candidate generation at test time, and a separate autoformalizer translates the winning informal proof into Lean 4 for verification.","core_discovery":"On the paper's own terms, KG-Prover discovers that injecting related mathematical statements retrieved from a ProofWiki-derived knowledge graph into the prompt of a general-purpose LLM, and iteratively expanding retrieval to neighboring nodes when Lean verification fails, reliably improves proof success rates across benchmarks. The headline results are a rise from 20.49% to 31.97% for Llama 3.1 8B on miniF2F-test and 52.9% for o4-mini with beam search, with consistent gains on ProofNet and MUSTARDSAUCE. The authors present this as evidence that graph-structured knowledge, rather than additional training, can supply the missing concepts and dependencies that LLMs need for formal mathematical proof.","pith_inferences":["The paper leaves implicit that the same traversal-retrieval design could serve other multi-step reasoning tasks where a concept graph exists, turning verifier feedback into a retrieval signal.","A testable extension is to substitute domain-specific concept graphs, such as physics or chemistry formalisms, and check whether the same depth-scaling curve appears; that would show the mechanism is graph structure rather than mathematics-specific content.","Their failure analysis reports about 35% of failures come from translating a largely correct informal proof into Lean, which suggests the next bottleneck may be autoformalization quality rather than retrieval coverage.","An ablation that fixes the LLM-call budget across methods would clarify how much of the reported gain is due to graph structure versus simply more attempts and more context."],"forward_implications":["Any general-purpose LLM in the study improves on at least one of the three benchmarks when graph context is added, with the largest jump on miniF2F-test.","Scaling traversal depth, candidate count, and beam width keeps improving accuracy, with the first three depth steps delivering most of the gain.","Finetuned Lean provers also gain from the graph: TheoremLlama's pass@128 rises from 35.04% to 36.89% when KG-Prover context is included.","Because retrieval, informal proof generation, autoformalization, and verification are separate stages, each can be replaced or upgraded independently in future systems."],"supporting_citations":[{"why":"Supplies the source corpus: the knowledge graph is built by parsing its pages into 60,000+ nodes and 300,000+ edges.","marker":"(ProofWiki, 2025)"},{"why":"Lean 4 is the verification target; formal proofs are checked by Lean.","marker":"(de Moura and Ullrich, 2021)"},{"why":"DeepSeek-Prover-V1.5 is used as the autoformalizer that translates informal proofs into Lean 4, and its RLPAF loop motivates the verification-refinement design.","marker":"(Jiang et al., 2024)"},{"why":"miniF2F-test is the primary benchmark on which the headline 21% and 52.9% results are measured.","marker":"(Zheng et al., 2022)"},{"why":"ProofNet is one of the three evaluation datasets, providing hard undergraduate-level theorem statements.","marker":"(Azerbayev et al., 2023)"},{"why":"MUSTARD/MUSTARDSAUCE is the third benchmark, generated via GPT-4, used with 250 problems.","marker":"(Huang et al., 2024)"},{"why":"text-embedding-3-large supplies the semantic embeddings that drive node retrieval and graph traversal.","marker":"(Neelakantan et al., 2022)"},{"why":"Self-consistency motivates the best-of-N candidate selection and judge-based ranking.","marker":"(Wang et al., 2023)"},{"why":"Beam search over proof candidates with verifier feedback is the scaling strategy for the top results.","marker":"(Sun et al., 2023)"}],"fun_headline_variants":["Graph-retrieved prompts boost LLM theorem proving up to 21%","Knowledge graph lifts LLM proof rates 21% with no fine-tuning","KG-Prover scales test-time compute: 21% better theorem proving","Graph-based think time improves LLM theorem-proving by 21%"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the accuracy gains come from the knowledge graph's structure and traversal, not from the extra test-time compute or a weak retrieval baseline, because KG-Prover is allowed up to 30 LLM calls per problem while the RAG baseline uses a fixed context with only retries.","fun_headline_variants_meta":{"raw":{"variants":["Graph-retrieved prompts boost LLM theorem proving up to 21%","Knowledge graph lifts LLM proof rates 21% with no fine-tuning","KG-Prover scales test-time compute: 21% better theorem proving","Graph-based think time improves LLM theorem-proving by 21%"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000387,"raw_usage":{"total_tokens":2014,"prompt_tokens":884,"completion_tokens":1130,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":500,"completion_tokens_details":{"reasoning_tokens":1051}},"tokens_in":500,"tokens_out":1130,"duration_ms":10085,"temperature":1.0,"reasoning_tokens":1051,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T13:29:48.998744+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a compute-matched control that spends the same 30 LLM calls per problem on best-of-N sampling or repeated chain-of-thought retries with no graph context; if that control matches or beats KG-Prover's 31.97% on miniF2F-test, the claim that the graph drives the gains would be refuted.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the source corpus: the knowledge graph is built by parsing its pages into 60,000+ nodes and 300,000+ edges."}],"review_version":1}