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

TL;DR

Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework investigates whether LLMs can learn formal Boolean logic reasoning by generating synthetic Hilbert-style proofs and validating them with an automated checker. The authors introduce a goal-directed proof-generation procedure and a Template Transformation augmentation to create diverse, structurally similar proofs, enabling robust training and testing. Empirical results show that an 8B Llama model trained on about 9000 proofs attains $0.98$ accuracy on depth-$7$ proofs, surpassing GPT-4o few-shot performance, with template transformation also benefiting smaller models and improving generalization to more complex expressions. The study highlights that semantic generalization and proof diversity can be achieved with synthetic data and automated validation, though performance naturally declines with increasing proof depth due to the intrinsic co-NP hardness of Boolean reasoning, underscoring both promise and limits for scalable formal reasoning in LLMs.

Abstract

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.

Figures (9)

• Figure 1: Overview: The training phase generates synthetic proofs and applies template transformations for fine-tuning. Inference produces a candidate proof for the query ("Does the goal follow from the assumptions?"); this proof is formally validated.
• Figure 2: Comparison of Llama3-8B (LLM) and Llama3-1B (SLM) model variants' testing accuracies across different training data sizes. Left: Impact of proof width on accuracy. Right: Impact of proof depth on accuracy. Models with and without Template Transformation (TT) are compared.
• Figure 3: Impact of Template Transformation probability ($\alpha_{TT}$) on model performance. The left subplot shows test accuracy across different model widths (0-3), while the right subplot demonstrates the effect on models of varying depths (4-13).
• Figure 4: Example prompt used for Depth 4 Problems with one shot
• Figure 5: Adapted prompt for Depth 4 Problems with one shot

Theorems & Definitions (4)

• Theorem 1.1
• proof
• Theorem 1.2
• proof