Pith. sign in

REVIEW 3 major objections 7 minor 1 cited by

Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations

T0 review · 3 major / 7 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 This paper claims that four targeted interventions—syntactic parsing before formalisation, quantifier and consistency checks, logical-expression-guided proof sketches, and step-level proof feedback—make LLM-driven theorem proving of NLI…

desk verdict A solid, incremental system paper whose refinement-rate gains are real, but whose headline faithfulness metric is unvalidated and should be reframed or fixed before publication. read the letter →

arxiv 2505.24264 v1 pith:A3TAFEGS submitted 2025-05-30 cs.CL cs.AI

Xin Quan , Marco Valentino , Louise A. Dennis , André Freitas This is my paper
classification cs.CLcs.AI
keywords naturallanguageinferencetheoremprovingautoformalisationexplanationrefinementlargemodelsIsabelle/HOLformalverificationfaithfulness
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

Natural language explanations in NLI can be checked by translating them into formal logic and asking a theorem prover to verify that the premise entails the hypothesis, but the translation step (autoformalisation) often drops or distorts meaning and the LLM often fails to build valid proofs. This paper tries to show that the bottleneck is in the surrounding pipeline rather than the prover, and that four targeted interventions fix most of it: syntactic parsing before formalisation, explicit quantifier and consistency checks, logical-expression-guided proof-sketch generation, and detailed step-level feedback when a proof attempt fails. Across three NLI datasets (e-SNLI, QASC, WorldTree) and four LLMs, the framework lifts the share of explanations that end up verified from 41% to 95%, 17% to 90%, and 7% to 73% over the baseline, with fewer iterations and fewer LLM calls. The paper's central claim is that these interventions make autoformalisation more faithful and make the verification loop more effective and cheaper.

What carries the argument

The machinery that carries the argument is the Faithful-Refiner refinement loop, built around four interventions. First, an LLM performs syntactic parsing of each sentence and maps subject, verb phrase, and complements onto agent, event, and patient roles in Neo-Davidsonian event semantics, so that the formalisation is anchored to grammatical structure rather than free-form translation. Second, a soft critique stage prompts the LLM to fix quantifiers that conflict with real-world knowledge, while a hard critique stage uses the theorem prover's own error output to repair syntax, and a consistency check replaces the theorem's conclusion with False to detect contradictory axioms. Third, the LLM extracts logical propositions and relations from the explanation, SymPy derives additional implications, and the LLM writes a step-by-step proof sketch with automated-theorem-prover placeholders instead of planning the whole proof at once. Fourth, when a proof step fails, the failed step plus its context is fed back to the LLM to refine the explanation, and unnecessary explanatory sentences are dropped once a proof is found. Faithfulness is measured by a rule-based informalisation algorithm that converts logical forms back into natural language and compares them to the originals by cosine similarity.

What would settle it

Sample 100 formalised explanations, back-translate them with the rule-based informaliser, and have human raters judge whether each informalised sentence means the same as the original; if the cosine-similarity ranking does not match human ratings, the reported faithfulness gains would not reflect semantic fidelity. A second check: run the pipeline on explanations known to be invalid but whose formalisations are internally consistent, and see whether the theorem prover still verifies them.

Watch

Extended reading notes

Core claim

The paper's central claim is that the failure of LLM-plus-theorem-prover verification of NLI explanations is driven mainly by preventable weaknesses in autoformalisation and proof construction, not by the theorem prover itself. To establish this, the authors introduce Faithful-Refiner, a pipeline that parses sentences syntactically before translating them into Neo-Davidsonian event semantics, applies soft and hard critiques (quantifier refinement against real-world knowledge, syntax repair from the prover's error messages, and a consistency check that tries to prove False), and then guides the LLM to write step-by-step proof sketches from extracted logical propositions, relations, and derived implications. When a step fails, the failed step is used as detailed feedback to refine the natural-language explanation, and the loop repeats. The reported evidence is an increase in autoformalisation faithfulness of 18.46%, 34.2%, and 39.77% relative to the baseline on e-SNLI, QASC, and WorldTree, and refinement rates rising from 41% to 95%, 17% to 90%, and 7% to 73% across the three datasets.

Load-bearing premise

The headline faithfulness numbers rest on the assumption that the rule-based back-translation from logical forms to natural language preserves meaning well enough that cosine similarity to the original sentence is a true measure of semantic fidelity, since that metric is never checked against human judgment; the paper also assumes that a theorem-prover proof of the formalised theory implies the original natural-language explanation is logically valid.

Editorial extensions

If this is right

  • Share of explanations that end up verified rises from 41% to 95% on e-SNLI, 17% to 90% on QASC, and 7% to 73% on WorldTree across the four LLMs tested.
  • Average LLM calls needed to refine an explanation fall by 58.6% on e-SNLI, 39.4% on QASC, and 31.2% on WorldTree, so the pipeline is also cheaper.
  • Ablation results indicate that removing step-level proof feedback or syntax-error refinement causes the largest drops in refinement rate, so those two components carry the most weight.
  • Removing logical-expression guidance raises required iterations and lowers refinement rates, suggesting the proof sketch prevents hallucinated or unfocused proof steps.
  • The consistency check that tries to prove False catches contradictory axiom sets, preventing the principle of explosion from generating spurious verifications.

Reading between the lines

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

  • The faithfulness metric depends entirely on the rule-based informaliser's ability to preserve meaning; until that back-translation is validated against human judgment, part of the reported gain could reflect the informaliser matching the framework's own formalisation style rather than true semantic fidelity.
  • The same four interventions could transfer to other autoformalisation settings, such as mathematical statement formalisation, where faithfulness is currently measured by round-trip translation rather than downstream proof success.
  • A testable extension is to vary LLM temperature or add confidence thresholds, since the paper's own limitations note that degraded model output or noisy proof feedback can break the refinement loop.
  • On WorldTree, much of the gain comes from the LLM supplying missing real-world axioms in later iterations; the framework's success there is therefore sensitive to the LLM's implicit knowledge, not just to the prover.
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 / 7 minor

Summary. The paper introduces Faithful-Refiner, a neuro-symbolic framework for verifying and refining natural-language NLI explanations with Isabelle/HOL. It builds on the Explanation-Refiner baseline and adds four interventions: (i) syntactic parsing to guide autoformalisation into Neo-Davidsonian event semantics, (ii) quantifier and logical-consistency critiques, (iii) extraction of logical propositions/relations with SymPy-derived implications to guide proof-sketch generation, and (iv) detailed proof-step feedback for iterative refinement. Experiments are conducted on 100-instance samples of e-SNLI, QASC, and WorldTree with four LLMs (GPT-4o, GPT-4o-mini, Llama3.1-70b, Deepseek-V3), reporting higher refinement rates, fewer iterations and LLM calls, a rule-based informalisation/cosine-similarity faithfulness metric, and a manual error analysis of variable, implication, and quantifier errors.

Significance. If the results are taken at face value, the framework is a practically important advance: the refinement-rate improvements are large and consistent across four LLMs, the ablations isolate the contribution of syntax-error refinement and detailed feedback, and the efficiency gains (fewer iterations and API calls) are directly useful. The use of an external theorem prover as a verifier is a strength, and the code and data are released with the paper. The main weakness is that the 'faithfulness' claim rests on an unvalidated metric; the refinement-rate claims do not depend on it, but the paper's headline framing does. The combination of external TP verification, systematic ablations, and reproducible artifacts makes this a valuable contribution to LLM-symbolic reasoning for NLI, provided the faithfulness claims are appropriately re-scoped or validated.

major comments (3)
  1. [§4.2, Appendix B, Figure 6] The faithfulness metric is a cosine similarity between the original sentence and a rule-based informalisation of the Neo-Davidsonian logical form, with no validation against human judgments. Figure 6 itself illustrates the problem: 'The boy is inside of the building.' is scored 0.9344 against the ungrammatical 'Boy in side building.' Because the syntactic-parsing prompt encourages the LLM to reuse the source sentence's content words, the metric can be high even when the logical form is semantically wrong (e.g., swapped roles, missing arguments, wrong quantifier scope). The headline autoformalisation improvements (+18.46%, +34.2%, +39.77% in the abstract) are therefore not yet established as faithfulness improvements. Please either add a human evaluation of whether the informalised forms preserve the meaning of the original sentences, or reframe the results as 'lexical similarity after rule-based informalisation' rather than 'faithfulness'.
  2. [§3.3, §4.2, Table 1, Limitations] The 'logically valid explanation' status is a proof in Isabelle of the LLM-produced formal theory, but no direct check ties that proof back to the natural-language meaning. The manual evaluation in Table 2 counts variable, implication, and quantifier errors in the formal objects; it does not ask annotators whether the proved formal claim corresponds to the original NL explanation. The Limitations correctly state that 'LLMs can still introduce variable inconsistencies, erroneous implications, and incorrect quantifiers that are not fully resolved by automated checking.' To support the validity claims, the paper should either add a human evaluation comparing the TP-verified formalisation (or its informalisation) to the intended NL meaning, or explicitly restrict the validity claim to the formalised theory and note that TP success does not by itself certify NL-level validity.
  3. [§4.1, Tables 1–3] The headline numbers are computed on 100 instances per dataset by design, yet the paper reports no uncertainty estimates (bootstrap CIs, standard errors) or significance tests. Given the baseline rates are low (e.g., 15–31% on WorldTree), the absolute improvements are large; nevertheless, the lack of error bars makes it impossible to judge whether smaller differences — such as the ablation of quantifier refinement, which sometimes improves the refinement rate (+4%, +3% in Table 2) — are meaningful. Please report bootstrap confidence intervals or standard errors for the main refinement rates and faithfulness scores, or at least explicitly acknowledge the sample-size limitation when interpreting component-wise differences.
minor comments (7)
  1. [Figure 3] The legend entry 'Ours-Llama3.1-70b3.1-70b' appears to be a typo for 'Ours-Llama3.1-70b'.
  2. [Figure 5] The caption says 'at each syntax error refinement stage' but the plots show logical consistency errors; please align the caption and axis labels with the content.
  3. [§2 and §3.1] The text contains missing spaces, e.g., 'anexplanation' and 'define anexplanation'; please proofread these passages.
  4. [§4.2] The sentence 'We then calculate the cosine similarity between these reconstructed (informalised) sentences between the original sentences as the faithfulness of autoformalisation' is garbled; it should read 'between the reconstructed sentences and the original sentences'.
  5. [§4.1] The citation 'GPT-4o (OpenAI, 2023)' refers to the GPT-4 technical report; the model is GPT-4o and should cite the appropriate GPT-4o system card or model documentation.
  6. [Table 2] The manual-evaluation sampling is described as 'a randomly sampled set of 100 Isabelle/HOL theories across all iterations for each LLM'; please specify whether this is 100 per condition or 100 per LLM overall, and clarify how the sample relates to the ablation conditions in the same table.
  7. [Algorithm 1] The algorithm iterates over all pairs of literals (literals × literals) and checks entailment, which is exponential in the number of propositions; a brief note on the practical size of this enumeration would help reproducibility.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: external theorem-prover verification anchors the claims; the faithfulness metric is an unvalidated proxy but not a fitted or self-referential input.

full rationale

The central verification claim is anchored by an external checker: an explanation is counted as refined only when Isabelle/HOL with Sledgehammer derives the goal from the formalized premises and axioms (Section 3.3, Table 1, Figure 3). The proposed components (syntactic parsing, quantifier and consistency checks, logical-relation guidance, and detailed proof-step feedback) are fixed interventions rather than parameters fitted to the reported outcomes, and their contribution is tested by ablations against the same external prover (Table 2). The baseline, Explanation-Refiner, is the authors' prior system, and the paper states it 'followed the same prompts used in Explanation-Refiner' for autoformalisation; but this is methodological continuity and a comparative baseline, not a load-bearing justification whose conclusion is imported from the citation. The main validity concern is the faithfulness metric in Section 4.2 and Appendix B: faithfulness is operationalized as cosine similarity between the original sentence and a rule-based informalisation of the formal logical form, a proxy that is never validated against human semantic judgments. That is a measurement-validity risk, not circularity: the informalisation algorithm is deterministic, does not use the final reported outcome as an input, and does not guarantee similarity by construction. Moreover, the theorem-proving and refinement-rate results do not depend on this metric. No step in the paper's derivation reduces by construction to a fitted parameter, a self-citation chain, or a definition that presupposes its own conclusion.

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

The central claim leans on several domain assumptions about the adequacy of the formal representation, the validity of theorem-prover verification, and the soundness of the paper's own evaluation metric. No new entities are introduced.

assumptions (5)
  • domain assumption Neo-Davidsonian event semantics is an adequate formal representation for the premises, hypotheses, and explanations in these NLI datasets.
    Invoked in Section 3.1 to justify converting syntactic parses into event-based predicates; if this representation loses or distorts meaning, the theorem prover may prove a different statement than the NLP one.
  • domain assumption Theorem-prover success on the constructed Isabelle/HOL theory indicates that the original natural-language explanation logically entails the hypothesis.
    Section 2 defines explanation validity as p_i union E_i entails h_i via the autoformalised theory; this requires the formalisation to be faithful, which the paper tries to ensure but cannot guarantee.
  • ad hoc to paper The rule-based informalisation algorithm recovers natural-language meaning from logical forms well enough for cosine similarity to serve as a faithfulness metric.
    Appendix B describes the algorithm and uses it to compute faithfulness scores in Figure 4; the metric is not externally validated.
  • standard math Isabelle/HOL with Sledgehammer and the external ATPs used are sound and reliable for the proof steps attempted.
    The paper relies on Isabelle/HOL (Nipkow et al., 2002) and Sledgehammer as the verification backend; these are established tools.
  • domain assumption The 100-instance samples from e-SNLI, QASC, and WorldTree are representative of the datasets.
    Section 4.1 states three sampled datasets each comprising 100 instances following Quan et al. (2024b); if the samples are biased, the reported percentages may not generalize.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations." pith.science (2026). https://pith.science/paper/A3TAFEGS

@misc{pith2026250524264,
  author       = {Pith},
  title        = {Pith review of: Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/A3TAFEGS}},
  note         = {Machine review of arXiv:2505.24264}
}
read the original abstract

Natural language explanations play a fundamental role in Natural Language Inference (NLI) by revealing how premises logically entail hypotheses. Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. However, TPs require translating natural language into machine-verifiable formal representations, a process that introduces the risk of semantic information loss and unfaithful interpretation, an issue compounded by LLMs' challenges in capturing critical logical structures with sufficient precision. Moreover, LLMs are still limited in their capacity for rigorous and robust proof construction within formal verification frameworks. To mitigate issues related to faithfulness and robustness, this paper investigates strategies to (1) alleviate semantic loss during autoformalisation, (2) efficiently identify and correct syntactic errors in logical representations, (3) explicitly use logical expressions to guide LLMs in generating structured proof sketches, and (4) increase LLMs' capacity of interpreting TP's feedback for iterative refinement. Our empirical results on e-SNLI, QASC and WorldTree using different LLMs demonstrate that the proposed strategies yield significant improvements in autoformalisation (+18.46%, +34.2%, +39.77%) and explanation refinement (+29.5%, +51.5%, +41.25%) over the state-of-the-art model. Moreover, we show that specific interventions on the hybrid LLM-TP architecture can substantially improve efficiency, drastically reducing the number of iterations required for successful verification.

Figures

Figures reproduced from arXiv: 2505.24264 by the authors.

Figure 1
Figure 1. An illustration of our proposed interventions for improving LLM-driven theorem proving for NLI. The [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. An example of a proof sketch constructed by the model to verify an explanation from the e-SNLI dataset. [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Top – Number of logically valid explanations at each refinement iteration. Bottom – Number of theories [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (8 more)
Figure 4
Figure 4. Figure 4: Top – The average faithfulness of the autoformalisation process across different LLMs. Bottom – The [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Number of theories that contain logical consistency error at each syntax error refinement stage. [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 6
Figure 6. Figure 6: An example of the faithfulness between two informalised logical forms [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: An example of an autoformalised Isabelle/HOL theory in the e-SNLI dataset. [PITH_FULL_IMAGE:figures/full_fig_p016_7.png]
Figure 8
Figure 8. Figure 8: An example of an autoformalised Isabelle/HOL theory in the QASC dataset. [PITH_FULL_IMAGE:figures/full_fig_p017_8.png]
Figure 9
Figure 9. Figure 9: An example of an autoformalised Isabelle/HOL theory in the QASC dataset. [PITH_FULL_IMAGE:figures/full_fig_p017_9.png]
Figure 10
Figure 10. Figure 10: An example of an autoformalised Isabelle/HOL theory in the WorldTree dataset. [PITH_FULL_IMAGE:figures/full_fig_p019_10.png]
Figure 11
Figure 11. Figure 11: An example of an autoformalised Isabelle/HOL theory in the WorldTree dataset. [PITH_FULL_IMAGE:figures/full_fig_p020_11.png]

Discussion (0). Sign in to comment.

Forward citations

Cited by 1 Pith paper

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

  1. Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning

    cs.CL 2025-06 conditional novelty 6.0 of 10

    A taxonomy-guided ensemble of LLM judges correlates with human ratings of autoformalizations (up to 0.662 on Isabelle/HOL) better than coarse-grained judges and reference metrics, but validation is partly in-sample an...

Reference graph

Works this paper leans on

48 extracted references · 17 canonical work pages · cited by 1 Pith paper

  1. [1]

    Ayush Agrawal, Siddhartha Gadgil, Navin Goyal, Ashvni Narayanan, and Anand Tadipatri. 2022. https://arxiv.org/abs/2211.07524 Towards a mathematics formalisation assistant using large language models . Preprint, arXiv:2211.07524

    arXiv 2022

  2. [2]

    Oana-Maria Camburu, Tim Rockt\" a schel, Thomas Lukasiewicz, and Phil Blunsom. 2018. https://proceedings.neurips.cc/paper_files/paper/2018/file/4c7a167bb329bd92580a99ce422d6fa6-Paper.pdf e-snli: Natural language inference with natural language explanations . In Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc

    2018

  3. [3]

    Qianglong Chen, Feng Ji, Xiangji Zeng, Feng-Lin Li, Ji Zhang, Haiqing Chen, and Yin Zhang. 2021. https://doi.org/10.18653/v1/2021.acl-long.196 KACE : Generating knowledge aware contrastive explanations for natural language inference . In Proceedings of the 59th Annual Meeting of the Association for Computational Linguistics and the 11th International Join...

    work page doi:10.18653/v1/2021.acl-long.196 2021

  4. [4]

    Dhairya Dalal, Marco Valentino, Andre Freitas, and Paul Buitelaar. 2024. https://doi.org/10.18653/v1/2024.acl-long.14 Inference to the best explanation in large language models . In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 217--235, Bangkok, Thailand. Association for Computation...

    doi:10.18653/v1/2024.acl-long.14 2024

  5. [5]

    DeepSeek-AI. 2024. https://arxiv.org/abs/2412.19437 Deepseek-v3 technical report . Preprint, arXiv:2412.19437

    arXiv 2024

  6. [6]

    Rabe, Talia Ringer, and Yuriy Brun

    Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. https://arxiv.org/abs/2303.04910 Baldur: Whole-proof generation and repair with large language models . Preprint, arXiv:2303.04910

    arXiv 2023

  7. [7]

    Simon Frieder, Julius Berner, Philipp Petersen, and Thomas Lukasiewicz. 2024. https://arxiv.org/abs/2312.04556 Large language models for mathematicians . Preprint, arXiv:2312.04556

    work page Pith review arXiv 2024

  8. [8]

    Carvalho, and André Freitas

    João Pedro Gandarela, Danilo S. Carvalho, and André Freitas. 2025. https://arxiv.org/abs/2408.16779 Inductive learning of logical theories with llms: An expressivity-graded analysis . Preprint, arXiv:2408.16779

    arXiv 2025

Show all 48 references
  1. [9]

    Aaron Grattafiori, Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, and Ahmad Al-Dahle. 2024. https://arxiv.org/abs/2407.21783 The llama 3 herd of models . Preprint, arXiv:2407.21783

    2024 arXiv

  2. [10]

    Xuanli He, Yuxiang Wu, Oana-Maria Camburu, Pasquale Minervini, and Pontus Stenetorp. 2024. https://doi.org/10.18653/v1/2024.acl-long.728 Using natural language explanations to improve robustness of in-context learning . In Proceedings of the 62nd Annual Meeting of the Associat...

    2024 doi

  3. [11]

    Peter Jansen, Elizabeth Wainwright, Steven Marmorstein, and Clayton Morrison. 2018. https://aclanthology.org/L18-1433/ W orld T ree: A corpus of explanation graphs for elementary science questions supporting multi-hop inference . In Proceedings of the Eleventh International Co...

    2018

  4. [12]

    Albert Jiang, Konrad Czechowski, Mateja Jamnik, Piotr Milos, Szymon Tworkowski, Wenda Li, and Yuhuai Tony Wu. 2022 a . Thor: Wielding hammers to integrate language models and automated theorem provers. In NeurIPS

    2022

  5. [13]

    Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timoth \'e e Lacroix, Yuhuai Wu, and Guillaume Lample. 2022 b . https://api.semanticscholar.org/CorpusID:253098549 Draft, sketch, and prove: Guiding formal theorem provers with informal p...

    2022 arXiv

  6. [14]

    Dongwei Jiang, Marcio Fonseca, and Shay Cohen. 2024. https://doi.org/10.18653/v1/2024.naacl-long.416 L ean R easoner: Boosting complex logical reasoning with lean . In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguis...

    2024 doi

  7. [15]

    Tushar Khot, Peter Clark, Michal Guerquin, Peter Alexander Jansen, and Ashish Sabharwal. 2019. QASC : A dataset for question answering via sentence composition. In AAAI

    2019

  8. [16]

    Shashank Kirtania, Priyanshu Gupta, and Arjun Radhakrishna. 2024. https://aclanthology.org/2024.nlrse-1.6/ LOGIC - LM ++: Multi-step refinement for symbolic formulations . In Proceedings of the 2nd Workshop on Natural Language Reasoning and Structured Explanations (@ACL 2024),...

    2024

  9. [17]

    Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and Shay B. Cohen. 2025. https://arxiv.org/abs/2502.13137 Theorem prover as a judge for synthetic data generation . Preprint, arXiv:2502.13137

    2025

  10. [18]

    Jinu Lee, Qi Liu, Runzhi Ma, Vincent Han, Ziqi Wang, Heng Ji, and Julia Hockenmaier. 2025. https://arxiv.org/abs/2502.16757 Entailment-preserving first-order logic representations in natural language entailment . Preprint, arXiv:2502.16757

    2025 arXiv

  11. [19]

    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. 2024. https://openreview.net/forum?id=zlw6AHwukB A survey on deep learning for theorem proving . In First Conference on Language Modeling

    2024

  12. [20]

    Tongxuan Liu, Wenjiang Xu, Weizhe Huang, Yuting Zeng, Jiaxing Wang, Xingyu Wang, Hailong Yang, and Jing Li. 2025. https://arxiv.org/abs/2409.17539 Logic-of-thought: Injecting logic into contexts for full reasoning in large language models . Preprint, arXiv:2409.17539

    2025 arXiv

  13. [21]

    Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, and Zhijiang Guo. 2024 a . https://arxiv.org/abs/2410.10135 Formalalign: Automated alignment evaluation for autoformalization . Preprint, arXiv:2410.10135

    2024 arXiv

  14. [22]

    Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, and Zhijiang Guo. 2024 b . https://arxiv.org/abs/2406.01940 Process-driven autoformalization in lean 4 . Preprint, arXiv:...

    2024 arXiv

  15. [23]

    Maienborn, K

    C. Maienborn, K. von Heusinger, and P. Portner. 2011. https://books.google.co.uk/books?id=-026poXzQDMC Semantics: An International Handbook of Natural Language Meaning . Number v. 1 in Handbooks of Linguistics and Communication Science. De Gruyter Mouton

    2011

  16. [24]

    Aaron Meurer et al. 2017. https://doi.org/10.7717/peerj-cs.103 SymPy: symbolic computing in Python . PeerJ Comput. Sci., 3:e103

    2017 doi

  17. [25]

    Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002. Isabelle/HOL: a proof assistant for higher-order logic. Springer

    2002

  18. [26]

    Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. https://doi.org/10.18653/v1/2023.emnlp-main.313 LINC : A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers . ...

    2023 doi

  19. [27]

    OpenAI. 2023. https://doi.org/10.48550/ARXIV.2303.08774 GPT-4 technical report . CoRR, abs/2303.08774

    2023 doi arXiv

  20. [28]

    Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang. 2023. https://doi.org/10.18653/v1/2023.findings-emnlp.248 Logic- LM : Empowering large language models with symbolic solvers for faithful logical reasoning . In Findings of the Association for Computational Linguistics...

    2023 doi

  21. [29]

    Terence Parsons. 1990. Events in the Semantics of English: A Study in Subatomic Semantics. MIT Press

    1990

  22. [30]

    Lawrence Charles Paulson and Jasmin Christian Blanchette. 2012. https://api.semanticscholar.org/CorpusID:598752 Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers . In IWIL@LPAR

    2012

  23. [31]

    Stanislas Polu and Ilya Sutskever. 2020. https://arxiv.org/abs/2009.03393 Generative language modeling for automated theorem proving . Preprint, arXiv:2009.03393

    2020 arXiv

  24. [32]

    Becker, Arto Hellas, Paul Denny, and Brent N

    Seth Poulsen, Sami Sarsa, James Prather, Juho Leinonen, Brett A. Becker, Arto Hellas, Paul Denny, and Brent N. Reeves. 2024. https://doi.org/10.1145/3626252.3630928 Solving proof block problems using large language models . In Proceedings of the 55th ACM Technical Symposium on...

    2024

  25. [33]

    Chengwen Qi, Ren Ma, Bowen Li, He Du, Binyuan Hui, Jinwang Wu, Yuanjun Laili, and Conghui He. 2025. https://arxiv.org/abs/2502.06563 Large language models meet symbolic provers for logical reasoning evaluation . Preprint, arXiv:2502.06563

    2025 arXiv

  26. [34]

    Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. 2024 a . https://aclanthology.org/2024.eacl-long.1/ Enhancing ethical explanations of large language models through iterative symbolic refinement . In Proceedings of the 18th Conference of the European Chapter of the...

    2024

  27. [35]

    Dennis, and Andre Freitas

    Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024 b . https://doi.org/10.18653/v1/2024.emnlp-main.172 Verification and refinement of natural language explanations through LLM -symbolic theorem proving . In Proceedings of the 2024 Conference on Empirical Meth...

    2024 doi

  28. [36]

    Mohammad Raza and Natasa Milic-Frayling. 2025. https://arxiv.org/abs/2501.16961 Instantiation-based formalization of logical reasoning tasks using language models and logical solvers . Preprint, arXiv:2501.16961

    2025 arXiv

  29. [37]

    Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. 2024. https://arxiv.org/abs/2310.04353 An in-context learning agent for formal theorem-proving . Preprint, arXiv:2310.04353

    2024 arXiv

  30. [38]

    Mokanarangan Thayaparan, Marco Valentino, and André Freitas. 2020. https://arxiv.org/abs/2010.00389 A survey on explainability in machine reading comprehension . Preprint, arXiv:2010.00389

    2020 arXiv

  31. [39]

    Marco Valentino, Mokanarangan Thayaparan, and Andr \'e Freitas. 2022. https://aclanthology.org/2022.coling-1.134/ Case-based abductive natural language inference . In Proceedings of the 29th International Conference on Computational Linguistics, pages 1556--1568, Gyeongju, Rep...

    2022

  32. [41]

    Sean Welleck and Rahul Saha. 2023 b . https://arxiv.org/abs/2310.18457 Llmstep: Llm proofstep suggestions in lean . Preprint, arXiv:2310.18457

    2023 arXiv

  33. [42]

    Sarah Wiegreffe and Ana Marasović. 2021. https://arxiv.org/abs/2102.12060 Teach me to explain: A review of datasets for explainable natural language processing . Preprint, arXiv:2102.12060

    2021 arXiv

  34. [43]

    Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. https://proceedings.neurips.cc/paper_files/paper/2022/file/d0c6bc641a56bebee9d985b937307367-Paper-Conference.pdf Autoformalization with large language models . I...

    2022

  35. [44]

    Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024 a . https://arxiv.org/abs/2405.14333 Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data . Preprint, arXiv:2405.14333

    2024 arXiv

  36. [45]

    Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. 2024 b . https://arxiv.org/abs/2408.08152 Deepseek-prover-v1.5: Harnessi...

    2024 arXiv

  37. [46]

    Lan Zhang, Xin Quan, and Andre Freitas. 2024. https://doi.org/10.18653/v1/2024.emnlp-main.233 Consistent autoformalization for constructing mathematical libraries . In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 4020--4033, Mia...

    2024 doi

  38. [47]

    Xueliang Zhao, Wenda Li, and Lingpeng Kong. 2023. https://arxiv.org/abs/2305.16366 Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving . Preprint, arXiv:2305.16366

    2023 arXiv

  39. [48]

    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...

  40. [49]

    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.