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

We investigate whether large language models (LLMs) can master formal reasoning by focusing on the technically demanding task of constructing Boolean-logic proofs. Given a set of assumptions and a goal, a trained LLM produces a proof whose correctness is verified by an automated checker. To overcome the scarcity of real proofs, we devise a randomized procedure for synthesizing valid proofs and introduce Template Transformation, a data augmentation technique that bolsters the model’s ability to handle complex logical expressions. We propose black-box tests to quantify an LLM’s reasoning ability and show that accuracy is high for short proofs but falls as proof depth grows. Notably, template transformation yields accuracy gains even for smaller models, underscoring its scale-independent benefit.

arXiv preprint arXiv:2504.20213