{"id":"2f338dd5-bb9c-4c90-af69-f13cc723237a","arxiv_id":"2506.18383","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"Fine-tuning open-source LLMs on a prover-filtered preference dataset improves whole-problem translation of natural-language reasoning into first-order logic, cutting syntax errors and increasing logical correctness.","lead":"The paper builds a 26,000-example dataset that pairs English reasoning problems with first-order logic translations, using an automated theorem prover to filter good examples, and then fine-tunes open-source LLMs with preference optimization. The best fine-tuned models produce fewer syntax errors and more label-correct logic translations than strong few-shot baselines, including GPT-4 in one comparison.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The Prover9 label-match criterion is used both to filter training data and to measure success, so the reported gains over GPT-4 may reflect fitting a weak proxy rather than better FOL translation.","rationale":"The paper has real value: it releases a 26k dataset, shows consistent syntax-error reduction, and includes honest manual analyses of semantic errors. However, the translation-quality claim rests on a proxy that is not validated against semantic equivalence, and the paper's own analyses show label-correct outputs that are not faithful translations (e.g., either-or mistakes). The LINC comparison mismatch is a secondary confound that also deserves attention. Because the authors acknowledge the limitation and provide code and data, the appropriate verdict remains CONDITIONAL: the central claim is plausible but not established. My read agrees with the reader's weakest assumption, so no verdict change is needed.","tokens_in":19598,"tokens_out":7101,"duration_ms":76399,"concrete_test":"Sample 100 FOLIO-validation outputs from Qwen-KTO (and, for control, from GPT-4-LINC raw outputs) whose Prover9 label matches gold. For each, have two independent annotators classify whether the generated FOL story is semantically equivalent to the gold FOL story (allowing paraphrastic predicates but requiring same entailment relations), and also run Mace4 to flag inconsistent or trivially weak premise sets. If the share of label-correct-but-not-semantically-equivalent outputs is material (e.g., >20%) or differs little between Qwen-KTO and GPT-4-LINC, then the headline 'logically correct' advantage is not evidence of better translation quality.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim depends on the Prover9 label-match metric of §4.1, but that metric is also the data-selection filter of §3.2. A generated FOL story is admitted to D_sft/D_pref as 'correct' if its Prover9 label matches the NL label; the same criterion defines 'logically correct' in Tables 3–4. The Limitations section concedes that a correct label does not guarantee a correct program. The risk is concrete rather than hypothetical: with 330 Uncertain labels in FOLIO, D_sft contains 8,792 Uncertain samples, so many candidates can match the label by omission or by Prover9 failing to prove or refute rather than by faithful translation. §5.1's manual analysis already finds either-or mistakes (6/48 for Phi-KTO, 5/35 for Phi-SFT) among label-correct outputs, and the back-translation similarity in Table 13 (~89%) has no gold-FOL baseline. An inconsistent or under-specified premise set can yield the target label without semantic equivalence. Thus the reported '6% more logically correct and 8% less syntax errors' over GPT-4-LINC is at best unverified as a statement about translation quality, and the upward trend across models could in part be optimization toward a criterion that is easier to satisfy than semantic equivalence. A secondary concern is that the paper explicitly deviates from LINC's k-majority voting (§4.1) while comparing against LINC's published numbers; the headline margin should be recomputed under a single protocol.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper introduces LOGICPO, a procedure for bootstrapping a supervised and preference-optimization dataset for whole-problem natural-language-to-first-order-logic (NL-to-FOL) translation. Starting from the FOLIO training split, the authors use several LLMs with varying numbers of in-context demonstrations and temperatures to generate candidate FOL stories, keep those whose Prover9-computed conclusion label matches the FOLIO label in D_sft (and as chosen examples in D_pref), and use label-mismatching or error-producing stories as rejected examples. They then fine-tune Llama-3-8B, Gemma-2-2B, Phi-3.5-Mini, and Qwen-2.5-14B with SFT followed by DPO or KTO, and evaluate on FOLIO validation, ProofWriter, PrOntoQA, and ProverQA. The reported results show large reductions in syntax errors and improvements in the Prover9 label-match rate relative to few-shot baselines and the LINC GPT-3.5/GPT-4 numbers, with the best full-text-abstract result attributed to Qwen-2.5-14B SFT+KTO (70.20% 'logically correct' on FOLIO vs. 64.01% for GPT-4-LINC). The paper also includes manual semantic-error analysis, context-length ablations, and back-translation-based semantic similarity checks.","tokens_in":19843,"tokens_out":6905,"duration_ms":64387,"significance":"If the central claim is taken at face value, the paper makes a useful practical contribution: it shows that a bootstrapped preference dataset, generated without human gold FOL annotation beyond FOLIO's existing labels, can be used to fine-tune open-weight models that produce syntactically executable FOL with label-match rates close to or above GPT-4-LINC on FOLIO, while generalizing to other reasoning benchmarks. The release of the 26k dataset and code, the breadth of base models, and the explicit error-category analysis (Tables 5 and 6) are genuine strengths. The significance is moderated, however, by the fact that the main evaluation metric is the same Prover9 label-match criterion used to filter the training data, and by the uncontrolled comparison with the LINC baselines. The paper's contribution is therefore better characterized as improving a specific proxy for translation quality rather than establishing semantic equivalence; whether the gains reflect genuine translation quality needs additional evidence.","major_comments":[{"comment":"The comparison with GPT-4-LINC is not controlled. The paper explicitly deviates from LINC's k-majority voting by averaging 10 per-story outcomes, but the GPT-4-LINC numbers are taken from Olausson et al. (2023), which use k-majority voting. These two aggregation schemes measure different quantities: a model that produces the correct label in 6 of 10 samples is counted as 60% under the paper's metric but as fully correct under LINC's voting, and the discrepancy can go in either direction. The headline '6% more logically correct and 8% less syntax errors' in the full-text abstract should be recomputed under a single protocol, either by applying the paper's per-sample averaging to GPT-4-LINC outputs (if the raw outputs are available) or by applying majority voting to the fine-tuned models. Without this, the comparison is not valid evidence for 'consistently outperforms GPT-4'.","section":"§4.1, Tables 3–4"},{"comment":"The Prover9 label-match criterion is used both to select the training examples that enter D_sft and D_pref and to define the primary 'Logically Correct' metric. A generated FOL story is treated as correct if its Prover9-computed label equals the NL label, but, as the Limitations section concedes, a correct label does not guarantee a correct program. The scale of this concern is concrete: D_sft contains 8,792 Uncertain samples (Table 2), and Uncertain can be obtained by omitting premises, by using inconsistent predicates that prevent Prover9 from proving or refuting, or by other failures of faithful translation. The manual analysis in §5.1 already finds either-or mistakes in label-correct outputs (6/48 for Phi-KTO and 5/35 for Phi-SFT). The back-translation evaluation in §B.3 compares generated-FOL paraphrases only for LLAMA3 and GPT3.5 and has no gold-FOL baseline, so it does not establish that the fine-tuned models are semantically closer to the reference FOL. The claim that the models produce 'logically correct' translations should be qualified as 'Prover9-label-correct' until an independent evaluation (e.g., human semantic-equivalence judgments or back-translation against gold FOL) is reported for all compared models.","section":"§3.2, §4.1, Table 2, §5.1, §B.3"},{"comment":"The reported numeric differences between methods are averages over 5–10 generations without variance or significance testing. For instance, the FOLIO gain of SFT+KTO over SFT for Phi-3.5 is 3.09 points (61.52 vs 58.43) and for Qwen-2.5 is 12.36 points (70.20 vs 57.84), but adjacent cells differ by as little as 0.49 points (e.g., Qwen SFT vs 2-shot on ProofWriter in Table 4). Without error bars or confidence intervals, a claim such as 'SFT + KTO always leads to improvement compared to SFT' is not supportable as a general statement. I recommend reporting standard deviations or confidence intervals, especially for the headline comparison against GPT-4-LINC.","section":"§4.3 and Tables 3, 4, 9, 10, 11"}],"minor_comments":[{"comment":"The abstract presented at the top of the paper names Phi-3.5 and GPT-3.5-turbo as the best model and baseline, while the full-text abstract and §4.3 attribute the best results to Qwen-2.5-14B against GPT-4-LINC. These should be reconciled, since the current text leaves the reader unsure which claim is being made.","section":"Abstract"},{"comment":"Please clarify whether the preferred samples in D_pref are a subset of D_sft, since the text says samples with matching labels are included in both sets. If so, state this explicitly, because the two-stage training then reuses the same preferred examples, which is a design choice worth reporting.","section":"§3.2, Table 2"},{"comment":"The manual semantic analysis is performed only on label-correct True examples from three models. It would be more informative to also include False and Uncertain labels, since the automated metric's main weakness is for Uncertain, as acknowledged in §5.2 S3.","section":"§5.1, Table 5"},{"comment":"There are numerous typos and grammatical issues, including 'it's role' in the abstract, 'utilzing', 'synactic', 'exectutability', and 'recieve' in the appendix prompts. A careful proofreading pass is needed.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The paper reports a substantial empirical effort, but the central comparison with GPT-4-LINC is not controlled and the main metric is also the training-signal filter. I believe these are fixable with additional experiments, so I recommend major revision rather than rejection. I would also encourage the editor to ask the authors to reconcile the two different abstract claims before resubmission."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a real step forward for NL-to-FOL translation as a neurosymbolic bottleneck, but the headline margin over GPT-4-LINC is not yet established. The dataset and the SFT+preference-optimization recipe are the contribution; the claimed 6%/8% advantage is a hypothesis until the authors rerun the comparison under a single evaluation protocol.\n\nWhat's actually new: first use of DPO/KTO on whole-problem NL-to-FOL translation, backed by a 26k bootstrapped dataset from FOLIO, with code and data released. The pattern across four base models (Llama-3, Gemma-2, Phi-3.5, Qwen-2.5) is consistent: SFT plus KTO reduces syntax errors and raises Prover9 label-match rates on FOLIO, ProofWriter, ProntoQA, and even ProverQA, which was created through a different pipeline. That generalization is a point in the paper's favor. The manual semantic analysis (Table 5) and the qualitative error categorization are honest, including the either-or mistakes that produce correct labels for wrong reasons.\n\nThe soft spots are real but not fatal to the whole paper. The biggest is the label-match proxy: it's used both to filter Dsft/Dpref and to compute the main metric. A generated FOL can match the NL label without being semantically equivalent; the paper says so. With 8,792 Uncertain samples in Dsft, many candidates can match by making the conclusion unprovable. That doesn't invalidate the approach, but it means the reported gains over GPT-4 are at least partly fitting the filter. The comparison to LINC compounds it: the paper averages per-sample label matches over 10 outputs, while LINC's published numbers use k-majority voting. You can't claim a margin over a number produced by a different protocol. Also, the abstract contains two different central results (Phi-3.5 vs GPT-3.5 in one line, Qwen-2.5 vs GPT-4 in another), which suggests the headline was edited late. Minor but worth fixing: no training hyperparameters, no error bars, and the back-translation similarity has no gold-FOL baseline.\n\nWho's this for: anyone working on neurosymbolic pipelines or semantic parsing. The dataset is a real asset, and the paper's discussion of what remains hard (uncertain labels, either-or, predicate consistency) is useful. I'd bring it to a reading group and would cite the dataset, though with a hedge.\n\nRecommendation: send it out. The methodology deserves referee time; the GPT-4 comparison and the metric hygiene need to be cleaned up before the claims are taken at face value.","headline":"A useful dataset and preference-optimization recipe for whole-problem NL-to-FOL translation, but the GPT-4 comparison is not controlled and the label-match metric is partly self-referential.","tokens_in":20418,"tokens_out":2449,"would_cite":true,"duration_ms":22640,"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":"Fine-tuning open LLMs on a bootstrapped preference dataset turns them into first-order logic translators that beat GPT-4 on logical correctness and syntax errors.","keywords":["NL-to-FOL translation","preference optimization","DPO","KTO","logical reasoning","neurosymbolic","Prover9","LLM fine-tuning"],"falsifier":"A human-annotation study on a random sample of FOLIO validation outputs would settle it: if the translations judged 'logically correct' by label agreement are found to be semantically wrong (e.g., wrong predicates, missing quantifiers) in a large fraction of cases, and the LOGICPO-trained models show no better semantic fidelity than the baselines, then the reported gains are an artifact of the metric rather than real translation quality. Concretely, the manual analysis in §5.1 already suggests 'either-or' sentences are a known failure point; a larger annotated set that counts such semantic errors across all label-correct outputs would test the proxy directly.","tokens_in":19349,"feed_emoji":"🤖","tokens_out":7581,"duration_ms":62729,"temperature":0.7,"pith_summary":"The paper aims to make open-source large language models reliable translators of natural-language reasoning problems into first-order logic (FOL), so that neurosymbolic pipelines can offload the translation step to a cheap fine-tuned model instead of an expensive few-shot API. To do this, the authors bootstrap a 26k-example dataset, LOGICPO, from the expert-written FOLIO seed set: they generate many candidate FOL renderings of each story, keep those whose Prover9-computed logical conclusion matches the story's ground-truth label as positive examples, and use the mismatched ones as negative examples. They then fine-tune several open LLMs with supervised learning followed by direct preference optimization (DPO) or Kahneman-Tversky optimization (KTO). Their central finding is that this recipe produces translators that are both more logically correct and far less prone to syntax errors than sentence-wise baselines and GPT-3.5, with the best Qwen-2.5-14B model outperforming GPT-4's 8-shot results by 6% in logical correctness while making 8% fewer syntax errors on the FOLIO validation set.","feed_headline":"Finetuned open LLMs beat GPT-4 on logic-to-FOL","feed_subtitle":"A bootstrapped preference dataset plus DPO/KTO turns 14B open models into consistent FOL translators.","key_machinery":"The central machinery is the LOGICPO bootstrapping pipeline: candidate whole-problem FOL stories are generated by LLMs, filtered by label agreement with Prover9 to form a supervised set (D_sft) and a preference set (D_pref) of chosen/rejected pairs, and then a two-stage fine-tune applies SFT followed by DPO or KTO. What it does is teach the model not just what a correct translation looks like but what a near-miss incorrect translation looks like, and the whole-problem framing enforces predicate-level consistency across sentences, which sentence-wise parsers miss.","core_discovery":"The central claim is that the main bottleneck in neurosymbolic reasoning — converting a natural-language problem into a consistent first-order logic program — can be dramatically improved by training open-source LLMs on a preference dataset constructed from whole-problem translations rather than sentence-by-sentence parses. Starting from FOLIO's expert-written stories and labels, the authors use several LLMs to generate multiple FOL versions of each story, then accept a version as a 'chosen' example if its Prover9-evaluated conclusion label matches the ground truth, and as a 'rejected' example otherwise. Supervised fine-tuning on the accepted set followed by DPO or KTO on the chosen/rejected pairs yields models that produce internally consistent predicate use, far fewer syntax errors, and better logical accuracy than the sentence-wise LogicLLaMA baseline and GPT-3.5 few-shot variants. The strongest model, Qwen-2.5-14B fine-tuned with KTO, reaches 70.20% logical correctness and 4.56% syntax errors on FOLIO validation, surpassing GPT-4's 8-shot LINC results (64.01% correctness, 12.91% syntax errors); the same training transfers to ProofWriter, PrOntoQA, and ProverQA, where the models also outperform or match the baselines.","pith_inferences":["The label-matching filter may make the dataset self-reinforcing: examples that Prover9 can already decide are over-represented, so the reported gains could partly reflect training toward easy-to-prove fragments rather than general FOL competence; a distribution analysis of which stories survive the filter would test this.","Because the evaluation metric is the same Prover9 label match used to build the data, there is a risk of circularity: the models could be learning to satisfy the label criterion rather than to translate faithfully; an independent semantic metric (e.g., back-translation similarity or human-rated equivalence) on held-out data would separate the two.","The same recipe could be applied to other formal targets, but the authors only demonstrate English-to-FOL; the method's generality could be tested by porting the pipeline to, say, Python or SQL, where the label-matching oracle would be a different execution engine.","The paper does not report inference cost per problem; a practical extension would measure tokens and wall-clock time for the tuned models versus GPT-4 few-shot to quantify the 'efficient' claim in real deployment terms."],"forward_implications":["Neurosymbolic pipelines can replace expensive GPT-4 few-shot translation with a fine-tuned 14B open model that is both more accurate and cheaper per call, lowering the cost of end-to-end logical reasoning systems.","The bootstrapping recipe (generate, filter by solver label, build chosen/rejected pairs, apply SFT plus preference optimization) transfers across datasets and is a template for other low-resource formal languages such as SAT, SMT, or proof assistants.","KTO consistently improves over SFT alone across model families, whereas DPO does not; this suggests the preference signal from 'rejected' samples is valuable and that KTO's non-paired objective fits this data distribution better.","Whole-problem translation fixes predicate-level inconsistencies that sentence-wise parsers exhibit, because the model is trained on full stories rather than isolated sentences."],"supporting_citations":[{"why":"Supplies Prover9, the theorem prover that both filters training examples by label match and computes the reported logical-correctness and syntax-error metrics.","marker":"McCune, 2005–2010"},{"why":"Provides the FOLIO seed dataset of expert-written NL stories and ground-truth labels from which all LOGICPO training and validation examples are derived.","marker":"Han et al., 2024b"},{"why":"Defines the LINC baselines (GPT-3.5/GPT-4 few-shot) and the evaluation protocol the paper compares against.","marker":"Olausson et al., 2023"},{"why":"Introduces Direct Preference Optimization, one of the two preference methods applied after SFT.","marker":"Rafailov et al., 2024"},{"why":"Introduces Kahneman-Tversky Optimization, the preference method that consistently improves over SFT in the paper's experiments.","marker":"Ethayarajh et al., 2024"},{"why":"Presents LogicLLaMA, the sentence-wise NL-to-FOL baseline that the whole-problem approach claims to surpass.","marker":"Yang et al., 2024"},{"why":"Supplies the ProofWriter dataset used to test out-of-distribution generalization of the trained translators.","marker":"Tafjord et al., 2021"},{"why":"Supplies the PrOntoQA dataset used as a second out-of-distribution evaluation benchmark.","marker":"Saparov & He, 2023"}],"fun_headline_variants":["Open LLMs beat GPT-4 at logic translation via DPO","Preference-optimized LLMs turn NL to FOL better than GPT-4","LogicPO: DPO/KTO makes open LLMs logic-to-FOL champions","Whole-problem training lifts FOL translation past GPT-4"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole approach rests on the assumption that matching the final logical label with Prover9 is a reliable sign of a good translation, so that label matches can be used both to pick training examples and to measure success.","fun_headline_variants_meta":{"raw":{"variants":["Open LLMs beat GPT-4 at logic translation via DPO","Preference-optimized LLMs turn NL to FOL better than GPT-4","LogicPO: DPO/KTO makes open LLMs logic-to-FOL champions","Whole-problem training lifts FOL translation past GPT-4"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000187,"raw_usage":{"total_tokens":1366,"prompt_tokens":1017,"completion_tokens":349,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":633,"completion_tokens_details":{"reasoning_tokens":268}},"tokens_in":633,"tokens_out":349,"duration_ms":3826,"temperature":1.0,"reasoning_tokens":268,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T18:49:55.903294+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A human-annotation study on a random sample of FOLIO validation outputs would settle it: if the translations judged 'logically correct' by label agreement are found to be semantically wrong (e.g., wrong predicates, missing quantifiers) in a large fraction of cases, and the LOGICPO-trained models show no better semantic fidelity than the baselines, then the reported gains are an artifact of the metric rather than real translation quality. Concretely, the manual analysis in §5.1 already suggests 'either-or' sentences are a known failure point; a larger annotated set that counts such semantic errors across all label-correct outputs would test the proxy directly.","supporting_citations":[],"review_version":1}