Formal Proof Generation in Deductive Logic Systems with Open LLMs: An Empirical Study on Natural Deduction and Analytical Tableau

• Luana Stanz Oliveira Magalhães UFC
• Taís Rodrigues Sandes UFC
• Victor Aguiar Evangelista de Farias UFC
• Maria Viviane de Menezes UFC
• Carlos de Oliveira Caminha Neto UFC
• Davi Romero de Vasconcelos UFC

DOI: https://doi.org/10.5753/eniac.2026.31290

Resumo

Large Language Models (LLMs) have expanded the possibilities of automated reasoning, motivating interest in their ability to perform structured inferences. Logical deductive systems such as Natural Deduction and Analytical Tableau impose strict syntactic and semantic constraints, making them suitable benchmarks for evaluating formal reasoning capabilities. Despite recent progress, LLMs continue to exhibit notable limitations in constructing complete and formally valid proofs. In this paper, we investigate the performance of 7 small and medium-sized open-source LLMs (Phi-4, gpt-oss-20B, Mistral-small-3.2-24B-instruct-2506, Gemma-4-26B, Qwen3-32B, Qwen3.5-35B and gpt-oss-120B) in generating logical proofs within these two deductive systems. Proofs are generated from syntax based and rule extended prompts, in both zero shot and few shot settings. The correctness of the generated proofs is then assessed through formal verification using external proof checkers grounded in the inference rules of Natural Deduction and Analytical Tableau, ensuring rigorous rule-based validation. Our findings suggest that, in their current state, while models are capable of generating formally valid proofs under certain conditions, overall performance remains limited. Few-shot prompting consistently improves proof generation accuracy, and prompts augmented with explicit rule descriptions generally outperform syntax-only formulations. Furthermore, model size alone is not a reliable predictor of success, as smaller models occasionally approach or surpass the performance of larger alternatives.

Referências

Abd, S. E. and et al. (2026). Gemma 4 technical report. CoRR, abs/2607.02770.

Abdin, M., Aneja, J., Behl, H., Bubeck, S., Eldan, R., Gunasekar, S., Harrison, M., Hewett, R. J., Javaheripi, M., Kauffmann, P., et al. (2024). Phi-4 technical report. arXiv preprint arXiv:2412.08905.

Agarwal, S., Ahmad, L., Ai, J., Altman, S., Applebaum, A., Arbus, E., Arora, R. K., Bai, Y., Baker, B., Bao, H., et al. (2025). gpt-oss-120b & gpt-oss-20b model card. arXiv preprint arXiv:2508.10925.

Arkoudas, K. and Batzoglou, S. (2025). Stress-testing the reasoning competence of language models with formal proofs. In Findings of the Association for Computational Linguistics: EMNLP 2025, pages 12376–12394.

Brown, T., Mann, B., Ryder, N., Subbiah, M., Kaplan, J. D., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., et al. (2020). Language models are few-shot learners. Advances in neural information processing systems, 33:1877–1901.

Cobbe, K., Kosaraju, V., Bavarian, M., Chen, M., Jun, H., Kaiser, L., Plappert, M., Tworek, J., Hilton, J., Nakano, R., Hesse, C., and Schulman, J. (2021). Training verifiers to solve math word problems. volume abs/2110.14168.

Creswell, A., Shanahan, M., and Higgins, I. (2023). Selection-inference: Exploiting large language models for interpretable logical reasoning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net.

et al., S. H. (2024a). FOLIO: natural language reasoning with first-order logic. In Al-Onaizan, Y., Bansal, M., and Chen, Y., editors, Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Miami, Florida, USA, November 12–16, 2024, pages 22017–22031. Association for Computational Linguistics.

et al., S. H. (2024b). P-FOLIO: evaluating and improving logical reasoning with abundant human-written reasoning chains. In Al-Onaizan, Y., Bansal, M., and Chen, Y., editors, Findings of the Association for Computational Linguistics: EMNLP 2024, Miami, Florida, USA, November 12–16, 2024, volume 2024 of Findings of the Association for Computational Linguistics, pages 16553–16565. Association for Computational Linguistics.

Huth, M. and Ryan, M. D. (2004). Logic in computer science - modelling and reasoning about systems (2. ed.). Cambridge University Press.

Li, X., He, S., Lei, F., JunYang, J., Su, T., Liu, K., and Zhao, J. (2024a). Teaching small language models to reason for knowledge-intensive multi-hop question answering. ACL 2024:7804–7816.

Li, X., He, S., Wu, J., Yang, Z., Xu, Y., jun Jun, Y., Liu, H., Liu, K., and Zhao, J. (2024b). Mode-cotd: Chain-of-thought distillation for complex reasoning tasks with mixture of decoupled lora-experts. pages 11475–11485.

Lin, B. Y., Le Bras, R., Richardson, K., Sabharwal, A., Poovendran, R., Clark, P., and Choi, Y. (2025). Zebralogic: On the scaling limits of llms for logical reasoning. In Singh, A., Fazel, M., Hsu, D., Lacoste-Julien, S., Berkenkamp, F., Maharaj, T., Wagstaff, K., and Zhu, J., editors, Proceedings of the 42nd International Conference on Machine Learning, volume 267 of Proceedings of Machine Learning Research, pages 37889–37905. PMLR.

Lu, Z., Zhou, A., Ren, H., Wang, K., Shi, W., Pan, J., Zhan, M., and Li, H. (2024). Mathgenie: Generating synthetic data with question back-translation for enhancing mathematical reasoning of llms. In Proceedings of the Annual Meeting of the Association for Computational Linguistics (ACL).

McGinness, L. and Baumgartner, P. (2024). Automated theorem provers help improve large language model reasoning.

Mistral AI (2025). Model Card: Mistral Small 3.2 24B Instruct 2506. GGUF model repository by LM Studio Community. Accessed: 2026-05-01.

Mitra, A., Corro, L. D., Mahajan, S., Codas, A., Simões, C., Agrawal, S., Chen, X., Razdaibiedina, A., Jones, E., Aggarwal, K., Palangi, H., Zheng, G., Rosset, C., Khanpour, H., and Awadallah, A. (2023). Orca 2: Teaching small language models how to reason. CoRR, abs/2311.11045.

Pelletier, F. J. (2000). A history of natural deduction and elementary logic textbooks. Logical consequence: Rival approaches, 1:105–138.

Qwen Team (2026). Qwen3.5-35B-A3B. GGUF model repository by LM Studio Community.

Saparov, A. and He, H. (2023). Language models are greedy reasoners: A systematic formal analysis of chain-of-thought. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023. OpenReview.net.

Shridhar, K., Stolfo, A., and Sachan, M. (2023). Distilling reasoning capabilities into smaller language models. ACL 2023:7059–7073.

Silva, F. S. C. d., Finger, M., and Melo, A. C. V. d. (2017). Lógica para Computação. Cengage Learning, São Paulo, 1 edition.

Smullyan, R. M. (1995). First-Order Logic. Dover Publications.

Sprague, Z. R., Ye, X., Bostrom, K., Chaudhuri, S., and Durrett, G. (2024). Musr: Testing the limits of chain-of-thought with multistep soft reasoning. In The Twelfth International Conference on Learning Representations (ICLR).

Tafjord, O. et al. (2021). Proofwriter: Generating implications, proofs, and abductive reasoning. In ACL.

Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, Ł., and Polosukhin, I. (2017). Attention is all you need. Advances in Neural Information Processing Systems, 30.

Wang, P., Wang, Z., Li, Z., Gao, Y., Yin, B., and Ren, X. (2023). Scott: Self-consistent chain-of-thought distillation. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 5546–5558, Toronto, Canada. Association for Computational Linguistics.

Wang, S., Wei, Z., Choi, Y., and Ren, X. (2024). Can llms reason with rules? logic scaffolding for stress-testing and improving llms. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 7523–7543, Bangkok, Thailand. Association for Computational Linguistics.

Yang, A., Li, A., Yang, B., Zhang, B., Hui, B., Zheng, B., Yu, B., Gao, C., Huang, C., Lv, C., et al. (2025). Qwen3 technical report. arXiv preprint arXiv:2505.09388.