FOLLIE: Automated Reasoning over the First Dataset of Sentences with their First-Order Logical Representation for French

Maximos Skandalis

cs.CLNov 1, 2026

FOLLIE: Automated Reasoning over the First Dataset of Sentences with their First-Order Logical Representation for French

Authors: Maximos Skandalis

Organizations: LIRMM, CNRS & University of Montpellier, Montpellier, France

Abstract

FOLLIE (for First-Order Logic for Language Inference and Entailment for French) connects French sentences, compositional first-order representations and automated natural language inference (NLI). The first French NLI-ready, NL-to-FOL resource, it contains 19,983 inference records and 36,987 non-empty sentence-slot--formula mappings from six heterogeneous NLI sources, retaining French lexical material and source problem structure. Its silver annotations are produced by a neural--symbolic pipeline, with 111 separately identified LLM-assisted additions. The construction combines morphosyntactic analysis, probability-conditioned categorial multitagging, grammatical proof search, discourse representation and first-order semantic construction. Stage-wise experiments show substantial gains in derivation coverage; analyses of conjunction distributions, logical-operator incidence and scope alternation characterise the resulting resource. We then develop an automatic inference engine whose input-conditioned background theories address lexical relations, quantification, quantities, event structure and temporal dependencies. Prover9 supplies proofs for entailment and contradiction, while Mace4 supports bounded consistency checks. Three-way accuracies are 65.37% on all 335 FraCaS-FR problems, 70.33% on 300 GQNLI-FR problems and 71.35% on 9,399 eligible SICK-FR records pooled across splits. Agreement with reference labels among committed decisions is 93.53%, 100.00% and 98.66%, at commitment coverage of 41.49%, 37.00% and 15.05%, respectively. Worked constructions, axiom schemas and proof analyses explain these outcomes and identify the contributions of scope, reference, lexical knowledge and numerical structure. FOLLIE provides a French experimental basis for studying the representations and assumptions that connect sentence interpretation to deductive inference.

Figures & tables

Resource	Language and source	Annotation unit and scale	Formal target and provenance
FOLIO ( Han et al., 2024a )	Expert-authored English stories	1,430 query examples; 487 premise sets	Human-aligned FOL, shared story vocabulary and three-way labels
RuleTaker ( Clark et al., 2020 ) ; ProofWriter ( Tafjord et al., 2021 )	Generated English facts and rules; paraphrases	Theory–query instances; depth-specific datasets	Logic-program theories and labels; proof graphs in ProofWriter
LogicNLI ( Tian et al., 2021 )	Templates with manual linguistic revision	20K main train/dev/test problems	Unary-predicate formulas, directional derivations and four labels
FLD $\times$ 2 ( Morishita et al., 2024 )	Proof-first English verbalisation	110K train/dev/test problems	Logical formulas, derivations and three labels
MALLS ( Yang et al., 2024 )	LLM-generated English	28K sentence–formula pairs	1K human-annotated pairs; 27K filtered automatic targets
WillowNLtoFOL ( Deveci, 2026 )	Reviewed seeds; LLM-expanded English	16,014 sentence–formula pairs	FOL; structural checks and selective semantic review

Table 1: Representative logical resources. Counts retain their stated units; LogicNLI excludes auxiliary diagnostic sets. FOLLIE counts non-empty sentence-slot–formula mappings, including repeated occurrences (Table 4 ).

Panel of Figure 1 — Figure 1: Construction stages and retained representations. Multitagging widens the categories available to proof search; discourse normalisation fixes binding and accommodation before logical compilation.

Corpus	Split	$N$	$\beta$	Parsed	Coverage	Failed	Limits	Types/word
SICK-FR	all	19,680	1	18,294	92.96	1,386	0	1.0000
			0.1	19,285	97.99	395	0	1.0256
			0.01	19,564	99.41	116	0	1.0618
			0.001	19,619	99.69	61	0	1.1431
			0.0001	19,644	99.82	34	2	1.4157
FraCaS-FR	test	882	1	838	95.01	44	0	1.0000

Table 2: Multitagging and grammatical proof coverage for every FOLLIE component.

N

counts input sentence units; SICK-FR combines its splits. Coverage is

100\times\mathrm{Parsed}/N

, rounded to two decimal places; bold marks the highest evaluated coverage in each group. “Failed” excludes resource-limit failures (“Limits”), so the three outcome counts sum to

N

. Types/word is the mean number of retained categories. A dash marks an unavailable proof-search outcome: the final XNLI-FR and DACCORD rows contain category densities only. Derivation coverage does not establish semantic correctness.

Corpus	Split	Parsed units	Generated	Closed
FraCaS-FR		881	798	798 (90.58%)
GQNLI-FR		698	676	676 (96.85%)
SICK-FR		19,644	19,198	19,198 (97.73%)
DACCORD		2,210	1,695	1,677 (75.88%)
RTE3-FR	Development	1,899	1,589	1,569 (82.62%)
RTE3-FR	Test	1,788	1,530	1,515 (84.73%)

Table 3: Automatic compilation coverage after semantic reduction, DRS-to-FOL translation, formatting and alignment. Percentages divide generated representations passing the closure check by parsed units. Counts precede assisted completion and count sentence occurrences within source problem structures.

$e_{0}\ z_{0}\ x_{1}\ y_{1}\ z_{1}\ x_{2}\ y_{2}\ z_{2}$
$\|x_{2}\|>\textrm{$ 1 $}$
$\textrm{donnée}(x_{2})$
$\textrm{de}(x_{2},y_{2})$
$\|y_{2}\|>\textrm{$ 1 $}$
$\textrm{satellite}(y_{2})$
$\textrm{de}(y_{2},z_{2})$

Figure 2: Examples of lambda-term derivation, generated discourse and first-order representations for two French sentences. Each DRS separates its presuppositional background from its main content; the second example also contains labelled embedded content.

Source	Split	Rows	P mappings	H mappings	All mappings	NL types	P+H rows
DACCORD	test	952	859	838	1,697	1,523	601
FraCaS-FR	test	346	536	342	878	620	342
GQNLI-FR	test	300	403	300	703	326	300
RTE3-FR	dev.	790	814	775	1,589	1,399	592
RTE3-FR	test	790	748	782	1,530	1,346	593
SICK-FR	train	4,423	4,337	4,329	8,666	4,490	4,243

Table 4: Composition of FOLLIE, including the additional FraCaS-FR and GQNLI-FR completion layer. P+H rows contain at least one available premise mapping and one available hypothesis mapping; they need not contain every expected premise. NL types are deduplicated within each constituent file; the total is deduplicated across all files and is therefore not their sum.

Source	Split	Mappings	Total &	Mean (SD)	Median [Q1,Q3]	Min. ( $n$ )	Max. ( $n$ )	$\rho_{s}$
DACCORD	test	1,697	35,162	20.72 (10.24)	19 [14,26]	1 (1)	97 (1)	.924
FraCaS-FR	test	878	6,948	7.91 (5.03)	7 [5,9]	0 (1)	56 (5)	.823
GQNLI-FR	test	703	7,494	10.66 (5.28)	10 [7,15]	0 (3)	27 (6)	.942
RTE3-FR	dev.	1,589	28,519	17.95 (14.45)	13 [8,25]	0 (1)	127 (1)	.966
RTE3-FR	test	1,530	25,808	16.87 (13.18)	11 [7,24]	0 (3)	89 (2)	.965
SICK-FR	train	8,666	59,250	6.84 (3.66)	6 [4,9]	1 (56)	27 (1)	.898

Table 5: Conjunction-count distribution in the 36,987 aligned mappings. SD is the population standard deviation; Q1 and Q3 are nearest-rank quartiles. Parenthesised

n

gives the number of occurrences attaining each extreme.

\rho_{s}

is Spearman’s correlation with whitespace-token length.

Source/split	Mappings	$\neg$	$\lor$	$\to$	Any Boolean	$\exists$	$\forall$	Eq./neq	$<$ / $>$	Bare ?
DACCORD	1,697	379	61	140	442	1,697	118	1,155	1,445	200
FraCaS-FR	878	21	13	89	108	877	73	330	639	41
GQNLI-FR	703	66	18	6	87	703	3	550	386	33
RTE3-FR dev.	1,589	58	60	27	127	1,589	25	932	1,221	144
RTE3-FR test	1,530	58	41	28	107	1,530	25	834	1,198	133
SICK-FR train	8,666	957	8	92	965	8,666	58	1,908	1,790	173

Table 6: Incidence of logical and relational notation in aligned mappings. Each cell counts mappings containing the notation at least once; columns are non-exclusive. “Any Boolean” is the union of negation, disjunction and implication, excluding conjunction.

Source/split	$N_{s}$	$a_{Q}>0$ (%)	$\max a_{Q}$	$a_{B}>0$ (%)	$\max a_{B}$
DACCORD	1,697	20.27	3	23.22	4
FraCaS-FR	882	9.41	2	11.68	4
GQNLI-FR	700	7.71	1	10.00	1
RTE3-FR dev.	1,587	3.84	2	7.37	4
RTE3-FR test	1,530	3.92	2	6.21	3
SICK-FR, all splits	19,198	9.59	1	7.09	3

Table 7: Quantifier and Boolean scope alternation after NNF conversion.

N_{s}

counts the formulas included in the structural analysis, separately from the complete aligned-mapping population. Each percentage uses the

N_{s}

in its own row. SICK-FR pools all three splits.

Operation	Recognised configuration	Representation effect
Negative-determiner lift	aucun $(d)$ and des $(d,c)$	Replace an asserted marker by negation of the designated existential scope
Upper-bound lift	plus , a_ , exact num marker	Exclude a relevant group above the cardinal threshold
Sentence-negation repair	Lifted sortals, one negative existential, witness linker	Restore the selected negative-existential clause reading
Restrictor annotation	Vague quantifier with associated sortals	Add an exact restrictor signature; original conjuncts remain
Comparative separation	Gradable head in a measure comparison	Distinguish comparative from independently asserted positive predication
Duration abstraction	Number, time unit and duration role	Replace the measure frame by a sealed duration atom

Table 8: Principal preprocessing operations, subject to the semantic preconditions specified in the text.

First-Order Logic

See all 9 papers

Jun 1, 2026

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 FOLIO and a subset of 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 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

LLM-Assisted Annotation Human-in-the-Loop Annotation Natural Language Inference

Ask PDF

Sep 27, 2026

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

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.

Pu Suo, Ali Emami

Emory University

Language Model Error Detection Mathematical Reasoning Semantic Parsing

Ask PDF

Sep 26, 2026

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

Large Language Models (LLMs) are highly capable of natural language reasoning and appear to store a great deal of lexical knowledge, but it is still unclear how much of this knowledge they actually use when reasoning, and whether they use it in the right way. On the other hand, logic-based Natural Language Inference (NLI) systems provide transparent and formally grounded reasoning, but they need to be supplied with rich lexical knowledge to prove inferences beyond purely logical ones. In this paper, we evaluate whether LLMs can identify all lexical knowledge needed to solve NLI problems and how much this knowledge contributes to proof search in a logic-based NLI system. Our research focuses exclusively on structured lexical entailments (e.g., chinchilla

\sqsubseteq

small animal) as a proxy for structured explanations for NLI problems with an entailment label. First, we curate a dataset for a new task of explaining sentential entailments with a set of lexical entailments. The dataset is used to intrinsically evaluate LLMs on generating structured lexical explanations. Then, we use NLI as an extrinsic evaluation in a simple neuro-symbolic setting, assessing whether LLMs can supply sufficient lexical relations to LangPro, a natural-logic theorem prover for natural language. The results show that the proposed task remains challenging even for hosted proprietary LLMs, and that their contribution to theorem proving is moderate: generated relations are often only partially sound and may be tailored to the specific NLI problem rather than representing generally valid lexical knowledge.

Jorryt de Jong, Stefan Moraca, Ettore Cesari +1

Utrecht University, the Netherlands · Institute for Language Sciences, Utrecht University, the Netherlands

LLM Reasoning Natural Language Inference Logical Reasoning

Ask PDF

Abstract

First-Order Logic

Explore similar work

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

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

Explaining Textual Entailment with Lexical Entailments: Using LLMs to Supply Lexical Relations for Formal Proofs

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