Quizzing the Translation: A Prover-Grounded Evaluation Metric for NL$\rightarrow$FOL

Pu Suo; Ali Emami

cs.CLSep 27, 2026

Quizzing the Translation: A Prover-Grounded Evaluation Metric for NL $\rightarrow$ FOL

Authors: Pu Suo, Ali Emami

Organizations: Emory University

Abstract

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.

Figures & tables

	Prover-grnd.	Quant.-aware	Graded	Per-trans.	Diagn. trace
BLEU	$\boldsymbol{\times}$	$\boldsymbol{\times}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$
BERTScore	$\boldsymbol{\times}$	$\boldsymbol{\times}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$
Smatch++	$\boldsymbol{\times}$	$\boldsymbol{\times}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$
LE	$\boldsymbol{\sim}$	$\boldsymbol{\times}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$
LT	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$
EPR	$\boldsymbol{\checkmark}$	$\boldsymbol{\checkmark}$	$\boldsymbol{\times}$	$\boldsymbol{\times}$	$\boldsymbol{\times}$

Table 1: Capability comparison of NL

\rightarrow

FOL evaluation metrics.

\boldsymbol{\checkmark}

supported;

\boldsymbol{\times}

not supported;

\boldsymbol{\sim}

partially supported. SIV is the only metric combining all five.

Tier	$\varphi^{\prime}$ vs. $\varphi$	Skeleton	Example perturbation
Ref	equivalent	—	canonical re-serialization
OS	strictly stronger	intact	add a nucleus conjunct
P	strictly weaker	intact	drop a nucleus conjunct
OW	strictly weaker	broken	flip outer $\forall\to\exists$

Table 2: Severity tiers, ordered by structural distance from

\varphi

. Skeleton refers to the top-level quantifier-connective pattern. OW ranks below P because skeleton damage changes the formula’s structural meaning, not just its informational content. Ref candidates are logically equivalent canonical re-serializations of the gold (Vampire-verified); their surface form differs from the FOLIO gold string (§ 4 , Setup).

	Ref	OS	P	OW	$\eta^{2}$	$d$
Metric	$105$	$58$	$25$	$184$
SIV	$\mathbf{1.00}$	$\mathbf{.929}$	$\mathbf{.442}$	$\mathbf{.052}$	$\mathbf{.802}$	$\mathbf{4.71}$
LE	$1.00$	$.850$	$.796$	$.713$	$.075$	$1.50$
LT (bin.)	$1.00$	$.000$	$.000$	$.000$	—	—
LT (graded)	$1.00$	$.500$	$.500$	$.500$	$.000^{\ddagger}$	—
Smatch++	$1.00$	$.806$	$.629$	$.740^{\dagger}$	$.072$	$1.84$

Table 3: Per-tier means and effect sizes.

\eta^{2}

: variance explained by tier.

d

: Cohen’s

d

on Ref-vs-OW.

\dagger

: metric scores OW higher than P. LT binary;

\eta^{2}

and

d

are degenerate.

\ddagger

: graded-LT (bidirectional prover entailment scored

1/0.5/0

; § 4.2 ) is constant across the three error tiers, so its between-tier variance is zero. Bootstrap

95\%

CIs on

d

: SIV

[3.96,6.04]

, LE

[1.29,1.83]

, Smatch++

[1.59,2.19]

, BERTScore

[1.02,1.71]

, BLEU

[0.72,1.51]

; SIV’s interval does not overlap any baseline’s.

			Drop magnitude [ $95\%$ CI]		Detection rate
Class	$n$	Relation to ref.	SIV-recall	SIV-F1	recall	F1
arg_swap	$494$	incompatible	$.818$ $[.796,.841]$	$\mathbf{.757}$ $[.731,.784]$	$.998$	$\mathbf{.998}$
negation_drop	$132$	incompatible	$.861$ $[.820,.899]$	$\mathbf{.820}$ $[.770,.868]$	$1.000$	$\mathbf{.992}$
random_substitution	$638$	incompatible	$.960$ $[.949,.970]$	$\mathbf{.942}$ $[.928,.956]$	$1.000$	$\mathbf{.998}$
flip_outer_quantifier	$355$	strictly weaker	$.984$ $[.975,.992]$	$\mathbf{.975}$ $[.961,.986]$	$1.000$	$\mathbf{.997}$
restrictor_drop ⋆	$231$	strictly stronger	$.000$ $[.000,.000]$	$\mathbf{.169}$ $[.163,.175]$	$.000^{\star}$	$\mathbf{.996}$

Table 4: Six perturbation classes with per-class drop magnitude (

\text{score}(\text{ref})-\text{score}(\text{perturbed})

, mean with

95\%

bootstrap CIs) and within-pair detection rate.

\star

: strictly-stronger classes saturate SIV-recall at

1.0

on both reference and perturbed candidates by construction, so SIV-F1’s signal on these classes comes entirely from the contrastive arm.

Class	$n$	F1	P	R	R ${}_{\,\text{95\% CI}}$
restrictor_drop	$231$	$.996$	$.996$	$.996$	$.976$ – $1.00$
strengthen_q	$15$	$.933$	$.933$	$.933$	$.681$ – $.998$
negation_drop	$132$	$.778$	$1.00$	$.636$	$.548$ – $.718$
random_sub	$638$	$.634$	$.464$	$1.00$	$.994$ – $1.00$
arg_swap	$494$	$.482$	$1.00$	$.318$	$.277$ – $.361$
flip_outer_q	$355$	$.006$	$1.00$	$.003$	$.000$ – $.016$

Table 5: Per-class trace classifier performance. R

{}_{\,\text{95\% CI}}

: Clopper-Pearson interval. Analyses of arg_swap and flip_outer_q in § 6.3 and § 6.4 .

Metric	AUC	$95\%$ CI
SIV	$\mathbf{0.841}$	$[0.707,0.935]$
Smatch++	$0.814$	$[0.715,0.899]$
LE	$0.799$	$[0.650,0.922]$
LT	$0.791$	$[0.754,0.826]$
BLEU	$0.708$	$[0.533,0.857]$
BERTScore	$0.668$	$[0.526,0.796]$

Table 6: AUC for separating expert-labeled correct from incorrect translations on the compatible-vocabulary stratum (

n=185

, of which

10

incorrect; expert-adjudicated labels).

Appendix figures & tables4 assets

Supplementary material from the paper’s appendix.

Appendix

Operator	LE AUC	SIV AUC
OW_flip_outer_quantifier	$0.500$	$\mathbf{1.000}$
OS_strengthen_quantifier	$0.500$	$\mathbf{1.000}$

Appendix

Table 7: LE is at chance on both quantifier-manipulation operators; SIV saturates at

1.000

. This reproduces Brunello et al. (2026) ’s propositional-collapse prediction operator by operator on the stratified pool.

Candidate	SIV	LE	LT	Sm++	BLEU	BS
root negation	$\mathbf{.022}$	$.000$	$.000$	$.864$	$.419$	$.858$
( OW mean)	$.052$	$.713$	$.000$	$.740$	$.397$	$.822$

Appendix

Table 8: Root-negation boundary probe: the direct negation of the reference, scored for all

105

Experiment-1 premises (Vampire-verified incompatible,

105/105

), with the OW -tier means for comparison. Sm++: Smatch++; BS: BERTScore.

Operator	Axis	Provenance
negate_atom	polarity (atom)	prior a,b
flip_quantifier	quantifier type	prior a,b
flip_connective	connective	prior a,b
replace_subf._w_neg.	polarity (subf.)	adapted c
swap_binary_args	argument order	new
drop_restrictor_conj.	restrictor	new d

Appendix

Table 9: Contrastive-operator provenance. a Brunello et al. (2026) ; b Thatikonda et al. (2025) ; c literal-level negation generalized to subformulas; d derived from the Barwise–Cooper decomposition ( Barwise and Cooper, 1981 ) , not from an error taxonomy; e post-audit extension operator, verified but not used in the § 4 –§ 7 experiments (see below).

Reference stratum	$n$	Recall
$\mathbf{S_{5}}$ ground-atom relations	$127$	$\mathbf{0.882}$
$S_{8}$ other	$9$	$0.667$
$S_{6}$ negation	$16$	$0.250$
$S_{3}$ universal-multi-restrictor	$176$	$0.125$
$S_{2}$ universal-simple	$49$	$0.082$
$S_{4}$ nested-quantifier	$86$	$0.081$

Appendix

Table 10: arg_swap recovery by reference stratum (discussed in § 6.3 ).

Explore similar work

Jun 1, 2026cs.CL

Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling

Accurate translation from Natural Language to First-Order Logic (NL-to-FOL) underpins neurosymbolic AI systems and Natural Language Inference (NLI), making the quality of NL-to-FOL benchmarks essential---yet these datasets have never been rigorously audited. Our first contribution is to present a systematic human inspection of the validation split of \textsf{FOLIO} and a subset of \textsf{MALLS} test instances, finding that approximately 42.5% and 42% of entries, respectively, contain incorrect FOL formalizations (i.e., ground truth labels), with additional rates of ambiguous NL sentences (17.8% and 51%) and incorrect NLI labels in \textsf{FOLIO} (8.4%). Our second contribution is to develop and release corrected ground truths for such datasets, showing that annotation errors distort model evaluation on a reference benchmark task: testing three state-of-the-art LLMs (Gemma~4 31B-it, Qwen3-30B-A3B, and GPT-4o-mini) with the corrected ground truths yields accuracy gains from +11 to +23 percentage points. Motivated by these findings, we propose an LLM-based framework to support humans in manual reviewing NL-to-FOL datasets. By directing reviewers toward the most error-prone instances, we empirically show that it is possible to achieve 90% dataset accuracy after reviewing fewer than 20% of instances, compared to over 76% required by unguided review. We release all human-verified annotations and the code for our framework.

Andrea Brunello, Cristian Curaba, Luca Geatti +3

University of Udine, Italy

Legal Natural Language Processing Benchmarks Natural Language Inference Human Annotations Annotations First-Order Logic

Ask PDF

Sep 3, 2026cs.CL

Beyond BLEU: A Case for Redefining Sign Language Translation Benchmarks

BLEU-4 is the standard metric for evaluating sign language translation (SLT), but spoken-language metrics may not adequately reflect sign language proficiency. The multimodal, low-resource context of SLT allows models to exploit spurious correlations and spoken-language priors, rather than learning stronger sign representations. In this paper, we evaluate the relationship between spatio-temporal understanding and BLEU-4 across six SLT models on Phoenix-2014T and CSL-Daily, showing that gains in BLEU-4 are not on their own evidence of better sign language understanding. This work introduces an alternative inspired by language-learning assessment, using an open-weight-LLM QA protocol that measures salient content preservation. It aligns more closely with human rankings and is six to seven times more paraphrase-invariant than BLEU-4. Applied to SLT, this protocol targets content transfer, is more robust to train-test overlap, and gives a different picture of the field: the five gloss-free systems are largely within noise of one another on Phoenix-2014T, while the gloss-supervised system stands 9.3 points higher, a gap invisible to BLEU-4.

Oline Ranum, Edward Fish, Simon Hadfield +1

Centre for Vision, Speech and Signal Processing (CVSSP), University of Surrey

Gloss-Free Sign Language Translation Sign Language Translation Multilingual Benchmark Spatiotemporal

Ask PDF

Sep 3, 2026cs.CL

Last Translation Benchmark

For scientific progress, we need benchmarks that test the limits of state-of-the-art models, and evaluation methods that inform us about failure cases. As models get stronger, standard benchmarks for machine translation are approaching saturation. Further, automatic translation metrics are unreliable, opaque, and vulnerable to reward-hacking. Even gold human evaluation is not problem-free, because it often lacks reproducibility, objectivity, and scalability. Overall, this prevents us from tracking progress in the field and identifying pathways for improvement. We introduce the Last Translation Benchmark, a collection of human-authored and peer-reviewed examples (texts, images, audio, videos) that break leading machine translation models. We also present a new evaluation approach: each example comes with handcrafted verification rules describing concrete failure cases on that example, therefore allowing reliable and actionable future evaluation. The Last Translation Benchmark is a live dataset that accepts ongoing contributions. The latest version is LTBv1, containing accepted contributions prior to September 1st 2026, with future releases planned as new data is continuously collected.

Vilém Zouhar, Niyati Bafna, Mukund Choudhary +257

Machine Translation Quality Reproducibility

Ask PDF