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

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.

## introduction large language models (llms), such as openai's gpt models @xcite ), google's gemini models @xcite , and meta's llama models @xcite , are typically trained on high-resource natural languages (e.g., english, spanish, and chinese). this focus on high-resource languages disadvantages speakers of low-resource languages, as training models for these languages are more challenging due to their inherent complexity @xcite . furthermore, semantic ambiguity, grammatical complexities, and contextual dependencies in natural languages can limit the capabilities of an llm in precise logical reasoning. since natural language often relies on implied meaning, subtle cues, and flexible syntax, models trained primarily on data using these principles * these authors contributed equally to this work. may struggle to follow strict rules needed for logical reasoning @xcite . to isolate these reasoning abilities from language-specific challenges, we propose the evaluation of llms within a controlled setting using formal logical language. logical languages, characterized by strict syntax and precise semantics, eliminate many of the extraneous factors present in natural languages, allowing us to focus squarely on pattern recognition and problem solving. although prior benchmarks, such as logiglue @xcite , provide structured reasoning tasks, these typically rely on predefined reasoning steps, making it challenging to determine whether an llm can autonomously identify and apply logical rules. in contrast, our benchmark, rosetta-pl, evaluates whether llms can discover logical patterns within a propositional language, thereby measuring reasoning ability without relying on predefined inference steps or extraneous linguistic factors. research on applying llms to logic-based problem solving is relatively scarce, and while chain-ofthought (cot) prompting has gained popularity in natural language tasks @xcite , its effectiveness in logical or symbolic contexts remains largely unexplored @xcite . we address this gap by constructing rosetta-pl by translating the lean workbook dataset @xcite into our own propositional language and fine-tuning chatgpt (brown et al., 2020) using the translated dataset. we evaluate logical accuracy in our custom language while varying training data parameters such as training set size and the method of translation. our experiments point towards potentially effective training strategies and provide preliminary estimates on the dataset size needed to approach benchmark-level logical understanding. by setting aside language-specific factors, we focus on the relationship between pattern recognition and data requirements, offering insights that impact language training in both high-and low-resource settings. ## background large language models (llms) have excelled at tasks involving unstructured natural language, yet their capacity for structured logical reasoning remains underexplored @xcite . the inherent ambiguities of natural language, such as polysemy and idiomatic expressions, can obscure true reasoning capabilities. in contrast, formal logical languages, defined by strict syntax and unambiguous semantics, offer a controlled testbed for evaluating pattern recognition and rule-based inference @xcite . propositional logic, a fundamental component of formal logic, employs connectives (e.g., ∧, ∨, ¬) to combine atomic propositions into complex expressions whose truth values are fully determined by their parts @xcite . this clarity makes it an ideal framework for assessing whether llms can autonomously learn and generalize logical rules-a skill central to disciplines like mathematics and programming @xcite . recent benchmarks have begun to probe the symbolic reasoning of llms. for example, logic-lm demonstrates that llms can solve logic puzzles when aided by external symbolic solvers @xcite . meanwhile, logiglue @xcite and logic bench @xcite evaluate multi-step reasoning based on predefined inference templates, and chain-of-thought prompting has been shown to improve arithmetic performance @xcite . other studies have further enriched this landscape: for example, the symbcot framework integrates symbolic expressions and logic rules directly into chain-of-thought (cot) thereby boosting reasoning fidelity @xcite , while research examining the impact of symbolic solver choices has revealed that tool selection (e.g., z3, prover9, or pyke) can cause performance variations of up to 50% @xcite . furthermore, work on step-by-step symbolic verification has demonstrated that automated checks of intermediate reasoning steps can substantially enhance overall accuracy @xcite . however, these approaches tend to rely on surface-level statistical correlations rather than genuine discovery of novel logical patterns @xcite . to bridge this gap, our work translates natural language logic problems into a propositional lan-guage, thereby eliminating linguistic complexities and focusing solely on intrinsic pattern recognition. building on formal frameworks such as lean4 @xcite , we investigate how well llms can learn and generalize new logical structures-a capability that also carries implications for improving training strategies in low-resource language settings @xcite . ## results figure 1 displays the comparative performance of four fine-tuned gpt-4o models evaluated on both "seen" and "unseen" datasets. specifically, models were fine-tuned with 25,214, 20,000, and 10,000 distinct queries using translation key 1, and with 25,214 queries using translation key 2. additionally, lean (untranslated) versions of both testing sets serve as benchmarks. our experiments demonstrate that gpt-4o exhibits superior problem-solving performance in our custom propositional language compared to lean on average. on the "seen" dataset, gpt-4o achieved an average accuracy over all tests in of 95.97% in our propositional language versus 76.08% in lean, with a small uncertainty @xmath0.33% @xmath1.36% respectively. in contrast, on the "unseen" dataset, gpt-4o performed better when tested in lean than in our custom language-attaining 99.89% accuracy with lean compared to 97.56% with translation key 1 (± 0.06% @xmath2.44% respectively). as expected, translation key 2 yielded a substantially lower accuracy of 64.1% (± 0.75%) due to its arbitrary mapping. the model was fine-tuned solely on translated data, so it specializes in those patterns, resulting in high performance on seen translated examples but poor performance on seen lean examples. for unseen data, it falls back on its broader pre-training, which helps it perform better on unseen lean problems. additionally, our experiments indicate that gpt-4o solves problems more accurately with translation key 1 than with translation key 2, with average accuracies of 92.68% compared to 80.36% respectively-highlighting the importance of preserving logical relationships in the translation process. for seen data in the custom translated format, the fine-tuned gpt-4o consistently achieves higher accuracy by specializing in the patterns and syntax introduced during fine-tuning, outperforming the base model. in contrast, on seen lean data, the base gpt-4o retains its general lean knowledge from pre-training and achieves similar results to the fine-tuned model. when it comes to unseen data, the fine-tuned gpt-4o expectedly outperforms the base model on unseen translated examples. tables 1 , 3 , and 4 provides a detailed summary of all dataset permutations and average performance metrics, shedding light on any potential anomalies. ## discussion our findings align with previous studies @xcite , demonstrating that the accuracy of logical reasoning depends significantly on prompt formulation and task representation. the use of translation keys in our experiments illustrates that preserving inherent logical relationships-as in translation key 1-yields better performance than employing arbitrary mappings. this is analogous to natural language, where inverse or comparable relationships between symbols facilitate comprehension. our results also reveal a general trend where accuracy increases with training set size, echoing prior research that shows llms can perform well even with limited data @xcite . however, as shown in figure 1 , this trend is not strictly linear. there are occasions where smaller datasets outperformed larger datasets, such as the "seen" dataset in our propositional language having a 0.467% greater accuracy with 10000 samples compared to 20,000 samples. we attribute these fluctuations to certain factors, such as overfitting in larger training sets. unlike earlier studies that evaluated existing models @xcite , our approach using a custom propositional language uncovers unique aspects of pattern recognition in llms. notably, our analysis revealed that gpt-4o's performance on unseen data is better in lean than it is in our custom language. we attribute this to gpt-4o's prior exposure to lean-like syntax during pre-training lean, as a formal proof assistant, shares structural similarities with theorem-proving and programming languages. in contrast, the custom language, especially under translation key 2, disrupted logical structure, thereby impeding generalization. this suggests that fine-tuning benefits significantly when the training data preserves logical consistency, aligning with the model's pretraining experience. this is further reinforced by the observation that models fine-tuned with translation key 1 performed better across all testing sets than those finetuned with translation key 2. additionally, the fine-tuned models-especially those with translation key 1-consistently exhibited superior performance on both seen and unseen data, and this performance improved with larger training set sizes. this demonstrates gpt's ability to generalize logical information. the llm extracted logical information from our custom language and used it to improve its logical accuracy in lean. notably, it performed better with translation key 1-which preserves logical relationships-than with translation key 2, which disrupts them. while distinguishing between these effects is challenging, future work could explore fine-tuning an llm with minimal exposure to lean syntax to better understand the impact of pre-training familiarity compared to logical structure preservation. comparing performance across runs provided insights into whether gpt-4o could robustly handle shifts in symbolic representation and how sensitive its performance is to different training configurations. our experiments indicate that gpt-4o's performance plateaus at around 20,000 training examples. this plateau may result from dataset redundancy, model capacity limitations, or the relative simplicity of the tasks. when the dataset contains many similar patterns, the model's exposure to novel challenges is limited, and once key patterns are internalized, additional training yields diminishing returns. in summary, our findings suggest that gpt-4o can achieve high problem-solving accuracy in a propositional language when fine-tuned appropriately. the choice of translation key, dataset characteristics, and training set size must be managed carefully to mitigate overfitting and ensure robust generalization beyond seen patterns. ## conclusion our investigation confirms that fine-tuning gpt-4o on a custom propositional language not only facilitates high-level logical reasoning but also underscores the critical role of maintaining relational integrity within training data. specifically, our work shows that using structured translation strategies significantly enhances model performance. this improvement is achieved by aligning the training data with the inherent logical patterns familiar from the model's pre-training, allowing gpt-4o to generalize more effectively, particularly when transitioning from seen to unseen examples. furthermore, our analysis highlights that an optimally balanced training set is essential: while increased dataset size improves performance up to a threshold (around 20,000 examples), additional data yields diminishing returns, suggesting the need for more efficient data utilization methods. these findings not only validate the importance of structured prompts and contextual cues but also offer practical guidelines for optimizing llm training in both high-and low-resource language scenarios. collectively, our results contribute to a deeper understanding of how targeted data curation and translation methodologies can bolster logical reasoning in large language models.