# Quizzing the Translation: A Prover-Grounded Evaluation Metric for NLrightarrowFOL

arXiv: https://arxiv.org/abs/2609.33612 · HTML: https://mlsanity.com/paper/2609.33612/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 14 of its 34 references that are in the map.
- First posted on arXiv 27 Sep 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 14 of 14)

- [BERTScore: Evaluating Text Generation with BERT](https://mlsanity.com/paper/1904.09675/) (2019)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Harnessing the Power of Large Language Models for Natural Language to First-Order Logic Translation](https://mlsanity.com/paper/2305.15541/) (2023)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [SMATCH++: Standardized and Extended Evaluation of Semantic Graphs](https://mlsanity.com/paper/2305.06993/) (2023)
- [Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalization](https://mlsanity.com/paper/2507.07399/) (2025)
- [ASSESS: A Semantic and Structural Evaluation Framework for Statement Similarity](https://mlsanity.com/paper/2509.22246/) (2025)
- [Entailment-Preserving First-order Logic Representations in Natural Language Entailment](https://mlsanity.com/paper/2502.16757/) (2025)
- [Assessing the Sensitivity and Alignment of FOL Closeness Metrics](https://mlsanity.com/paper/2501.08613/) (2025)
- [Do LLMs Really Struggle at NL-FOL Translation? Revealing their Strengths via a Novel Benchmarking Strategy](https://mlsanity.com/paper/2511.11816/) (2025)
- [Improving Symbolic Translation of Language Models for Logical Reasoning](https://mlsanity.com/paper/2601.09446/) (2026)
- [A Theorem-Proving-Based Evaluation of Neural Semantic Parsing](https://mlsanity.com/paper/2510.11225/) (2025)

## Abstract (arXiv)

A standard pipeline for symbolic reasoning over natural-language problems translates them into first-order logic and invokes a theorem prover. The translation step is the bottleneck: swap "every" for "some" and every inference that follows is corrupted. Yet today's metrics often score more broken translations higher than less broken ones, because BLEU, BERTScore, and Smatch++ reward surface overlap that the worst errors happen to preserve. We introduce SIV, which derives two kinds of probes from the target formula and uses a theorem prover to verify the candidate translation against each. Positive probes are statements the candidate must entail, which detect translations that drop content; contrastive probes are statements the candidate must not entail, which detect translations that assert more than the original. On a controlled pool of perturbed FOLIO translations, the severity of the error accounts for 80% of SIV's score variance, compared with at most 17% for any prior metric. Across six error classes on a disjoint pool, SIV scores the reference above the perturbed candidate in over 99% of pairs. Because each probe is labeled with what it tests, the failure pattern also supplies a labeled error trace, recovering the perturbation class at macro-F1 0.638, nearly double the score-only baseline. On 434 expert-audited real LLM translations, SIV attains the top AUC, uniquely detects and grades expert-labeled major errors, and abstains, rather than mis-scoring, on out-of-vocabulary translations.