Assessing the Sensitivity and Alignment of FOL Closeness Metrics (2025)

Abstract: The recent successful paradigm of solving logical reasoning problems with tool-augmented large language models (LLMs) leverages translation of natural language (NL) statements into First-Order Logic (FOL) and external theorem provers. However, the correctness of FOL statements, comprising operators and text, often go unverified due to the lack of a reliable evaluation metric for comparing generated and ground-truth FOLs. In this paper, we conduct a comprehensive study on the sensitivity of existing metrics—NL, FOL, and graph-based— and their alignment with LLM as a judge on FOL evaluation to measure robustness. We introduce operator and text-based perturbations to ground-truth FOL statements to assess metric sensitivity. We then evaluate metric robustness by comparing them against LLMs judgement. Our empirical findings highlight a clear oversensitivity in the n-gram metric BLEU for text perturbations. The operator perturbation affects the semantic graph metric Smatch++ for structural changes, and the FOL metric for specific operator changes. We observe a closer alignment between BertScore and LLM judgement, proving the importance of semantic evaluation. Additionally, we show that combining metrics enhances both robustness and sensitivity compared to using individual metrics.

## introduction large language models (llms) have advanced natural language reasoning, but logical and mathematical reasoning have long relied on formal, structured languages for proving deductions and theorems, a process that predates deep neural networks @xcite . this approach remains relevant today, especially for reasoning tasks that can be solved using formal statements. in case of firstorder logic (fol), llm generations are used as intermediate steps and subsequently passed to theorem provers to solve the problem @xcite @xcite . compared to the chain-of-thought (cot) approach @xcite , where the model first reasons and then solves, fol generation demonstrated superior reliability by offloading the reasoning task to an external tool. translating natural language (nl) into fol enhanced the overall rigor of the process. generating fol from nl is a challenging task that tests the ability of llms to accurately interpret and convert informal language into a formal, structured token sequence @xcite . the lack of ground truth for fol generations complicates direct verification. @xcite addressed this challenge by developing a system specifically for fol generation, incorporating an operator-based evaluator to rate the outputs. this evaluation is combined with bleu score, using a threshold as a metric in a reward model. however, the reliance on thresholds complicates the interpretation of translation quality. manually assessing formal logic generations is labor-intensive and has received relatively less attention compared to traditional text translation metrics. in this work, we analyze existing natural language translation, tree, and graph evaluation metrics, focusing on those that offer strong sentencelevel comparisons. we establish a framework to systematically introduce perturbations and analyze the existing metrics in the presence of these anomalies in formal language, specifically first-order logic. metric sensitivity helps reveal the degree to which each metric responds to specific types of perturbations. to further assess these metrics on real-world examples, we generate sample fols for nl statements in folio @xcite and @xcite datasets using an llm and rank them against ground truth values. the ranking is conducted using established metrics, and llm-based evaluators. after a small-scale experiment to select the llm most aligned with human judgment for this task, we measure how well each metric-based ranking aligns with the selected llm's judgments foot_1 . our experiments reveal that bertscore has a better alignment as an individual metric, and its combination with other metrics could further boost its alignment. our findings provide insights into the sensitivity of current metrics and their applicability to symbolic generation tasks. ## fol closeness metrics evaluation scores in natural language generation, such as bleu @xcite and rouge @xcite , perform n-gram matching between reference text and candidate outputs. me-teor @xcite , while also based on n-gram overlap, incorporates additional factors known to result in improved correlation with human judgments. bertscore (zhang et al., 2020) leverages contextual embeddings generated by a pre-trained bert @xcite to compute cosine similarity between sentences. in contrast, logical equivalence @xcite evaluates fol translations by comparing the truth values of formal statements, abstracting away from their textual semantics. another relevant domain is abstract meaning representation (amr) graph metrics, which compare the structural similarity of semantic graphs. given the structured nature of fol statements, we leverage smatch++ (opitz, 2023), which incorporates preprocessing, alignment, and sub-graph scoring. these metrics capture different dimensions of divergence between ground truth and translations: traditional metrics focus on surface-level and semantic discrepancies, while formal evaluation methods assess deeper logical consistency. we present results demonstrating how a representative set of these metrics respond to variations in logical constructs within formal language translations. ## results and discussion we present results from the two variations. ## conclusion this study has explored the sensitivity of various metrics in evaluating the closeness of generated first-order logic (fol) translations of natural language statements and the ground-truth. by carefully analyzing the sensitivity of existing metrics through perturbations of ground-truth fols, we identified critical gaps in commonly used metrics. commonly used fol metrics are not sufficient for handling anomalies in fol generation while bertscore in isolation and in combination with other metrics offer the most reliable measure. future work. the conclusions presented in this paper highlight the opportunity to choose a sensitivity-or alignment-based metric depending on the application. the identified metric combinations can serve as a reward function to support the development of translation models or formal generation systems in reasoning spaces. we also emphasize that a dependable automatic metric is essential, not only for rigorous evaluation but also for training the next generation of models that accurately translate natural language into formal symbolic representations. this need is particularly urgent for autoformalization @xcite . we hope the systematic evaluation framework presented here will encourage the development of even more reliable metrics.