Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning

Shaun Baek, Shaun Esua-Mensah, Cyrus Tsui, Sejan Vigneswaralingam, Abdullah Alali, Michael Lu, Vasu Sharma, Sean O'Brien, Kevin Zhu

TL;DR

Rosetta-PL introduces a controlled benchmark by translating Lean Workbook problems into a custom propositional language to assess LLM logical reasoning and generalization, decoupled from natural language. The study fine-tunes GPT-4o on this dataset and compares translation strategies, showing that preserving logical relationships (Translation Key 1) yields significantly higher accuracy than arbitrary mappings (Translation Key 2). Results reveal a performance plateau around 20,000 training examples, with seen generalization improving with data up to that point and unseen generalization benefiting from prior Lean familiarity. The findings offer practical guidance for data design and translation strategies to enhance formal reasoning in LLMs, with implications for both high- and low-resource language settings.

Abstract

Large Language Models (LLMs) are primarily trained on high-resource natural languages, limiting their effectiveness in low-resource settings and in tasks requiring deep logical reasoning. This research introduces Rosetta-PL, a benchmark designed to evaluate LLMs' logical reasoning and generalization capabilities in a controlled environment. We construct Rosetta-PL by translating a dataset of logical propositions from Lean into a custom logical language, which is then used to fine-tune an LLM (e.g., GPT-4o). Our experiments analyze the impact of the size of the dataset and the translation methodology on the performance of the model. Our results indicate that preserving logical relationships in the translation process significantly boosts precision, with accuracy plateauing beyond roughly 20,000 training samples. These insights provide valuable guidelines for optimizing LLM training in formal reasoning tasks and improving performance in various low-resource language applications.

Rosetta-PL: Propositional Logic as a Benchmark for Large Language Model Reasoning

TL;DR

Rosetta-PL introduces a controlled benchmark by translating Lean Workbook problems into a custom propositional language to assess LLM logical reasoning and generalization, decoupled from natural language. The study fine-tunes GPT-4o on this dataset and compares translation strategies, showing that preserving logical relationships (Translation Key 1) yields significantly higher accuracy than arbitrary mappings (Translation Key 2). Results reveal a performance plateau around 20,000 training examples, with seen generalization improving with data up to that point and unseen generalization benefiting from prior Lean familiarity. The findings offer practical guidance for data design and translation strategies to enhance formal reasoning in LLMs, with implications for both high- and low-resource language settings.

Abstract

Large Language Models (LLMs) are primarily trained on high-resource natural languages, limiting their effectiveness in low-resource settings and in tasks requiring deep logical reasoning. This research introduces Rosetta-PL, a benchmark designed to evaluate LLMs' logical reasoning and generalization capabilities in a controlled environment. We construct Rosetta-PL by translating a dataset of logical propositions from Lean into a custom logical language, which is then used to fine-tune an LLM (e.g., GPT-4o). Our experiments analyze the impact of the size of the dataset and the translation methodology on the performance of the model. Our results indicate that preserving logical relationships in the translation process significantly boosts precision, with accuracy plateauing beyond roughly 20,000 training samples. These insights provide valuable guidelines for optimizing LLM training in formal reasoning tasks and improving performance in various low-resource language applications.
Paper Structure (13 sections, 3 equations, 3 figures, 4 tables)

This paper contains 13 sections, 3 equations, 3 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Method
  4. Objective
  5. Dataset
  6. Experimental Methodology
  7. Translation Strategies:
  8. Evaluation Procedure:
  9. Results
  10. Discussion
  11. Conclusion
  12. Future Research
  13. Appendix

Figures (3)

  • Figure 1: Comparison of GPT-4o accuracy across datasets ("Seen" and "Unseen") using different translation keys and varying dataset sizes.
  • Figure 2: Mapping between Lean's logical symbols and their corresponding representations in our custom propositional language. (Part 1/2)
  • Figure 3: Mapping between Lean's logical symbols and their corresponding representations in our custom propositional language. (Part 2/2)