Translating natural language (NL) into logical formalisms like First-Order Logic (FOL) has long been a challenge across multiple disciplines, including mathematics, computer science, and education. Traditional computational linguistics methods have struggled with this task due to the complexity and ambiguity of natural language. However, advancements in Natural Language Processing (NLP), particularly the introduction of Large Language Models (LLMs), have opened up new possibilities for tackling this challenge. Despite their potential, a systematic approach to evaluating the performance of LLMs in NL-to-FOL translation is still lacking. In this study, we take a first step towards filling in this gap. We examine a large dataset based on students' eforts in formalizing natural language statements from the book “Language, Proof, and Logic”. Based on this dataset, we propose a preliminary evaluation pipeline to assess LLM performance in NL-to-FOL translation tasks, considering both syntactic and semantic aspects. We then apply this pipeline to evaluate two recent LLMs, Meta's Llama 3.1 (8B) and Google DeepMind's Gemma 2 (9B). Our findings validate the proposed approach, revealing key similarities and diferences between LLM-generated and student-produced formulas, and provide valuable insights into the current capabilities of LLMs in this domain.
Translating natural language (NL) into logical formalisms like First-Order Logic (FOL) is a longstanding
challenge that spans multiple disciplines, including mathematics, computer science, and education. In
mathematics, this translation facilitates automated theorem proving [
Historically, traditional computational linguistics methods have attempted to tackle this task, but
with limited success, often struggling to maintain accuracy and consistency when dealing with
complex or ambiguous sentences (see, for instance, the survey paper [
Our study represents a first step in this direction. We examine a large dataset derived from research on the challenges students face when formalizing natural language statements into FOL [11, 12, 13, 14], as outlined in the book “Language, Proof, and Logic” [15]. Based on this dataset, we propose an initial pipeline to evaluate the performance of LLMs in translating natural language phrases into firstorder logic formulas, considering both syntactic and semantic aspects. We then apply this pipeline to assess the performance of the two recent LLMs Meta’s LLM Llama 3.1 (8B) [16, 17] and Google DeepMind’s Gemma 2 (9B) [18]. While our work is not yet intended as a full-fledged benchmark, the experimental results validate the proposed approach and highlight key similarities and diferences between LLM-generated formulas and those produced by students, ofering valuable insights into the current capabilities of LLMs in this domain. These findings warrant further exploration and, in addition, emphasize the need for continued investigation into the interaction between the fields of NLP and formal methods.
The paper is structured as follows: Section 2 introduces the dataset and preprocessing steps undertaken for analysis. Section 3 outlines our evaluation pipeline for assessing LLM performance on NL-to-FOL translation tasks, which is then experimentally evaluated in Section 4. Finally, Section 5 provides concluding remarks, discusses the limitations of the current study and outlines future research directions.
The dataset we considered is an extract of the years 2001–2010 from the Grade Grinder Corpus Release 1.0 [11], kindly provided to us privately by the authors. It consists of correct and incorrect answers, continuously collected through a dedicated tutoring software, from students responding to questions posed in the book “Language, Proof, and Logic” [15]. Each question involves a natural language utterance describing a situation in Tarski’s World [19], where students are tasked with formulating a corresponding First-Order Logic (FOL) expression to encode the given text.
Our extract contains 16,265,166 answers, both correct and incorrect, submitted by 50,608 students. After a pre-processing phase, each answer includes a student identifier, the logic formula written by the student, the corresponding natural language phrase, and a Boolean flag indicating whether the answer is correct. Additionally, each entry contains an attribute indicating the sequential attempt number, as students may make multiple attempts to answer the same question while interacting with the tutoring software (see Table 1). Note that there may be more than one correct answer per phrase due to the equivalence of diferent logic formulas and the flexibility of the allowed syntax, which includes relations along with their opposites. This is summarized in Table 2.
Overall, answers refer to 208 distinct natural language phrases, which we categorized along 6 dificulty levels. To such an extent, based on the work of [13], for each phrase we calculated the percentage of failed first-attempt answers as well as the so-called stickiness value, i.e., the average number of attempts made by students before reaching a correct answer. We then performed K-means clustering on these two variables, identifying 6 clusters relying on an instance separation criterion; they are summarized in Table 3. Note how, overall, the number of phrases decreases as the dificulty level increases. For each phrase, the ground truth is given by the set of (unique) correctly submitted formulas, a number which ranges from a minimum of 1 to a maximum of 1150, with an average of 99.
In this section, we provide an account of the pipeline we developed to evaluate natural language to formula translation, which is summarized in Figure 1. Suppose an LLM is given a natural language phrase , belonging to our considered dataset, that describes a situation in Tarski’s World; in response, it generates a formal representation of this phrase as a FOL formula . To evaluate the syntactic and semantic correctness of , we proceed as follows: 1. The formula is parsed using Python’s Lark library [20], following a specifically designed FOL grammar describing formulas of Tarski’s World (see Table 2). The parsing may fail, due to grammar violations. In such case, we rely on a set of hard-coded rules, primarily based on regular expressions, to identify these kinds of syntax errors: • Relation/arity: a relation that is not part of the defined syntax or is used with incorrect arity; • Connectives and quantifiers: non-adherence to the syntax or misuse of a connective (e.g., ∧ connective without one of the conjuncts); • Constants and variables: non-adherence to the naming conventions; • Structure: unpaired or misused parentheses; • Other: residual category for the parsing errors which could not be automatically classified. At this point, the errors identified in the formula are kept track of, the formula is labeled as both syntactically and semantically incorrect, and the pipeline ends. Otherwise, if the parsing of succeeds, the formula is passed down to the next point in the pipeline; 2. Relying on Python’s ZSS library [21], we calculate the tree edit distance [22] between and each possible ground truth for the phrase , identifying the most similar formula ; 3. We evaluate the logical equivalence between and relying on the Z3 theorem prover [23].
Specifically, we verify the unsatisfiability of ¬( ↔ ); 4. If the two formulas are found to be equivalent, is labeled as both syntactically and semantically correct. Otherwise, if they are non-equivalent, the formula is labeled as syntactically correct but not semantically correct, and we also output the distance calculated at Point 2., with the idea that it represents the cost of semantically transforming into .
Start: Natural Language Phrase
LLM generates FOL formula Parse with Lark (FOL Grammar)
Check for syntax errors: relation/arity, connectives,
variables, structure Parsing Successful?
No
Identify syntax errors (regular expressions) Yes
Output Errors
Syntactically and Semantically Incorrect Compute tree edit distance between and ground truths for ,
selecting as the most similar formula
Equivalent?
Yes No Syntactically and Semantically Correct Syntactically
Correct, Semantically
Incorrect (Output distance)
In this section, we apply our pipeline and considered dataset to evaluate the LLMs Meta’s Llama 3.1 (8B) and Google DeepMind’s Gemma 2 (9B). To instruct the models to translate a natural language utterance, we used the DSPy framework [24] (Prompt 1). For the purpose of this preliminary study, we focus solely on the first attempts made by students, totaling 14,452,492 answers. This ensures a fair comparison with the LLMs, which, at present, are not involved in any form of iterative answering process.
Table 4 compares the accuracy of the LLMs in first-attempt formula generation with that of the average student. Overall, the LLMs achieve better results than the students. The comparison becomes more interesting when examining performance across diferent dificulty levels: while the average student’s accuracy, of course, consistently decreases as the dificulty increases, the LLMs’ performance is more varied. Llama 3.1 (8B) performs worse than the average student at the super-low and low dificulty levels, but outperforms at the higher levels. Gemma 2 (9B), while slightly surpassing LLama 3.1 overall, scores notably low at the Mid-low dificulty level.
Upon closer examination, it was found that among the 12.5% of formulas incorrectly generated by Llama 3.1 (8B), no exclusively semantic errors were made, as the pipeline had already exited at Translate / Formalize English sentences into formulae of first − order language . === vocabulary to use === The vocabulary of the domain , part of a model for a first − order language , must be the following one : Constants symbol : lower case character from a to f Variables symbol : lower case character from s to z === Relations to use === Each element indicates the name of a relation and its arity ( name / arity ): [’ Tet /1 ’ , ’ Cube /1 ’ , ’ Dodec /1 ’ , ’ Small /1 ’ , ’ Medium /1 ’ , ’ Large /1 ’ , ’ SameShape /2 ’ , ’ SameSize /2 ’ , ’ Larger /2 ’ , ’ Smaller /2 ’ , ’ SameCol /2 ’ , ’ SameRow /2 ’ , ’ Adjoins /2 ’ , ’ FrontOf /2 ’ , ’ RightOf /2 ’ , ’ LeftOf /2 ’ , ’ BackOf /2 ’ , ’ Between /3 ’] Equality binary relation with symbol : = Explanation of the relation Between :
Between (x , y , z) means that x is between y and z Explanation of the relation Larger :
Larger (x , y) means that x is larger than y === symbols you MAY USE === Equality binary relation with symbol : = Logical operator symbols : ¬, ∧, ∨ , → , ↔ Quantifier symbols : ∃, ∀ === symbols you MUST NEVER USE === Symbols that are not allowed : "̸=" === output constraint === The FOL formula is the first element of the output , with the prefix ’ = ’.
Prompt 1: Instructions prompted to the LLMs to translate English sentences into FOL.
Mid-low
the syntax-checking stage. The distribution of syntax error types within these incorrect formulas is shown in Table 5 (columns labeled with ‘L’). Despite the large percentage of uncategorized syntax errors (Other), it can be observed that the remaining errors generally involve the incorrect use of connectives or quantifiers. As for Gemma 2 (9B), exactly 3 formulas, belonging to the 12,02% of the incorrectly generated ones, passed the syntax check but failed the semantic test, with an average tree edit distance of 15. Looking again at Table 5 (columns labeled with ‘G’), here the kinds of syntax errors detected are slightly more variegate, though errors involving connectives and quantifiers remain predominant.
Table 6 considers the agreement between the two LLMs. Notably, in 94.23% of cases, a phrase can be correctly formalized by at least one model, while in only 5.77% of cases neither model is able to produce a correct formula. For the 81.25% of the phrases, both models can derive the right formalization. Regarding the dificulty levels, it is noteworthy that, although the two LLMs share the same accuracy on the Mid-high level (93.10%, Table 4), they correctly formalize diferent sets of phrases.
Finally, in [12] it emerges that, for the students, the choice of the logical connective to be used in the formalization is a critical factor. Specific words, identified in both [ 12] and [15], have been found to be linked to this choice and are recognized as common sources of errors [12]. Therefore, in Table 7 we investigate whether LLMs make more or fewer mistakes than students when restricted to sentences containing words that are typically associated with errors. The accuracy distributions difer between the two LLMs and when compared to student results, suggesting that common sources of mistakes for students do not always apply to the models. Here, a notable case is that of at least (column ‘AL’).
In this work, we took an initial step toward defining a pipeline for evaluating LLMs on the task of formalizing natural language utterances into FOL formulas. We applied the pipeline to Meta’s Llama 3.1 (8B) and Google DeepMind’s Gemma 2 (9B), comparing their performance to that of students on the same tasks, using a large dataset based on Tarski’s World. Already from our preliminary analyses, several interesting points emerged: () both LLMs slightly outperform the average student; () there is no clear alignment between the phrases found dificult by the students and those deemed dicfiult by the LLMs; () the vast majority of errors made by the LLMs are syntactic in nature; () despite being of comparable size, the two LLMs exhibit diferent behaviors that, if strategically combined, could enhance translation performance; and () the common sources of mistakes for students difer from those of the considered LLMs.
Incidentally, these findings prompt important pedagogical questions, particularly concerning how the “thinking” in LLMs may fundamentally difer from student reasoning. For example, while LLMs rely on pattern recognition without an understanding of semantics, students learn through logical reasoning, which may indicate that LLM-generated feedback could be better suited for tasks with lower cognitive demands or for assisting below-average students rather than top-performing ones. Future studies could explore these distinctions further to assess whether LLMs can reliably assist students in tasks requiring deeper semantic comprehension or if they are more efective as support tools for students needing guidance with fundamental concepts. Additionally, it is worth investigating the specific ways in which the nature of LLM errors (primarily syntactic) contrasts with student errors, which could inform a targeted approach for LLM-based feedback that addresses common student mistakes more accurately.
Other than this, for future work, we plan to: extend our analyses to additional models and prompting techniques; evaluate the alignment between accuracy improvements across repeated student submissions and multiple attempts by LLMs; investigate the (self-)correcting capabilities of LLMs; build on the notion of tree edit distance to define a metric for measuring the semantic distance between formulas; and conduct a more in-depth text analysis to uncover patterns and regularities related to formalization accuracy.
First and foremost, the authors thanks the invaluable support of David J. Barker-Plummer and John W. Etchemendy from Stanford University that provided us with the dataset to perform the experimentation. All the authors but RF and EM acknowledge the support from the 2024 Italian INdAM-GNCS project “Certificazione, monitoraggio, ed interpretabilità in sistemi di intelligenza artificiale”, ref. no. CUP E53C23001670001. LG, AM, and NS also acknowledge the support from the Interconnected Nord-Est Innovation Ecosystem (iNEST), which received funding from the European Union Next-GenerationEU (PIANO NAZIONALE DI RIPRESA E RESILIENZA (PNRR) – MISSIONE 4 COMPONENTE 2, INVESTIMENTO 1.5 – D.D. 1058 23/06/2022, ECS00000043). In addition, AM acknowledges the support from the MUR PNRR project FAIR - Future AI Research (PE00000013) also funded by the European Union Next-GenerationEU. Finally, EM and AM also acknowledge the support from the Autonomous region Friuli-Venezia Giulia for the project “Automazione Conversazionale e Voice&Speech Analytics per l’Active and Assisted Living” funded by the regional program FESR 2021-2027. This manuscript reflects only the authors’ views and opinions, neither the European Union nor the European Commission can be considered responsible for them. [11] D. Barker-Plummer, R. Cox, R. Dale, Student translations of natural language into logic: The Grade Grinder corpus release 1.0, in: Proceedings of the 4th international conference on educational data mining, 2011, pp. 51–60. [12] D. Barker-Plummer, R. Cox, R. Dale, J. Etchemendy, An empirical study of errors in translating natural language into logic, in: Proceedings of the Annual Meeting of the Cognitive Science Society, volume 30, 2008. [13] D. Barker-Plummer, R. J. Cox, R. Dale, Dimensions of dificulty in translating natural language into ifrst-order logic, Educational Data Mining (2009). URL: https://api.semanticscholar.org/CorpusID: 551970. [14] D. Barker-Plummer, R. Dale, R. J. Cox, A. Romanczuk, Using edit distance to mine for errors in a natural language to logic translation corpus, Educational Data Mining (2012). URL: https: //api.semanticscholar.org/CorpusID:15216148. [15] D. Barker-Plummer, J. Barwise, J. Etchemendy, Language, Proof, and Logic: Second Edition, 2nd ed., Center for the Study of Language and Information/SRI, 2011. [16] Meta AI, Llama 3.1: Large language models for multilingual applications, https://www.llama.com/, 2024. Accessed: 2024-09-15. [17] A. Dubey, A. Jauhri, A. Pandey, A. Kadian, et al., The Llama 3 herd of models, arXiv preprint arXiv:2407.21783 (2024). [18] Team Gemma, M. Riviere, S. Pathak, P. G. Sessa, C. Hardin, S. Bhupatiraju, L. Hussenot, T. Mesnard, B. Shahriari, A. Ramé, et al., Gemma 2: Improving open language models at a practical size, arXiv preprint arXiv:2408.00118 (2024). [19] D. Barker-Plummer, J. Barwise, J. Etchemendy, A. Liu, Tarski’s World: Revised and expanded edition, 2007. [20] E. Shinan, et al., Lark: A modern parsing library for python, https://github.com/lark-parser/lark, 2024. Accessed: 2024-09-05. [21] T. Akhade, et al., ZSS: A python library for tree edit distance, https://pythonhosted.org/zss/, 2024.
Accessed: 2024-09-19. [22] K. Zhang, D. Shasha, Simple fast algorithms for the editing distance between trees and related problems, SIAM journal on computing 18 (1989) 1245–1262. [23] L. de Moura, et al., Z3 theorem prover, https://github.com/Z3Prover/z3, 2024. Accessed: 2024-09-07. [24] O. Khattab, A. Singhvi, P. Maheshwari, et al., DSPy: Compiling declarative language model calls into self-improving pipelines, arXiv preprint arXiv:2310.03714 (2023).