Pith. sign in

REVIEW 2 major objections 3 minor 3 cited by

Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation

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

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

Pith's one-line read The paper claims that pairing LLM-written stories with symbolic proof checks can generate a scalable, diverse first-order-logic benchmark whose hardest problems state-of-the-art models still cannot reliably solve.

desk verdict Useful new benchmark with a real faithfulness bug in its example; deserves review but needs a fix. read the letter →

arxiv 2502.06563 v2 pith:FJMVCPCP submitted 2025-02-10 cs.CL

Chengwen Qi , Ren Ma , Bowen Li , He Du , Binyuan Hui , Jinwang Wu , Yuanjun Laili , Conghui He This is my paper · ORCID
classification cs.CL
keywords first-orderlogicreasoninglogicalbenchmarkchain-of-thoughtsymbolicproverLLMdatagenerationfaithfulchainsQAfine-tuning
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

The paper proposes ProverGen, a three-stage pipeline for generating first-order-logic reasoning problems without handcrafting templates. An LLM writes a background story and renders logical rules in natural language, while the symbolic prover Prover9 builds the reasoning tree backward from a goal and verifies the truth value of every step. The resulting dataset, ProverQA, has 1,500 problems in three difficulty tiers and includes proof-style intermediate steps for every problem. The authors report that strong LLMs barely exceed 50% accuracy on the hardest tier even with chain-of-thought prompting, and that fine-tuning an 8-billion-parameter model on ProverGen-generated data improves its scores on other benchmarks. The value of the claim, if correct, is that fresh, proof-checked reasoning data can be produced at scale and used to train as well as evaluate models.

What carries the argument

The load-bearing mechanism is top-down reasoning-tree construction with Prover9 as the truth-value calculator: the goal is the root, each sampled logical expression introduces new facts, and the prover assigns them truth values that make the derivation valid. Around that skeleton, the framework layers LLM-generated background stories, LLM translation with universal-versus-specific rule selection, and two kinds of distractions (unrelated facts about other subjects, and related facts that lead to 'Uncertain'). The formal layer uses seven first-order-logic connectives, with equivalence represented as exclusive disjunction.

What would settle it

Take the Appendix D hard example and formalize the English sentences independently: 'Buster is either obedient or playful, but not necessarily both' is compatible with Buster being both, so the step concluding 'Buster is not playful' does not follow; then measure how often such connective slippage appears in a random sample of ProverQA problems. If the fraction is not near zero, the benchmark's answers are not faithful to the Prover9-verified skeletons.

Watch

Extended reading notes

Core claim

The central claim is that LLMs and symbolic provers belong together in the data-generation stage, not only in the solve-and-verify stage: the LLM supplies natural-language diversity and the prover supplies logical soundness. ProverGen first generates a background story from a subject name and keyword, then constructs a logic skeleton top-down, starting from the desired conclusion and repeatedly sampling expressions that relate the current fact to new premises while Prover9 computes the truth values that keep the chain valid. Statement translation then converts the verified skeleton into English, choosing a universal or subject-specific wording for each rule, and the completed problem is augmented with two types of distractions and shuffled premises. The paper argues that ProverQA is the first synthetic dataset to combine scalability, diverse language, symbolic representations, and faithful reasoning chains, and that its evaluation shows state-of-the-art models struggle even with chain-of-thought prompting.

Load-bearing premise

The framework assumes that the LLM's translation from symbolic formulas into English preserves the exact logical meaning of each connective, especially whether 'or' means one-or-the-other-but-not-both rather than one-or-both; the quality checks confirm that names and predicates appear but do not check connective semantics, so a mistranslated disjunction can make the English problem entail a different answer than the verified skeleton.

Editorial extensions

If this is right

  • New FOL benchmarks can be generated on demand at controlled difficulty levels, which makes it harder for models to succeed through memorized test answers.
  • Fine-tuning on ProverGen-generated data improves out-of-distribution logical reasoning, suggesting the generated chains teach a generalizable deductive skill rather than a template pattern.
  • The sub-50% accuracy of strong models on the hard tier, with chain-of-thought prompting, indicates that multi-step formal reasoning remains an open problem for current LLMs.
  • Both added distractions and shuffled premise order reduce model accuracy, so evaluation design choices materially change measured reasoning ability.

Reading between the lines

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

  • A direct test of the framework's soundness would formalize the English statements of each ProverQA problem back into FOL and compare the entailment with the Prover9-verified skeleton; the current quality checks only verify that names and predicates appear in the translation, not that connective semantics survived.
  • If translation slippage between exclusive and inclusive 'or' is not rare, then benchmark scores mix formal deduction with a separate skill of guessing the intended reading from ambiguous English.
  • The logic-skeleton layer is driven by a prover rather than by learned parameters, so swapping the prover and the translation prompt could extend the same pipeline to other formal systems.
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

2 major / 3 minor

Summary. The paper proposes ProverGen, a three-stage pipeline for generating first-order-logic reasoning datasets: an LLM generates a background story; Prover9 is used to construct a top-down reasoning skeleton and compute truth values; and an LLM translates the symbolic facts, rules, and goals into natural language, selecting universal or specific versions of rules. The resulting benchmark, ProverQA, contains 1,500 instances in easy/medium/hard splits with two types of distractions and shuffled premises. The authors evaluate GPT-4o, Claude-3.5, and open-weight models under standard and CoT prompting, finding low accuracy on the hard subset; they also fine-tune Llama3.1-8B-Instruct on ProverQA and report gains on in-distribution and out-of-distribution benchmarks.

Significance. If the translation stage faithfully preserved the Prover9-verified skeleton, ProverGen would be a valuable contribution: it would combine scalable generation, linguistic diversity, formal verification, and accessible proof chains, and the OOD fine-tuning results would suggest the data are useful beyond the benchmark itself. The use of an external symbolic prover for skeleton construction and truth-value assignment is a genuine strength, as are the released code and the contamination-avoidance rationale. The central soundness claim, however, rests on the unverified assumption that the LLM-generated natural-language premises are logically equivalent to the symbolic formulas, and the paper exhibits a concrete counterexample to that assumption.

major comments (2)
  1. [Appendix D, ProverQA-Hard, Step 4] The proof chain in the hard example derives 'Buster is not playful' from 'Buster is obedient' and 'Buster is either obedient or playful, but not necessarily both.' Read literally, the premise is an inclusive disjunction: it permits both conjuncts to be true, and from the truth of 'obedient' nothing follows about 'playful.' The displayed inference is therefore invalid, and the final answer 'Buster is loving' is not entailed by the stated context (a model with obedient=true, playful=true, loving=false satisfies all premises but makes the goal false). If the skeleton's formula was an exclusive disjunction, then the English translation should have said 'but not both,' as it does elsewhere in the same appendix; in that case the natural-language premise is not a faithful translation. Either way, this instance contradicts the paper's claim that ProverQA provides logically sound, prover-verified problems and faithful intermediate reasoning steps. The authors should correct this example and conduct a systematic connective-level audit of the whole dataset.
  2. [Appendix H] The quality-control section verifies only that names and predicates appear in the natural-language translations; it does not check that logical connectives (especially inclusive vs. exclusive disjunction) are preserved. The manual audit of 60 examples is reported as showing zero translation errors, but Appendix D contains a visible counterexample, so the audit protocol is not adequate to support the general soundness claim. I recommend an automated or semi-automated check that re-translates each natural-language premise back to a formal formula (or uses a logical-equivalence validator) and reports the error rate; if a nontrivial fraction of instances fail, the benchmark should be regenerated before the evaluation claims are reinstated.
minor comments (3)
  1. [Section 3.2.3 / Figure 2] The translation of the XOR rule f5 -> (f1 xor f4) as 'If Sawyer is a performer, then he either has good dance skills or is a musician' omits the 'but not both' qualification that is needed for XOR; this strengthens the case for a connective-level quality check.
  2. [Appendix C] The text says GPT-4 was evaluated on the corrupted-dataset control, while Table 6 reports GPT-4o; please align the model name.
  3. [Reproducibility statement] The phrase 'framewrok' contains a typo and should read 'framework.'

Circularity Check

1 steps flagged · score 2.0 of 10

Only mild circularity: training-set size and hyperparameters were tuned against out-of-distribution performance, so the reported OOD gain is partly self-selected. The core Prover9-based generation chain and external benchmark evaluations are otherwise independent.

  1. fitted input called prediction [Appendix F (Training Details)]
    "Our experiments show that, as the number of training instances increased, the model’s performance consistently improved on in-distribution datasets and two out-of-distribution datasets: ProofWriter and ProntoQA. However, performance on FOLIO fluctuated as the number of training instances increases. After further experimentation, we found that 5,000 is a sweet spot that reaches a good balance between in-distribution and out-of-distribution performance."

    The training configuration (notably the 5,000-instance training-set size, and hyperparameters selected on held-out validation sets) was chosen with explicit reference to out-of-distribution performance on ProofWriter, ProntoQA, and FOLIO. The paper then presents the resulting OOD gains (OOD Avg Δ +7.5) as evidence that ProverQA training data improves generalization. Since the configuration was selected partly to maximize OOD performance, the reported OOD improvement is not a fully independent confirmation of the framework's generalizability; it is partially forced by the model-selection process. The in-distribution gains and the difficulty-level benchmark results remain independent, so the circularity is mild.

full rationale

The paper's central generation pipeline is anchored to an external symbolic prover (Prover9) for constructing reasoning trees and computing truth values, and its evaluation is anchored to external benchmarks (ProntoQA, ProofWriter, FOLIO) and to held-out ProverQA subsets. Those components give the main claims independent content, so no definitional or self-citation circularity is load-bearing. The only genuine circular step is in Appendix F: training-set size and hyperparameters were tuned with an eye to out-of-distribution performance, making the headline 'consistent improvements on OOD test sets' partly a selection artifact rather than an independent prediction. This is a mild form of fitted-input-called-prediction, not a collapse of the whole derivation. Separately, there is a non-circularity correctness concern that should be weighed under validity risk: Appendix D's ProverQA-Hard example states 'Buster is either obedient or playful, but not necessarily both' and then uses that premise to conclude 'Buster is not playful', an inference valid only under exclusive-or; the phrase 'not necessarily both' is the standard English signal for inclusive-or. Appendix H's translation quality control checks only that names and predicates appear in the natural-language output, not that connective semantics are preserved, and the manual audit of 60 examples claims zero translation errors despite this exhibited counterexample. This threatens the claim that all ProverQA chains are faithful to the Prover9-verified skeleton, but it is a data-fidelity/validity issue rather than a by-construction circularity, so it does not raise the circularity score.

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

The paper's claims rest on the reliability of Prover9, on the translation fidelity of the LLM, on the common-sense adjudication between universal and specific rules, and on the representativeness of a 60-example manual audit. No new scientific entities are introduced.

free parameters (2)
  • Difficulty chain lengths = easy: 1-2, medium: 3-5, hard: 6-9 steps
    Hand-chosen thresholds that define the benchmark's difficulty levels; not fitted to data but arbitrary and load-bearing for the 'hard' result.
  • ProverQA train-set size = 5,000 instances
    Selected in Appendix F after 'further experimentation' as a sweet spot balancing ID and OOD performance; the choice depends on the OOD benchmarks, so the reported OOD gains are partly tuned.
assumptions (4)
  • domain assumption Prover9's logical results are sound for the generated FOL fragments and are correctly used to assign truth values in the reasoning tree.
    Section 3.2.2 relies on the symbolic prover to ensure premises support the goal and to compute truth values of facts and distractions.
  • domain assumption LLM translations preserve the semantics of the logical connectives (AND, OR, XOR, implies, not, for all, exists) in natural language.
    The pipeline's quality checks verify entity presence, not meaning; Appendix D's hard example raises doubt about this assumption.
  • ad hoc to paper When LLMs choose between universal and specific rules based on common sense, the chosen version does not change the logical truth values of the skeleton.
    Section 3.2.3 uses this heuristic without a formal consistency check; a mismatch could make the English problem differ from the Prover9-verified problem.
  • domain assumption The 60 manually audited examples are representative of all 1,500 instances.
    Section H uses this sample to claim less than 2% error likelihood, but a 60-instance sample cannot support that bound at conventional confidence.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation." pith.science (2026). https://pith.science/paper/FJMVCPCP

@misc{pith2026250206563,
  author       = {Pith},
  title        = {Pith review of: Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FJMVCPCP}},
  note         = {Machine review of arXiv:2502.06563}
}
read the original abstract

First-order logic (FOL) reasoning, which involves sequential deduction, is pivotal for intelligent systems and serves as a valuable task for evaluating reasoning capabilities, particularly in chain-of-thought (CoT) contexts. Existing benchmarks often rely on extensive human annotation or handcrafted templates, making it difficult to achieve the necessary complexity, scalability, and diversity for robust evaluation. To address these limitations, we propose a novel framework called ProverGen that synergizes the generative strengths of Large Language Models (LLMs) with the rigor and precision of symbolic provers, enabling the creation of a scalable, diverse, and high-quality FOL reasoning dataset, ProverQA. ProverQA is also distinguished by its inclusion of accessible and logically coherent intermediate reasoning steps for each problem. Our evaluation shows that state-of-the-art LLMs struggle to solve ProverQA problems, even with CoT prompting, highlighting the dataset's challenging nature. We also finetune Llama3.1-8B-Instruct on a separate training set generated by our framework. The finetuned model demonstrates consistent improvements on both in-distribution and out-of-distribution test sets, suggesting the value of our proposed data generation framework. Code available at: https://github.com/opendatalab/ProverGen

Figures

Figures reproduced from arXiv: 2502.06563 by the authors.

Figure 1
Figure 1. An overview of our ProverGen framework. (a) [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. A generated FOL problem (a) with its corresponding reasoning process (b). [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Symbolic Neural Generation with Applications to Lead Discovery in Drug Design

    cs.LG 2025-10 conditional novelty 6.0 of 10

    A hybrid system that learns symbolic interval constraints from a few examples and uses an LLM plus rejection filtering to generate new candidate drug molecules.

  2. Logical Reasoning with Outcome Reward Models for Test-Time Scaling

    cs.CL 2025-08 conditional novelty 5.0 of 10

    Outcome reward models trained on multi-sample chain-of-thought plus deliberately flawed 'echo' rationales improve Best-of-N test-time verification for deductive reasoning.

  3. Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations

    cs.CL 2025-05 conditional novelty 5.0 of 10

    The proposed Faithful-Refiner, combining syntactic parsing, quantifier and consistency checks, logical-relation guidance, and detailed proof feedback, raises explanation refinement rates on three NLI benchmarks by lar...

Reference graph

Works this paper leans on

25 extracted references · 14 canonical work pages · cited by 3 Pith papers

  1. [3]

    Oran-bench-13k: An open source benchmark for assessing llms in open radio access networks

    Pranshav Gajjar and Vijay K Shah. Oran-bench-13k: An open source benchmark for assessing llms in open radio access networks. arXiv preprint arXiv:2407.06245,

    arXiv

  2. [5]

    F7": "playful

    Your answer should be in JSON format with the provided keys. User: background story: Moriarty was a large, fluffy Maine Coon cat with a surprisingly warm and gentle nature. Despite his intimidating size and the mysterious name inspired by a famous literary villain, Moriarty was the epitome of warmth and comfort. He lived in a cozy bookstore run by Mrs. Li...

    work page 2025

  3. [7]

    Mistral 7b

    Albert Q Jiang, Alexandre Sablayrolles, Arthur Mensch, Chris Bamford, Devendra Singh Chaplot, Diego de las Casas, Florian Bressand, Gianna Lengyel, Guillaume Lample, Lucile Saulnier, et al. Mistral 7b. arXiv preprint arXiv:2310.06825,

    arXiv

  4. [8]

    Mixtral of experts

    Albert Q Jiang, Alexandre Sablayrolles, Antoine Roux, Arthur Mensch, Blanche Savary, Chris Bam- ford, Devendra Singh Chaplot, Diego de las Casas, Emma Bou Hanna, Florian Bressand, et al. Mixtral of experts. arXiv preprint arXiv:2401.04088,

    arXiv

  5. [9]

    Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang

    doi: 10.1109/ TASLP.2023.3293046. Jian Liu, Leyang Cui, Hanmeng Liu, Dandan Huang, Yile Wang, and Yue Zhang. Logiqa: a chal- lenge dataset for machine reading comprehension with logical reasoning. In Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelli- gence, pp. 3622–3628,

    arXiv 2023

  6. [10]

    Faithful chain-of-thought reasoning

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

    work page 2023

  7. [15]

    An investigation of llms’ inefficacy in understanding converse relations

    Chengwen Qi, Bowen Li, Binyuan Hui, Bailin Wang, Jinyang Li, Jinwang Wu, and Yuanjun Laili. An investigation of llms’ inefficacy in understanding converse relations. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 6932–6953,

    work page 2023

  8. [16]

    Clutrr: A diag- nostic benchmark for inductive reasoning from text

    Koustuv Sinha, Shagun Sodhani, Jin Dong, Joelle Pineau, and William L Hamilton. Clutrr: A diag- nostic benchmark for inductive reasoning from text. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (EMNLP-IJCNLP), pp. 4506–4515,

    work page 2019

Show all 25 references
  1. [17]

    Haitian Sun, William W Cohen, and Ruslan Salakhutdinov

    URL https://arxiv.org/ abs/2403.01081. Haitian Sun, William W Cohen, and Ruslan Salakhutdinov. Conditionalqa: A complex reading comprehension dataset with conditional answers. arXiv preprint arXiv:2110.06884,

    arXiv

  2. [18]

    Proofwriter: Generating implications, proofs, and abductive statements over natural language

    Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pp. 3621–3634,

    2021

  3. [19]

    Diagnosing the first-order logical reasoning ability through logicnli

    Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. Diagnosing the first-order logical reasoning ability through logicnli. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pp. 3738–3747,

    2021

  4. [20]

    Large lan- guage models still can’t plan (a benchmark for llms on planning and reasoning about change)

    12 Published as a conference paper at ICLR 2025 Karthik Valmeekam, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. Large lan- guage models still can’t plan (a benchmark for llms on planning and reasoning about change). In NeurIPS 2022 Foundation Models for Decision ...

    2025

  5. [22]

    Ar-lsat: Investigating analytical reasoning of text

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

    arXiv

  6. [23]

    category

    A P ROMPT FOR GENERATING BACKGROUND STORY System: You will be given a keyword and a name (can be a person’s name or an animals’ name). Your task is to generate a background story with no more than 150 words according to the keyword about this name. Your answer should be in JSO...

    2025

  7. [25]

    2-shot) into the prompt did not consistently improve the performance of LLMs

    It can be concluded that incorporating more examples (5-shot vs. 2-shot) into the prompt did not consistently improve the performance of LLMs. This inconsistency may stem from several factors, including variations in the models’ in-context learning capabilities. Table 7: The p...

    2025

  8. [1995]

    Linc: A neurosymbolic approach for logical reasoning by com- bining language models with first-order logic provers

    Theo X Olausson, Alex Gu, Ben Lipkin, Cedegao E Zhang, Armando Solar-Lezama, Joshua B Tenenbaum, and Roger P Levy. Linc: A neurosymbolic approach for logical reasoning by com- bining language models with first-order logic provers. In The 2023 Conference on Empirical Methods in...

    2023

  9. [2005]

    Smith, Mateusz Paprocki, Ond ˇrej ˇCert´ık, Sergey B

    11 Published as a conference paper at ICLR 2025 Aaron Meurer, Christopher P. Smith, Mateusz Paprocki, Ond ˇrej ˇCert´ık, Sergey B. Kirpichev, Matthew Rocklin, Amit Kumar, Sergiu Ivanov, Jason K. Moore, Sartaj Singh, Thilina Rath- nayake, Sean Vig, Brian E. Granger, Richard P. ...

    2025

  10. [2008]

    The lean theorem prover (system description)

    Leonardo De Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). InAutomated Deduction-CADE-25: 25th International 10 Published as a conference paper at ICLR 2025 Conference on Automated Deduction, Berlin, Ger...

    2025

  11. [2015]

    The llama 3 herd of models

    Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The llama 3 herd of models. arXiv preprint arXiv:2407.21783,

    arXiv

  12. [2017]

    doi: 10.7717/peerj-cs.103

    ISSN 2376-5992. doi: 10.7717/peerj-cs.103. URL https://doi.org/10.7717/peerj-cs.103. George A Miller. Wordnet: a lexical database for english. Communications of the ACM , 38(11): 39–41,

    doi

  13. [2019]

    Sola: Solver-layer adaption of llm for better logic reasoning

    Yu Zhang, Hui-Ling Zhen, Zehua Pei, Yingzhao Lian, Lihao Yin, Mingxuan Yuan, and Bei Yu. Sola: Solver-layer adaption of llm for better logic reasoning. arXiv preprint arXiv:2402.11903,

  14. [2021]

    Folio: Natural language reasoning with first-order logic

    Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Luke Benson, Lucy Sun, Ekaterina Zubova, Yujie Qiao, Matthew Burtell, et al. Folio: Natural language reasoning with first-order logic. arXiv preprint arXiv:2209.00840,

    arXiv

  15. [2022]

    Won’t get fooled again: Answering questions with false premises

    Shengding Hu, Yifan Luo, Huadong Wang, Xingyi Cheng, Zhiyuan Liu, and Maosong Sun. Won’t get fooled again: Answering questions with false premises. arXiv preprint arXiv:2307.02394 ,

    arXiv

  16. [2023]

    Chatgpt is fun, but it is not funny! humor is still challenging large language models

    Sophie Freya Jentzsch and Kristian Kersting. Chatgpt is fun, but it is not funny! humor is still challenging large language models. In 61st Annual Meeting of the Association for Computational Linguistics, ACL 2023,

    2023

  17. [2024]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang

    URL https://openai.com/index/hello-gpt-4o/. Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-lm: Empower- ing large language models with symbolic solvers for faithful logical reasoning. arXiv preprint arXiv:2305.12295,

    arXiv

Pith tools

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