Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework

📄 arXiv: 2504.20213v1 📥 PDF

作者: Yuan Xia, Akanksha Atrey, Fadoua Khmaissia, Kedar S. Namjoshi

分类: cs.LG, cs.AI

发布日期: 2025-04-28

💡 一句话要点

提出数据驱动框架，评估大语言模型在布尔逻辑证明中的推理能力

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 逻辑推理 布尔逻辑 证明构建 数据增强 模板转换 形式验证

📋 核心要点

  1. 现有真实逻辑证明数据稀缺，阻碍了LLM在逻辑推理方面的训练和评估。
  2. 提出一种随机合成有效证明的方法，并结合模板转换进行数据增强，提升模型处理复杂逻辑表达式的能力。
  3. 实验表明，该方法能有效提升LLM在短证明推理上的能力，且模板转换对不同规模模型均有效。

📝 摘要（中文）

本文研究了大语言模型（LLM）的逻辑推理能力。为了获得精确且易于处理的公式，选择了在布尔逻辑中构建证明这一概念简单但技术复杂的任务。训练后的LLM接收一组假设和一个目标作为输入，并生成一个从假设中正式推导出目标的证明作为输出。自动证明检查器可以捕获不正确的证明。训练的关键障碍是真实世界证明的稀缺。我们提出了一种高效的随机程序来合成有效的证明，并引入了模板转换，这是一种数据增强技术，可以增强模型处理复杂逻辑表达式的能力。中心评估问题是LLM是否真正学会了推理。我们提出了测试来衡量黑盒LLM的推理能力。通过这些衡量标准，实验表明，对于具有短证明的断言，LLM具有很强的推理能力，但随着证明复杂性的增加而下降。值得注意的是，模板转换即使对于较小的模型也能提高准确性，这表明其在模型规模上的有效性。

🔬 方法详解

问题定义：论文旨在评估大型语言模型（LLM）在形式逻辑推理方面的能力，具体任务是构建布尔逻辑证明。现有方法缺乏足够的真实世界证明数据，难以有效训练和评估LLM的逻辑推理能力。

核心思路：论文的核心思路是通过数据驱动的方法，解决训练数据不足的问题。首先，设计一种高效的随机过程来合成有效的逻辑证明。其次，引入模板转换（Template Transformation）作为一种数据增强技术，以提高模型对复杂逻辑表达式的泛化能力。

技术框架：整体框架包含数据生成、模型训练和评估三个主要阶段。数据生成阶段使用随机过程合成有效的布尔逻辑证明，并应用模板转换进行数据增强。模型训练阶段使用合成数据训练LLM，使其学习从假设推导出目标的证明过程。评估阶段设计了一系列测试，用于衡量LLM的推理能力，包括对不同复杂度的证明进行评估。

关键创新：论文的关键创新在于提出了一种有效的数据合成和增强方法，解决了LLM在形式逻辑推理任务中训练数据稀缺的问题。模板转换是一种新颖的数据增强技术，能够显著提高模型对复杂逻辑表达式的鲁棒性。

关键设计：数据生成过程采用随机化的方法，确保生成多样化的有效证明。模板转换通过替换逻辑表达式中的变量和运算符，生成新的训练样本。具体参数设置和网络结构等技术细节在论文中未详细说明，属于未知信息。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，该方法能够显著提高LLM在布尔逻辑证明任务中的准确率，尤其是在处理短证明时。模板转换作为一种数据增强技术，即使对于较小的模型也能提高准确性，表明其在不同模型规模上的有效性。具体性能提升数据未知。

🎯 应用场景

该研究成果可应用于需要形式逻辑推理的领域，如程序验证、智能合约安全审计、知识图谱推理等。通过提升LLM的逻辑推理能力，可以提高自动化推理系统的可靠性和效率，并为开发更智能的AI系统奠定基础。

📄 摘要（原文）

This paper investigates the logical reasoning capabilities of large language models (LLMs). For a precisely defined yet tractable formulation, we choose the conceptually simple but technically complex task of constructing proofs in Boolean logic. A trained LLM receives as input a set of assumptions and a goal, and produces as output a proof that formally derives the goal from the assumptions. Incorrect proofs are caught by an automated proof checker. A critical obstacle for training is the scarcity of real-world proofs. We propose an efficient, randomized procedure for synthesizing valid proofs and introduce Template Transformation, a data augmentation technique that enhances the model's ability to handle complex logical expressions. The central evaluation question is whether an LLM has indeed learned to reason. We propose tests to measure the reasoning ability of a black-box LLM. By these measures, experiments demonstrate strong reasoning capabilities for assertions with short proofs, which decline with proof complexity. Notably, template transformation improves accuracy even for smaller models, suggesting its effectiveness across model scales.