Pith. sign in

REVIEW 3 major objections 4 minor 53 references

Do Large Language Models Excel in Complex Logical Reasoning with Formal Language?

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Most current LLMs reason less accurately when asked to answer in formal code than in plain text, and only a 'thinking' model keeps high performance across Python, Z3, and CSP formats.

desk verdict A broad, reusable evaluation map of 31 models across 66 tasks and four trajectory formats, but the headline numbers rest on an unvalidated LLM judge and would need that fixed before I'd trust the ranking. read the letter →

arxiv 2505.16998 v1 pith:7R3OKJUT submitted 2025-05-22 cs.CL cs.AI

Jin Jiang , Jianing Wang , Yuchen Yan , Yang Liu , Jianhua Zhu , Mengdi Zhang , Xunliang Cai , Liangcai Gao This is my paper · ORCID
classification cs.CLcs.AI
keywords formallanguagereasoningprogram-of-thoughtZ3solverconstraintsatisfactionproblemslogicalevaluationthinkingmodelsrejectedfine-tuningLLM
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper asks whether current large language models actually reason better when prompted to write formal code—Python, Z3, or constraint-satisfaction programs—instead of answering in natural language. Across 66 logical-reasoning tasks spanning deductive, inductive, abductive, and mixed-form reasoning, the authors find that for most models the answer is no: accuracy falls as the trajectory format moves from text to formal languages, and execution rates collapse on the hardest tasks. The exception is a class of long-reasoning 'thinking' models, one of which keeps high and stable accuracy in all four formats. The paper also shows that rejected fine-tuning on filtered, executable, correct formal trajectories raises a 7B model's average accuracy from 34.0 to 42.0 and its execution rate from 65.3 to 76.0, narrowing the gap with much larger models. If the findings hold, formalization is not a free reliability boost for most LLMs; it helps only when the model already reasons strongly, and formal-language training data is a practical lever for smaller models.

What carries the argument

The central mechanism is the trajectory format, formalized as LLM(Q) = <s1, s2, ..., sn> --Exec--> A: the model emits a sequence of steps in one of four languages (free text, executable Python, Z3 solver code, or python-constraint CSP code), an external engine executes the trajectory to produce answer A, and an LLM judge compares A with a reference answer. The evaluation manipulates this mechanism along three axes—model family (Instruct versus Thinking, 7B to 72B), reasoning-type taxonomy (deductive, inductive, abductive, mixed-form), and trajectory format—using zero-shot prompts with a three-step self-refinement pass for formal languages. The same trajectory machinery drives the training intervention: rejected fine-tuning samples GPT-4o trajectories, keeps only those that execute and match the reference answer, and mixes them with general-domain data to fine-tune a 7B base model.

What would settle it

Take a random sample of model completions in Z3 and CSP formats, have human logicians score them against ground truth, and compare those scores with Qwen-2.5-72B-Instruct's rubric judgments; if agreement on formal trajectories is near chance, the paper's central findings would collapse. A simpler check is to count how often the judge marks a completion wrong when the executed output is semantically correct but not string-identical to the reference.

Watch

Extended reading notes

Core claim

The central claim is that current mainstream LLMs are more adept at natural-language reasoning than at formal-language reasoning: across a 66-task suite, most models' accuracy declines as trajectories move from Text to Python (PoT) to Z3 to CSP, and the drop is steepest on difficult tasks such as the bbeh series. Thinking models significantly outperform Instruct models, especially when formal language is employed, but the advantage does not hold at small parameter scale, where a distilled 7B thinking model performs worse on CSP than comparable Instruct models. The only evaluated model that stays ahead in all tasks and all four trajectory formats is QwQ-32B. A generalization analysis finds that PoT data transfers best to other formats, that Z3 and CSP transfer well across reasoning types, and that CSP is hard to generalize from but easy to generalize to; the authors attribute formal-language failures to a lack of pertinent training knowledge. Finally, a rejected fine-tuning method using GPT-4o-sampled, execution-verified trajectories improves Qwen2.5-7B's average accuracy from 34.0% to 42.0% and its execution rate from 65.3% to 76.0%.

Load-bearing premise

Every headline accuracy number is produced by one automatic judge, Qwen-2.5-72B-Instruct, comparing each model's completion against a reference answer; if that judge systematically marks correct but differently expressed answers as wrong, especially for formal trajectories, the formal-language deficit and the training gains would not be supported.

Editorial extensions

If this is right

  • If the central claim is correct, prompting current Instruct models to solve logic problems by writing Python, Z3, or CSP code will not reliably improve accuracy and will often lower it, especially on hard inductive and mixed-form tasks.
  • Thinking models are the category most able to exploit formal language, but this only holds at sufficient parameter scale; small distilled thinking models lose their advantage in CSP and Z3.
  • Formalization does not cure inductive reasoning: every evaluated model shows limited inductive capability in all four trajectory formats.
  • Program-of-thought data is the best cross-format training signal, transferring positively to Text, Z3, and CSP, while CSP data transfers negatively to PoT and Z3.
  • Rejected fine-tuning with filtered formal trajectories is a cheap way to improve small models, raising a 7B model's average accuracy by 8 points and its execution rate by about 11 points.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Because the paper uses zero-shot prompts only, a natural extension is to test whether few-shot formalization or chain-of-thought-then-code pipelines reverse the formal-language deficit; the current result suggests the deficit is in the model's formal knowledge, not the prompt format.
  • The CSP asymmetry—hard to transfer from, easy to transfer to—suggests CSP is a distinct representational skill that is readily teachable once basic reasoning exists; a testable extension is to measure whether small amounts of CSP data improve downstream formal-language performance more than equal amounts of PoT data.
  • The excluded formal systems (Lean, Prolog, Coq, SMT-LIB) may behave differently from Python, Z3, and CSP because they require proof construction rather than answer search; the paper's transfer findings do not automatically extend to them.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The manuscript presents FormalEval, a three-axis evaluation of LLMs on 66 logical reasoning tasks using Text, PoT, Z3, and CSP trajectory formats. Part I evaluates 10 models spanning Instruct and Thinking series and claims that Thinking models significantly outperform Instruct models, especially under formal language, that all models are weak in inductive reasoning, and that Text generally outperforms formal languages except for QwQ-32B. Part II studies transfer across reasoning types and trajectory formats, concluding that PoT transfers well while CSP transfers poorly. Part III applies rejection-sampling fine-tuning (RFT) to Qwen2.5-7B with formal-relative training data, reporting average accuracy gains of about +8 points and a +17-point CSP gain. The paper includes per-task result tables, case studies, and a public code/data link.

Significance. If the measurement methodology is sound, the paper provides a useful large-scale evaluation resource and several falsifiable findings about formal-language reasoning, and its RFT recipe is a practical contribution for small models. The paper ships detailed per-task tables and a public repository, which is commendable. However, the central claims rest on a single unvalidated LLM judge, so the ordinal comparisons and the RFT gains are not yet established. The contribution is primarily empirical, and its value depends entirely on measurement validity.

major comments (3)
  1. [Appendix D.1 (Figure 14); Tables 4-6] Every accuracy number in the paper, including the headline Thinking-vs-Instruct gap and the Part III RFT gains, is produced by asking Qwen-2.5-72B-Instruct to compare a model completion with a reference answer using the rubric in Figure 14. The paper reports no human agreement, no judge calibration on known-correct or known-wrong outputs, and no error analysis on formal trajectories. This matters especially for formal formats because execution rates are far below 100% on many tasks: for example, Table 6 shows Qwen2.5-7B gsm8k PoT Exec Rate 21.3 and bbeh_temporal_sequence PoT Exec Rate 0.0, and Table 5 shows GPT-4o bbeh_zebra_puzzles Z3 Exec Rate 49.0. On such items the judge is not grading an executed result; it is grading unexecuted code plus whatever textual explanation the model emitted. If the judge systematically rewards verbose reasoning traces or penalizes terse code, the abstract's first finding and the reported +17.0 CSP gain would be artifacts. This concern must be addressed by reporting judge agreement against human labels or deterministic answer matching, separately per format and per model family, and by re-checking whether the ordinal claims survive that validation.
  2. [Section 3.1; Abstract] The claim that Thinking models 'significantly outperform' Instruct models is a categorical statistical statement, but the paper reports only point estimates with no confidence intervals, significance tests, or effect-size measures. For instance, Tables 4 and 5 allow per-format averages to be compared, but there is no uncertainty quantification around any of the averages or per-task differences, and the phrase 'significantly' is used without a defined test. Given that the comparisons are made on fixed benchmark subsets and the judge itself is stochastic, the authors should report bootstrap confidence intervals or paired significance tests across the 66 tasks (or justify deterministic evaluation). Without this, the headline finding is not quantitatively supported as stated.
  3. [Section 4.1; Table 3] The Introduction states that training data for the generalization experiments has 'the same scale size' to make a fair comparison, but Table 3 shows that the fine-grained training groups range from 1042 samples (Inductive_CSP) to 1820 samples (Abductive_Text), a difference of about 75%, and the coarse-grained groups range from 6346 to 7448 samples. These size differences can confound the cross-format and cross-reasoning-type transfer comparisons in Figures 4 and 5. The authors should either match training set sizes exactly or control for data quantity through ablations before claiming that one format transfers better than another.
minor comments (4)
  1. [Section 3.1] There is a typo in the phrase 'Deducitve-BBH_web'; it should be 'Deductive-BBH_web'.
  2. [Section 2.2 / Appendix D.1] Part I mentions a three-step self-refinement process for formal-language trajectories, but the prompts in Figures 11-13 do not describe this refinement, and Appendix D.1 does not specify how refinement is implemented or how many attempts are made. Please clarify the self-refinement protocol for reproducibility.
  3. [Table 2] The MATH row shows '5000 *7500' across the Eval and Train columns, which is ambiguous; please clarify the meaning of the asterisk and how the subset was sampled to balance the dataset.
  4. [Section 5.1] The phrase 'we collect the portions of current evaluation datasets that overlap with training data' is ambiguous and could be read as suggesting that evaluation benchmarks were used in training; please specify the official train/test splits used, and describe how data leakage was avoided for all 66 tasks.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: headline findings are empirical measurements on external benchmarks and do not reduce to fitted inputs, self-citations, or definitions.

full rationale

I walked the paper's claimed derivation chain. The central claims are empirical evaluations: trajectory formats are defined by execution semantics (Section 2.2), and the headline findings in Section 3.1 ('Thinking models significantly outperform Instruct models, especially when formal language is employed') are summaries of accuracy measurements across 31 models and 66 task subsets against external benchmark references. No parameter is fitted to produce a headline result, and no equation equates a prediction to its input by construction. The generalization analysis in Part II trains on the training splits of the collected datasets and evaluates on separate evaluation splits; gains are reported as deltas over a baseline, so the measured transfer effects are not forced by data overlap. Part III's RFT experiment filters teacher samples by executability and reference correctness, then evaluates on evaluation tasks; the reported improvements are external measurements rather than renamed fit values. Citations to prior work (e.g., Xu et al. 2025, Pan et al. 2023) are to independent groups and are not load-bearing self-citations. The main methodological concern is that all accuracy numbers come from a single unvalidated LLM judge, Qwen-2.5-72B-Instruct (Appendix D.1, Figure 14). That is a measurement-validity and soundness concern, not a circularity concern, because the judge is not a parameter fitted to the paper's conclusions and the claims do not reduce to the judge's own outputs. The Limitations section openly discusses coverage and model-currency limitations but does not reveal any circular step. Therefore the appropriate circularity score is 0.

Assumptions & free parameters 4 free parameters · 4 assumptions · 0 invented entities

The paper is an empirical benchmark study, so it has no fitted theoretical constants. The hand-chosen experimental settings listed below are load-bearing for the reported gains and rankings. The axioms capture the unvalidated classification and measurement assumptions on which every conclusion depends.

free parameters (4)
  • Self-refinement steps for formal-language trajectories = 3
    Section 3 states 'we apply a three-step self-refinement process during code execution'; number of refinement rounds is hand-chosen and directly affects formal-format accuracies.
  • Per-dataset training sample cap for RFT = 3000
    Section 5.1 caps extracted training samples at 3,000 per dataset; this changes the composition of the 28,060-sample formal training set and therefore the reported gains.
  • SFT training epochs = 3
    Appendix D.2 sets epochs=3 with LR 1e-5; results in Part II and III depend on this choice.
  • Maximum generation length = 16384
    Appendix D.1 sets max generation length to 16K tokens; for long formal trajectories this truncation could depress accuracy.
assumptions (4)
  • domain assumption The 66 tasks are correctly partitioned into deductive, inductive, abductive, and mixed-form reasoning categories.
    Section 2.1 and Table 2 assign each dataset to a reasoning type without inter-annotator validation; per-type findings depend on this mapping.
  • domain assumption Qwen-2.5-72B-Instruct's judge prompt (Appendix D.1) produces correct correctness labels for every format and task.
    No judge accuracy or human agreement is reported; all accuracy scores in Tables 1, 4-7 rest on this assumption.
  • standard math Python 3.12, the Z3 solver, and python-constraint faithfully execute the generated trajectories and produce the intended answer.
    Section 2.2 and Appendix C assume the executors are sound; this is a standard property of these tools but is not verified for the generated code.
  • ad hoc to paper The taxonomy in Section 2.1 (premise to conclusion for deduction, etc.) is a valid operationalization of logical reasoning types for NLP benchmarks.
    This is the paper's own categorization framework, inspired by Xu et al. 2025, and is not independently validated.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Do Large Language Models Excel in Complex Logical Reasoning with Formal Language?." pith.science (2026). https://pith.science/paper/7R3OKJUT

@misc{pith2026250516998,
  author       = {Pith},
  title        = {Pith review of: Do Large Language Models Excel in Complex Logical Reasoning with Formal Language?},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7R3OKJUT}},
  note         = {Machine review of arXiv:2505.16998}
}
read the original abstract

Large Language Models (LLMs) have been shown to achieve breakthrough performance on complex logical reasoning tasks. Nevertheless, most existing research focuses on employing formal language to guide LLMs to derive reliable reasoning paths, while systematic evaluations of these capabilities are still limited. In this paper, we aim to conduct a comprehensive evaluation of LLMs across various logical reasoning problems utilizing formal languages. From the perspective of three dimensions, i.e., spectrum of LLMs, taxonomy of tasks, and format of trajectories, our key findings are: 1) Thinking models significantly outperform Instruct models, especially when formal language is employed; 2) All LLMs exhibit limitations in inductive reasoning capability, irrespective of whether they use a formal language; 3) Data with PoT format achieves the best generalization performance across other languages. Additionally, we also curate the formal-relative training data to further enhance the small language models, and the experimental results indicate that a simple rejected fine-tuning method can better enable LLMs to generalize across formal languages and achieve the best overall performance. Our codes and reports are available at https://github.com/jiangjin1999/FormalEval.

Figures

Figures reproduced from arXiv: 2505.16998 by the authors.

Figure 1
Figure 1. Evaluation framework with three specific di [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Radar plots illustrating the performance (%) of multiple LLMs across different reasoning task types [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Preferred reasoning task performance across different trajectory formats ( [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (10 more)
Figure 4
Figure 4. Figure 4: Generalization performance across fine-grained (task type × format) configurations. Each cell shows the performance gain (∆) from training on the row configuration and evaluating on the column configuration Text PoT Z3 CSP Evaluation Dimension Text PoT Z3 CSP Training …
Figure 5
Figure 5. Figure 5: Generalization performance across reasoning [PITH_FULL_IMAGE:figures/full_fig_p007_5.png]
Figure 6
Figure 6. Figure 6: Case for Text. 3.2. These issues are closely related to semantic understanding. They are better suited for textual representation and are difficult to address using formalized languages. Return to section 3.2. Case Study for PoT (BBH_dyck_language) Complete the rest of…
Figure 7
Figure 7. Figure 7: Case for PoT. Symbolic reasoning tasks are inherently well-suited to programming languages, and such [PITH_FULL_IMAGE:figures/full_fig_p017_7.png]
Figure 8
Figure 8. Figure 8: Case for Z3. Z3 (which, in this context, incorporates the first-order logic reasoning capabilities of Prover9) [PITH_FULL_IMAGE:figures/full_fig_p018_8.png]
Figure 9
Figure 9. Figure 9: Case for CSP. The problems in ARLSAT involve numerous conditional constraints, which closely resemble [PITH_FULL_IMAGE:figures/full_fig_p019_9.png]
Figure 10
Figure 10. Figure 10: Case Study for Few-Shot Formal-Eval in Logic-LM—>Our Zero-Shot Evaluation (AR-LSAT). Logic-LM [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Prompt for PoT Prompt for Z3 {question} Let's write code in Python that utilizes z3- solver to solve the problem. Requires code to start with: ``from z3 import *''. Please give the python code in the following format: ```python ``` and print the final result.", [PITH…
Figure 12
Figure 12. Figure 12: Prompt for Z3 Prompt for CSP {question} Let's write code in Python that utilizes python-constraint to solve the question. The task is to parse the problem as a constraint satisfaction problem , defining the domain , variables , and contraints. Requires code to start w…
Figure 13
Figure 13. Figure 13: Prompt for CSP Prompt for Model Evaluation [Instruction] Please act as an impartial judge and evaluate the quality of the response provided by an AI assistant to the user question displayed below. Your evaluation should consider the correctness. You will be given a re…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

53 extracted references · 34 canonical work pages

  1. [1]

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, and 1 others. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774

    arXiv 2023

  2. [2]

    Jinze Bai, Shuai Bai, Yunfei Chu, Zeyu Cui, Kai Dang, Xiaodong Deng, Yang Fan, Wenbin Ge, Yu Han, Fei Huang, and 1 others. 2023. Qwen technical report. arXiv preprint arXiv:2309.16609

    arXiv 2023

  3. [3]

    Rama Krishna Sai Bhagavatula, Ronan Le Bras, Chaitanya Malaviya, Yejin Choi, and Noah A Smith. 2020. Abductionrules: Training transformers to explain unexpected inputs. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 4246--4258

    work page 2020

  4. [4]

    Xiao Bi, Deli Chen, Guanting Chen, Shanhuang Chen, Damai Dai, Chengqi Deng, Honghui Ding, Kai Dong, Qiushi Du, Zhe Fu, and 1 others. 2024. Deepseek llm: Scaling open-source language models with longtermism. arXiv preprint arXiv:2401.02954

    arXiv 2024

  5. [5]

    Nikolaj Bj rner, Anh-Dung Phan, and Lars Fleckenstein. 2015. z-an optimizing smt solver. In Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21, pages 194--19...

    work page 2015

  6. [6]

    Andrei Bulatov, Peter Jeavons, and Andrei Krokhin. 2005. Classifying the complexity of constraints using finite algebras. SIAM journal on computing, 34(3):720--742

    work page 2005

  7. [7]

    Benjamin Callewaert, Simon Vandevelde, and Joost Vennekens. 2025. Verus-lm: a versatile framework for combining llms with symbolic reasoning. arXiv preprint arXiv:2501.14540

    arXiv 2025

  8. [8]

    Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, and 1 others. 2021. Training verifiers to solve math word problems. In null

    work page 2021

Show all 53 references
  1. [9]

    Denise D Cummins, Todd Lubart, Olaf Alksnis, and Robert Rist. 1991. Conditional reasoning and causation. Memory & cognition, 19:274--282

    1991

  2. [10]

    Peter A Flach and Antonis C Kakas. 2000. Abduction and Induction: Essays on their relation and integration, volume 18. Springer Science & Business Media

    2000

  3. [11]

    Robert Friedman. 2023. Large language models and logical reasoning. Encyclopedia, 3(2):687--697

    2023

  4. [12]

    Luyu Gao, Aman Madaan, Shuyan Zhou, Uri Alon, Pengfei Liu, Yiming Yang, Jamie Callan, and Graham Neubig. 2023. Pal: Program-aided language models. In International Conference on Machine Learning, pages 10764--10799. PMLR

    2023

  5. [13]

    Vinod Goel. 2007. Anatomy of deductive reasoning. Trends in cognitive sciences, 11(10):435--441

    2007

  6. [14]

    Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Alex Vaughan, and 1 others. 2024. The llama 3 herd of models. arXiv e-prints, pages arXiv--2407

    2024

  7. [15]

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, and 1 others. 2025. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948

    2025 arXiv

  8. [16]

    Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, and 1 others. 2024. Folio: Natural language reasoning with first-order logic. In Proceedings of the 2024 Conference on Empirical Methods in Na...

    2024

  9. [17]

    Joy He-Yueya, Gabriel Poesia, Rose Wang, and Noah Goodman. 2023. Solving math word problems by combining language models with symbolic solvers. In The 3rd Workshop on Mathematical Reasoning and AI at NeurIPS'23

    2023

  10. [18]

    Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the math dataset. Sort, 2(4):0--6

    2021

  11. [19]

    Philip N Johnson-Laird. 1999. Deductive reasoning. Annual review of psychology, 50(1):109--135

    1999

  12. [20]

    Mehran Kazemi, Bahare Fatemi, Hritik Bansal, John Palowitch, Chrysovalantis Anastasiou, Sanket Vaibhav Mehta, Lalit K Jain, Virginia Aglietti, Disha Jindal, Peter Chen, and 1 others. 2025. Big-bench extra hard. arXiv preprint arXiv:2502.19187

    2025 arXiv

  13. [21]

    Mehran Kazemi, Quan Yuan, Deepti Bhatia, Najoung Kim, Xin Xu, Vaiva Imbrasaite, and Deepak Ramachandran. 2023. Boardgameqa: A dataset for natural language reasoning with contradictory information. Advances in Neural Information Processing Systems, 36:39052--39074

    2023

  14. [22]

    Gonzalez, Hao Zhang, and Ion Stoica

    Woosuk Kwon, Zhuohan Li, Siyuan Zhuang, Ying Sheng, Lianmin Zheng, Cody Hao Yu, Joseph E. Gonzalez, Hao Zhang, and Ion Stoica. 2023. Efficient memory management for large language model serving with pagedattention. In Proceedings of the ACM SIGOPS 29th Symposium on Operating S...

    2023

  15. [23]

    Fangyu Lei, Qian Liu, Yiming Huang, Shizhu He, Jun Zhao, and Kang Liu. 2024. S3eval: A synthetic, scalable, systematic evaluation suite for large language model. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistic...

    2024

  16. [24]

    Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. 2021. Logiqa: a challenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial I...

    2021

  17. [25]

    Qiyuan Liu, Ming Yan, Yiyang Liu, Pan Lu, Siwei Wang, and Songfang Huang. 2020. Logiqa: A challenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 1866--1877

    2020

  18. [26]

    Qing Lyu, Shreya Havaldar, Adam Stein, Li Zhang, Delip Rao, Eric Wong, Marianna Apidianaki, and Chris Callison-Burch. 2023. Faithful chain-of-thought reasoning. In The 13th International Joint Conference on Natural Language Processing and the 3rd Conference of the Asia-Pacific...

    2023

  19. [27]

    Theo X Olausson, Alex Gu, Benjamin Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger Levy. 2023. Linc: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference o...

    2023

  20. [28]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. 2023. Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806--3824

    2023

  21. [29]

    Gaurav Parmar, Shikhar Murari, and Mohit Bansal. 2023. Logicbench: A challenging benchmark for logical reasoning with large language models. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 148--168

    2023

  22. [30]

    S RANISE. 2003. The smt-lib format: An initial proposal. 1st PDPAR, 2003

    2003

  23. [31]

    Abulhair Saparov and He He. 2023. Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. In The Eleventh International Conference on Learning Representations

    2023

  24. [32]

    Koustuv Sinha, Shagun Sodhani, Jin Dong, Joelle Pineau, and William L Hamilton. 2019. Clutrr: A diagnostic benchmark for inductive reasoning from text. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Con...

    2019

  25. [33]

    Mirac Suzgun, Nathan Scales, Nathanael Scharli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Michael Petrov, Vincent Y Zhao, Ryan Murphy, Adam Roberts, and 1 others. 2022. Challenging big-bench tasks and whether chain-of-thought can solve them. arXiv preprint arXiv:2210.09261

    2022 arXiv

  26. [34]

    Fumiya Uchiyama, Takeshi Kojima, Andrew Gambardella, Qi Cao, Yusuke Iwasawa, and Yutaka Matsuo. 2023. Which programming language and what features at pre-training stage affect downstream logical inference performance? Findings of the Association for Computational Linguistics: ...

    2023

  27. [35]

    Marco Valentino, Mokanarangan Thayaparan, and Andr \'e Freitas. 2022. Case-based abductive natural language inference. In Proceedings of the 29th International Conference on Computational Linguistics, pages 1556--1568

    2022

  28. [36]

    Xinyi Wang, Liangming Pan, and William Yang Wang. 2024. Logic-lm++: Multi-step refinement for symbolic formulations. In The Twelfth International Conference on Learning Representations

    2024

  29. [37]

    Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Fei Xia, Ed Chi, Quoc V Le, Denny Zhou, and 1 others. 2022. Chain-of-thought prompting elicits reasoning in large language models. Advances in neural information processing systems, 35:24824--24837

    2022

  30. [38]

    Jason Weston, Antoine Bordes, Sumit Chopra, Tomas Mikolov, and Alexander Rush. 2015. Towards ai-complete question answering: A set of prerequisite toy tasks. In null

    2015

  31. [39]

    Jason Weston, Antoine Bordes, Sumit Chopra, Alexander M Rush, Bart Van Merri \"e nboer, Armand Joulin, and Tomas Mikolov. 2016. Towards ai-complete question answering: A set of prerequisite toy tasks. In 4th International Conference on Learning Representations, ICLR 2016

    2016

  32. [40]

    Yuan Xia, Akanksha Atrey, Fadoua Khmaissia, and Kedar S Namjoshi. 2025. Can large language models learn formal logic? a data-driven training and evaluation framework. arXiv preprint arXiv:2504.20213

    2025 arXiv

  33. [41]

    Siheng Xiong, Yuan Yang, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2024. Strategies for improving nl-to-fol translation with llms: Data generation, incremental fine-tuning, and verification. arXiv preprint arXiv:2409.16461

    2024 arXiv

  34. [42]

    Fangzhi Xu, Qika Lin, Jiawei Han, Tianzhe Zhao, Jun Liu, and Erik Cambria. 2025. Are large language models really good logical reasoners? a comprehensive evaluation and beyond. IEEE Transactions on Knowledge & Data Engineering, pages 1--15

    2025

  35. [43]

    Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2023 a . Harnessing the power of large language models for natural language to first-order logic translation. arXiv preprint arXiv:2305.15541

    2023 arXiv

  36. [44]

    Zonglin Yang, Xinya Du, Rui Mao, Jinjie Ni, and Erik Cambria. 2023 b . Logical reasoning over natural language as knowledge representation: A survey. In The 61st Annual Meeting Of The Association For Computational Linguistics

    2023

  37. [45]

    Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. Satlm: Satisfiability-aided language models using declarative prompting. In Proceedings of NeurIPS

    2023

  38. [46]

    Nathan Young, Qiming Bao, Joshua Bensemann, and Michael J Witbrock. 2022. Abductionrules: Training transformers to explain unexpected inputs. In Findings of the Association for Computational Linguistics: ACL 2022, pages 218--227

    2022

  39. [47]

    Fei Yu, Hongbo Zhang, Prayag Tiwari, and Benyou Wang. 2024. Natural language reasoning, a survey. ACM Computing Surveys, 56(12):1--39

    2024

  40. [48]

    Jing Zhang, Bo Chen, Lingxi Zhang, Xirui Ke, and Haipeng Ding. 2021. Neural, symbolic and neural-symbolic reasoning on knowledge graphs. AI Open, 2:14--35

    2021

  41. [49]

    Yixin Zhao, Adina Williams, Emily Dinan, Mohit Bansal, Mark Yatskar, and Yejin Choi. 2021. Adversarial nli: A new benchmark for natural language understanding. In null

    2021

  42. [50]

    Victor Zhong, Chandra Bhagavatula, Ronan Le Bras, Yejin Choi, and Noah A Smith. 2022. Analytical reasoning of text: Unifying machine reading and logical reasoning. In Findings of the Association for Computational Linguistics: NAACL 2022, pages 2307--2323

    2022

  43. [51]

    Wanjun Zhong, Siyuan Wang, Duyu Tang, Zenan Xu, Daya Guo, Jiahai Wang, Jian Yin, Ming Zhou, and Nan Duan. 2021. Ar-lsat: Investigating analytical reasoning of text. arXiv e-prints, pages arXiv--2104

    2021

  44. [52]

    online" 'onlinestring :=

    ENTRY address archivePrefix author booktitle chapter edition editor eid eprint eprinttype howpublished institution journal key month note number organization pages publisher school series title type volume year doi pubmed url lastchecked label extra.label sort.label short.list...

  45. [53]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 gl...

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.