This paper explores how natural-language descriptions of formal languages can be compared to their formal representations and how semantic differences can be explained. This is motivated from educational scenarios where learners describe a formal language (presented, e.g., by a finite state automaton, regular expression, pushdown automaton, context-free grammar or in set notation) in natural language, and an educational support system has to (1) judge whether the natural-language description accurately describes the formal language, and to (2) provide explanations why descriptions are not accurate. To address this question, we introduce a representation language for formal languages, Nile, which is designed so that Nile expressions can mirror the syntactic structure of natural-language descriptions of formal languages. Nile is sufficiently expressive to cover a broad variety of formal languages, including all regular languages and fragments of context-free languages typically used in educational contexts. Generating Nile expressions that are syntactically close to natural-language descriptions then allows to provide explanations for inaccuracies in the descriptions algorithmically. In experiments on an educational data set, we show that LLMs can translate natural-language descriptions into equivalent, syntactically close Nile expressions with high accuracy - allowing to algorithmically provide explanations for incorrect natural-language descriptions. Our experiments also show that while natural-language descriptions can also be translated into regular expressions (but not context-free grammars), the expressions are often not syntactically close and thus not suitable for providing explanations.
Figures & tables
Language
Format
#
#RD
R1
{abn∣n≥1}
Set
276
28
R2
{ε}∪{wa∣w∈{a,b}∗}
RE
273
22
R3
{w∈{a,b}∗∣w contains aaa}
NFA
255
29
C1
{w∈{a,b}∗∣#b(w)≥#a(w)}
CFG
209
45
C2
{anbn∣n∈N0}
PDA
201
17
R4
{ambn∣m even,n odd}
Set
205
18
Table 1: Exercises in the dataset including format in which the language is presented to students, number of submissions ( # ), and number of non-equivalent Nile expressions produced by the LLM in our experiments ( #RD ) for the submissions.
all
Regular languages
Context-free languages
Design data
Validation data
Design data
Validation data
#
%
#
%
#
%
#
%
#
%
all descriptions
2040
100%
711
100%
585
100%
348
100%
396
100%
RQ 1 : How well can LLMs decide whether a natural-language description fits to a formal language?
(M1) Directly
1956
95.88%
676
95.08%
564
96.41%
343
98.56%
373
94.19%
(M2) Via classical representation (RE / CFG)
1913
93.77%
704
99.02%
572
97.78%
309
88.79%
328
82.83%
Table 2: Summary of the evaluation of RQs 1 to 3. Overall performance, performance for regular languages R1 – R6 and performance for context-free languages C1 – C5 is shown. For RQ 1, the LLM was asked to judge correctness directly or to construct a formal representation (RE, CFG, Nile ) which was then checked for correctness algorithmically. For RQs 2 and 3, the LLM was asked to construct a semantically and syntactically matching formal representation. Only design data (languages R1 – R3, C1, C2) has been used for conceptual and prompt design. Posthoc adjusting the prompt for Nile with two additional examples for non-covered idioms increases the performance to 87.86% △ , 93.69% ∗ , 85.86% ∗∗ , and 80.30% ∗∗∗ . A more detailed evaluation can be found in Appendix B in the appendix.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Task
{L}
{L,L~1,(...)}
{L~1}
{L~1,L~2,(...)}
∅
R1
73
50
78
25
50
R2
157
32
51
15
18
R3
121
22
66
21
25
C1
52
2
114
17
24
C2
50
19
89
5
38
R4
91
32
77
1
4
Appendix
Table 3: Categorization of submissions per task by correctness, ambiguity and validity.
Design data
all
all
R1
R2
R3
C1
C2
#
%
#
%
#
%
#
%
#
%
#
%
#
%
all descriptions
2040
100%
1059
100%
226
100%
255
100%
230
100%
185
100%
163
100%
describing the solution language: {L}
956
453
73
157
121
52
50
describing non-solution language(s): {L~1,(...)}
862
481
103
66
87
131
94
describing non- and solution language(s): {L,L~1,(...)}
222
125
50
32
22
2
19
Appendix
Table 4: Detailed data for the evaluation of RQs 1 to 3. Overall performance, performance for regular languages R1 – R3 and performance for context-free languages C1 – C2 is shown. For RQs 2 and 3, the LLM was asked to construct a semantically and syntactically matching formal representation (RE, CFG, Nile ). For RQ 1, in addition to formally checking equivalence of the LLM output to the solution language, the LLM was also asked to judge equivalence directly. Only design data (languages R1 – R3, C1, C2) has been used for conceptual and prompt design. The prompt (M3 ∗ ) denotes a posthoc extension of prompt (M3) by two additional examples for non-covered Nile idioms. This adjustment significantly increased the performance for R5 and C3. We further distinguish descriptions according to whether they unambiguously describe the solution language, unambiguously describe non-solution languages, or can describe a solution and a non-solution language, corresponding to Category (1), Categories (3) – (4), and Category (2) respectively, as defined in Section A.5 . Since ambiguous submissions achieve a RQ 1 performance of 100% by definition, the corresponding rows have been omitted.
Validation data
all
R4
R5
R6
C3
C4
C5
#
%
#
%
#
%
#
%
#
%
#
%
#
%
all descriptions
981
100%
201
100%
192
100%
192
100%
153
100%
126
100%
117
100%
describing the solution language: {L}
503
91
111
156
86
22
37
describing non-solution language(s): {L~1,(...)}
381
78
52
26
48
100
77
describing non- and solution language(s): {L,L~1,(...)}
97
32
29
10
19
4
3
Appendix
Table 5: Detailed data for the evaluation of RQs 1 to 3. Performance for regular languages R4 – R6 and for context-free languages C3 – C5 is shown. For RQs 2 and 3, the LLM was asked to construct a semantically and syntactically matching formal representation (RE, CFG, Nile ). For RQ 1, in addition to formally checking equivalence of the LLM output to the solution language, the LLM was also asked to judge equivalence directly. Only design data (languages R1 – R3, C1, C2, see Table 4 ) has been used for conceptual and prompt design. The prompt (M3 ∗ ) denotes a posthoc extension of prompt (M3) by two additional examples for non-covered Nile idioms. This adjustment significantly increased the performance for R5 and C3. We further distinguish descriptions according to whether they unambiguously describe the solution language, unambiguously describe non-solution languages, or can describe a solution and a non-solution language, corresponding to Category (1), Categories (3) – (4), and Category (2) respectively, as defined in Section A.5 . Since ambiguous submissions achieve a RQ 1 performance of 100% by definition, the corresponding rows have been omitted.
Regular languages
Context-free languages
all
Design data
Validation data
all
Design data
Validation data
#
%
#
%
#
%
#
%
#
%
#
%
all descriptions
1296
100%
711
100%
585
100%
744
100%
348
100%
396
100%
describing the solution language: {L}
709
351
358
247
102
145
describing non-solution language(s): {L~1,(...)}
412
256
156
450
225
225
describing non- and solution language(s): {L,L~1,(...)}
175
104
71
47
21
26
Appendix
Table 6: Detailed data for the evaluation of RQs 1 to 3. Accumulated performance for regular languages and context-free languages (overall and split into design data and validation data as indicated in Tables 4 and 5 ) is shown. For RQs 2 and 3, the LLM was asked to construct a semantically and syntactically matching formal representation (RE, CFG, Nile ). For RQ 1, in addition to formally checking equivalence of the LLM output to the solution language, the LLM was also asked to judge equivalence directly. Only design data (languages R1 – R3, C1, C2, see Table 4 ) has been used for conceptual and prompt design. The prompt (M3 ∗ ) denotes a posthoc extension of prompt (M3) by two additional examples for non-covered Nile idioms. This adjustment significantly increased the performance for R5 and C3. We further distinguish descriptions according to whether they unambiguously describe the solution language, unambiguously describe non-solution languages, or can describe a solution and a non-solution language, corresponding to Category (1), Categories (3) – (4), and Category (2) respectively, as defined in Section A.5 . Since ambiguous submissions achieve a RQ 1 performance of 100% by definition, the corresponding rows have been omitted.
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⊑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
Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.
Joost J. Joosten, Marina López Chamosa, Sofía Santiago Fernández
Universitat de Barcelona, Barcelona, Spain · Centre de Recerca Matem`atica, Barcelona, Spain · Formal Vindications S.L., Barcelona, Spain
When an LLM formalizes natural language, how do we know the output is faithful? We propose a roundtrip verification approach which does not require ground-truth annotations: formalize a statement, translate the result back to natural language, re-formalize, and use a formal tool to check logical equivalence. When the two formalizations agree, this provides evidence of a faithful formalization. When they disagree, a stage-level diagnosis localizes the error to a specific translation step, and a scoped repair operator attempts to correct that step. We evaluate the framework on two statutory domains (the Texas Transportation Code and the Texas Parks and Wildlife Code) using two LLMs (Claude Opus~4.6 and GPT-5.2) with three repair baselines. Diagnosis-guided scoped repair is the most effective method, with effectiveness contingent on the reliability of the diagnosis function. Across both domains and both models, under our full repair system, rules that fail the equivalence check show 1.4x-2.5x more natural language inference (NLI) drift than rules that pass it.