{"id":"6103b35c-5b4b-4893-8d7d-b88d5da9aa4c","arxiv_id":"2509.10249","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"On first-order logic reasoning with small language models, the compact CLIF grammar achieves accuracy close to natural language, though natural language remains the best representation.","lead":"This paper tests whether small language models can solve logic reasoning problems when the input is written in a compact formal notation instead of plain English. On the FOLIO dataset, a notation called CLIF performed nearly as well as natural language, suggesting formal grammars are a practical substitute for reasoning prompts.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"CLGC transformation fidelity is unverified and demonstrably broken in Table 3; since CLIF data for the headline comparison comes from the same pipeline, the CLIF-vs-NL gap is meaningful only after a semantic equivalence check.","rationale":"The reader's weakest assumption correctly identifies the transformation pipeline as the keystone of the empirical claim. The paper's own Table 3 provides direct counterevidence for MINIFOL and CGIF: row 7 maps a negated XOR to an AND, and rows 5 and 6 drop negations. The CLIF rows in the same table are correct, so the concern is not that CLIF is already shown to be corrupted; it is that the common pipeline that generated all formal-language datasets has no semantic verification, and the demonstrated failures prove the pipeline can change truth conditions. Because the central result (CLIF 0.6157 vs NL 0.6600 on Flan-T5-large) depends entirely on the CLIF test inputs being faithful renderings of the FOLIO problems, the unsupported equivalence is the most load-bearing vulnerability. Lack of error bars is secondary: it affects the strength of the numeric claim but not whether the compared inputs are the intended reasoning problems. The proposed check (automated equivalence verification of every transformed CLIF pair, plus recomputation after excluding mismatches) would settle the concern. The reader already conditioned acceptance; this review finds no reason to move beyond CONDITIONAL, hence UNCHANGED.","tokens_in":15461,"tokens_out":7328,"duration_ms":63928,"concrete_test":"Run the CLGC pipeline on all FOLIO premises/conclusion pairs, parse the FOL and CLIF outputs, translate both into a common first-order syntax, and use a theorem prover (e.g., Vampire, E, or an SMT solver like Z3) to verify logical equivalence for every pair; report the per-grammar mismatch rate. If the CLIF mismatch rate is zero, re-run Table 6 after excluding any mismatched examples; if the mismatch rate is nonzero, recompute the accuracies on the corrected or excluded data and assess whether CLIF still remains competitive with NL.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim that compact CLIF can substitute for NL (Table 6: 0.6157 vs 0.6600) presupposes that the CLGC pipeline's outputs are logically equivalent to the FOLIO FOL annotations. The paper provides no equivalence proof or automated check, and its own Table 3 shows the pipeline is not meaning-preserving. Row 7 maps ¬(Manager(james)⊕AppearIn(james,company)) to MINIFOL (manager(james) ∧ appearin(james,company)), which is not equivalent: the FOL formula is true when both atoms have the same truth value, while the MINIFOL formula is true only when both are true. Row 5 and Row 6 additionally drop the negation on ¬In and ¬Work in MINIFOL and CGIF. These are not cosmetic: if the same fidelity failure occurs in CLIF at any nontrivial rate, the accuracy difference of 0.044 could reflect corrupted problem content rather than representation quality. The CLIF examples shown happen to be correct, but the pipeline is a generic grammar-mapping algorithm with manual grammar updates (Section 3.3), so correctness of a few examples does not establish correctness of the 1,204 generated examples. Without released transformed data or a semantic equivalence check, the headline comparison is unverified.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The manuscript investigates whether small language models (SLMs) can reason over first-order logic problems when the input is expressed in formal grammars rather than natural language. The authors introduce the Syllogistic Evaluation Framework (SEF) for classifying FOLIO reasoning pairs and the Common Logic Grammar Construction (CLGC) pipeline that translates the FOLIO FOL annotations into CLIF, CGIF, TFL, TFL+, and a custom MINIFOL. They then evaluate Flan-T5-small/base/large, GPT-2, Phi-3.5-mini-instruct, and Gemma-2-2b-it under supervised fine-tuning (with and without LoRA), zero-shot prompting, and 8-shot prompting, with additional variations including grammar-context passing and tokenizer re-training. The main claim is that CLIF, a compact formal language, can largely substitute for natural language while preserving SLM reasoning performance, based on CLIF matching or closely trailing NL in Tables 5 and 6. The paper concludes that compact formal representations are viable for bootstrapping ontology engineering with SLMs, though it positions the work as preliminary.","tokens_in":15783,"tokens_out":7859,"duration_ms":60829,"significance":"The paper addresses a timely and practical question—whether the input representation of logical problems can be made more compact without hurting SLM performance—with a broad configuration matrix spanning multiple models, grammars, and training regimes on the public FOLIO benchmark. The SEF syllogism-type breakdown in Table 13 is a useful descriptive lens, and the tokenizer re-training comparison in Table 12 is an interesting exploratory direction. The central claim is falsifiable and, if substantiated, would be practically relevant for ontology engineering because it would permit more efficient encoding of logical knowledge for SLMs. However, the empirical evidence as presented does not yet establish the claim: the transformation pipeline that generates the formal-language datasets is not shown to be meaning-preserving, and the headline comparisons lack statistical support. The paper's strengths are its scope and the specificity of the research questions; those strengths would be better leveraged by pairing the wide comparison with a smaller set of rigorously verified and repeated experiments.","major_comments":[{"comment":"The CLGC pipeline is not demonstrated to preserve the truth conditions of the FOL formulas it translates. For instance, the formula ¬(Manager(james) ⊕ AppearIn(james, company)) is rendered in MINIFOL as (manager(james) ∧ appearin(james, company)), which is not logically equivalent; the rows for ∀x ((Employee(x)∧(¬In(x, homecountry)))→Work(x, home)) and ∀x (Manager(x) → ¬Work(x, home)) drop the negations on ¬In and ¬Work in both MINIFOL and CGIF. Since all formal-language datasets used in the Section 4 experiments are produced by this pipeline, the accuracy comparisons for CLIF, CGIF, TFL, TFL+, and MINIFOL are only interpretable if every generated formula is verified to be logically equivalent to its FOL source. At minimum, the authors need to provide an automated equivalence check (or a released dataset with per-formula verification) and to rerun or clearly qualify the affected results.","section":"Section 3.2.3 and Table 3"},{"comment":"All reported metrics are from single runs with no error bars, confidence intervals, or significance tests. The headline CLIF-vs-NL difference for Flan-T5-large in Table 6 is 0.6600 vs 0.6157 in accuracy; without repeated seeds or a significance test, this gap is within plausible random variation and cannot support the claim that CLIF ties or ranks second-best to NL. The same issue affects the grammar-prompting comparison in Table 8, where only one model is used and metric changes are inconsistent (e.g., CLIF F1 improves while precision drops; TFL+ precision drops from 0.5634 to 0.3618).","section":"Sections 4.1-4.2, Tables 5-6"},{"comment":"The comparison between Flan-T5-small and the larger models is confounded by the fine-tuning setup. Flan-T5-small rows are fully fine-tuned without LoRA, whereas the Flan-T5-large rows are marked with an asterisk and use PEFT-LoRA. Consequently, the text's claim that the smallest model outperforms larger, fine-tuned models is not supported by the table: Flan-T5-large* achieves a higher accuracy than Flan-T5-small on NL (0.4729 vs 0.4384). Any conclusion about model-size effects must compare models trained with the same fine-tuning procedure.","section":"Section 4.2, Table 5"},{"comment":"Several rows across different models and grammars report exactly identical metrics (e.g., accuracy 0.3546, precision 0.1182, recall 0.3333, F1 0.1745 for many entries in Table 9, and for all entries in Table 10). This strongly suggests that these configurations collapse to a constant prediction, such as always predicting the majority class, and therefore those rows carry no information about the language being tested. The paper should report per-configuration prediction distributions and should not use such rows to draw conclusions about grammar performance, for example the statement in Section 4.2 that CLIF is a more compact contender in the 8-shot setting.","section":"Section 4.2, Tables 9-10"}],"minor_comments":[{"comment":"The sentence 'Our findings show that it is possible to substitute Natural Language (NL) with a more compact logical language while maintaining a strong performance on reasoning tasks and hope to use these results...' is a fragment; the subject of 'hope' is unclear and the sentence should be rewritten.","section":"Abstract"},{"comment":"Algorithm 1 uses the variable D in the loop over statements without defining it in the Require or Ensure block; please clarify the notation so the loop is unambiguous.","section":"Algorithm 1"},{"comment":"Reference [29] (a paper on jailbreaking via language games) does not appear to support the claim that the language in which a model receives a problem affects its success rate; a more directly relevant citation on input representation or prompt language effects would be appropriate.","section":"Section 2.1, reference [29]"},{"comment":"The text says that Table 8 shows CLIF outperforming all other languages in the zero-shot setting, but the table only reports Gemma-2-2b-it on CLIF, FOL, TFL+, and TFL; it does not include NL, CGIF, MINIFOL, or the other models, so the statement is stronger than the evidence.","section":"Section 4.2, Table 8"},{"comment":"The Tokenizer Re-Train column lists the CLIF condition with vocabulary size 32128 for both 'Yes' and 'No', which is confusing because re-training without resizing should preserve the size; clarify whether the re-trained CLIF tokenizer was resized and unify the notation.","section":"Table 12"},{"comment":"The prose describing Table 14 says the model reasons 'False' as opposed to 'Uncertain' on a single occasion, but the table shows several label differences across NL, CLIF, and TFL+; describe the error pattern more precisely so the reader can map the text to the table.","section":"Section 4.2, Table 14"}],"recommendation":"major_revision","confidential_remarks":"The paper is framed as a preliminary PhD-stage study, and its broad configuration matrix is ambitious. The central obstacle is the unverified and demonstrably error-prone transformation pipeline, which undercuts the main comparison until corrected. I would encourage a revision that narrows the scope to verified transformations and adds statistical rigor, rather than expanding the number of grammars and models."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the take: this is a workshop-grade preliminary study with a genuinely new empirical comparison—seven input grammars for small-model first-order reasoning on FOLIO—but the headline claim that CLIF can substitute for natural language is not yet supported because the pipeline that generated the CLIF data is unverified and demonstrably corrupts at least one target grammar.\n\nThe genuinely new thing is the systematic comparison itself, and the CLGC transformation pipeline as a reusable tool. The idea that input representation affects LM reasoning is already known, but nobody has laid out CLIF, CGIF, TFL, TFL+, MINIFOL, FOL and NL side by side on the same benchmark with sub-3B models. The SEF syllogism categorization is a nice addition. The paper is honest about being a first step and describes the setup well enough to reproduce.\n\nWhat the paper does well: the results tables are informative, and the observation that CLIF is competitive with NL on Flan-T5-large in full supervised fine-tuning (0.6157 vs 0.6600 accuracy) is plausible and worth chasing.\n\nThe soft spots are real, though correctable. The biggest is the CLGC pipeline. Table 3 shows a direct counterexample: the FOL formula ¬(Manager(james) ⊕ AppearIn(james, company)) is transformed into MINIFOL as (manager(james) ∧ appearin(james, company)), which is not logically equivalent—XOR negation does not reduce to conjunction. Two other rows also drop negations. That means the pipeline is not meaning-preserving. If the same class of error appears in any nontrivial fraction of the 1,204 generated CLIF examples, the CLIF-vs-NL gap could come from corrupted problem content rather than grammar quality. The authors mention manual grammar revisions but give no equivalence proof, no automated check, and no released transformed data. Second, all head-to-head claims rest on single runs without error bars or significance tests. Third, comparing Flan-T5-large with LoRA (Table 5) to full fine-tunes (Table 6) mixes two variables, so statements about model scaling are muddy. Fourth, some 8-shot tables show identical accuracy across all grammars (e.g., Gemma-2-2b-it at 0.3546), which suggests the model is ignoring the examples; that deserves at least a sentence of discussion.\n\nNone of this is fatal for a first look. The research question is sound, and the paper is coherent in what it attempts. The citation pattern is appropriate. I would send this to a serious workshop referee, with the expectation of heavy revision. For my own work, I would not yet cite the accuracy numbers, but I would cite the comparison as prior art if I were writing in this exact niche. It is a good reading-group paper because the pipeline-fidelity problem makes for a sharp methodological discussion.","headline":"Useful new grammar comparison on FOLIO, but the CLIF-vs-NL claim is unproven because the CLGC pipeline is not meaning-preserving and demonstrably corrupts at least one target grammar.","tokens_in":16285,"tokens_out":3840,"would_cite":false,"duration_ms":31049,"reading_group":"yes","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 claims that small language models can be fed compact formal logic grammars instead of natural language and still reason nearly as well, with CLIF matching NL on Flan-T5-small and falling only slightly behind on Flan-T5-large.","keywords":["small language models","logical reasoning","knowledge representation","CLIF","common logic","FOLIO","grammar construction","ontology engineering"],"falsifier":"Count, over the whole FOLIO test and validation sets, how many transformed formulas differ in satisfiability or truth value from their FOL originals (e.g., the shown MINIFOL output for ¬(Manager(james) ⊕ AppearIn(james, company)) is (manager(james) ∧ appearin(james, company)), which is satisfiable when the original is false). If even a small percentage of inputs are corrupted, the accuracy comparisons across grammars no longer compare the same reasoning problems.","tokens_in":15271,"feed_emoji":"🧠","tokens_out":5521,"duration_ms":44160,"temperature":0.7,"pith_summary":"The paper is a first attempt to answer whether natural language is the best input for small language models solving first-order logic reasoning tasks. On the FOLIO dataset, with supervised fine-tuning, representing premises and conclusions in the compact formal grammar CLIF matches natural-language accuracy on Flan-T5-small (0.4384 vs 0.4384) and comes close on Flan-T5-large (0.6157 vs 0.6600). The authors take this as evidence that a more compact logical language can substitute for natural language while preserving reasoning performance. If this holds, ontology engineering could be bootstrapped by feeding SLMs formal logical statements rather than verbose English, reducing input length while keeping the model's reasoning abilities intact.","feed_headline":"Compact logic language matches natural language for SLM reasoning","feed_subtitle":"Fine-tuned small models reason nearly as well from CLIF logic formulas as from English on FOLIO, with far fewer tokens.","key_machinery":"The machinery is a pipeline that converts first-order logic formulas between grammars: it parses FOL with a BNF grammar, builds a parse tree, maps the tree to a target grammar (CLIF, CGIF, TFL, TFL+, MINIFOL), and regenerates the text. This pipeline plus the Syllogistic Evaluation Framework (SEF), which classifies each FOLIO problem as Disjunctive, Hypothetical, Categorical, or Complex, defines the experimental comparison. The conversion step is load-bearing because all accuracy differences across grammars are attributed to the language itself; if the conversions change logical meaning, the comparison collapses.","core_discovery":"The central claim is that the choice of the formal representation matters less than the literature assumes: a compact logical grammar, CLIF, can carry first-order reasoning tokens nearly as well as natural language in small models. The evidence comes from a controlled comparison across six models, seven input languages, and three learning settings, with FOLIO as the fixed reasoning benchmark. In the strongest setting, supervised fine-tuning on an A100 GPU, Flan-T5-large reaches 0.6157 accuracy with CLIF against 0.6600 with natural language, and Flan-T5-small ties natural language exactly at 0.4384. The authors conclude that no single grammar outperforms natural language, but compact formalisms come close enough to be viable substitutes, especially for models under three billion parameters.","pith_inferences":["If the CLGC conversions were verified to preserve first-order meaning, the accuracy gap between CLIF and NL would measure representation cost directly; one testable extension is to run the same comparison on datasets like ProofWriter or RuleTaker, where formulas are synthetic and can be checked for equivalence exactly.","The observed CLIF-vs-NL closeness suggests an input-compression effect: the model may be using the same latent reasoning machinery while struggling less with surface forms; this could be tested by measuring accuracy versus the amount of fine-tuning data for CLIF and NL.","For ontology engineering, the practical implication is that SLMs could consume ontology axioms in CLIF directly, shrinking prompts and avoiding paraphrase ambiguity; this is an extension beyond the paper's experiments, which stop at FOLIO-style reasoning."],"forward_implications":["Compact formal grammars like CLIF can be used to shorten LM inputs without giving away much reasoning accuracy, so they may be practical for low-resource settings.","The conclusion is not that NL is best, but that a compact grammar is competitive; thus grammar choice should be measured alongside model size and training method.","Grammar prompting helps in zero-shot but not few-shot or fine-tuning, so its benefit is setting-dependent.","Tokenizer re-training on a compact grammar can boost small models (e.g., Flan-T5-small on TFL+) but does not scale to larger models.","SEF-based breakdown shows performance is concentrated in Disjunctive and Hypothetical syllogisms, with Categorical too sparse to evaluate."],"supporting_citations":[{"why":"Supplies the FOLIO benchmark with natural-language and first-order-logic versions of every premises-conclusion pair used in the experiments.","marker":"[23]"},{"why":"Defines the Common Logic conceptual-graph family, including CLIF and CGIF, the target grammars built by the CLGC pipeline.","marker":"[31]"},{"why":"Provides the introduction to Common Logic that the paper uses to implement the CLIF and CGIF grammars.","marker":"[33]"},{"why":"Introduces term logic (TFL), the formal language whose grammar the pipeline implements and evaluates.","marker":"[34]"},{"why":"LoRA is the parameter-efficient fine-tuning method used to train the larger models in the constrained-GPU settings.","marker":"[37]"},{"why":"Grammar prompting for domain-specific generation motivates the zero-shot BNF grammar prompt experiments.","marker":"[38]"}],"fun_headline_variants":["Logic formulas rival English for small-model reasoning","SLMs reason nearly as well from CLIF as from English","Token-efficient logic for small language models","Formal grammar, near-English reasoning in small LMs","CLIF logic: compact substitute for natural language in SLMs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The conversion from first-order logic to each alternative grammar must preserve the meaning of every formula, but no equivalence proof or automated verification is supplied, and Table 3 shows a MINIFOL output that is not equivalent to its FOL input.","fun_headline_variants_meta":{"raw":{"variants":["Logic formulas rival English for small-model reasoning","SLMs reason nearly as well from CLIF as from English","Token-efficient logic for small language models","Formal grammar, near-English reasoning in small LMs","CLIF logic: compact substitute for natural language in SLMs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000703,"raw_usage":{"total_tokens":3120,"prompt_tokens":841,"completion_tokens":2279,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":457,"completion_tokens_details":{"reasoning_tokens":2203}},"tokens_in":457,"tokens_out":2279,"duration_ms":15625,"temperature":1.0,"reasoning_tokens":2203,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T15:56:08.231933+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Count, over the whole FOLIO test and validation sets, how many transformed formulas differ in satisfiability or truth value from their FOL originals (e.g., the shown MINIFOL output for ¬(Manager(james) ⊕ AppearIn(james, company)) is (manager(james) ∧ appearin(james, company)), which is satisfiable when the original is false). If even a small percentage of inputs are corrupted, the accuracy comparisons across grammars no longer compare the same reasoning problems.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Grammar prompting for domain-specific generation motivates the zero-shot BNF grammar prompt experiments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the FOLIO benchmark with natural-language and first-order-logic versions of every premises-conclusion pair used in the experiments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines the Common Logic conceptual-graph family, including CLIF and CGIF, the target grammars built by the CLGC pipeline."},{"cited_title":"Sowa, Introduction to common logic, 2011","cited_arxiv_id":null,"evidence_quote":"Provides the introduction to Common Logic that the paper uses to implement the CLIF and CGIF grammars."},{"cited_title":"Sommers, G","cited_arxiv_id":null,"evidence_quote":"Introduces term logic (TFL), the formal language whose grammar the pipeline implements and evaluates."}],"review_version":2}