{"id":"baa636e6-afc9-4e9e-a596-de0a10aa123a","arxiv_id":"2506.15211","paper_version":1,"verdict":"REJECT","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"high","formal_verification":"none","parameter_count":4,"one_line_summary":"Training on Prolog and PDDL representations improved several LLM reasoning benchmarks, but the controlled comparison does not show prototype training beats natural language training, and the abstract overstates the result.","lead":"The authors add Prolog-coded logic puzzles and PDDL-coded planning tasks to the training data of a large language model, then measure changes on reasoning benchmarks. Their central claim that abstract 'reasoning prototypes' explain the gains is contradicted by their own ablations, where natural-language training performed as well or better.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The paper's own matched ablation contradicts the abstract's central claim: Table 4 shows +NL (58.1 transfer, 45.0 dev) beats +Prolog (54.2, 44.1), so prototype training does not show enhanced generalization over natural-language training on structurally similar problems.","rationale":"The reader's weakest assumption concerns whether the automated Prolog/PDDL formalizations faithfully preserve the semantics of the original natural-language problems; that is a serious threat to the mechanism claim because a lossy conversion would make the matched ablation invalid. My primary concern, however, is more direct: the central comparative claim is contradicted by the paper's own Table 4, regardless of whether the formalization is faithful. The abstract promises enhanced generalization from prototype training relative to natural-language training, yet +NL beats +Prolog on both the transfer set and the development set. Table 5's category-level analysis does not rescue the claim because the apparent successes are sparse, small-sample subsets while the aggregate direction is consistent. This is not a matter of missing confidence intervals; the point estimate itself points the wrong way. The separate formalization-fidelity concern would matter for any revised, weaker claim of comparability, but it is not needed to show that the stated claim is unsupported. I therefore concur with the reader's REJECT verdict and do not propose moving it. A revision that downgrades the claim to 'comparable,' includes all Enigmata categories with pre-registered inclusion criteria, reports uncertainty, and releases the paired data and conversion prompts could make a weaker empirical claim defensible.","tokens_in":13393,"tokens_out":5010,"duration_ms":52848,"concrete_test":"Recompute the Section 3.3 ablation on the full Enigmata-Eval benchmark with no categories excluded, and report per-sample bootstrap confidence intervals for the +Prolog minus +NL difference on both the transfer and development sets. If the upper bound of the interval does not exceed zero, the abstract's claim that prototype training shows enhanced generalization over natural-language training is falsified by the paper's own experimental design.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The abstract and Section 3.3 assert that learning in prototype space achieves enhanced generalization to structurally similar problems compared with natural-language training. The controlled evidence for this is the matched 453-sample ablation in Table 4. The table directly contradicts the claim: on the transfer set, +NL scores 58.1 versus +Prolog 54.2; on the development set, +NL scores 45.0 versus +Prolog 44.1. Table 5's category-level breakdown does not repair this: the aggregate direction favors NL in both sets, and the categories where +Prolog surpasses +NL are a small, non-pre-registered subset with sample sizes ranging from 4 to 757. The Logic transfer subset where +Prolog regresses below baseline is dismissed as 'limited samples' (n=32), but category-level cherry-picking with such tiny counts cannot support a claim of enhanced generalization. Additionally, the main Enigmata-Eval result in Section 3.1 depends on excluding four benchmark categories post hoc, and no error bars, public code, or public data are provided. Since the strongest empirical evidence for the mechanism is internally inconsistent with the paper's stated claim, the central claim is unsupported as written. A weaker claim of comparability would be more defensible, but the abstract's comparative 'enhanced generalization' claim fails on the paper's own results.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes ProtoReasoning, a framework for improving LLM reasoning by converting natural-language logic and planning problems into formal prototype representations (Prolog for logic, PDDL for planning), deriving ground-truth answers with interpreters, generating additional problems through prompt-based evolution, and supervised fine-tuning a 15B-active-parameter MoE model on the resulting data. The main experiments report gains on Enigmata-Eval (+4.7 percentage points), internal planning and Nexus-Hard evaluations (+6.3 and +6.4 points), MMLU (+4.0), and AIME24 (+1.0). The paper's central scientific claim is that training in prototype space improves generalization to structurally similar natural-language problems relative to training on natural-language versions of the same problems, based on a matched 453-sample ablation. The results in Table 4 do not support that claim: natural-language training outperforms Prolog training on both the transfer set (58.1 vs 54.2) and the development set (45.0 vs 44.1), and the Section 3.3 text itself describes the result as 'comparable' rather than superior.","tokens_in":13629,"tokens_out":5197,"duration_ms":53952,"significance":"If the hypothesis were established, the framework's ability to synthesize and verify reasoning data at scale would be a useful contribution to reasoning-model training. The paper has genuine strengths: interpreter-based verification is a principled way to obtain correct labels, the three PDDL task formulations (generation, completion, reordering) are sensible, and the matched ablation design is the right experimental shape for isolating representation format. However, the evidence as presented is insufficient: the signature ablation contradicts the headline claim, benchmark exclusions are post hoc, no uncertainty quantification is reported, and the internal evaluation sets are not described. The conceptual contribution ('reasoning prototypes') is asserted rather than formally defined, and Section 5 itself concedes this lack of formal rigor. As a result, the paper does not currently validate its claimed mechanism.","major_comments":[{"comment":"The abstract and Introduction state that the ablation confirms 'enhanced generalization' to structurally similar problems compared with natural-language training, but Table 4 shows the opposite: +NL scores 58.1 on the transfer set and 45.0 on the development set, while +Prolog scores 54.2 and 44.1. The Section 3.3 text softens this to 'comparable', yet the abstract and contributions still claim superiority. This is a direct contradiction in the central evidence, and the hypothesis-validation conclusion is unsupported as written. The authors must either provide a corrected statistical analysis that supports the comparative claim or explicitly withdraw it.","section":"Abstract and §3.3, Table 4"},{"comment":"Four Enigmata-Eval categories (Campsite, Car Painting, Star Battle, and Sum Skyscraper) are excluded post hoc with the justification that baseline models struggled primarily with instruction following. This exclusion changes the reported headline gain and is not part of the benchmark's standard protocol. The paper should report results both with and without the excluded categories, and it should explain why instruction-following failures are not relevant to the logical-reasoning abilities the paper claims to improve.","section":"§3.1, Enigmata-Eval evaluation"},{"comment":"The paper reports no error bars, confidence intervals, or significance tests for any of the differences, despite stating that each sample was evaluated three times (ten times for AIME24). The key ablation difference (58.1 vs 54.2) is in the opposite direction from the claimed effect, and the category-level comparisons in Table 5 involve very small samples (for example, n=4 for the Sequential transfer set and n=32 for the Logic transfer set). Without uncertainty quantification, the claim that prototypes produce comparable or superior generalization is not established.","section":"§3.1 and §3.3, Tables 2-5"},{"comment":"The prototype constructor relies on LLM prompt engineering to transform natural-language problems into Prolog and PDDL, but the paper provides no verification that the formalization is semantically faithful to the original problem, no error analysis of the transformation step, and no discussion of cases where the LLM simplified or altered the reasoning structure. Since the training labels are interpreter-verified for the formalized problem rather than the original problem, a systematic transformation error would mean the model is trained on a different task than the evaluation benchmark. The authors should include a transformation-fidelity audit on at least a representative sample.","section":"§2.2.1 and §2.3.1"}],"minor_comments":[{"comment":"The abstract reports '+4.7%' and '+6.3%' but Table 2 displays absolute percentage-point increases; please use consistent terminology to avoid ambiguity.","section":"Abstract and Table 2"},{"comment":"Equation (1) has a dangling formatting artifact ('DProlog = {⟨QProlog,A⟩ i ,') and should be typeset cleanly.","section":"Equation (1)"},{"comment":"The internal evaluation sets described as 'the Seed Project testing set' and 'Nexus-Hard' are not characterized in terms of size, sampling procedure, or prompt format, which prevents external verification of the reported results.","section":"§3.1"},{"comment":"The baseline dataset is described as 100K samples 'from the Seed Project' without a citation or public identifier; please name the exact dataset or provide a reference.","section":"§3.1"},{"comment":"Section 5 acknowledges that the precise definition of 'reasoning prototypes' lacks formal rigor and that the underlying mechanism requires deeper investigation; this limitation should be reflected in the abstract and contributions rather than appearing only in the closing paragraph.","section":"§5"}],"recommendation":"reject","confidential_remarks":"The discrepancy between the abstract and Table 4 is serious enough that a revision limited to wording changes would not be sufficient; the paper would need a new, adequately powered comparison with uncertainty quantification, as well as transparency about the internal evaluation sets and the post hoc benchmark exclusions. The paper is primarily an empirical systems contribution, and its theoretical framing is not formalized, but the empirical contradiction is the decisive issue."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear Colleague,\n\nThe bottom line: this paper is worth a look for its empirical recipe, but the abstract oversells it. The central claim that learning in 'prototype space' generalizes better than natural-language training is directly contradicted by their own Table 4: +NL scores 58.1 on the transfer set and 45.0 on the dev set, while +Prolog scores 54.2 and 44.1. The paper's ablation section honestly says 'comparable,' but the abstract and conclusion say 'enhanced.' That's a load-bearing inconsistency.\n\nWhat's genuinely new: an automated pipeline that converts natural-language logic problems into Prolog and planning problems into PDDL, with interpreter-based verification, used to augment SFT at a meaningful scale (4,196 Prolog and 2,424 PDDL instances on a 150B MoE with 15B active). The planning task formulations (Plan Generation, Completion, Reordering) are a nice touch. The reported gains on planning tasks (+6.3%), MMLU (+4.0%), and even AIME24 (+1.0%) are plausible and useful to people building reasoning data. The authors also acknowledge in the conclusion that 'reasoning prototypes' lack formal rigor—that's honest.\n\nSoft spots, in order of severity:\n\n1. The overclaim. The matched ablation is the only controlled test of the mechanism, and it favors NL. The category-level breakdown doesn't repair this; the aggregate is what matters.\n\n2. Post hoc exclusion of four Enigmata-Eval categories. The stated reason—baselines struggle with instruction-following—might be legitimate, but there is no pre-registered criterion.\n\n3. No error bars or significance tests. The gains are small, and without variance we can't tell if they're noise.\n\n4. Autoformalization semantics. The pipeline trusts that LLM-generated Prolog/PDDL faithfully captures the original problem, with no analysis of formalization errors. The interpreter verification only validates the formalization, not the match to the original.\n\n5. No code or data released yet, limiting reproducibility.\n\nWho is this for? People working on symbolic data generation for reasoning, and anyone studying cross-domain transfer. It deserves a serious referee, because the recipe and the negative result about prototypes are both informative. My recommendation: send it to review, but the referee report should demand (a) replacing 'enhanced generalization' with 'comparable to NL,' (b) reporting all Enigmata categories or pre-registering exclusions, (c) error bars, and (d) a commitment to release artifacts. A revision that does those things would be a solid empirical paper.","headline":"A useful verified-symbolic-data recipe undercut by an overclaim: the paper's own matched ablation shows natural-language training beats prototype training, so the abstract's claim of enhanced generalization fails.","tokens_in":14242,"tokens_out":3825,"would_cite":false,"duration_ms":36644,"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":"This paper argues that training LLMs on Prolog and PDDL prototypes—not natural language—is what makes reasoning transfer across domains.","keywords":["reasoning prototypes","cross-domain generalization","Prolog","PDDL","verifiable rewards","supervised fine-tuning","logical reasoning","planning"],"falsifier":"Sample a random set of the reported 4,196 Prolog and 2,424 PDDL training instances, have independent human experts translate each formal encoding back into natural language, and measure whether the reconstructed problems match the original source problems; if a substantial fraction mismatch, or if retraining on human-corrected encodings changes benchmark scores, the claim that prototype training teaches the original reasoning structure is refuted.","tokens_in":13131,"feed_emoji":"🧩","tokens_out":6169,"duration_ms":58656,"temperature":0.7,"pith_summary":"The paper proposes that cross-domain generalization in large reasoning models comes from shared abstract reasoning prototypes, which are common logical and planning skeletons hidden under different surface representations. It introduces ProtoReasoning, a framework that converts natural-language logic problems into Prolog and planning problems into PDDL, verifies answers with interpreters, and fine-tunes a large Mixture-of-Experts model on these formal problems. The authors report gains over the baseline on logical reasoning, planning, MMLU, and AIME24, and argue that training in prototype space transfers to structurally similar natural-language problems about as well as training on natural language itself. The intended contribution is a mechanism-level account of why long-chain-of-thought reasoning transfers across domains, together with a scalable data pipeline that requires no human-annotated answers.","feed_headline":"Training on Prolog and PDDL lifts LLM reasoning across domains","feed_subtitle":"The paper argues that formal prototypes, not natural language, carry transferable reasoning skills.","key_machinery":"The load-bearing machinery is the pair of prototype representations paired with verifiers. Prolog encodes logical relations as facts and rules resolved by unification and backtracking; PDDL separates domain types, predicates, and action schemas from problem objects, initial state, and goal, with plans validated by the VAL checker or solved optimally using FastDownward. A four-stage constructor pipeline uses an LLM to transform natural-language problems into these formalisms, evolves them for complexity, and derives ground-truth answers by running the interpreter. The verification system standardizes outputs as JSON for Prolog and as VAL-checked plans for PDDL, enabling the pipeline to synthesize arbitrary numbers of correct training examples without human-annotated answers. A three-phase training recipe—teacher distillation, difficulty stratification via rejection sampling, and quality filtration—turns the verified examples into a supervised fine-tuning set for a sparse 150B-parameter MoE model with 15B activated parameters.","core_discovery":"The central claim is that reasoning prototypes—canonical formal structures such as Prolog programs for logical puzzles and PDDL specifications for planning—are the foundation of generalizable reasoning in large language models. Learning to solve problems encoded in these prototypes, with interpreter-verified answers, is said to teach the model the underlying reasoning pattern rather than a surface format. The authors support this by showing that adding prototype-representation training to a standard supervised fine-tuning dataset improves performance on logic, planning, general knowledge, and mathematics benchmarks, and by ablation results in which the Prolog-trained model reaches transfer performance close to, though not above, a natural-language-trained model on matched problems. The paper frames this as evidence that the prototype captures the reasoning essence, making the representation unimportant once the structure is learned.","pith_inferences":["If the automated formalization step is lossy, the model may be learning to solve Prolog and PDDL reformulations rather than the original natural-language problems; a direct test is to compare transfer after human-corrected formalizations against the automated ones.","The paper's own Table 4 shows natural-language training outperforming Prolog training on both the matched transfer set and the development set, so the current evidence supports a weaker claim: prototype training is a data-efficient approximation of natural-language training, not clearly superior to it.","The prototype lens suggests a concrete research program: define reasoning prototypes formally, for instance as equivalence classes of problem structures under representation-preserving transformations, and measure transfer as a function of structural distance between prototype spaces.","Since verification is decoupled from language, the framework could extend to other verifiable formalisms such as constraint solvers or theorem provers, and to reinforcement learning with verifiable rewards where interpreter feedback replaces hand-written answer keys."],"forward_implications":["If prototypes are the basis of transfer, then reasoning training data can be generated synthetically in formal languages at arbitrary scale, since correctness is guaranteed by interpreters rather than human labels.","Reasoning skills learned in Prolog and PDDL should transfer to any natural-language task sharing the same underlying structure, implying that benchmark gains on Enigmata-Eval, MMLU, and AIME24 are instances of a general mechanism rather than isolated improvements.","The three PDDL task types—generation, completion, and reordering—decompose planning into component abilities, so prototype training could target specific planning sub-skills in a model.","Because the framework needs no problem-answer pairs, data construction cost shifts from annotation to prompt engineering and verification, which could scale to other formalizable domains."],"supporting_citations":[{"why":"Defines Prolog, the logic prototype representation that the entire logical-reasoning pipeline trains on.","marker":"[7]"},{"why":"Defines PDDL, the planning prototype representation used for all planning tasks.","marker":"[3]"},{"why":"Provides the VAL plan validator used to verify model-generated PDDL plans.","marker":"[14]"},{"why":"Supplies FastDownward, the solver used to generate optimal plans and reference values for optimization tasks.","marker":"[12]"},{"why":"Serves as the teacher model whose reasoning chains are distilled to create the augmented training data.","marker":"[10]"},{"why":"Provides the Enigmata-Eval benchmark used for logical-reasoning evaluation and for the matched Prolog-versus-natural-language ablation.","marker":"[5]"},{"why":"Supplies the MMLU general-knowledge benchmark used to test out-of-domain generalization.","marker":"[13]"},{"why":"Supplies AIME24, the mathematical reasoning benchmark used for out-of-domain evaluation.","marker":"[2]"}],"fun_headline_variants":["Prototype training boosts LLM logic, planning, and math","Formal prototypes teach transferable reasoning to LLMs","Interpreter-verified prototypes sharpen LLM reasoning","Prolog and PDDL teach LLMs reasoning, not just language","ProtoReasoning: formal prototypes improve LLM reasoning"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole argument rests on the assumption that the automated LLM transformation from natural-language problems into Prolog and PDDL preserves the original problem's meaning exactly, so that an interpreter-verified answer to the formalized version is also the correct answer to the original problem; if the transformation is systematically lossy or simplifying, the model is being trained on different problems than the ones used for evaluation.","fun_headline_variants_meta":{"raw":{"variants":["Prototype training boosts LLM logic, planning, and math","Formal prototypes teach transferable reasoning to LLMs","Interpreter-verified prototypes sharpen LLM reasoning","Prolog and PDDL teach LLMs reasoning, not just language","ProtoReasoning: formal prototypes improve LLM reasoning"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000876,"raw_usage":{"total_tokens":3800,"prompt_tokens":970,"completion_tokens":2830,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":586,"completion_tokens_details":{"reasoning_tokens":2749}},"tokens_in":586,"tokens_out":2830,"duration_ms":17915,"temperature":1.0,"reasoning_tokens":2749,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T19:40:51.198267+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Sample a random set of the reported 4,196 Prolog and 2,424 PDDL training instances, have independent human experts translate each formal encoding back into natural language, and measure whether the reconstructed problems match the original source problems; if a substantial fraction mismatch, or if retraining on human-corrected encodings changes benchmark scores, the claim that prototype training teaches the original reasoning structure is refuted.","supporting_citations":[{"cited_title":"Prentice hall Upper Saddle River, 1994","cited_arxiv_id":null,"evidence_quote":"Defines Prolog, the logic prototype representation that the entire logical-reasoning pipeline trains on."},{"cited_title":"Pddl| the planning domain definition language","cited_arxiv_id":null,"evidence_quote":"Defines PDDL, the planning prototype representation used for all planning tasks."},{"cited_title":"Val: Automatic plan validation, continuous effects and mixed initiative planning using pddl","cited_arxiv_id":null,"evidence_quote":"Provides the VAL plan validator used to verify model-generated PDDL plans."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies FastDownward, the solver used to generate optimal plans and reference values for optimization tasks."},{"cited_title":"URLhttps://artofproblemsolving.com/wiki/index","cited_arxiv_id":null,"evidence_quote":"Supplies AIME24, the mathematical reasoning benchmark used for out-of-domain evaluation."}],"review_version":2}