pith. machine review for the scientific record. sign in

arxiv: 2605.04941 · v1 · submitted 2026-05-06 · 💻 cs.CL

Recognition: unknown

UFAL-CUNI at SemEval-2026 Task 11: An Efficient Modular Neuro-symbolic Method for Syllogistic Reasoning

Ivan Kart\'a\v{c}, Jan Bronec, Krist\'yna Onderkov\'a, Mateusz Lango, Ond\v{r}ej Du\v{s}ek, Zden\v{e}k Kasner

Authors on Pith no claims yet

Pith reviewed 2026-05-08 16:26 UTC · model grok-4.3

classification 💻 cs.CL
keywords neuro-symbolicsyllogistic reasoningfirst-order logictheorem proverlarge language modelscontent effectmodular systemSemEval task
0
0 comments X

The pith

A modular neuro-symbolic system parses syllogisms into first-order logic with a 4B LLM then applies a theorem prover to reach conclusions with competitive accuracy and reduced content effects.

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

The paper describes a system for SemEval-2026 Task 11 that uses a small language model to translate natural language syllogisms into first-order logic statements and feeds those statements to an automated theorem prover for deduction. This modular design separates formal logical steps from the surface content of the premises to reduce unwanted biases. Experiments demonstrate that the approach reaches competitive accuracy on most subtasks while showing lower content effects than direct LLM methods. Ablation results indicate the system outperforms pure zero-shot LLM baselines in the 4B parameter range, though multilingual handling remains limited when relying on the small models for parsing.

Core claim

The central claim is that translating natural language syllogisms to first-order logic via a 4B-parameter LLM and then using an automated theorem prover produces accurate reasoning with relatively low content effect, outperforming standalone LLM zero-shot baselines in the same size range on the task subtasks.

What carries the argument

The LLM-based parser that converts natural language syllogisms to first-order logic representations, paired with an automated theorem prover for deduction.

Load-bearing premise

The small LLM must produce accurate translations of natural language syllogisms into first-order logic that preserve the intended logical meaning for the prover to operate on the correct structure.

What would settle it

If the system's accuracy stays high on syllogisms where the parser makes systematic translation errors while content-only baselines also succeed, this would indicate the symbolic step is not driving the results.

Figures

Figures reproduced from arXiv: 2605.04941 by Ivan Kart\'a\v{c}, Jan Bronec, Krist\'yna Onderkov\'a, Mateusz Lango, Ond\v{r}ej Du\v{s}ek, Zden\v{e}k Kasner.

Figure 1
Figure 1. Figure 1: Overview of our system: 1 Machine Translation translates multilingual inputs to English (for subtasks 3 and 4); 2 FOL Parser translates natural language propositions into FOL formulas in LaTeX format; 3 Transpiler rewrites LaTeX formulas to the target Prover9 syntax; 4 Prover9 determines the validity of the syllogism; 5 Relevance Retrieval removes irrelevant premises by using the prover to check which prem… view at source ↗
Figure 3
Figure 3. Figure 3: Sensitivity of the combined score (CS) metric view at source ↗
Figure 4
Figure 4. Figure 4: Prompt template for the FOL parser. For each natural language proposition, the LLM is instructed to view at source ↗
Figure 5
Figure 5. Figure 5: Prompt template for the FOL parser used to parse the initial proposition of a syllogism. view at source ↗
Figure 6
Figure 6. Figure 6: Prompt template for translation used in subtasks 3 and 4. view at source ↗
Figure 7
Figure 7. Figure 7: Prompt template for translation self-evaluation. view at source ↗
Figure 8
Figure 8. Figure 8: Prompt template for translation with feedback provided by the self-evaluation step. view at source ↗
Figure 9
Figure 9. Figure 9: Prompt template for the zero-shot end-to-end baseline. view at source ↗
Figure 10
Figure 10. Figure 10: Prompt template for the zero-shot end-to-end baseline with relevant premise identification. view at source ↗
Figure 11
Figure 11. Figure 11: Prompt template for the ablation where the FOL parser parses propositions directly to the Prover9 syntax. view at source ↗
Figure 12
Figure 12. Figure 12: Prompt template for the initial step in the ablation where the FOL parser parses propositions directly to view at source ↗
Figure 13
Figure 13. Figure 13: Prompt template for the FOL parser used for single-step parsing. Unlike the multi-step setup, the LLM is view at source ↗
Figure 14
Figure 14. Figure 14: Prompt template for the LLM prover. You are given a syllogism that has been determined to be valid. Your task is to identify which premises are actually relevant (necessary) for the conclusion to follow. Premises: {premises} Conclusion: {conclusion} Return ONLY a JSON array of 0-based indices of the relevant premises. For example: [0, 2] view at source ↗
Figure 15
Figure 15. Figure 15: Prompt template for the LLM-based relevant premise retrieval. view at source ↗
read the original abstract

This paper describes our system submitted to SemEval-2026 Task 11: Disentangling Content and Formal Reasoning in Large Language Models. We present an efficient modular neuro-symbolic approach, combining a symbolic prover with small reasoning LLMs (4B parameters). The system consists of an LLM-based parser that translates natural language syllogisms to a first-order logic (FOL) representation, an automated theorem prover, and two optional modules: machine translation for multilingual inputs and a symbolic retrieval component for the identification of relevant premises. The system achieves competitive accuracy and relatively low content effect on most subtasks. Our ablations show that this approach outperforms LLM-based zero-shot baselines in this parameter size range, but also reveal limited multilingual capabilities of small LLMs. Finally, we include a discussion of the task's main ranking metric and analyze its limitations.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript describes a modular neuro-symbolic system submitted to SemEval-2026 Task 11 on disentangling content and formal reasoning in LLMs. It uses a 4B-parameter LLM to parse natural-language syllogisms into first-order logic, feeds the output to an automated theorem prover, and optionally adds machine translation for multilingual inputs and symbolic retrieval for relevant premises. The system is claimed to deliver competitive accuracy with relatively low content effect on most subtasks, to outperform zero-shot LLM baselines in the 4B-parameter regime, and to expose limitations of small LLMs in multilingual settings; the paper also critiques the task's primary ranking metric.

Significance. If the reported performance numbers and ablations hold, the work demonstrates that small LLMs can be paired with symbolic reasoning components to achieve stronger formal inference and reduced content bias than pure neural baselines of comparable size. The emphasis on modularity, efficiency, and explicit discussion of the task metric are constructive contributions to the neuro-symbolic reasoning literature.

major comments (2)
  1. [§4] §4 (Results and Ablations): The central claim that the neuro-symbolic architecture is responsible for competitive accuracy and low content effect rests on the assumption that the 4B LLM parser produces accurate FOL translations. No independent parser evaluation (exact-match accuracy, semantic equivalence, or error analysis on a held-out syllogism set) is reported, so it remains possible that the LLM is still performing implicit reasoning and the prover contributes little; this directly weakens the modularity argument and the attribution of gains to the symbolic component.
  2. [§4.2] §4.2 (Ablation tables): The outperformance versus zero-shot baselines is presented as evidence for the modular approach, yet without parser-level metrics it is impossible to isolate whether the theorem prover or the retrieval module drives the improvement; a minimal additional ablation that replaces the parser with gold FOL would be required to substantiate the neuro-symbolic benefit.
minor comments (2)
  1. [§3] §3 (System description): The FOL representation and the interface between parser and prover are described at a high level; a short example showing an input syllogism, its parsed FOL, and the prover output would clarify the pipeline for readers.
  2. [Table 1] Table 1 and §5 (Multilingual results): The reported drop in multilingual performance is noted but not accompanied by an error breakdown (e.g., translation vs. parsing vs. reasoning failures); adding one or two representative failure cases would strengthen the discussion of small-LLM limitations.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for the thoughtful and constructive comments on our submission. We address each major comment below, clarifying our design choices and indicating where revisions are feasible.

read point-by-point responses

  1. Referee: §4 (Results and Ablations): The central claim that the neuro-symbolic architecture is responsible for competitive accuracy and low content effect rests on the assumption that the 4B LLM parser produces accurate FOL translations. No independent parser evaluation (exact-match accuracy, semantic equivalence, or error analysis on a held-out syllogism set) is reported, so it remains possible that the LLM is still performing implicit reasoning and the prover contributes little; this directly weakens the modularity argument and the attribution of gains to the symbolic component.

    Authors: We agree that standalone parser evaluation would strengthen attribution of gains to the symbolic component. Our existing ablations demonstrate that disabling the theorem prover reduces accuracy relative to the full pipeline, but we acknowledge this is indirect evidence. In the revision we will add a qualitative error analysis of parser outputs on a random sample of 100 syllogisms, reporting common failure modes such as quantifier scope errors and predicate misalignments. revision: yes

  2. Referee: §4.2 (Ablation tables): The outperformance versus zero-shot baselines is presented as evidence for the modular approach, yet without parser-level metrics it is impossible to isolate whether the theorem prover or the retrieval module drives the improvement; a minimal additional ablation that replaces the parser with gold FOL would be required to substantiate the neuro-symbolic benefit.

    Authors: A gold-FOL ablation would indeed provide the strongest isolation of the prover's contribution. Unfortunately, SemEval-2026 Task 11 supplies only natural-language premises, conclusions, and labels; no gold FOL translations are released. Performing the suggested ablation would require creating such annotations from scratch, which exceeds the resources available for the shared-task submission. Our reported ablations instead compare the complete pipeline against LLM-only and module-ablated variants using the task-provided data. revision: no

standing simulated objections not resolved
  • The requested gold-FOL parser ablation cannot be conducted because the task does not provide (and we did not create) gold-standard first-order logic translations.

Circularity Check

0 steps flagged

No circularity: empirical system description on external benchmark

full rationale

The paper is a standard SemEval system submission describing a modular neuro-symbolic pipeline and reporting accuracy on the shared-task test set. No derivations, equations, fitted parameters, or predictions appear; all claims reduce to direct empirical measurements and ablations against zero-shot baselines. No self-citations are load-bearing for any uniqueness theorem or ansatz, and the central performance numbers are externally verifiable on the task data.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No new mathematical axioms, free parameters, or invented entities are introduced; the work relies on standard first-order logic and existing LLM capabilities.

pith-pipeline@v0.9.0 · 5484 in / 1104 out tokens · 35114 ms · 2026-05-08T16:26:37.088367+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

23 extracted references · 14 canonical work pages · 1 internal anchor

  1. [1]

    Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers),

    Tiwalayo Eisape and Michael Henry Tessler and Ishita Dasgupta and Fei Sha and Sjoerd van Steenkiste and Tal Linzen , bibsource =. Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Volume 1: Long Papers),. doi:10.18653/V1/2024.NAACL-LONG.466 , editor =

    work page doi:10.18653/v1/2024.naacl-long.466 2024

  2. [2]

    Proceedings of the 20th International Workshop on Semantic Evaluation (SemEval-2026) , title =

    Valentino, Marco and Ranaldi, Leonardo and Pucci, Giulia and Ranaldi, Federico and Freitas, Andr. Proceedings of the 20th International Workshop on Semantic Evaluation (SemEval-2026) , title =

    2026

  3. [3]

    Findings of the Association for Computational Linguistics,

    Geonhee Kim and Marco Valentino and Andr. Findings of the Association for Computational Linguistics,

  4. [4]

    and Gu, Alex and Lipkin, Benjamin and Zhang, Cedegao E

    Theo Olausson and Alex Gu and Benjamin Lipkin and Cedegao E. Zhang and Armando Solar. Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing,. doi:10.18653/V1/2023.EMNLP-MAIN.313 , editor =

    work page doi:10.18653/v1/2023.emnlp-main.313 2023

  5. [5]

    doi: 10.18653/v1/2023.findings-emnlp.248

    Liangming Pan and Alon Albalak and Xinyi Wang and William Yang Wang , bibsource =. Findings of the Association for Computational Linguistics:. doi:10.18653/V1/2023.FINDINGS-EMNLP.248 , editor =

    work page doi:10.18653/v1/2023.findings-emnlp.248 2023

  6. [6]

    PNAS nexus , number =

    Lampinen, Andrew K and Dasgupta, Ishita and Chan, Stephanie CY and Sheahan, Hannah R and Creswell, Antonia and Kumaran, Dharshan and McClelland, James L and Hill, Felix , doi =. PNAS nexus , number =

  7. [7]

    The Eleventh International Conference on Learning Representations,

    Abulhair Saparov and He He , bibsource =. The Eleventh International Conference on Learning Representations,

  8. [8]

    Evans, J St BT and Barston, Julie L and Pollard, Paul , journal =

  9. [9]

    Klauer, Karl Christoph and Musch, Jochen and Naumer, Birgit , journal =

  10. [10]

    Fortieth

    Marco Valentino and Geonhee Kim and Dhairya Dalal and Zhixue Zhao and Andr. Fortieth. doi:10.1609/AAAI.V40I39.40617 , editor =

    work page doi:10.1609/aaai.v40i39.40617

  11. [11]

    Journal of Statistical Theory and Practice , month =

    Li, Ta-Hsin and Megiddo, Nimrod , day =. Journal of Statistical Theory and Practice , month =. doi:10.1007/s42519-026-00545-8 , issn =

    work page doi:10.1007/s42519-026-00545-8

  12. [12]

    arXiv , author =:2505.09388 , primaryclass =

    work page internal anchor Pith review arXiv

  13. [13]

    Gemma 3 Technical Report

    Gemma Team , bibsource =. CoRR , timestamp =. doi:10.48550/ARXIV.2503.19786 , eprint =

    work page Pith review doi:10.48550/arxiv.2503.19786

  14. [14]

    Tversky, Amos and Kahneman, Daniel , journal =

  15. [15]

    Smith, Robin , booktitle =

  16. [16]

    Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing,

    Leonardo Bertolazzi and Albert Gatt and Raffaella Bernardi , bibsource =. Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing,. doi:10.18653/V1/2024.EMNLP-MAIN.769 , editor =

    work page doi:10.18653/v1/2024.emnlp-main.769 2024

  17. [17]

    Faithful logical reasoning via symbolic chain-of-thought , url =

    Jundong Xu and Hao Fei and Liangming Pan and Qian Liu and Mong. Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers),. doi:10.18653/V1/2024.ACL-LONG.720 , editor =

    work page doi:10.18653/v1/2024.acl-long.720 2024

  18. [18]

    doi:10.18653/v1/2025.findings-emnlp.926 , editor =

    Zhou, Yujun and Ye, Jiayi and Ling, Zipeng and Han, Yufei and Huang, Yue and Zhuang, Haomin and Liang, Zhenwen and Guo, Kehan and Guo, Taicheng and Wang, Xiangqi and Zhang, Xiangliang , booktitle =. doi:10.18653/v1/2025.findings-emnlp.926 , editor =

    work page doi:10.18653/v1/2025.findings-emnlp.926 2025

  19. [19]

    Goodman , bibsource =

    Gabriel Poesia and Kanishk Gandhi and Eric Zelikman and Noah D. Goodman , bibsource =. Trans. Mach. Learn. Res. , timestamp =

  20. [20]

    Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies,

    Tongxuan Liu and Wenjiang Xu and Weizhe Huang and Yuting Zeng and Jiaxing Wang and Xingyu Wang and Hailong Yang and Jing Li , bibsource =. Proceedings of the 2025 Conference of the Nations of the Americas Chapter of the Association for Computational Linguistics: Human Language Technologies,. doi:10.18653/V1/2025.NAACL-LONG.510 , editor =

    work page doi:10.18653/v1/2025.naacl-long.510 2025

  21. [21]

    Edward J Hu, Yelong Shen, Phillip Wallis, Zeyuan Allen-Zhu, Yuanzhi Li, Shean Wang, Liang Wang, Weizhu Chen, and 1 others

    Alejandro Salamanca and Diana Abagyan and Daniel D'souza and Ammar Khairi and David Mora and Saurabh Dash and Viraat Aryabumi and Sara Rajaee and Mehrnaz Mofakhami and Ananya Sahu and Thomas Euyang and Brittawnya Prince and Madeline Smith and Hangyu Lin and Acyr Locatelli and Sara Hooker and Tom Kocmi and Aidan N. Gomez and Ivan Zhang and Phil Blunsom and...

    work page doi:10.48550/arxiv.2603.11510

  22. [22]

    Dennis and Andr

    Xin Quan and Marco Valentino and Louise A. Dennis and Andr. Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing,. doi:10.18653/V1/2024.EMNLP-MAIN.172 , editor =

    work page doi:10.18653/v1/2024.emnlp-main.172 2024

  23. [23]

    CoRR , timestamp =

    Shashank Kirtania and Priyanshu Gupta and Arjun Radhakirshna , bibsource =. CoRR , timestamp =. doi:10.48550/ARXIV.2407.02514 , eprint =

    work page doi:10.48550/arxiv.2407.02514