Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition
Paper · 2026 · Lei Xu, Pierre Beckmann, Marco Valentino et al.
Summary
Most neuro-symbolic systems pair an LLM with a single logical solver, or require the reasoning paradigm to be fixed in advance. This makes them hard to use on mixed problem sets whose reasoning type is not known. The authors propose an adaptive framework that works in three stages:
- An LLM breaks a natural-language problem into structured sub-questions and labels each with a reasoning type (LP, FOL, CSP or SMT).
- A router sends each sub-question to the matching symbolic engine, such as Pyke for LP or Prover9 for FOL.
- An LLM autoformalizes the input into that engine's syntax before the engine solves it.
Evaluation covers ProntoQA, ProofWriter, FOLIO, LogDed, TREC trials, a mixed dataset and new multi-question stress tests. Frontier LLMs identify the needed paradigm very reliably. Dynamic solver composition clearly beats pure prompting baselines. The main bottleneck is producing valid formal code, especially for small models, and fine-tuning helps substantially. The work shows that LLMs can act as orchestrators for multiple formal solvers.
Key points
- Reasoning-type identification exceeds 90% accuracy, and large frontier models reach over 98%.
- On the mixed dataset with GPT-4o, the framework scores 92.1%. This is 17.0 points above zero-shot, 21.4 above CoT and 23.7 above Symbolic CoT.
- On sequences of heterogeneous questions, pure LLM methods reach only 27.3%, while the framework reaches up to 54.4%.
- Small models (Llama-3.1-8B, Qwen-2.5-7B, Qwen-2.5-Coder-7B) struggle, with 60–80% of their errors caused by invalid formalization. Fine-tuning on frontier-model demonstrations raises them to 41.0%, 50.1% and 59.6%.
- The code and data are released at github.com/idiap/adaptive_symbolic_reasoning.
Institutions
Fields, topics and concepts
📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 16,667 worksArtificial Intelligence · 16,194 worksArts and Humanities · 16,039 worksLanguage and Linguistics · 15,891 works
🧭 Topics 2Research subjects and languages the work is about.Language models & pretraining · 3,320 worksReasoning · 1,426 works
Cite
Cite as Lei Xu, Pierre Beckmann, Marco Valentino and Andre Freitas. 2026. Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition. Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers).
@inproceedings{xu2026adaptive,
title = {{Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition}},
author = {Lei Xu, Pierre Beckmann, Marco Valentino and Andre Freitas},
booktitle = {Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers)},
year = {2026},
doi = {10.18653/v1/2026.eacl-long.54},
url = {https://doi.org/10.18653/v1/2026.eacl-long.54}
}References
- Benjamin Callewaert, Simon Vandevelde, and Joost Vennekens. 2025. Verus-lm: a versatile framework for combining llms with symbolic reasoning. arXiv preprint arXiv:2501.14540. find
- Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient smt solver. In Tools and Algorithms for the Construction and Analysis of Systems, pages 337– 340, Berlin, Heidelberg. Springer Berlin Heidelberg. find
- DeepSeek-AI. 2024. Deepseek-v3 technical report. Preprint, arXiv:2412.19437. find
- Bruce Frederiksen. 2008. Applying expert system technology to code reuse with pyke. PyCon: Chicago. find
- Formalization Bottleneck. The framework’s performance is fundamentally limited by the quality of auto-formalization. Invalid formalization constitutes the primary error source for smaller models, indicating that the translation from natural language to formal representations remains a critical bottl… find
- Daya Guo, Dejian Yang, Haowei Zhang, Ruoyu Zhang Junxiao Song, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, and et al. Xiao Bi. 2025. Deepseekr1: Incentivizing reasoning capability in llms via reinforcement learning. Preprint, arXiv:2501.12948.
- Solver Coverage. While our framework supports four solver types (LP, FOL, CSP, SMT), it does not cover the full spectrum of formal reasoning paradigms. Mathematical reasoning, probabilistic inference, temporal logic, and other specialized reasoning domains are not addressed. However, the proposed mo… find
- Adam Ishay, Zhun Yang, and Joohyung Lee. 2023. Leveraging large language models to generate answer set programs. In Proceedings of the 20th International Conference on Principles of Knowledge Representation and Reasoning. \#\# Acknowledgments This work was partially funded by the Swiss National Scienc… find
- Franciszek Górski, Oskar Wysocki, Marco Valentino, and Andre Freitas. 2025. Integrating expert knowledge into logical programs via llms. arXiv preprint arXiv:2502.12275. — [arXiv:2502.12275](https://arxiv.org/abs/2502.12275) find
- Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle-Solano, Hannah Szabó, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, and 16 others. 2024. FOLIO:…
- Rushang Karia, Daniel Bramblett, Daksh Dobhal, Pulkit Verma, and Siddharth Srivastava. 2024. ∀uto∃val: Autonomous assessment of llms in formal synthesis and interpretation tasks. Preprint, arXiv:2403.18327. — [arXiv:2403.18327](https://arxiv.org/abs/2403.18327) find
- Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. 2022. Large language models are zero-shot reasoners. arXiv preprint arXiv: 2205.11916.
- Llama team. 2024. The llama 3 herd of models. arXiv preprint arXiv: 2407.21783.
- Tharindu Madusanka, Marco Valentino, Iqra Zahid, Ian Pratt-Hartmann, and Riza Theresa Batista-Navarro. 2025. Unravelling the logic: Investigating the generalisation of transformers in numerical satisfiability problems. In Proceedings of the 63rd Annual Meeting of the Association for Computational Li… find
- Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2025b. Faithful and robust LLM-driven theorem proving for NLI explanations. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 17734–17755, Vienna, Austria. Associat… find
- W. McCune. 2005–2010. Prover9 and mace4. http://www.cs.unm.edu/~mccune/mace4/. ↗
- Qwen Team. 2024. Qwen2.5 technical report. arXiv preprint arXiv: 2412.15115. find
- Nicholas Nethercote, Peter J Stuckey, Ralph Becket, Sebastian Brand, Gregory J Duck, and Guido Tack. 2007. Minizinc: Towards a standard cp modelling language. In International conference on principles and practice of constraint programming, pages 529– 543. Springer. find
- Hyun Ryu, Gyeongman Kim, Hyemin S Lee, and Eunho Yang. 2025. Divide and translate: Compositional first-order logic translation and verification for complex logical reasoning. In The Thirteenth International Conference on Learning Representations. find
- Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua 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 on Empirical Methods in Natural Lan…
- OpenAI. 2024. Gpt-4o system card. arXiv preprint arXiv: 2410.21276.
- Liangming Pan, Alon Albalak, Xinyi Wang, and William 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.
- Zhuoshi Pan, Qizhi Pei, Yu Li, Qiyao Sun, Zinan Tang, H. Vicky Zhao, Conghui He, and Lijun Wu. 2025. Rest: Stress testing large reasoning models by asking multiple problems at once. Preprint, arXiv:2507.10541.
- Xin Quan, Marco Valentino, Danilo Carvalho, Dhairya Dalal, and Andre Freitas. 2025a. PEIRCE: Unifying material and formal reasoning via LLM-driven neuro-symbolic refinement. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations),… find
- Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. 2024a. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), p… find
- Xin Quan, Marco Valentino, Louise A. Dennis, and Andre Freitas. 2024b. Verification and refinement of natural language explanations through LLM-symbolic theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 2933–2958, Miami, Florida, USA. A…
- 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.
- Ian Soboroff. 2021. Overview of trec 2021. In TREC. find
- Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowycz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W. Kocurek, Ali Safaya, Ali Tazarv, an… — Beyond the Imitation Game: Quantifying and extrapolating the capabilities of language models
- Trans. Mach. Learn. Res., 2023. find
- Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. 2021. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634, Online. Association for Computational Linguistics.
- Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. Advances in neural information processing systems, 35:32353–32368.
- Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. 2024. Faithful logical reasoning via symbolic chain-of-thought. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 13326–13365, Bangkok, Thailand. Associat…
- Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2023a. Harnessing the power of large language models for natural language to first-order logic translation. arXiv preprint arXiv:2305.15541. find
- Zhun Yang, Adam Ishay, and Joohyung Lee. 2023b. Coupling large language models with logic programming for robust and general reasoning from text. In Findings of the Association for Computational Linguistics: ACL 2023, pages 5186–5219. find
- Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. Satlm: Satisfiability-aided language models using declarative prompting. In Proceedings of NeurIPS. find
- Lan Zhang, Marco Valentino, and Andre Freitas. 2025. Autoformalization in the wild: Assessing llms on real-world mathematical definitions. Preprint, arXiv:2502.12065. find
- Yue Zhang, Yafu Li, Leyang Cui, Deng Cai, Lemao Liu, Tingchen Fu, Xinting Huang, Enbo Zhao, Yu Zhang, Yulong Chen, Longyue Wang, Anh Tuan Luu, Wei Bi, Freda Shi, and Shuming Shi. 2023. Siren’s song in the ai ocean: A survey on hallucination in large language models. arXiv preprint arXiv: 2309.01219.
- Yaowei Zheng, Richong Zhang, Junhao Zhang, Yanhan Ye, Zheyan Luo, Zhangchi Feng, and Yongqiang Ma. 2024. Llamafactory: Unified efficient fine-tuning of 100+ language models. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 3: System Demonstrations),…
Updated
This page in Markdown → https://md.research.elamur.ai/free/en/papers/xu-2026-adaptive-llm-symbolic-reasoning-dynamic/