Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

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

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Evandro de Barros Costa,
  • Jean Felipe Duarte Tenório,
  • Alison Bruno Martires Soares,
  • Rian Américo Brito da Silva,
  • Wallace Lins Casado de Sousa,
  • Davi Silva de Melo Lins,
  • Dante de Araújo Costa

摘要

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.