用自动生成的逻辑证明训练模型，验证其形式推理能力。
Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework
- 通过随机生成有效布尔逻辑证明，解决真实证明数据稀缺问题。
- 短证明任务中模型推理准确率高，复杂度上升时性能下降。
- 模板变换技术提升小模型表现，适合研究逻辑推理的学者使用。
本文研究大语言模型（LLM）的形式逻辑推理能力。针对概念简单但技术复杂的布尔逻辑证明任务，训练模型根据前提推导目标结论。输入为一组假设和待证目标，输出为形式化证明，错误证明由自动检查器识别。训练主要挑战在于真实证明数据稀少，为此提出一种高效的随机化证明生成方法，并引入模板变换（Template Transformation）作为数据增强手段，提升模型处理复杂逻辑表达式的能力。核心评估问题是模型是否真正掌握推理能力，因此设计了黑箱测试方法。实验表明，在短证明场景下模型具备强推理能力，但随证明复杂度增加而下降。值得注意的是，模板变换显著提升小模型精度，表明其在不同规模模型上均有效。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。