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

Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling
Jun 1, 2026Andrea Brunello, Cristian Curaba, Luca Geatti +3Legal Natural Language Processing Benchmarks Natural Language Inference
University of Udine, Italy
Beyond BLEU: A Case for Redefining Sign Language Translation Benchmarks
Sep 3, 2026Oline Ranum, Edward Fish, Simon Hadfield +1Gloss-Free Sign Language Translation Sign Language Translation
Centre for Vision, Speech and Signal Processing (CVSSP), University of Surrey
Last Translation Benchmark
Sep 3, 2026Vilém Zouhar, Niyati Bafna, Mukund Choudhary +257Machine Translation Quality Reproducibility

Jun 1, 2026, cs.CLJ/K move · Enter open · S save

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

Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani+2

University of Udine, Italy

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

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

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

Beyond BLEU: A Case for Redefining Sign Language Translation Benchmarks

Last Translation Benchmark