Large Language Models Performance in Propositional Logic Proofs: Solving and Evaluating Argument Validity

doi:10.1007/978-3-031-98281-1_24

Large Language Models Performance in Propositional Logic Proofs: Solving and Evaluating Argument Validity

2026-01-01

0

PRE

AI

E

Evandro Costa *

J

Jean Felipe Duarte Tenório

Wallace Lins Casado de Sousa

D

Davi Silva de Melo Lins

C

Costa, Dante de Araujo

DOI：10.1007/978-3-031-98281-1_24

Original

Original request for help

Save

Abstract

En 中文

The present study investigates the ability of Large Language Models (LLMs) in generating and evaluating formal proofs within propositional logic. Specifically, we examine whether an LLM can accurately construct formal proofs to determine the validity of logical arguments and if other independent LLMs can reliably assess the correctness of such proofs. That is, when a LLM plays the problem solver role, the other involved LLMs play the role of evaluator. The evaluation comprises 12 diverse propositional logic proof problems, classified into distinct characteristics. Experimental scenarios were designed such that one model, exemplified by DeepSeek, performed the solver role by generating formal proofs, while three other models, represented by Qwen, GPT, and Gemini, independently evaluated the validity of these proofs. Our findings for each different configuration are described in this article, revealing positive results in favor of the LLMs used.

Keywords:

Argument validity via natural deduction

Large Language Models

Propositional Logic

Computing Education

Large Language Models Performance in Propositional Logic Proofs: Solving and Evaluating Argument Validity

Abstract

Journal

Organization