$\forall$uto$\exists$$\lor\!\land$L: Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks
Under review as a conference paper at ICLR 2025

UTO

L: AUTONOMOUS EVALUATION OF LLMS

∀
FOR TRUTH MAINTENANCE AND REASONING TASKS

∃∨∧

Anonymous authors
Paper under double-blind review

ABSTRACT

∀

∀

uto

uto

∃∨∧

This paper presents
L, a novel benchmark for scaling Large Language
Model (LLM) assessment in formal tasks with clear notions of correctness, such
as truth maintenance in translation and logical reasoning.
L is the first
benchmarking paradigm that offers several key advantages necessary for scaling
objective evaluation of LLMs without human labeling: (a) ability to evaluate
LLMs of increasing sophistication by auto-generating tasks at different levels
of difficulty; (b) auto-generation of ground truth that eliminates dependence on
expensive and time-consuming human annotation; (c) the use of automatically
generated, randomized datasets that mitigate the ability of successive LLMs to
overfit to static datasets used in many contemporary benchmarks. Empirical
L is highly indicative of its
analysis shows that an LLM’s performance on
performance on a diverse array of other benchmarks focusing on translation and
reasoning tasks, making it a valuable autonomous evaluation paradigm in settings
where hand-curated datasets can be hard to obtain and/or update.

∃∨∧

∃∨∧

uto

∀

1

INTRODUCTION

Foundation Models such as Large Language Models (LLMs) have been demonstrated to successfully
perform many natural language tasks involving formal syntax such as autoformalization – utilizing
LLMs in converting natural language (NL) to formal syntax (FS) such as source code, math etc.,
(Wu et al., 2022; Liang et al., 2023; Guan et al., 2023), informalization – using LLMs to convert FS
to NL (e.g. code summarization), reasoning – using LLMs to perform sound reasoning or derive
proofs. Although these methods have been successful in small-scale scenarios, their effectiveness
in maintaining truth across NL and FS remains uncertain due to the difficulty in assessing truth
maintenance in such tasks. Multiple authors have noted that existing benchmarks and evaluation
methodologies for such tasks are susceptible to the Benchmark Contamination Problem due to their
use of static datasets, e.g, HumanEval (Chen et al., 2021; Wu et al., 2022; Han et al., 2022). One
effective method to mitigate this problem in existing benchmarks is creating new data (Xu et al.,
2024). However, scaling such datasets as LLMs evolve is a tedious and expensive process since their
data-generation task requires expert annotators to hand-generate well-balanced datasets. Moreover,
such benchmarks often rely on insufficient/incomplete measures of evaluation (e.g, BLEU scores
(Callison-Burch et al., 2006), ranking disparities in LLM-generated code on test cases in HumanEval
vs HumanEval+ (Liu et al., 2023a)), and thus, provide misleading signals on LLM capabilities.

This paper addresses three key desiderata for benchmarking LLM capabilities for truth maintenance
across NL and FS: (D1) Can we dynamically generate out-of-distribution datasets without relying on
human annotators? (D2) How do we accurately assess an LLM’s truth maintenance capabilities?
(D3) Can our metric serve as a predictor of LLM performance in FS-based tasks?

For §D1, we introduce a new approach that utilizes context-free grammars to generate well-balanced,
out-of-distribution datasets on the fly. For §D2, we perform closed-loop testing of LLM capabilities
using formal verifiers to automatically evaluate its truth maintenance capabilities. To answer §D3, we
show that our metrics can serve as predictors of LLM performance on other, well-known benchmarks.

Main contributions Our key contributions are as follows:

1. A new, dynamic approach for automatic synthesis of well-balanced test datasets that are

unlikely to be memorized or seen during the LLM’s training process.

1

000
001

002
003
004
005
006
007

008
009
010
011
012
013

014
015
016
017
018

019
020
021
022
023
024

025
026
027
028
029
030

031
032
033
034
035
036

037
038
039
040
041

042
043
044
045
046
047

048
049
050
051
052
053

Under review as a conference paper at ICLR 2025

2. The utilization of formal verifiers such as theorem provers to provably validate syntax-
independent notions of correctness without having to exhaustively test over all possible truth
valuations of formal syntax involving logic.

3.

uto

∃∨∧

L: a scalable, plug-and-play assessment system for benchmarking new LLMs as
∀
and when they are developed. Our system can be extended to any class of formal syntax that
uses a grammar and admits an equivalence checker.

4. We show that LLM performance on our metric serves as an effective indicator of LLM per-
formance on other metrics across a wide variety of tasks such as first-order logic reasoning,
etc. Thus, our metric offers a scalable and efficient surrogate for evaluating new LLMs in
such tasks where other metrics may be limited due to the unavailability of new datasets. Our
empirical evaluation shows that SOTA LLMs are unable to maintain truth effectively.

2 FORMAL FRAMEWORK

(Large) Language Models (L)LMs LMs are non-linear functions represented by (billons of) param-
eters θ that, given a set of input tokens x1, . . . , xn, typically representing NL, predict the output token
x1, . . . , xn, y1, . . . , yi; θ). The input tokens contains context κ
yi+1 using the distribution P (yi+1
|
(also known as a prompt) that provides the necessary information for the task (e.g., instructions, etc).
It is known that κ significantly impacts the response quality y1, . . . , yn (Sahoo et al., 2024).

Propositional Logic Propositional logic is a branch of logic that utilizes propositions and logical
operators (e.g., conjunction:
, etc) to construct sentences that can be used to perform reasoning
using the rules of logic. For example, propositions, p1 = It is raining, p2 = It is sunny can be used
to create a sentence P = p1
p1 is observed, then one can use the rules of
inference to deduce that p2 is true (Huth & Ryan, 2004).

p2. If P is true and

∧

∨

¬

∀

Equivalence in Propositional Logic Two sentences in propositional logic, P1 and P2, are equivalent,
P1
p2
≡
since

P2, iff their truth values agree for all possible assignments. E.g.,
True, False
p2.
p1, p2
}

True, False

p2) =

} × {

≡ ¬

∨ ¬

∨ ¬

p2)

∈ {

(p1

(p1

First-order Logic (FOL) FOL differs from propositional logic in that sentences are constructed
using predicates, quantifiers, and objects. A popular example is the syllogism where, given two
Mortal(x) and Man(Socrates), one can conclude that
first-order logic sentences
→
Mortal(Socrates). A first-order logic sentence F can be interpreted using a universe
, a substitution
operator σ, and an interpretation function

(Russell & Norvig, 2020).

x. Man(x)

p1

p1

¬

∧

¬

∧

¬

U

∀

,

Equivalence in First-order Logic Two sentences, F1, F2 in first-order logic are equivalent, F1
iff they are equivalent under all possible models. E.g.,

x. Man(x)

Man(y).

y.

F2,

≡

¬∀

≡ ∃

¬

Regular Expressions A regular expression (regex) is a sequence of characters that can be used to
determine whether a particular string matches the pattern or language induced by the regex. For
example, the regex 200(00)∗1 using Σ =
matches all strings possible using Σ that begin
0, 1, 2
{
with a two, followed by one or more pairs of zeroes, and end with a one (Hopcroft et al., 2001).

}

≃

Equivalence between Regular Expressions Two regexes, R1 and R2 are equivalent, R1
represent the same language. It is known that R1
finite automata (DFAs), D1, D2, are isomorphic, i.e., D1

≡
D2 (Hopcroft et al., 2001).

R2, if they
R2 if their corresponding minimal deterministic

≡

We refer to sentences (strings) in first-order and propositional logic (regexes) as formal syntax FS in
this paper. We now provide a definition of (Auto/In)formalization in the context of LLMs and FS.
Definition 2.1 (Autoformalization:
autoformalization,

). Given an LLM L, an NL description ψ and context κ,

L(ψ, κ), is defined as using L to translate ψ to FS φ s.t.

ψ.

A

−1
L (φ, κ′)

A

≡

Example One possible autoformalization of “Every human drinks coffee but some are not dependent
on it” in FOL is
∀
Definition 2.2 (Informalization:
informalization,

). Given an LLM L, an expression φ in FS and context κ,

L(φ, κ), is defined as using L to translate φ to NL ψ s.t.

Dependent(y, Coffee).

Drinks(x, Coffee)

x. Human(x) =

y. x = y

⇒
I

∧ ¬

∧ ∃

φ.

A

I

−1
L (ψ, κ′)
I

≡

Example It is easily seen that informalization is the inverse of autoformalization. Therefore, the
Dependent(y, Coffee) can be
FOL formula
informalized to the sentence “Every human drinks coffee but some are not dependent on it”.

Drinks(x, Coffee)

x. Human(x) =

y. x = y

∧ ¬

∧ ∃

⇒

∀

2

I

054
055

056
057
058
059
060
061

062
063
064
065
066
067

068
069
070
071
072

073
074
075
076
077
078

079
080
081
082
083
084

085
086
087
088
089
090

091
092
093
094
095

096
097
098
099
100
101

102
103
104
105
106
107

Under review as a conference paper at ICLR 2025

−1
L (ψ, κ′)

−1(φ, κ)

≡

A

ψ and

y. Human(y) =

φ. It is possible that a different
Note that we only require
I
LLM (or the same with a different seed) would autoformalize the same example to a syntacti-
cally different but semantically equivalent formula –

∧
Dependent(y, Coffee). Similarly, an LLM can informalize differently. The
¬∀
example above could be informalized by the same LLM to “All humans drink coffee but some are
L(ψ, κ′) and vice versa. We assume
not dependent on it”. Thus, it is not necessary that
A
that the context κ, κ′ provided contains the prompt and any necessary vocabulary that is needed for
the task (e.g., Human(x) represents that x is a human, etc.). Henceforth, unless specified, we skip
κ, κ′ and L in the notation for

Drinks(x, Coffee)

x. Human(x) =

L(φ, κ) =

and

⇒

⇒

≡

∀

I

.

A

I

Given an LLM L, we define truth maintenance as L’s ability to be able to understand its own
N+, we use (
translations. Given n
φn
that is obtained using L when starting with FS φ0, where ψi =

)n(φ0), to refer to a sequence φ0

→
(φi) and φi+1 =

→
(ψi).

A ◦ I

. . .

ψ0

→

∈

I

A

A ◦ I

A ◦ I

Definition 2.3 (LLM Truth Maintenance w.r.t. (
(

)n(φ0) obtained using L, we define truth maintenance as φi

)n(φ0)). Given an LLM L and a sequence
φj for any i, j
.

}
)n(φ0)
The Need for Truth Maintenance The ability of an LLM to maintain truth across (
for FS such as first-order logic, etc., is foundational and underlies many aspects of the capabilities
of LLMs surrounding reasoning, semantically accurate translation, etc. In fact, for programming,
it has been shown that autoformalization can help with the reasoning abilities of LLMs since they
frame reasoning as generation of FS (Chen et al., 2021). Others (Wu et al., 2022) have made similar
observations and have highlighted the need for benchmarks and metrics for assessing the truth
maintenance capabilities of LLMs. In this paper, we further show through our empirical evaluation
that truth maintenance on these types of FS is indicative of performance on related tasks.

0, . . . , n

A ◦ I

∈ {

≡

x. Human(x) =

Naturally, LLMs may not autoformalize, reason, etc., correctly due to issues such as hallucination
(Ji et al., 2023), etc. For the example earlier, the LLM could autoformalize by omitting the x = y
Dependent(y, Coffee). This seems
Drinks(x, Coffee)
statement to yield
innocuous but changes the meaning since y is no longer required to be a human, and thus it interprets
as “All humans drink coffee, and, there are some elements of the universe that are not dependent on
coffee.” Such issues have profound implications in synthesizing specifications and/or programs. Thus,
an LLM must be able to understand its own generated output across NL and FS, and it is imperative
)n(φ0).
to create a benchmark that can faithfully assess the truth maintenance of LLMs w.r.t. (

∧ ∃

⇒

y.

¬

∀

A ◦ I

3 OUR APPROACH FOR ASSESSING TRUTH MAINTENANCE

uto

A ◦ I

)n(φ0).

L, for autonomously assessing an LLM’s ability to maintain
We now describe our approach,
∃∨∧
truth w.r.t. (
L provides dynamically generated datasets that can be scaled
arbitrarily by systematically generating out-of-distribution, well-balanced ground-truth data (§D1
)n(φ0)
– Sec. 1), provides §D2 by using intrinsic LLM capabilities to automatically assess (
without requiring any labeled annotations and using formal verifiers to rigorously check and guarantee
the correctness of (

)n(φ0) without having to engage in an exhaustive search process.

∀
uto
∃∨∧

A ◦ I

∀

A ◦ I

Dynamic Dataset Generation We use context-free grammars (CFGs) (Hopcroft et al., 2001) – a set
of production rules over terminal and non-terminal symbols – for dynamically generating datasets.

AB
aA
|
b

ε

S

A

a A

B

b

ε

S
A
B

→
→
→

G

(a) CFG

for the language a∗b

(b) Parse tree when using

to obtain the string ab (d = 2).

G

with 3 production rules and the infix parse tree that is obtained by repeatedly
An example CFG
applying the rules to yield the string ab is illustrated above. The depth of this tree is often used to
measure the descriptional complexity d of a given string generated using the CFG. (Csuhaj-Varjú &
Kelemenová, 1993). CFGs can be used to dynamically generate arbitrarily large amounts of data.

G

3

108
109

110
111
112
113
114
115

116
117
118
119
120
121

122
123
124
125
126

127
128
129
130
131
132

133
134
135
136
137
138

139
140
141
142
143
144

145
146
147
148
149

150
151
152
153
154
155

156
157
158
159
160
161

Under review as a conference paper at ICLR 2025

Figure 1: The ∀uto∃∨∧L pipeline for autonomous evaluation of LLM truth maintenance w.r.t. (A ◦ I)n(φ0).

Another advantage is that CFGs can be customized with minimal human effort to generate diverse
datasets whose ground-truth data possesses specific properties. For example, a dynamic dataset
that only consists of k–SAT sentences – propositional logic in the Canonical Normal Form (P 0
1 ∨
. . .
px,
– can be easily generated. We enrich the
generated sentence with context via a customizable Vocabulary Generation step, which automatically
provides the necessary vocabulary for performing the task (e.g., providing English meanings to allow
for human-like NL) by using terms from a vocabulary database or by using an LLM.

. . . where P j

i ∈ {

P 1
k )

P 0
k )

1 ∨

(P 1

. . .

px

∧

¬

∨

∧

∨

}

Automatic Truth Maintenance w.r.t. (
assess truth maintenance without any human annotations by evaluating φi
approach is based on the following intuition. Let
maps FS φ to NL ψ. Similarly, let
FS φ. In general, there are many possible correct informalizations (autoformalizations) of φ
(ψ

)n(φ0) We develop a novel technique that can soundly
φi+1. Our
→
ψ be a non-deterministic function that
φ be a non-deterministic function that maps NL ψ to
FS
−1 are not well-defined.

are not injective (1:1) functions and thus

NL). Thus,

−1 and

A ◦ I

and

: φ

: ψ

ψi

→

→

→

A

∈

I

∈

I

A

I

A

I

A

A

and

and

Our key observation is that if
evaluate its truth maintenance by composing
LLM. Now, if L preserves truth, then ψ =
φ′ =
is quite challenging to check whether
I
intervention. However, if L preserves truth, φ′ =
even if they are not syntactically identical. Thus, we only need to check if φ
φ0 = p1
p1, ψ0 =
p1 using Idempotence.”, and φ′
A ◦ I
check if ψ0 is an accurate representation of φ0, but easy to check if φ0

come from the same system (e.g., an LLM), then we can
. Let φ be any FS expression and let L be an
I
A
(φ) will be an accurate NL representation of φ and
I
(ψ) will be a semantically equivalent FS representation of ψ. Since ψ is an NL description, it
(φ) is indeed an accurate representation of φ without human
(φ)) will be semantically equivalent to φ
φ′. For example, let
(φ1) = “A conjunction of propositions p1 and p1 that can be simplified to
)1(φ0). It is very difficult to
φ1 using a formal verifier.
L uses formal syntax φ as input and produces formal syntax φ′
Formal Verification Since
∀
φ′. As a result,
as output, we can use formal verifiers to check whether φ
L avoids brittle
syntactic equivalence checks and exhaustive tests of semantic equivalence that require evaluations of
all possible truth valuations of formulas or executions of regexes.

(ψ0) = p1 for a sequence (

(
I
A

1 =

∃∨∧

∃∨∧

uto

uto

A

≡

≡

≡

∧

∀

I

uto

∃∨∧

L Overall Pipeline We use the above insights to automatically assess LLM truth main-
∀
tenance by using the same LLM L to represent
respectively. Fig. 1 shows our overall
and
I
to automatically generate a ground-truth FS expression
assessment process. Briefly, we use a CFG
φ0. Next, we use a vocabulary generation process to generate a context for φ0. This can either
use abstract terms or use NL elements for more human-like scenarios (§D1). We then evaluate
(φ0, κ) using context κ designed for
(
A ◦ I
(φ0)), and we use
informalization. The context of L is cleared (note that we only use the output of

)1(φ0) by using an LLM L to first generate ψ0 =

A

G

I

I

4

162
163

164
165
166
167
168
169

170
171
172
173
174
175

176
177
178
179
180

181
182
183
184
185
186

187
188
189
190
191
192

193
194
195
196
197
198

199
200
201
202
203

204
205
206
207
208
209

210
211
212
213
214
215

FS LLM  VerificationGround-truth Data and Context GenerationQuery  ?Formal SyntaxGeneratorInput Grammar: FS Autoformalization: Clear 's Context A conjunction of  thepropositions p1, p2, p1;also expressed p1 andp2 by idempotence TrueExample 1 (Vocabulary is abstract)AutomaticVocabularyGenerationFS VocabVocabularyDatabase : It is raining: It was sunny yesterdayThe sun was bright theday before whilst it israining heavily today TrueExample 2 (Vocabulary is real-world)  [a-z]+@[a-z]+.comAn regular expressionfor email with a set ofcharacters separatedby @, ending in .com \W+@\W+.comFalseExample 3 (Vocabulary is real-world)(numbers are not allowed in )  ?LLM Clear 's ContextClear 's ContextClear 's ContextProver9Prover9Prover9NL VocabInformalization: LLM LLM   ?  ?Under review as a conference paper at ICLR 2025

S
S
P

S
P

S
→
(P
→
v
→ ¬

∧
∨
v
|
(a) 3–SAT

∨

(S
S)
|

∨

S)

P )

S
S
S

(S
(

∧
→
S)
¬
→
v
v
|
→ ¬

(b) Propositional Logic

S
F
F

f. S)
F )

∀
∧
F )

F
(
|
(F
(
¬

(
f. S)
|
(F
F )
|
p
p
|

→
→
|¬
→
(c) First-order Logic

∃
∨

ΣK
|

S
S
K

(S)K
→
SΣK
→
ε
→ ∗|

(d) Regular Expression

Figure 2: CFGs (described in Sec. 4) used for synthesizing the datasets in ∀uto∃∨∧L.

L to generate φ1 =
A
(e.g., Z3 (de Moura & Bjørner, 2008), Prover9 (McCune, 2010)) to assess if φ0
elements of FS. If φ0

(ψ0, κ′) using context κ′ designed for autoformalization. We then use a verifier
φ1 since both are

φ1 then we can repeat the process by evaluating (

≡
)1(φ1) similarly.

A ◦ I

∀

∧

Example: Consider example 2 in Fig. 1.
uto
L uses the grammar in Fig. 2b to automatically
∃∨∧
generate a ground truth FS sentence as φ0 = p1
p1. We can use any vocabulary to generate
p2
∧
meaning for the propositions; p1 : It is raining today, p2 : It was sunny yesterday. Next, the LLM
L is prompted with Prompt 1 to perform informalization yielding NL ψ0 =
(φ0). L can perform
any simplification or other paraphrasing necessary. For example, L could informalize φ0 above to
ψ0 =“The weather status was sunny yesterday whilst it is raining today.” Notice that the LLM-
generated NL statement automatically reflects a simplification using the Commutative (a
a)
and Idempotent (a
a) properties. Next, L is asked to autoformalize ψ0 without any context
≡
other than the vocabulary to use and a prompt for autoformalization (Appendix F). In this case, the
p2. We use a theorem prover such as Prover9 (McCune,
LLM could return φ1 =
)1(φ0).
2010) to show that φ0

A
φ1 and thus assess L’s truth maintenance capabilities w.r.t. (

(ψ0) = p1

A

≡

∧

∧

∧

∧

a

b

b

≡

≡

A ◦ I

4 DATASETS AND ASSESSMENT FRAMEWORK

uto

L is open-source1, is written in Python 3, includes several pre-computed datasets, and is
∀
easily customizable for adding new datasets, prompts, LLMs, etc. We now describe the datasets and
metrics that any newly developed LLM can be evaluated on by using

L out-of-the-box.

∃∨∧

uto

∀

∃∨∧

Pre-generated Datasets and Dynamic Dataset Generator We provide 5 datasets using the grammars
in Fig. 2. All datasets are arranged based on the descriptional complexity d (# of operators for logic,
parse tree depth for regex) with around 500 samples per complexity for a total of 20k samples per
dataset. Other dimensions for categorization are available as metadata.

(Fig. 2a) k–SAT(n) Dataset (
propositions p1, . . . , pn. This dataset is used for prompt calibration due to its toy structure.

10k) The terminal v is replaced with a vocabulary of n

| ∼

|D

∗

(Fig. 2b) Propositional Logic: PL(n) Dataset (
replaces terminals by randomly selecting from a list n propositions.

| ∼

|D

∗

19k) Similar to k–SAT, this dataset also

∈ {

x1, x2, . . .
}

19k each)
(Fig. 2c) First-order Logic: FOL(np, no) Synthetic (S), English (E) Datasets (
The terminals p are replaced with predicates of the form p(v1, . . . , vn) where pi is a predicate name
selected from a list of np predicates, vi is either an object o from a list of no objects or is a free
variable f
that is appropriately annotated within the scoping rules. The objects and
predicate names are auto-generated synthetically for the synthetic version of the dataset. The English
version of the dataset uses VerbNet (Schuler, 2005) for predicate names and Faker (Faraglia, 2024)
for object names. The English dataset allows for informalization to produce more abstract sentences
that closely resemble the NL statements in SOTA autoformalization datasets. For example, an FS
statement Boom(Richard)
Exercise(Yolonda) yields a more natural NL statement such as “The
expression states that Richard does not experience a boom, and Yolonda does not engage in exercise”.

| ∼

|D

∧

∗

where n is a user-specified constant.

(Fig. 2d) Regular Expression: RE(n) Dataset (
1
}
Dataset Diversity Our overall dataset’s total number of unique samples
85k. We also
|
provide zero-shot and 2-shot prompts for each dataset, making the total dataset size 170k for off-
the-shelf evaluation and continual assessment of any new LLMs. Similarly,
85% of the samples in
all datasets are composed of unique CFG parse trees (trees obtained by sampling the CFG but not

18k) The vocabulary Σ is the set

0, . . . , n

| ∼

|D

|D

−

∼

∼

is

{

∗

∗

1Source code (and appendix) is included in the supplement. We will make it public post acceptance.

5

216
217

218
219
220
221
222
223

224
225
226
227
228
229

230
231
232
233
234

235
236
237
238
239
240

241
242
243
244
245
246

247
248
249
250
251
252

253
254
255
256
257

258
259
260
261
262
263

264
265
266
267
268
269

Under review as a conference paper at ICLR 2025

Prompt 1: Informalization (

I

) for Logic (others available in Appendix F)

⟨

Your task is to convert a
formula, appearing after
Propositional Logic, First-order Logic
⟩
[FORMULA], to a natural description that represents the formula. Only natural language
terms are allowed to be used and do not copy the formula in your description. Your
description should allow one to reconstruct the formula without having access to it, so make
sure to use the correct names in your description. Explicitly describe the predicates. You may
use terms verbatim as specified in the vocabulary below.

[VOCABULARY]

Operators: List of operators followed by their NL interpretations

Objects: The objects in the universe (if any)

Propositions: The propositions in the universe and their NL interpretations (if any)
Predicates: The predicates in the universe and their NL interpretations (if any)
Examples:

Few-shot examples of the task (if any)

Example Prompt
Your task . . .

Operators:
Propositions:
Formula:

represents conjunction,

represents disjunction, . . .

∧
p1 : It is raining, p2 : It was sunny yesterday
p1

p2

p1

∨

∧

∧

Example Response: The sun was bright the day before whilst it is
raining today.

injecting the vocabularies). Expressions with the same parse tree but different vocabularies such as
p1
10% of our dataset. Such samples provide a robust
check against positional bias in the LLM. Additional information is presented in App. M.

p1)), etc., compose

p1, ((p2)

p2, p2

∼

∧

∧

∧

uto

∃∨∧

Efficient Dynamic Dataset Generation As LLMs evolve, users can easily generate datasets in
L by simply providing CFGs and/or vocabularies. We provide a dataset generator (described
∀
in App. B) that uses a user-provided CFG and vocabulary to dynamically generate user-controlled,
diverse datasets up to a user-specified metric such as number of operators, parse tree depth, etc. Our
generator is guaranteed to be able to generate any string that is representible using the CFG (App. B).

Robust Parser We use open-source libraries to robustly parse the LLM-generated output. We use
the Natural Language Toolkit (NLTK) library (Bird et al., 2009) for parsing logic and use Reg2Dfa
(Reg, 2017) for regexes. LLM output that cannot be parsed is said to be syntactically non-compliant.
Additionally, we also use scripts to ensure that the informalization step does not copy elements of FS
into NL (e.g., complete or any parts of FS) that would otherwise make autoformalization trivial.

Prompt Calibration As stated in Sec. 2, prompts are crucial for LLM performance. To ensure that
our results can be viewed in terms of LLM capabilities themselves and not a characteristic of using
“bad” prompts, we conducted extensive prompt engineering and ensured that at least one LLM
95% accuracy on a constrained (but representative) grammar, e.g.,
could perform
3-SAT(12) (Fig. 7). For §A4, rather than asking for only a yes or no answer, we use Chain-of-Thought
(CoT) so that LLMs can utilize their generated outputs to improve their reasoning (Wei et al., 2022).

L with

∃∨∧

uto

≥

∀

Evaluation Metrics

uto

L automatically assesses LLMs and provides reports that help answer:

∀

uto

uto

∃∨∧

∃∨∧

L indicative of performance on other benchmarks We compute the

∀
A1. Is performance on
correlation and predictive power of
∃∨∧
A2. Are LLMs syntactically compliant?
L evaluates the ability of LLMs to generate
∃∨∧
∀
syntactically correct output by computing the ratio of generated FS that could be successfully parsed.
)n(φ0)? We compute a quantitative measure of
A3. Are LLMs able to maintain truth w.r.t. (
)n(φ0) by computing the accuracy of an LLM to yield FS φ1 s.t.
LLM truth maintenance w.r.t. (
A ◦ I
φ0
A4. Can LLMs be used as verifiers?
the answer to φ0

∀
∃∨∧
φ1 instead of using a formal verifier during (

L pipeline (we used n = 1 for our evaluation to keep costs low).

L evaluates whether an LLM L can be used to provide

L w.r.t. other benchmarks.
uto

φ1 using the

)1(φ0).

A ◦ I

∃∨∧

uto

uto

≡

∀

∀

≡

A ◦ I

6

270
271

272
273
274
275
276
277

278
279
280
281
282
283

284
285
286
287
288

289
290
291
292
293
294

295
296
297
298
299
300

301
302
303
304
305
306

307
308
309
310
311

312
313
314
315
316
317

318
319
320
321
322
323

Under review as a conference paper at ICLR 2025

Figure 3: Correlation between scores on ∀uto∃∨∧L and static benchmarks from the literature. The Pearson
correlation coefficient (ρ) and the p-value (values ≤ 0.05 are statistically significant) are annotated in the top
left. ∀uto∃∨∧L scores use a comparable descriptional complexity d (App. K.4). R represents a reasoning task.
Grey hexagons ((cid:146)) represent data from 10 other models (tabular data is included in Appendix).

5 ASSESSMENT OF SOTA LLMS ON THE

UTO

∀

∃∨∧

L BENCHMARK

L to
To motivate research in the area and showcase our framework’s strengths, we used
evaluate 17 SOTA closed and open-source LLMs of various parameter sizes. For clarity, we plot
select models, grey out the data from the others, and refer the reader to App. N for a comprehensive
overview. We analyze §A1 using Fig.3 and Fig. 4. We analyze §A2, A3, and A4 using results obtained
by using

L on our generated datasets (Fig. 5). We present our analyses below.

∃∨∧

uto

uto

∀

∀

∃∨∧

∀

uto

∃∨∧

§A1: Is performance on
L indicative of performance on other benchmarks Our hypothesis is
that the ability for truth maintenance on foundational concepts (propositional logic, first-order logic,
regexes, etc.) will be indicative of an LLM’s reasoning abilities. To evaluate this, we compare the
L vs. performance in other benchmarks focused on FS-tasks such
performance of LLMs on
as reasoning, autoformalization, etc. Our results (Fig. 3) indicate that there is a positive correlation
between LLM performance on
L and other logic-based benchmarks on a myriad of tasks
∀
such as autoformalization, logical reasoning, code generation, etc.

∃∨∧

∃∨∧

uto

uto

∀

We use 5 popular benchmarks: (a) FOLIO(R;{NL,FOL}) (Han et al., 2022), a popular logical
reasoning benchmark with ground truth in both NL and FS; (b) FOLIO(
) evaluates if an LLM
can (auto/in)formalize NL (FS) accurately; (c) LogiEval(R;{PL,FOL}) (Patel et al., 2024) a reasoning
benchmark with ground truth in propositional and first-order logic; (d) HumanEval(
) (Chen et al.,
2021), a code autoformalization benchmark; (e) Big Bench Hard (BBH) (Suzgun et al., 2023). These
benchmarks are contrasted in Sec. 6, and example prompts of these benchmarks are included in
Appendix K. We ran 5 runs across all these benchmarks except BBH (due to resource limitations)
using the most comparable
L dataset. For BBH, we use the reported numbers in the literature
as scores for the models (sources are included in Appendix K).

/
{A

∃∨∧

uto

I}

A

∀

∀

∀

∀

≥

uto

uto

∃∨∧

L exhibits a strong, positive correlation ρ

0.7 with other
Our results (Fig. 3) show that
static benchmarks on FS-based tasks and even on reasoning tasks such as FOLIO. However,
L
uto
evaluates truth maintenance capabilities of LLMs by automatically generating its own data and without
L can be observed in LogiEval for
requiring any hand-annotation. Similar results using
ρ < 0.7) for the FOL
propositional logic. Our results only showcase a moderate correlation (0.5
version of LogiEval. We investigated and found LogiEval is an imbalanced dataset where 80% of
samples are from the positive class. Furthermore, this imbalance is also present in the problem
difficulty with a heavy skew towards easy problems. This lead to lower overall performance (and
consequently predictive power) of models like GPT-4o-mini that actually try to reason and provide
L also
no answers compared to models like LLama-3.1-8b that only answer yes. Similarly,
∃∨∧
) and HumanEval.
serves as a predictor for autoformalization, as evident in our results on FOLIO (
P|Y ). Given two benchmarks X and Y , where LLMs L1, L2 score
P|Y (X), is the
y2).
y1
y2. Formally, the predictive power
|
≥

Definition 5.1 (Predictive Power:
x1, x2 on X and score y1, y2 on Y respectively, the predictive power of Y w.r.t X,
P|Y (X) = P (x1
probability that x1

x2 if y1

∃∨∧

∃∨∧

uto

x2

A

≥

≤

≥

∀

Predictive Power
L can be used as a performance predictor for other metrics. We evaluated
∀
this capability using the predictive power as defined above. The probabilities were obtained using
Maximum Likelihood Estimation over

for a benchmark X.

L, X

∃∨∧

and

uto

uto

X,

⟨∀

∃∨∧

⟩

⟨

∀

∃∨∧

L
⟩

≥
uto

7

324
325

326
327
328
329
330
331

332
333
334
335
336
337

338
339
340
341
342

343
344
345
346
347
348

349
350
351
352
353
354

355
356
357
358
359
360

361
362
363
364
365

366
367
368
369
370
371

372
373
374
375
376
377

0.25.5.7510.25.5.751BenchmarkScoreρ=0.81p=0.00FOLDataset,d≤6FOLIO(R;NL)0.25.5.751ρ=0.83p=0.00FOLDataset,d≤6FOLIO(R;FOL)0.25.5.751ρ=0.79p=0.00FOLDataset,d≤30LogiEval(R;PL)0.25.5.751ρ=0.64p=0.01FOLDataset,d≤30LogiEval(R;FOL)0.25.5.751ρ=0.82p=0.00FOLDataset,d≤6FOLIO(A)0.25.5.751ρ=0.75p=0.00REDataset,d≤7HumanEval(A)∀uto∃∨∧LScoreChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3TrendLineOtherModels(n=10)Under review as a conference paper at ICLR 2025

Figure 5: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using ∀uto∃∨∧L to assess
LLMs w.r.t. §A2, §A3, §A4 on the packaged datasets (Sec. 4). The x-axis represents an increasing descriptional
complexity. Our prompt calibration, few-shot, other model results, etc. are included in the appendix.

∀

uto

∃∨∧

Our results (Fig. 4) show that an LLM’s perfor-
L is a strong predictor of its
mance on
performance on FS-based benchmarks. Our met-
ric is also more robust at measuring truth mainte-
nance than length-dependent, NL-based metrics
)
like BLEU scores. For example, in a FOLIO(
I
informalization task, changing the generated NL
ψ =“the weather status was sunny yesterday
and is raining today” to ψ′ =“the weather sta-
tus was sunny yesterday and is not raining today”
still achieves a high BLEU(ψ′, ψ) score of 0.74
(BLEU(ψ, ψ) = 1) but does not maintain truth.
Even for such metrics,

P|∀uto∃∨∧L > 0.5.
These results show that performance on
∀

Figure 4: Predictive power of ∀uto∃∨∧L w.r.t other
benchmarks. Benchmark metrics appear after the colon.

uto

∃∨∧

L is indicative of performance on other benchmarks.
)1(φ0)
§A2: Are LLMs syntactically compliant? As seen in Fig. 5, SOTA LLMs can perform (
well when the formal syntax has low descriptional complexity (e.g., few operators in logic). But, as the
descriptional complexity increases, the ability of LLMs to autoformalize their own informalizations
decreases. One surprising result here is that for regexes, GPT-4o performs much worse than Phi and
LLama-3, which are much smaller models. We observed that GPT-4o tends to expand the Kleene
Star recursively, leading to invalid regexes. For logic, we observed that LLMs do not make mistakes
in the operators or symbols used but often misplace parentheses, creating malformed expressions.

A ◦ I

)n(φ0)? Our results show that, except for the
§A3: Are LLMs able to maintain truth w.r.t. (
A ◦ I
)1(φ0) well as the descriptional complexity
prompt calibration task, LLMs cannot perform even (
increases. One common failure is the lack of understanding of precedence and associativity rules for
the formal syntax. The evaluated LLMs often cannot place the correct operators in the correct scope,
leading to quick verification failures. We provide an analysis of failing cases in Appendix G.

A◦I

Bounding the false positive rate of
against different informalizations of the same FS. Thus, when
truth (
of φ0. We now bound the probability of false positives that may occur due to hallucinations.

L is that it is robust
∀
∃∨∧
L outputs that LLM maintains
(ψ0) is a semantically equivalent translation

)n(φ0) on FS φ0, the intermediate NL =

L One key advantage of

A ◦ I

∃∨∧

∃∨∧

uto

uto

uto

∀

∀

I

IL(φ0)
−−−−→

AL(ψ0)
−−−−−→

Given an LLM L, let φ0
)1(φ0) s.t. φ0
(
A ◦ I
uto
the chance of
∀
informalizes an FS expression
let pA be the probability of autoformalizing ψ0,

φ1 be an execution of the
L pipeline for
φ1 but ψ0 is not an accurate representation of φ0. We statistically analyze
L providing such false positives. Let pI be the probability with which L
(φ0) = ψ0 s.t. ψ0 is an accurate representation of φ0. Similarly,
(ψ0) = φ1, s.t. φ1 is semantically equivalent to

≡
∃∨∧

∃∨∧

uto

ψ0

∀

I

A

8

378
379

380
381
382
383
384
385

386
387
388
389
390
391

392
393
394
395
396

397
398
399
400
401
402

403
404
405
406
407
408

409
410
411
412
413
414

415
416
417
418
419

420
421
422
423
424
425

426
427
428
429
430
431

0.25.5.751§A2:SyntacticCompliancePropositionalLogic(12)0.25.5.751§A3:Accuracy0102030400.25.5.751§A4:F1ScoreFOL(8,12)−S010203040FOL(8,12)−E010203040RegularExpression(2)010203040#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepthChatGPTGPT-4oGPT-4o-miniPhi3MistralLLama3OtherLLMs(n=10)BenchmarkX(Annotatedbars)0.25.5.751P|∀uto∃∨∧L(X)0.890.850.810.730.860.740.750.770.680.780.86FOLIO(NL):AccuracyFOLIO(FOL):AccuracyLogiEval(PL):AccuracyLogiEval(FOL):AccuracyFOLIO(A):AccuracyFOLIO(I):BLEUFOLIO(I):ROUGEFOLIO(I):METEORFOLIO(I):BERTHumanEval(A):AccuracyBBH(R):AccuracyUnder review as a conference paper at ICLR 2025

432
433

434
435
436
437
438
439

440
441
442
443
444
445

446
447
448
449
450

451
452
453
454
455
456

457
458
459
460
461
462

463
464
465
466
467
468

469
470
471
472
473

474
475
476
477
478
479

480
481
482
483
484
485

ψ0, i.e. φ0
φ1

≡

≡

φ1. Let pH be the probability that L hallucinates FS φ1 by autoformalizing ψ0 s.t.

φ0 even though ψ0 is not an accurate representation of φ0.

∀

uto

ψ0 yields an
L, the sequence φ0
It can be seen that for a false positive to be output by
incorrect NL description, the sequence ψ0
φ1 autoformalizes incorrectly and hallucinates in the
right way to produce φ1
φ0. The probability of such a sequence corresponds to L making two
mistakes, with the second mistake being such that it generated an expression equivalent to φ0. This
)n(φ0), this probability is (1
pA)npn
can be expressed as (1
H
A◦I
φi (Sec. 3). As LLM technology improves, we
since
≡
∀
∃∨∧
expect pI, pA
L
decreases as n increases. This low likelihood of false positives is further confirmed empirically by
our analysis of correlation and predictive power w.r.t. other benchmarks presented above.

−
A ◦ I
0. As a result, the probability of false positives provided by
→

−
L computes (
1 and pH

)1(φi) if φi−1

≡
pI)(1

pA)pH . For (

pI)n(1

∃∨∧

∃∨∧

uto

uto

→

→

→

−

−

∀

§A4: Can LLMs serve as verifiers? We use φ1 generated by GPT-4o (the best performing LLM) and
φ1 to check if its output matches that of a formal verifier.
asked an LLM L to evaluate whether φ0
It is clear from Fig. 5 that even in this setting (and despite using Chain-of-Thought), LLMs cannot
serve as verifiers for anything but toy expressions (low descriptional complexity), after which F1
scores fall sharply. Our results show that using LLM-as-a-judge is not ideal in applications where
truth maintenance is important. We found that LLMs generally struggle to provide correct answers
once formulae are larger in general. For smaller expressions, we found that LLMs have difficulties
with negations in logic. Due to space limitations, we present some examples and an analysis of the
kinds of syntactic structures that LLMs fail to verify correctly in the Appendix (App. L, Fig. 20).

≡

5.1 EVALUATING LARGE REASONING MODELS (LRMS) USING

UTO

∀

∃∨∧

L

LRMs are LLMs that also perform some reason-
ing steps (e.g., search) as a part of their genera-
tion process. We evaluated OpenAI’s o1, which
is the latest LRM available. Due to o1 being 6x
more expensive, we regenerated a small dataset
= 200) and av-
with 5 points per category (
eraged the results across 3 runs with zero-shot
prompts. Our results are shown in Fig. 6 and
it can be seen that even SOTA LRMs cannot
maintain truth effectively in (

)1(φ0).

|D|

A ◦ I

6 RELATED WORK

Figure 6: ∀uto∃∨∧L results on OpenAI o1 on a small
dataset |D| = 200. Dashed lines indicate accuracy.

Logical Reasoning RuleTaker (Clark et al., 2020) and ProntoQA (Saparov & He, 2023) generate
datasets by using simple “if-then" and syllogisms rules to create reasoning questions. Similar
grammars are used by LogicNLI (Tian et al., 2021) and CLUTRR (Sinha et al., 2019). LogiEval
(Patel et al., 2024) uses fixed inference rules and LLMs to generate reasoning problems. While
these techniques are dynamic, they are limited in their ability to produce interesting reasoning
problems across different domains.
L is multi-dimensional providing 5 different datasets,
allows multiple customization options, and can generate an infinite number of unique syntax trees.

∃∨∧

uto

∀

FOLIO (Han et al., 2022) utilizes human experts to generate a set of reasoning questions based on
real-world text sources. They generate questions in both NL and FS for propositional and first-order
logic that require 7 levels of reasoning. A similar approach is employed by ReClor (Yu et al., 2020)
and (Srivastava et al., 2023). A key weakness of these approaches is their reliance on human experts..

Autoformalization HumanEval is a popular benchmark for evaluating LLM capabilities of autofor-
malizing source code. LLM autoformalizations are evaluated via hand-written test cases. It has been
shown by Liu et al. (2023a) through the HumanEval+ dataset that the test cases in HumanEval are
incomplete and can provide misleading rankings. StructuredRegex (Ye et al., 2020) used crowdsourc-
ing for generating regex datasets. In contrast,
L requires no human annotations and utilizes
uto
∀
formal verifiers for checking the truth maintenance and thus does not share such drawbacks.

∃∨∧

,
FOLIO(
{A
coded annotations of

) (Han et al., 2022) tests the (auto/in)formalization abilities of LLMs by using hand-
pairs. However, as noted by the authors, they cannot check truth

I}

NL, FS
⟨

⟩

9

0102030400.25.5.751§A1:SyntacticCompliancePL(12)010203040FOL(8,12)−E0.25.5.751§A2:Accuracy#ofOperators:∧,∨,¬Under review as a conference paper at ICLR 2025

maintenance effectively and rely on an inference engine to compute truth values for each conclusion.

uto

∃∨∧

L uses theorem provers to check equivalence and thus is sound in its accuracy evaluation.

∀
MALLS (Yang et al., 2023) is an autoformalization dataset for first-order logic that was generated
using GPT-4. Their use of LLMs for generating the data limits the diversity of the dataset since
and the authors suggest to only use this dataset for fine-tuning and not for evaluation. In contrast,
L generates correct FS and has a sound evaluation metric for truth maintenance.

∀
Autoformalization approaches such LeanEuclid (Murphy et al., 2024), DTV (Zhou et al., 2024),
LINC (Olausson et al., 2023), SatLM (Ye et al., 2020), Logic-LM (Pan et al., 2023) and others
(Wu et al., 2022) utilize formal verifiers to provide sound evaluation metrics but utilize hand-coded
datasets that limit their use in evaluating newer LLMs unlike

∃∨∧

uto

uto

L.

∀

∃∨∧

Informalization Wu et al. (2022) and ProofNet (Azerbayev et al., 2023) use static datasets to evaluate
LLM informalization capabilities. They use metrics such as BLEU scores that are known to not
be indicative of accuracy for FS-based tasks (Ren et al., 2020). Jiang et al. (2023) develop MMA,
a dataset of formal and informal pairs generated using GPT-4. They note that their dataset is an
approximate measure due to using LLMs without manual validation. In contrast,
L is
∀
autonomous and provides sound measures of LLM capabilities w.r.t. truth maintenance.

∃∨∧

uto

7 CLOSING REMARKS

uto

uto

∃∨∧

∃∨∧

∀
L autonomously evaluates (

Conclusions This paper introduced
L, a new benchmark for autonomous assessment of LLM
truth maintenance. Our approach to dataset synthesis allows us to scale without any human labeling.
)n(φ0) and provides accurate results by using verifiers
∀
to guarantee correctness over all inputs. Our framework is easily extensible and provides several
prepackaged datasets (and o.o.d. dataset generators) to quickly assess new LLMs. Furthermore, our
evaluation indicates that SOTA LLMs and LRMs are not performant in this task. Finally, we show
that our metric can be used as an indicator of performance on other FS-based tasks and thus can be
used as a surrogate benchmark for evaluating new LLMs as and when they are developed.

A ◦ I

Broader Impact We introduce a new way to automatically assess whether LLMs can understand
L can
their own generations and preserve their truth while automatically scaling datasets.
be used to robustly evaluate the suitability and safety of using LLMs in FS-based tasks such as
autoformalization, code generation, etc. and can be used as a surrogate to estimate performance
when new LLMs are developed. Our work can pave the way for the development of new autonomous
techniques for evaluating LLMs in other, more free-structured syntax like conversational AI.

∃∨∧

uto

∀

Limitations and Future Work One interesting extension of current work is to utilize the λ-calculus
to further expand the datasets that can be generated. Our framework assumes that the generated NL
uses the English vocabulary. Adding support for other languages is an interesting extension for future
work. Another limitation pertains to the use of formal verifiers. It is well-known that first-order
logic is undecidable (Huth & Ryan, 2004). We mitigate this by using FS verifiers loaded with the
appropriate timeout and logging mechanisms (0.66% of our results experienced a timeout). This can
be mitigated by using CFGs that generate decidable strings. One interesting application of
L
is to use the generated evaluations as datasets for back-translation to improve the autoformalization
capabilities of models (Jiang et al., 2023). Finally, using formal verifiers as tools which the LLM can
call is an interesting extension of our benchmark that would further facilitate the assessment of §A4.

∃∨∧

uto

∀

Threats to Validity Our reported results for paid APIs are dependent on the model checkpoints used
to be available. Similar to existing LLM evaluation methodologies, one must use pass@k and other
detailed measures such as std. deviations to increase confidence. We report pass@1 due to the high
2 prompts but do report std. deviations across
85k
cost of pass@k for our complete dataset
10 runs (on a single batch of 2k samples) in App. H. As is the case with all approaches, our approach
assumes the soundness of the verifier programs and parsing libraries used. Software bugs in the
L. Our use of
verifier program or parsing libraries could cause false signals to be output by
open-source popular libraries such as Prover9, NLTK reduces our exposure to such risk.

∃∨∧

| ∼

uto

|D

×

∀

∗

Ethical Considerations Our work involves using LLMs for generating text. Naturally, it is imperative
to ensure that appropriate guardrails are in place to prevent offensive content from being generated
and/or displayed. We do not use any personally identifiable information in

uto

L.

∀

∃∨∧

10

486
487

488
489
490
491
492
493

494
495
496
497
498
499

500
501
502
503
504

505
506
507
508
509
510

511
512
513
514
515
516

517
518
519
520
521
522

523
524
525
526
527

528
529
530
531
532
533

534
535
536
537
538
539

Under review as a conference paper at ICLR 2025

540
541

542
543
544
545
546
547

548
549
550
551
552
553

554
555
556
557
558

559
560
561
562
563
564

565
566
567
568
569
570

571
572
573
574
575
576

577
578
579
580
581

582
583
584
585
586
587

588
589
590
591
592
593

REFERENCES

Reg2dfa. https://github.com/Jack-Q/reg2dfa, 2017. Accessed: 2024-06-01.

Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and
Jeremy Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics.
CoRR, abs/2302.12433, 2023.

Satanjeev Banerjee and Alon Lavie. METEOR: An automatic metric for MT evaluation with
improved correlation with human judgments. In Proceedings of the ACL Workshop on Intrinsic
and Extrinsic Evaluation Measures for Machine Translation and/or Summarization, pp. 65–72,
Ann Arbor, Michigan, June 2005. Association for Computational Linguistics. URL https:
//www.aclweb.org/anthology/W05-0909.

Steven Bird, Ewan Klein, and Edward Loper. Natural Language Processing with Python. O’Reilly,

2009.

Chris Callison-Burch, Miles Osborne, and Philipp Koehn. Re-evaluating the role of Bleu in machine

translation research. In Proc. EACL, 2006.

Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared
Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri,
Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan,
Scott Gray, Nick Ryder, Mikhail Pavlov, Alethea Power, Lukasz Kaiser, et al. Evaluating large
language models trained on code. arXiv preprint arXiv:2107.03374, 2021.

Peter Clark, Oyvind Tafjord, and Kyle Richardson. Transformers as soft reasoners over language. In
Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence (IJCAI),
2020.

Erzsébet Csuhaj-Varjú and Alica Kelemenová. Descriptional complexity of context-free grammar

forms. Theoretical Computer Science, 112(2):277–289, 1993.

Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: An efficient SMT solver. In International
Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.

TJ Dunham and Henry Syahputra. Reactor mk. 1 performances: Mmlu, humaneval and bbh test

results. arXiv preprint arXiv:2406.10515, 2024.

Daniele Faraglia. Faker. https://arhttps://github.com/joke2k/faker, 2024. Ac-

cessed: 2023-06-01.

Clémentine Fourrier, Nathan Habib, Alina Lozovskaya, Konrad Szafer, and Thomas Wolf. Open
llm leaderboard v2. https://huggingface.co/spaces/open-llm-leaderboard/
open_llm_leaderboard, 2024.

IBM Granite Team. Granite 3.0 language models, 2024.

Lin Guan, Karthik Valmeekam, Sarath Sreedharan, and Subbarao Kambhampati. Leveraging pre-
trained large language models to construct and utilize world models for model-based task planning.
Advances in Neural Information Processing Systems, 36:79081–79094, 2023.

Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James
Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alex Wardle-Solano, Hannah Szabo,
Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, Ansong
Ni, Linyong Nan, Jungo Kasai, Tao Yu, Rui Zhang, Alexander R. Fabbri, Wojciech Kryscinski,
Semih Yavuz, Ye Liu, Xi Victoria Lin, Shafiq Joty, Yingbo Zhou, Caiming Xiong, Rex Ying,
Arman Cohan, and Dragomir Radev. FOLIO: Natural language reasoning with first-order logic.
arXiv preprint arXiv:2209.00840, 2022.

Pengcheng He, Xiaodong Liu, Jianfeng Gao, and Weizhu Chen. Deberta: Decoding-enhanced bert
with disentangled attention. In International Conference on Learning Representations, 2021. URL
https://openreview.net/forum?id=XPZIaotutsD.

11

Under review as a conference paper at ICLR 2025

J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and
ISBN

Computation. Addison-Wesley series in computer science. Addison-Wesley, 2001.
9780201441246.

Michael Huth and Mark Dermot Ryan. Logic in Computer Science - Modelling and Reasoning about

Systems. Cambridge University Press, 2nd edition, 2004.

Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Ye Jin Bang,
Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. ACM
Computing Surveys, 55(12):1–38, 2023.

Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization. CoRR,

abs/2311.03755, 2023.

Jacky Liang, Wenlong Huang, Fei Xia, Peng Xu, Karol Hausman, Brian Ichter, Pete Florence, and
Andy Zeng. Code as policies: Language model programs for embodied control. In 2023 IEEE
International Conference on Robotics and Automation (ICRA), pp. 9493–9500. IEEE, 2023.

Chin-Yew Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summarization
Branches Out, pp. 74–81, Barcelona, Spain, July 2004. Association for Computational Linguistics.
URL https://www.aclweb.org/anthology/W04-1013.

Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. Is your code generated by
chatgpt really correct? rigorous evaluation of large language models for code generation. In Conf.
NeurIPS, 2023a.

Jiawei Liu, Chunqiu Steven Xia, Yuyao Wang, and Lingming Zhang. Is your code generated by
chatgpt really correct? rigorous evaluation of large language models for code generation. In
Conference on Advances in Neural Information Processing Systems (NeurIPS), 2023b.

William McCune. Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/,

2010.

Microsoft. Phi-3 technical report: A highly capable language model locally on your phone. https:

//arxiv.org/pdf/2404.14219, 2024. Accessed: 2023-06-01.

MistralAI.

Introducing the world’s best edge models.

https://mistral.ai/news/

ministraux/, 2024. [Accessed 22-11-2024].

Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autofor-

malizing euclidean geometry. In Proc. ICML, 2024.

Theo Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua B.
Tenenbaum, and Roger Levy. LINC: A neurosymbolic approach for logical reasoning by combining
language models with first-order logic provers. In Proc. EMNLP, 2023.

OpenAI. Gpt-4o. https://arxiv.org/pdf/2303.08774.pdf, 2023. Accessed: 2023-06-

01.

OpenAI.

https://openai.com/index/
gpt-4o-mini-advancing-cost-efficient-intelligence/, 2024. Accessed:
2024-09-29.

Gpt-4o-mini.

Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-lm: Empowering large
language models with symbolic solvers for faithful logical reasoning. In EMNLP Findings, 2023.

Nisarg Patel, Mohith Kulkarni, Mihir Parmar, Aashna Budhiraja, Mutsumi Nakamura, Neeraj
Varshney, and Chitta Baral. Multi-logieval: Towards evaluating multi-step logical reasoning
ability of large language models. arXiv preprint arXiv:2406.17169, 2024.

Qwen2. Qwen 2.5. https://qwen2.org/qwen2-5/, 2024. [Accessed 22-11-2024].

Shuo Ren, Daya Guo, Shuai Lu, Long Zhou, Shujie Liu, Duyu Tang, Neel Sundaresan, Ming Zhou,
Ambrosio Blanco, and Shuai Ma. Codebleu: a method for automatic evaluation of code synthesis.
CoRR, 2020.

12

594
595

596
597
598
599
600
601

602
603
604
605
606
607

608
609
610
611
612

613
614
615
616
617
618

619
620
621
622
623
624

625
626
627
628
629
630

631
632
633
634
635

636
637
638
639
640
641

642
643
644
645
646
647

Under review as a conference paper at ICLR 2025

648
649

650
651
652
653
654
655

656
657
658
659
660
661

662
663
664
665
666

667
668
669
670
671
672

673
674
675
676
677
678

679
680
681
682
683
684

685
686
687
688
689

690
691
692
693
694
695

696
697
698
699
700
701

Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Pearson, 4th edition,

2020.

Pranab Sahoo, Ayush Kumar Singh, Sriparna Saha, Vinija Jain, Samrat Mondal, and Aman Chadha.
A systematic survey of prompt engineering in large language models: Techniques and applications.
arXiv preprint arXiv:2402.07927, 2024.

Abulhair Saparov and He He. Language models are greedy reasoners: A systematic formal analysis
of chain-of-thought. In International Conference on Learning Representations (ICLR), 2023.

Karin Kipper Schuler. VerbNet: A Broad-coverage, Comprehensive Verb Lexicon. PhD thesis,

University of Pennsylvania, 2005. AAI3179808.

Koustuv Sinha, Shagun Sodhani, Jin Dong, Joelle Pineau, and William L. Hamilton. CLUTRR: A
diagnostic benchmark for inductive reasoning from text. In Proceedings of the 2019 Conference
on Empirical Methods in Natural Language Processing and the 9th International Joint Conference
on Natural Language Processing (EMNLP-IJCNLP), 2019.

Aarohi Srivastava, Abhinav Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam
Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska,
Aitor Lewkowycz, Akshat Agarwal, Alethea Power, et al. Beyond the imitation game: Quantifying
and extrapolating the capabilities of language models. Transactions on Machine Learning Research,
2023. ISSN 2835-8856.

Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung,
Aakanksha Chowdhery, Quoc Le, Ed Chi, Denny Zhou, and Jason Wei. Challenging BIG-
bench tasks and whether chain-of-thought can solve them. In Findings of the Association for
Computational Linguistics: ACL 2023, 2023.

Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. Diagnosing the
first-order logical reasoning ability through LogicNLI. In Proceedings of the 2021 Conference on
Empirical Methods in Natural Language Processing (EMNLP), 2021.

Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi,
Quoc V Le, and Denny Zhou. Chain of thought prompting elicits reasoning in large language
models. In Conference on Advances in Neural Information Processing Systems (NeurIPS), 2022.

Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and
Christian Szegedy. Autoformalization with large language models. In Conference on Advances in
Neural Information Processing Systems (NeurIPS), 2022.

Cheng Xu, Shuhao Guan, Derek Greene, and M-Tahar Kechadi. Benchmark data contamination of

large language models: A survey. arXiv preprint arXiv:2406.04244, 2024.

Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. Harnessing the power of
large language models for natural language to first-order logic translation. CoRR, abs/2305.15541,
2023. doi: 10.48550/ARXIV.2305.15541.

Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Benchmarking multimodal regex synthesis with

complex structures. In Proc. ACL, 2020.

Yi. 01-ai. https://huggingface.co/01-ai/Yi-1.5-34B-Chat, 2024. Accessed: 2024-

11-22.

Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. ReClor: A reading comprehension dataset
requiring logical reasoning. In International Conference on Learning Representations (ICLR),
2020.

Tianyi Zhang*, Varsha Kishore*, Felix Wu*, Kilian Q. Weinberger, and Yoav Artzi. Bertscore:
Evaluating text generation with bert. In International Conference on Learning Representations,
2020. URL https://openreview.net/forum?id=SkeHuCVFDr.

Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, and Yuhuai Wu.
Don’t trust: Verify - grounding LLM quantitative reasoning with autoformalization. In Proc. ICLR
2024, 2024.

13

Under review as a conference paper at ICLR 2025

A APPENDIX ORGANIZATION

Our anonymized code is provided with our paper submission. Due to space limitations (our complete
results are over 4GB), we have provided two of the batches of the zero-shot prompting results and
FOLIO and LogiEval datasets.

The appendix is organized as follows. Appendix Appendix B provides the algorithm used for dataset
generation. Appendix C discusses prompt tuning and validating our prompts on 3SAT. Appendix D
provides the parameters we used when generating the five datasets discussed in the paper. Appendix
E provides additional information on our experimental setup, including the computational resources
used. Appendix F discusses the prompts and provides examples. Appendix G is our detailed analysis
of the empirical results from the main paper. Appendix H discusses an experiment we ran to evaluate
the standard deviation error. Appendix I includes additional results from our zero-shot prompting
experiments using other metrics for categorization. Appendix J evaluates an experiment we performed
comparing few-shot prompting compared to zero-shot. Finally, Appendix K provides the experimental
setup of the benchmarks we evaluated, data values and sources of scores collected, the
L
scores used for comparison, and additional correlation results.

∃∨∧

uto

∀

B DATASET GENERATION

In this section, we provide the algorithm for generating formal syntax (FS) expressions and show that
it can generate all possible expressions from the grammar and vocabulary.

Our approach,
L, generates datasets by constructing a context-free grammar (CFG) tree
using the grammars discussed in Section 4. Since it is intractable to generate the full tree, we control
the branching factor and randomly expand the branches of this tree to generate formulae.

∃∨∧

uto

∀

, branching factor n, tree depth depth, sample count sample_count,

Algorithm 1 Dataset Generation
, vocabulary

1: Inputs: CFG

−

N

←

,
}

, n)

t
N

1], n)

N
for ν

← ⟨⟩
[d

N ← {
′

sampleN(
′ do

generateNChildren(ν,

∈ N
ν,
ν
N
←
T
[d] +=
N
t
t
← N
N
end for

V
G
and categorization metric m.
2: Outputs: set of FS expressions φ
0 : [None]
3:
4: for d = 1, 2, . . . , depth do
5:
6:
7:
8:
9:
10:
11: end for
12: M
←
13: φ
← ⟨⟩
14: for k
∈
sampleCFGExpressions(M [k], sample_count)
Mk
15:
←
buildFSExpressions(Mk,
φk ←
16:
φ
φ
17:
←
18: end for
19: Return: φ

categorizeExpressionsIntoDict(

keys(M ) do

ν
N
∪ T

t, m)

φk

N

∪

V

G

)

ν

The dataset generation algorithm is shown in Algorithm 1. This algorithm constructs a CFG tree
by maintaining non-terminal nodes at each tree level (
t), where each
terminal node represents a completed CFG expression (line 3). For generating nodes at a certain level
in the tree, n nodes from the previous level are sampled (line 5). Each node is branched n times
using the CFG to produce nodes at the current tree level, and all the leaf nodes are collected (lines 7
through 9). As a result, by iteratively performing this process for each tree level, we obtain a set of
leaf nodes (CFG expressions).

) and all the leaf nodes (

N

N

The leaf nodes are then categorized based on the specified metric (e.g., tree depth, number of operators,
etc.) (line 12). For each metric value, a fixed number of CFG expressions corresponding to that

14

702
703

704
705
706
707
708
709

710
711
712
713
714
715

716
717
718
719
720

721
722
723
724
725
726

727
728
729
730
731
732

733
734
735
736
737
738

739
740
741
742
743

744
745
746
747
748
749

750
751
752
753
754
755

Under review as a conference paper at ICLR 2025

value are sampled (line 15). Using the vocabulary, an FS expression is constructed from each CFG
expression (line 16). Consequently, the final dataset of FS expressions contains an equal number for
each metric value (line 17). This set of FS expressions is the final result produced by the algorithm
(line 19).

The vocabulary is fixed in length, with a hyperparameter controlling the number of unique propositions
for propositional logic. Similarly, for first-order logic, the number of unique variables, constants, and
predicates are also hyperparameters. Also, regular expressions have a hyperparameter controlling
the alphabet size. When these expression components are needed for building the FS expression,
the exact one is selected using uniform random selection. In the special case of first-order logic
predicates, the grounded predicate is generated by randomly selecting a predicate and then selecting
constants depending on the predicate’s arity. In the case of the arbitrary vocabulary, the arity for a
predicate is randomly assigned. To add variables, each constant has a certain probability of being
replaced by a variable.

Guaranteed Expression Coverage The dataset generator (Algorithm 1) is guaranteed to generate all
possible formal syntax expressions that can be produced for a grammar and vocabulary. Let φ be
an FS expression that can be constructed using the rules from CFG
. Note
that φ corresponds to a CFG expression φCF G, derived by substituting the vocabulary with the CFG
symbols. Due to uniform selection, the probability of φ being generated from φCF G is greater than
zero. Furthermore, the CFG expression represents a leaf node in the CFG tree that can be reached by
applying the CFG rules in a specific sequence. Due to the random sampling of rules at each node,
there is a non-zero probability of generating this particular path in the tree. Thus, φ can be generated
using the dataset generator algorithm.

and the vocabulary

V

G

C 3-SAT PROMPT CALIBRATION

In this section, we discuss the KSAT results used to calibration the prompts.

We tested several prompts for 3-SAT to verify that our prompts are sufficient to prompt the LLM
to correctly perform informalization and autoformalization. Additionally, we verified that the
equivalence verification prompt prompted the LLMs to give an accurate yes-or-no answer. The
performance of all six LLMs on 3-SAT for §A2, §A3, and §A4 are shown in Figure 7.

Figure 7: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) for 3-SAT from using
L to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the

uto

∃∨∧
∀
# of operators.

The best-performing models we tested (GPT-4o and GPT-4o-mini) achieved nearly perfect syntactic
compliance, accuracy, and equivalence verification even as the number of operators increased. This

15

756
757

758
759
760
761
762
763

764
765
766
767
768
769

770
771
772
773
774

775
776
777
778
779
780

781
782
783
784
785
786

787
788
789
790
791
792

793
794
795
796
797

798
799
800
801
802
803

804
805
806
807
808
809

0.000.250.500.751.00§A2:SyntacticCompliance3–SAT(12)0.000.250.500.751.00§A3:Accuracy01020304050600.000.250.500.751.00§A4:F1Score#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)ChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3Under review as a conference paper at ICLR 2025

proves that the prompts we used in our experiments are sufficient for prompting the model for
performing the tasks for §A2, §A3, and §A4.

For the other LLMs tested, syntactic compliance and accuracy diminished as the number of operators
increased. However, when evaluating the equivalence of GPT-4o results, all LLMs achieved near-
perfect accuracy regardless of operator number. Due to most of GPT-4o results being positive cases,
the results support that LLMs can verify two equivalent 3-SAT formulae as equivalent.

D DATASET GENERATION HYPERPARAMETERS

In Table 1, we provide the hyperparameters used to generate the five datasets.

Table 1: Hyperparameters used for producing the five datasets.

Parameter Type

Hyperparameter

Value Description

General

depth
n

sample_count

40
200

50

Maximum depth of the CFG tree.
Branching factor of produced CFG
tree.
Number of CFGS for each metric
value to select.

First-Order Logic

free_variable_prob 0.25

max_free_variables
∞
max_predicate_arity 2
min_predicate_arity 1
num_objects
12
num_predicates
8

Propositional Logic

num_propositions

Regular Expression alphabet_size

12

2

Probability of a constant being re-
placed by a variable.
Maximum number of unique variables.
Maximum predicate arity.
Minimum predicate arity.
Number of unique constants.
Number of unique predicates.

Number of unique propositions.

Alphabet size.

E EXPERIMENTAL SETUP

In this section, we will provide the details of our experimental setup for generating the datasets and
running

L for evaluating each LLM’s performance.

uto

∀

∃∨∧

We ran our experiments using Python 3.10.13 with package versions shown in Table 2. We also
repackaged Prover9 (McCune, 2010) to improve performance where this repackaged version can be
found in our code base.

Dataset Generation: We generated five datasets using the
dataset generation algorithm with the hyperparameters shown in
Table 1 using the number of operators as the categorization metric
for all but regular expression, where we used CFG tree depth. We
generated 10 batches for each dataset, resulting in approximately
20k samples for each dataset with an equal distribution for each
operator number.

Evaluating and Verification: The closed-source models (GPT-
3.5-turbo, GPT-4o, and GPT-4o-mini) were accessed using their
API using a temperature of 0.1. The open-source models LLama-
3-8B-Instruct and Mistral-v0.2-7B-Instruct were locally hosted
on a server with a 13th Gen Intel(R) Core(TM) i9-13900K and
Nvidia RTX 4090 GPU using the model’s default parameters
with a temperature of 1. Similarly, Phi-3-medium-4k-instruct was
locally hosted on a server using a Nvidia A100-XM4-80GB GPU.

Table 2: Python package versions
used for empirical evaluation.
Version

Python Package

openai
nltk
tqdm
anthropic
backoff
tiktoken
transformers
Faker
networkx

1.45.0
3.8.1
4.66.4
0.26.1
2.2.1
0.6.0
4.41.1
25.2.0
3.3

16

810
811

812
813
814
815
816
817

818
819
820
821
822
823

824
825
826
827
828

829
830
831
832
833
834

835
836
837
838
839
840

841
842
843
844
845
846

847
848
849
850
851

852
853
854
855
856
857

858
859
860
861
862
863

Under review as a conference paper at ICLR 2025

Prompt 2: Few-Shot First-Order Logic Informalization Prompt

[TASK]
Your task is to convert a first-order logic formula, appearing after [FORMULA], to a natural
description that represents the formula. Only natural language terms are allowed to be used
and do not copy the formula in your description. Your description should allow one to
reconstruct the formula without having access to it, so make sure to use the correct names in
your description. Explicitly describe the predicates. You may use terms verbatim as specified
in the vocabulary below.

p2

[EXAMPLE 1]
(
p1
¬
Disjunctive predicate logic expression consisting of three components: the negation of a
proposition labeled p2, the proposition p1, and again the negation of p2.

∨ ¬

p2)

∨

[EXAMPLE 2]
(
(p3
¬¬
The expression asserts that p2 is not false while both p3 and p1 are not true.

p1))

∧ ¬

p2

∨

[VOCABULARY]

represents disjunction
represents conjunction
represents negation

∨
∧
¬
( and ) represent parentheses
propositions can be used verbatim
predicates can be used verbatim

< x1 >< x2 > ... < xn > . represents universal quantification with x1... representing

∀
free variables

< x1 >< x2 > ... < xn > . represents existential quantification with x1... representing

∃
free variables
The objects are: p5, x1
The parameterized predicates are: pred3(?p0, ?p1)
The free variables are: x1

[FORMULA]

x1 pred3(p5, x1)

∀

Verification was performed on an AMD EPYC machine with 128
cores.

F PROMPTING

In this section, we provide the zero-shot and few-shot used in the main paper experiments.

The prompt for each dataset type provides the LLM with information on the problem type and the
vocabulary. For informalization, we prompt the model to produce just a natural language description.
We also provide the list of objects, predicates, propositions, and free variables in the formal syntax
expression. For autoformalization, the LLM is prompted to provide just the formal syntax expression
using the natural language description. Additionally, for first-order logic with a non-synthetic
grammar, we provide the predicate names and arity in the autoformalization prompt. Two examples
are provided for few-shot prompting.

For §A4, the prompt used for using an LLM to verify the equivalence of two formulae tells the
LLM about the type of datasets (e.g., propositional logic, first-order logic, and regular expression).
Using Chain-of-Thought prompting, the model is prompted to provide an explanation before giving a
yes-or-no answer in a parsable format. Below are examples of the exact prompts used.

17

864
865

866
867
868
869
870
871

872
873
874
875
876
877

878
879
880
881
882

883
884
885
886
887
888

889
890
891
892
893
894

895
896
897
898
899
900

901
902
903
904
905

906
907
908
909
910
911

912
913
914
915
916
917

Under review as a conference paper at ICLR 2025

Prompt 3: Few-Shot First-Order Logic Autoformalization Prompt

∨
∧
¬

[VOCABULARY]
to represent disjunction
Use
to represent conjunction
Use
Use
to represent negation
Use ( and ) to represent parentheses
Use
Use
The <free_variable_list> consists of a sequence of space separate free variables with the last
variable immediately followed by a period. Examples: (1) all x1 x2. (2) exists x4.
Use <predicate>(<parameter_list>) to represent predicates (Names and parameters are
provided in the description)

<free_variable_list> to represent universal quantification
<free_variable_list> to represent existential quantification

∀
∃

[TASK]
Your task is to interpret the natural language (NL) description of a first-order logic formula
and represent it as formal syntax using the vocabulary specified in the [VOCABULARY]
block above. Only output the formula and no other text. The NL description appears
immediately following the [NL DESCRIPTION] tag.

∨

p2

p1

p2)

[EXAMPLE 1]
Disjunctive predicate logic expression consisting of three components: the negation of a
proposition labeled p2, the proposition p1, and again the negation of p2.
(
¬
∨ ¬
[EXAMPLE 2]
The expression asserts that p2 is not false while both p3 and p1 are not true.
(
¬¬
[NL DESCRIPTION]
For all objects labeled x1, the predicate pred3 holds true with parameters p5 and x1.

p1))

∧ ¬

(p3

p2

∨

G ANALYSIS OF MAIN PAPER RESULTS

In this section, we analyze the main empirical results of the paper. Our results clearly show that
current SOTA LLMs are not performant in the truth maintenance task, which is why
L is
needed. As the expression complexity increases, the syntactic compliance, accuracy, and ability
to verify equivalence diminishes. We describe some of the errors that cause the low accuracy for
propositional logic, first-order logic, and regular expressions.

∃∨∧

uto

∀

G.1 PROPOSITIONAL LOGIC RESULTS

Informalization Errors: A common error was the LLM failed to describe the proposition names.
Another was the LLM failing to provide a complete description of the formula. For example, GPT-
3.5-turbo often described portions of the expression based on what propositions and operators it
contained. A common issue with GPT-4o, one of the best models, is that it often uses different
propositional symbols (see example 5 in Table 3). Finally, we also observed hallucinations were
the LLM attempted and failed to simplify the original formula (see example 4 in Table 3). These
interpretation errors resulted in the original meaning of the expression being lost.

Autoformalization Errors: We observed there were often syntactic issues where the description was
not fully translated into a formula or the parentheses did not match. An interesting result is that the
LLMs struggled to place the negation operator in the correct location. For example, GPT-4o often
p as predicate p "negated twice and combined" but failed to regenerate the original
describes
formula properly with this description.

∧ ¬

¬

p

18

918
919

920
921
922
923
924
925

926
927
928
929
930
931

932
933
934
935
936

937
938
939
940
941
942

943
944
945
946
947
948

949
950
951
952
953
954

955
956
957
958
959

960
961
962
963
964
965

966
967
968
969
970
971

Under review as a conference paper at ICLR 2025

972
973

974
975
976
977
978
979

980
981
982
983
984
985

986
987
988
989
990

991
992
993
994
995
996

997
998
999
1000
1001
1002

1003
1004
1005
1006
1007
1008

1009
1010
1011
1012
1013

1014
1015
1016
1017
1018
1019

1020
1021
1022
1023
1024
1025

Prompt 4: Few-Shot Regex Informalization Prompt

[TASK]
Your task is to convert the regular expression appear after [REGEX], to a natural description
that represents the regular expression. Only natural language terms are allowed to be used
and do not copy the regular expression in your description. Your description should allow
one to reconstruct the regular expression without having access to it, so make sure to use the
correctly account for scoping. You may use terms verbatim as specified in the vocabulary
below.

[VOCABULARY]
you may use symbols from the vocabulary
you can use *

[EXAMPLE 1]
(1*)0*
The regex matches strings that starts with any number (including none) of the digit ’1’,
followed by any number (including none) of the digit ’0’.

[EXAMPLE 2]
(01*)
The regex matches strings that begin with a ’0’ followed directly by any number (including
none) of ’1’s.

[FORMULA]
0

Prompt 5:

Few-Shot Regex Autoformalization Formal [VOCABULARY]
Use * to represent zero or more duplications of the same expression
Use ( and ) to represent parentheses

[TASK]
Your task is to interpret the natural language (NL) description of a regular expression and
represent it as formal syntax using the vocabulary specified in the [VOCABULARY] block
above. Only output the regular expression and no other text. The NL description appears
immediately following the [NL DESCRIPTION] tag.

[EXAMPLE 1]
The regex matches strings that starts with any number (including none) of the digit ’1’,
followed by any number (including none) of the digit ’0’.
(1*)0*

[EXAMPLE 2]
The regex matches strings that begin with a ’0’ followed directly by any number (including
none) of ’1’s.
(01*)

[NL DESCRIPTION]
The regex matches strings that start with the digit ’0’.

G.2 FIRST-ORDER LOGIC RESULTS

Informalization Errors: Similar to propositional logic, we observed the LLM often failed providing
enough details resulting in incorrect formulas being generated. A significant source of errors we

19

Under review as a conference paper at ICLR 2025

Prompt 6: Zero-Shot Propositional Logic Informalization Prompt

[TASK]
Your task is to convert a propositional logic formula, appearing after [FORMULA], to a
natural description that represents the formula. Only natural language terms are allowed to be
used and do not copy the formula in your description. Your description should allow one to
reconstruct the formula without having access to it, so make sure to use the correct names in
your description. Explicitly describe the predicates. You may use terms verbatim as specified
in the vocabulary below.

[VOCABULARY]

represents disjunction
represents conjunction
represents negation

∨
∧
¬
( and ) represent parentheses
propositions can be used verbatim
The propositions are: p5, p12, p4

[FORMULA]
(p5

p12

∨ ¬

∨ ¬

p4)

Prompt 7: Zero-Shot Propositional Logic Autoformalization Prompt

[TASK]
Your task is to interpret the natural language (NL) description of a propositional logic formula
and represent it as formal syntax using the vocabulary specified in the [VOCABULARY]
block above. Only output the formula and no other text. The NL description appears
immediately following the [NL DESCRIPTION] tag.

[VOCABULARY]
to represent disjunction
Use
to represent conjunction
Use
Use
to represent negation
Use ( and ) to represent parentheses

∨
∧
¬

[NL DESCRIPTION]
A disjunctive statement involving three propositions: p5, the negation of p12, and the
negation of p4.

observed when not providing the predicate names and arity was the LLM rephrasing its explanation
causing confusion when regenerating.

Autoformalization Errors: Beyond the errors observed in propositional logic, the most common
mistake made during autoformalization was the LLM confusing constants with variables (see example
2 in Table 4). Additionally, the LLMs often messed up the predicate arity. Mistral often used = and
= operators with the variables, which was not needed for any formluae in
L. Similarly, the
LLMs would often use their own grammar instead of the one provided in the prompt.

∃∨∧

uto

∀

G.3 REGULAR EXPRESSION RESULTS

Informalization Errors: Most of the errors observed were the LLMs giving the wrong explanation,
even for simple regular expressions. For example, GPT-4o often described c∗ as "one or more
occurrences of ’c’", where c is a character from the alphabet (see example 1 in Table 5). For the
other LLMs, it was quite common for the explanation to not give the actual character (see example
4 in Table 5). Overall, we observed a higher likelihood of SOTA LLMs hallucinating on regular
expressions compared to the other datasets.

20

1026
1027

1028
1029
1030
1031
1032
1033

1034
1035
1036
1037
1038
1039

1040
1041
1042
1043
1044

1045
1046
1047
1048
1049
1050

1051
1052
1053
1054
1055
1056

1057
1058
1059
1060
1061
1062

1063
1064
1065
1066
1067

1068
1069
1070
1071
1072
1073

1074
1075
1076
1077
1078
1079

̸
Under review as a conference paper at ICLR 2025

Prompt 8: First-Order Logic Verification Prompt

Your task is to say whether two First-Order Logic formulae are equivalent. The first formula
will appear right after [FORMULA 1] and the second after [FORMULA 2].
Give an explanation followed by a yes or no answer. The answer must show up at the end
with the format "[Answer]" followed by either a yes or no.

[Formula 1]

x1.

pred5(p7)

¬
∃
[Formula 2]

p7.

∃

pred5(p7)

¬

Table 3: Examples of errors the evaluated LLMs made while evaluating
tional logic dataset.

uto

∀

∃∨∧

L for the proposi-

φ

(

(

(

(

p11

¬

∧ ¬

p8)

p10

¬

(

∧

p9

¬

∨

p7))

p3

¬

∧ ¬

p7)

p2

¬¬

∨

p3)

(

p2

¬

∧

p5

∧ ¬

p6)

(φ)

I
The natural description of the formula is:
"It is not the case that both proposition p11
and proposition p8 are true."
The natural description of the formula is:
"It is not the case that proposition p10 is true
and either proposition p9 is false or
proposition p7 is true."
Here is the natural description of the given
formula: "The statement says that p3 is not
true and p7 is also not true."
The formula states that either the proposition
p2 is true or the proposition p3 is true.
Additionally, it specifies that the proposition
p2 is not false.
The formula describes a situation where the
first proposition is false, the second
proposition is true, and the third proposition
is false.

(
A ◦ I

)(φ)

(p11

(
¬

∧

p8))

(p10

¬

p9

(
¬

∨

∧

p7))

p3

(
¬

∨ ¬

p7)

(p2

p3)

∨

∧ ¬¬

p2

p

(
¬

∧

q

∧ ¬

r)

Autoformalization Errors: The most common mistake when constructing a regular expression from
or adding it when it was not needed (see example 3 in Table 5).
natural language was misplacing
Finally, even though we explicitly prompted the LLMs to use just
, sometimes the LLM would use
+.

∗

∗

H STANDARD DEVIATION EVALUATION

uto

∃∨∧

In this section, we perform an empirical analysis of the standard deviation of the syntactic compliance
and accuracy of the
L results. Due to the 10 batches having different data, the standard
∀
deviation cannot be computed reliably based on the performance of the individual batches. We
evaluated the standard deviation by running
L 10 times on the first batch of each dataset
uto
composed of 1974 propositional logic, 1900 first-order logic, and 1842 regular expressions examples.
Additionally, we evaluated GPT-3.5-turbo (ChatGPT) with a temperature of 1, LLama-3-8B-Instruct,
Mistral-v0.2-7B-Instruct, and Phi-3-medium-4k-instruct. We calculated the mean and standard
deviation of each independent run of

L and plotted the results in Figure 8.

∃∨∧

uto

∀

∀

∃∨∧

For propositional and first-order logic, the standard deviation of the evaluated LLMs is low. While
noisier, the standard deviation of the regular expression results were still less than 20% with the
better performing models having a lower standard deviation. Overall, this experiment shows that the

1080
1081

1082
1083
1084
1085
1086
1087

1088
1089
1090
1091
1092
1093

1094
1095
1096
1097
1098

1099
1100
1101
1102
1103
1104

1105
1106
1107
1108
1109
1110

1111
1112
1113
1114
1115
1116

1117
1118
1119
1120
1121

1122
1123
1124
1125
1126
1127

1128
1129
1130
1131
1132
1133

21

Under review as a conference paper at ICLR 2025

Table 4: Examples of errors the evaluated LLMs made while evaluating
logic dataset.

uto

∀

∃∨∧

L for the first-order

φ

pred8(p10)
(
¬
pred6(p8))
∧

∧

pred8(p5)

x1.

pred2(p4)

∃

∀

¬

¬¬

x1.

pred3(p5)

pred2(p3, p5)

(φ)

I
The formula states that it is not the case
that the predicate pred8 holds for the
object p10, and the predicate pred8
holds for the object p5, and the
predicate pred6 holds for the object p8,
all conjoined together.
Here is the natural description of the
given formula: "There exists an x1 such
that p4 is not an instance of pred2.
For all x1, it is not the case that
pred3(p5) is false.
There exists a relationship between the
objects p3 and p5 such that the predicate
pred2 holds true for these objects.

(
A ◦ I

)(φ)

(pred8(p10)
pred8(p5)
pred6(p8))

¬
∧
∧

x1.

∃

pred2(x1)

¬

x1.

(pred3(p5)

¬

pred3(p5))

∀
∨¬

p3 p5.pred2(p3, p5)

∃

Table 5: Examples of errors the evaluated LLMs made while evaluating with
regular expression dataset.

∀

uto

∃∨∧

L for the

φ

1∗0

(1∗)∗0

1∗11∗

(1)∗0

(φ)

I
The pattern consists of one or more occurrences of the digit
"1" followed by exactly one occurrence of the digit "0".
The regular expression describes a sequence that consists of
zero or more repetitions of the digit ’1’, followed by exactly
one ’0’. This entire pattern can repeat any number of times,
including zero times.
The pattern consists of zero or more occurrences of the
digit ’1’, followed by exactly one occurrence of the digit ’1’,
followed by zero or more occurrences of the digit ’1’.
Zero or more occurrences of the character or group of
characters before the asterisk.

)(φ)

(
A ◦ I
(1∗)10

((1∗)0)∗

1∗1∗1∗

(.∗)

noise of non-deterministic text generation does not significantly impact
evaluations.

I ADDITIONAL ZERO-SHOT PROMPTING RESULTS

uto

∀

∃∨∧

L or our results and

In this section, we evaluate other categorization metrics from the zero-shot prompting experiments
from the main paper. For the propositional and first-order logic datasets, the other categorization
metrics are the CFG parse tree depth needed to produce each FS expression and the individual number
of each operator (
). For regular expressions, we have discussed in the main paper that each
regular expression represents a minimal DFA that is unique up to isomorphism. Therefore, the other
categorization metrics for regular expressions are the number of nodes V , the number of edges E,
and the density of this minimal DFA. The density is calculated using Equation 1 where we discretize
the value by rounding to every tenth.

,
∧

,
∨

¬

Density =

E
|
V
|

|
| −

V
|

(
|

1)

(1)

Imbalanced Dataset Labels Due to the datasets being created by sampling an equal number of
expressions for each number of operators, taking this dataset and evaluating it in terms of the other

22

1134
1135

1136
1137
1138
1139
1140
1141

1142
1143
1144
1145
1146
1147

1148
1149
1150
1151
1152

1153
1154
1155
1156
1157
1158

1159
1160
1161
1162
1163
1164

1165
1166
1167
1168
1169
1170

1171
1172
1173
1174
1175

1176
1177
1178
1179
1180
1181

1182
1183
1184
1185
1186
1187

Under review as a conference paper at ICLR 2025

Figure 8: Average and standard deviation error of Zero-shot Pass@1 results from using
L
to assess LLMs w.r.t. §A2 and §A3 (Sec. 4) on the first batch of the packaged datasets. The x-axis
represents an increasing order of descriptional complexity.

∃∨∧

uto

∀

metrics results in an imbalanced dataset. To examine this effect, we have created Figures 9 and 10 to
perform an analysis of dataset imbalance on these other metrics.

For propositional and first-order logic, the dataset is actually quite balanced due to CFG tree depth
and the number of each individual operator having a high correlation to the total number of operators.
As such, other than metric values close to the extrema, the noise from the imbalanced data will be
marginal.

The regular expression dataset is less balanced due to a weaker correlation with the CFG tree depth.
The middle of the density graphs will be the most noisy since there is significantly less data for
densities of 0.1 and 0.2. The number of examples drops as the number of edges and nodes increases
with less than 10% of the data having more than 7 edges and/or nodes.

Figure 9: Count of the number of examples for each metric value for the regular expression datasets.
The pie charts increase in values counter-clockwise while going from lighter to darker.

Categorization Metrics Performance In Figures 11, 12,13, 14, and 15 the performance of each
LLM over these other categorization metrics are shown. Across the board, we observe a diminishing
performance regardless of the source of increasing complexity. Ignoring the noise from the low
number of examples closer to the extrema, the depth of the tree showed a similar behavior as the
operator number. Propositional logic performance was concave w.r.t the number of
operators
∨
since it becomes easier to describe expressions composed of exclusively
operators. A similar,
but weaker pattern is observed in the first-order logic results for the same reason. The negation
operator was not concave, showing how LLMs struggle to handle multiple negation operators.

and

and

∧

∨

∧

For regular expressions, increasing the number of nodes and edges reduces accuracy and the ability
to evaluate equality. Density does not seem to be a factor, as the dip at 0.1 can be associated with
noise due to the lower number of examples. Overall, these three metrics are much weaker factors in
how well the LLM performs compared to the CFG tree depth.

23

1188
1189

1190
1191
1192
1193
1194
1195

1196
1197
1198
1199
1200
1201

1202
1203
1204
1205
1206

1207
1208
1209
1210
1211
1212

1213
1214
1215
1216
1217
1218

1219
1220
1221
1222
1223
1224

1225
1226
1227
1228
1229

1230
1231
1232
1233
1234
1235

1236
1237
1238
1239
1240
1241

0.000.250.500.751.00§A2:SyntacticCompliance3–SAT(12)01020304050600.000.250.500.751.00§A3:AccuracyPropositionalLogic(12)010203040FOL(8,12)−S010203040FOL(8,12)−E010203040RegularExpression(2)010203040#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepthChatGPTPhiMistralLLama3RegularExpression(2)00.10.20.30.5Density1234567+#ofEdges1234567+#ofNodesUnder review as a conference paper at ICLR 2025

Figure 10: Count of the number of examples for each metric value for each of the datasets. Each row
is a dataset and each column is a different metric that can be used to categorize the dataset. The pie
charts increase in value counter-clockwise while going from lighter to darker.

Figure 11: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using
L
to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the depth of the
CFG tree to produce the formula.

∃∨∧

uto

∀

24

1242
1243

1244
1245
1246
1247
1248
1249

1250
1251
1252
1253
1254
1255

1256
1257
1258
1259
1260

1261
1262
1263
1264
1265
1266

1267
1268
1269
1270
1271
1272

1273
1274
1275
1276
1277
1278

1279
1280
1281
1282
1283

1284
1285
1286
1287
1288
1289

1290
1291
1292
1293
1294
1295

PropositionalLogic(12)1-23-45-67-89-1011-1213-1415-1617-1819-2021-2223-2425-2627-2829-3031-3233-3435-3637-3839-40CFGParseTreeDepth01234567891011121314151617+#of∧operator012345678910111213141516171819+#of∨operator01234567891011121314151617181920212223+#of¬operatorFirst-OrderLogic(8,12)(Synthetic)3-45-67-89-1011-1213-1415-1617-1819-2021-2223-2425-2627-2829-3031-3233-3435-3637-3839-4001234567891011121314151617+0123456789101112131415161718+012345678910111213141516171819202122+First-OrderLogic(8,12)(English)3-45-67-89-1011-1213-1415-1617-1819-2021-2223-2425-2627-2829-3031-3233-3435-3637-3839-4001234567891011121314151617+0123456789101112131415161718+012345678910111213141516171819202122+0.000.250.500.751.00§A2:SyntacticCompliancePropositionalLogic(12)0.000.250.500.751.00§A3:Accuracy0102030400.000.250.500.751.00§A4:F1ScoreFOL(8,12)−S010203040FOL(8,12)−E010203040RegularExpression(2)010203040CFGParseTreeDepthChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3Under review as a conference paper at ICLR 2025

L
Figure 12: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using
to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the number of
and operators (

) in the expression.

∃∨∧

uto

∀

∧

Figure 13: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using
L
to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the number of
or operators (

) in the expression.

∃∨∧

uto

∀

∨

25

1296
1297

1298
1299
1300
1301
1302
1303

1304
1305
1306
1307
1308
1309

1310
1311
1312
1313
1314

1315
1316
1317
1318
1319
1320

1321
1322
1323
1324
1325
1326

1327
1328
1329
1330
1331
1332

1333
1334
1335
1336
1337

1338
1339
1340
1341
1342
1343

1344
1345
1346
1347
1348
1349

0.000.250.500.751.00§A2:SyntacticCompliancePropositionalLogic(12)0.000.250.500.751.00§A3:Accuracy01020250.000.250.500.751.00§A4:F1ScoreFOL(8,12)−S0102025FOL(8,12)−E0102025#ofOperators:∧ChatGPTGPT-4oGPT-4o-miniPhiMistralLLama30.000.250.500.751.00§A2:SyntacticCompliancePropositionalLogic(12)0.000.250.500.751.00§A3:Accuracy01020250.000.250.500.751.00§A4:F1ScoreFOL(8,12)−S0102025FOL(8,12)−E0102025#ofOperators:∨ChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3Under review as a conference paper at ICLR 2025

1350
1351

1352
1353
1354
1355
1356
1357

1358
1359
1360
1361
1362
1363

1364
1365
1366
1367
1368

1369
1370
1371
1372
1373
1374

1375
1376
1377
1378
1379
1380

1381
1382
1383
1384
1385
1386

1387
1388
1389
1390
1391

1392
1393
1394
1395
1396
1397

1398
1399
1400
1401
1402
1403

L
Figure 14: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using
to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the number of
negation operators (

) in the expression.

∃∨∧

uto

∀

¬

Figure 15: Zero-shot Pass@1 results (avg. over 10 batches, higher values better) from using
L
to assess LLMs w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis is the metric on
the CFG tree to produce the regular expression formula.

∃∨∧

uto

∀

26

0.000.250.500.751.00§A2:SyntacticCompliancePropositionalLogic(12)0.000.250.500.751.00§A3:Accuracy0369120.000.250.500.751.00§A4:F1ScoreFOL(8,12)−S036912FOL(8,12)−E036912#ofOperators:¬(countedasanoperatoriﬀnotsucceededbyaterminal)ChatGPTGPT-4oGPT-4o-miniPhiMistralLLama30.000.250.500.751.00§A2:SyntacticComplianceRegularExpression(2)0.000.250.500.751.00§A3:Accuracy04812160.000.250.500.751.00§A4:F1ScoreRegularExpression(2)0481216RegularExpression(2)0.00.10.20.30.40.5#ofNodes#ofEdgesDensityChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3Under review as a conference paper at ICLR 2025

Figure 16: Syntactic compliance and accuracy difference of few-shot Pass@1 compared to zero-shot
Pass@1 results (avg. over 10 batches, higher values better) from using
L to assess LLMs
w.r.t. §A2, §A3, §A4 (Sec. 4) on the packaged datasets. The x-axis represents the increasing order of
descriptional complexity.

∃∨∧

uto

∀

J FEW-SHOT PROMPTING RESULTS

In this section, we discuss our few-shot prompting experiment and analyze the performance difference
between zero-shot and few-shot prompting on §A1 and §A2.

We evaluated on the same five datasets from the main paper’s experiments but inserted two exam-
ples into the prompts. First-order and predicate logic used the same two examples, while regular
expressions used their own two examples. In Figure 16, the performance difference of each LLM
when using few-shot prompting instead of zero-shot is shown. Using few-shot prompting increases
syntactic compliance as the model has access to the desired format for encoding and decoding.
For expressions with lower complexity, this translates to a better performance on §A2. However,
as complexity increases, the performance difference between zero-shot and few-shot prompting is
negligible due to having the correct format for parsing but failing maintaining the same formula.

K OTHER BENCHMARK CORRELATION AND

EVALUATION

UTO

∀

∃∨∧

L PREDICTIVE POWER

L and existing benchmarks
For evaluating the correlation between a LLM’s performance on
and measuring the predictive power of
L, in Section 5, we evaluated on FOLIO (Han et al.,
2022), Multi-LogicEval (Patel et al., 2024), and HumanEval (Chen et al., 2021). In this section we
discuss these experiments and cite the sources of the HumanEval results along with evaluate the
predictive power of

∃∨∧

∃∨∧

uto

uto

uto

L.

∀

∀

∀

∃∨∧

In this section, we discuss the experimental setup for the benchmark, the sources used for LLM
performance on other benchmarks, and the
L we used for evaluation. We also evaluate the
FOLIO premise benchmark further based on the operator numbers in each premise.

∃∨∧

uto

∀

K.1 FOLIO EXPERIMENTAL SETUPS

The FOLIO dataset is composed of premises and a conclusion for each sample where the task is
to conclude whether the conclusion is true, false, or unknown given the premises. Additionally,
the dataset provides an encoding into first-order logic for all the premises and conclusions. There-
fore, we evaluated each LLM on their abilities to (1) informalize a first-order logic premise, (2)
autoformalize a natural language premise, (3) correctly classifying the conclusion using the first-
order logic representations, and (4) correctly classifying the conclusion using the natural language
representations.

27

1404
1405

1406
1407
1408
1409
1410
1411

1412
1413
1414
1415
1416
1417

1418
1419
1420
1421
1422

1423
1424
1425
1426
1427
1428

1429
1430
1431
1432
1433
1434

1435
1436
1437
1438
1439
1440

1441
1442
1443
1444
1445

1446
1447
1448
1449
1450
1451

1452
1453
1454
1455
1456
1457

−0.250.000.250.500.751.00§A2:SyntacticCompliancePropositionalLogic(12)010203040−0.250.000.250.500.751.00§A3:AccuracyFOL(8,12)−S010203040FOL(8,12)−E010203040RegularExpression(2)010203040#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepthChatGPTGPT-4oGPT-4o-miniPhiMistralLLama3Under review as a conference paper at ICLR 2025

Prompt 9: FOLIO Premise Informalization Prompt

[TASK]
Your task is to convert a first-order logic formula, appearing after [FORMULA], to a natural
description that represents the formula. Only natural language terms are allowed to be used
and do not copy the formula in your description. Your description should allow one to
reconstruct the formula without having access to it, so make sure to use the correct names in
your description. Explicitly describe the predicates. You may use terms verbatim as specified
in the vocabulary below.

[EXAMPLE 1]

x(DrinkRegularly(x, cof f ee)

(

W antT oBeAddictedT o(x, caf f eine)))

∀
People regularly drink coffee, or they don’t want to be addicted to caffeine, or both.
[VOCABULARY]

¬

∨

represents disjunction
∨
represents conjunction
∧
represents negation
¬
represents implication
→
( and ) represent parentheses
propositions can be used verbatim
predicates can be used verbatim

< x1 >< x2 > ... < xn > . represents universal quantification with x1... representing

∀
free variables

< x1 >< x2 > ... < xn > . represents existential quantification with x1... representing

predicates

are:

awarethatdrug(?p0, ?p1),

∃
free variables
The objects are: caffeine
The
parameterized
wanttobeaddictedto(?p0, ?p1)
The free variables are: x

[FORMULA]

x. (

∀

wanttobeaddictedto(x, caf f eine)

¬

awarethatdrug(x, caf f eine))

→ ¬

For the FOLIO premise informalization and autoformalization experiments, the LLM was prompted
L where the example from the
using the same few-shot first-order logic prompt used by
prompt is another premise from the same FOLIO example to make sure both the example and the
evaluated premises have the same context. Premises were screened to make sure that we were able to
parse them into Prover9. Below is an example premises come from the FOLIO dataset.

∃∨∧

uto

∀

For evaluating the performance of each LLM on classifying whether the premises entailed the conclu-
sion, the same prompt was used for both the natural language and first-order logic representations of
the premises and conclusions. The prompts are inspired by the prompts used in Multi-LogiEval and
use Chain-of-Thought prompting and prompt the model to provide the answer in a parsable format.
An example for both premises using an example from the FOLIO dataset are shown below.

We evaluated the informalization results against the ground truth natural language representation
using BLEU (Callison-Burch et al., 2006), ROUGE (Lin, 2004), METEOR (Banerjee & Lavie, 2005),
and BERT Score (Zhang* et al., 2020). The model deberta-xlarge-mnli (He et al., 2021) was used for
the BERT score calculation. For the autoformalization results, we used the same verification process
as the main paper. For the FOLIO conclusion classification, the LLM’s answered was parsed out of
its response with the examples that could not be parsed being classified as "Unknown" and marked as
wrong. These examples were checked to verify the parser.

K.2 MULTI-LOGIEVAL EXPERIMENT SETUP

The task in Multi-LogicEval (Patel et al., 2024) is to answer a yes-or-no question using the provided
context, where the question was created using a certain depth of rules of logical reasoning. We used a
prompt similar to the one they used where we use Chain-of-Thought prompting and prompt the LLM

28

1458
1459

1460
1461
1462
1463
1464
1465

1466
1467
1468
1469
1470
1471

1472
1473
1474
1475
1476

1477
1478
1479
1480
1481
1482

1483
1484
1485
1486
1487
1488

1489
1490
1491
1492
1493
1494

1495
1496
1497
1498
1499

1500
1501
1502
1503
1504
1505

1506
1507
1508
1509
1510
1511

Under review as a conference paper at ICLR 2025

Prompt 10: FOLIO Premise Autoformalization Prompt

∨
∧
¬

[VOCABULARY]
to represent disjunction
Use
to represent conjunction
Use
Use
to represent negation
Use ( and ) to represent parentheses
The objects are: caffeine
The parameterized predicates are: awarethatdrug(?p0, ?p1),
wanttobeaddictedto(?p0, ?p1)
The free variables are: x

[TASK]
Your task is to interpret the natural language (NL) description of a first-order logic formula
and represent it as formal syntax using the vocabulary specified in the [VOCABULARY]
block above. Only output the formula and no other text. The NL description appears
immediately following the [NL DESCRIPTION] tag.

[EXAMPLE 1]
People regularly drink coffee, or they don’t want to be addicted to caffeine, or both.

x(DrinkRegularly(x, cof f ee)

(

W antT oBeAddictedT o(x, caf f eine)))

∀
[NL DESCRIPTION]
No one who doesn’t want to be addicted to caffeine is unaware that caffeine is a drug.

∨

¬

Prompt 11: FOLIO Natural Language Representation Prompt

For the following [PREMISES] containing rules of logical reasoning, perform step-by-step
reasoning to answer whether the [CONCLUSION] is True/False/Uncertain based on the
[PREMISES]. Use the following answer format:
Reasoning Steps:
Answer: True/False/Uncertain
[PREMISES]:
All people who regularly drink coffee are dependent on caffeine
People regularly drink coffee, or they don’t want to be addicted to caffeine, or both.
No one who doesn’t want to be addicted to caffeine is unaware that caffeine is a drug.
Rina is either a student who is unaware that caffeine is a drug, or she is not a student and is
she aware that caffeine is a drug.
Rina is either a student who depend on caffeine, or she is not a student and not dependent on
caffeine.
[CONCLUSION]:
Rina doesn’t want to be addicted to caffeine or is unaware that caffeine is a drug.

to provide the answer in a specific location to parse. Examples of these prompts are provided below
using examples from the Multi-LogiEval dataset.

K.3 HUMANEVAL AND BIG BENCH HARD SCORE SOURCES

To evaluate the correlation and predictive power of
L against commonly used LLM bench-
marks HumanEval (Chen et al., 2021) and Big Bench Hard (BBH) (Suzgun et al., 2023), we collected
the performance scores of the LLMs we evaulated on both benchmarks and report our findings and
sources in Table 6. We were unable to find any sources that evaluated GPT-4o-mini on BBH.

∃∨∧

uto

∀

29

1512
1513

1514
1515
1516
1517
1518
1519

1520
1521
1522
1523
1524
1525

1526
1527
1528
1529
1530

1531
1532
1533
1534
1535
1536

1537
1538
1539
1540
1541
1542

1543
1544
1545
1546
1547
1548

1549
1550
1551
1552
1553

1554
1555
1556
1557
1558
1559

1560
1561
1562
1563
1564
1565

Under review as a conference paper at ICLR 2025

Prompt 12: FOLIO First-Order Logic Representation Prompt

For the following [PREMISES] containing rules of logical reasoning, perform step-by-step
reasoning to answer whether the [CONCLUSION] is True/False/Uncertain based on the
[PREMISES]. Use the following answer format:
Reasoning Steps:
Answer: True/False/Uncertain
[PREMISES]:

W antT oBeAddictedT o(x, caf f eine)

x(DrinkRegularly(x, cof f ee)
x(DrinkRegularly(x, cof f ee)
x(
(Student(rina)
⊕ ¬
(IsDependentOn(rina, caf f eine)

∀
∀
∀
¬
¬
[CONCLUSION]:

→
(
∨

¬

¬

AwareT hatDrug(rina, caf f eine))

→ ¬

Student(rina))

⊕

IsDependentOn(x, caf f eine))

W antT oBeAddictedT o(x, caf f eine)))

AwareT hatDrug(x, caf f eine))

W antT oBeAddictedT o(rina, caf f eine)

¬

(

∨

AwareT hatDrug(rina, caf f eine))

¬

Prompt 13: Multi-LogicEval Prompt

"Given the context that contains rules of logical reasoning in natural language and question,
perform step-by-step reasoning to answer the question. Based on context and reasoning steps,
answer the question ONLY in ’yes’ or ’no.’ Please use the below format:
Context: At a university, students who study hard earn high grades. Those who participate in
extracurriculars develop leadership skills. However, students have restricted time outside of
classes. They can either study hard or they do not develop leadership skills from extracurricu-
lars.
Question: Can we conclude that Priya, a university student with limited free time, either earns
high grades or does not participate in extracurricular activities?
Reasoning steps: [generate step-by-step reasoning]
Answer: Yes/No"

Table 6: Reported performance of SOTA LLMs on HumanEval and Big Bench Hard (BBH) benchmarks. The
values under the Computed column are averaged over 5 runs from our experiments. Other results are reported
from online sources. A – indicates that we were not able to find any online source. We used our local computed
results when they were available.

Model

HumanEval Score

Computed

(Online)

BBH Score

(Online)

ChatGPT
GPT-4o
GPT-4o-mini
Llama-3.2-1B-Instruct
Qwen-2.5-1.5B-Instruct
Phi-3.5-Mini-Instruct
Mistral-7B-Instruct-v0.2
Llama-3-8B-Instruct
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
Ministral-8B-Instruct-2410
Gemma-2-9B-IT
Phi-3-Medium-4k-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B-Instruct
Llama-3-70B-Instruct

74.3
91.8
88.3
34.6
56.7
71.3
44.5
62.8
62.2
63.4
76.8
68.3
75.0
80.5
72.6
79.9

68 (OpenAI, 2024)
90.2 (OpenAI, 2024)
87.2 (OpenAI, 2024)
–
61.6 (Qwen2, 2024)
64.6 (Liu et al., 2023b)
42.1 (Liu et al., 2023b)
61.6 (Liu et al., 2023b)
64.6 (Granite Team, 2024)
66.5 (Microsoft, 2024)
76.8 (MistralAI, 2024)
68.9 (Qwen2, 2024)
62.2 (Microsoft, 2024)
83.5 (Qwen2, 2024)
75.2 (Yi, 2024)
77.4 (Liu et al., 2023b)

48.1 (OpenAI, 2023)
48.1 (Dunham & Syahputra, 2024)
–
8.7 (Fourrier et al., 2024)
19.8 (Fourrier et al., 2024)
36.7 (Fourrier et al., 2024)
24.0 (Fourrier et al., 2024)
24.5 (Fourrier et al., 2024)
51.6 (Fourrier et al., 2024)
63.4 (Microsoft, 2024)
8.7 (Fourrier et al., 2024)
42.1 (Fourrier et al., 2024)
49.4 (Fourrier et al., 2024)
48.4 (Fourrier et al., 2024)
44.3 (Fourrier et al., 2024)
50.2 (Fourrier et al., 2024)

30

1566
1567

1568
1569
1570
1571
1572
1573

1574
1575
1576
1577
1578
1579

1580
1581
1582
1583
1584

1585
1586
1587
1588
1589
1590

1591
1592
1593
1594
1595
1596

1597
1598
1599
1600
1601
1602

1603
1604
1605
1606
1607

1608
1609
1610
1611
1612
1613

1614
1615
1616
1617
1618
1619

Under review as a conference paper at ICLR 2025

Figure 17: Correlation between scores on ∀uto∃∨∧L and both autoformalization A and informalization I
for FOLIO premises. Each point represents a specific number of operators with arrows showing increasing
complexity (number of operators). The trendline across all the points is annotated with ×, the Pearson correlation
coefficient (ρ), and the p-value are annotated in the top left.

K.4 COMPUTED

UTO

∀

∃∨∧

L CONDITIONAL PERFORMANCE

uto

To compare against the performance on different benchmarks in Section 5, we needed to calculate the
L for the relevant portions of the datasets. For
conditional performance of each LLM on
∃∨∧
example, there are few premises in the FOLIO dataset with more than 6 operators meaning that the
most accurate comparison would be to evaluate our first-order logic dataset up to the same number of
operators. Therefore, we calculated the accuracy of the first-order logic formulae with less than seven
operators when calculating the correlation and predictive power. On MultiLogiEval, the number of
operators is dictated by the depth of the rules, so we took the average of all first-order logic examples
up to 30 in our dataset. On HumanEval, to the best of our knowledge using the average of regex with
CFG tree depth up to 7 is the best comparison.

∀

K.5 FOLIO ADDITIONAL CORRELATION FIGURES

In Section 5, we evaluated the correlation of other benchmarks compared to
L. For the
FOLIO dataset, we were able to calculate the exact number of operators in each problem, allowing
us to plot points comparing the autoformalization and informalization accuracy for each operator
number class to directly compare to the accuracy of the same number of operators in the first-order
logic dataset we generated.

∃∨∧

uto

∀

We plot these results in Figure 17 with the Pearson correlation coefficient. Each figure shows a
moderate to strong correlation with a statistically significant p-value of less than 0.05. As the compu-
L, autoformalization, and informalization
uto
tational complexity increases, performance on
∀
decreases. The autoformalization correlation is significantly stronger due to the informalization
evaluation metrics being much weaker at evaluating truth maintenance.

∃∨∧

L LLM AS VERIFIERS EVALUATION

In this section, we analyze the performance of LLMs on §A4, where we evaluate the performance
of using a LLM to verify whether the formal syntax expression φ is equivalent to the one produced
(φ). Figure 20 shows the number of positive and negative examples.
by GPT-4o after doing
Additionally, it breaks down the performance of each LLM on each dataset.

A ◦ I

The LLMs are clearly biased towards giving positive answers with a high ratio of false positives
to negative labels compared to false negatives to positive labels. A common case was the LLM
not recognizing that GPT-4o renamed predicates or constants producing a different formal syntax
expression. A structure that ChatGPT tends to struggle with is double negations. Below we provide
two examples where, even at the time of writing this rebuttal, ChatGPT failed to correctly verify
whether the two formulae are equivalent. Note that [FORMULA 2] is ChatGPT’s own response after
conducting (

)n(φ0) where φ0 = [FORMULA 1].

A ◦ I

In the case of Output Example 1, it can be clearly seen that ChatGPT failed to understand that the two
formulae are different. In particular, it was not able to correctly evaluate or reason that the second
regular expression represents a string that begins with a 1 followed by zero or one 0’s. This is despite
the LLM using a “Chain-of-thought” to help it arrive at an answer.

31

1620
1621

1622
1623
1624
1625
1626
1627

1628
1629
1630
1631
1632
1633

1634
1635
1636
1637
1638

1639
1640
1641
1642
1643
1644

1645
1646
1647
1648
1649
1650

1651
1652
1653
1654
1655
1656

1657
1658
1659
1660
1661

1662
1663
1664
1665
1666
1667

1668
1669
1670
1671
1672
1673

0.25.5.7510.25.5.751BenchmarkScoreρ=0.79p=0.00FOLIO(A)0.25.5.751ρ=0.70p=0.00FOLIO(I;BLEU)0.25.5.751ρ=0.64p=0.00FOLIO(I;ROUGE)0.25.5.751ρ=0.67p=0.00FOLIO(I;METEOR)0.25.5.751ρ=0.61p=0.00FOLIO(I;BERT)∀uto∃∨∧LScoreChatGPTGPT-4LLama3MistralPhiGPT-4o-miniUnder review as a conference paper at ICLR 2025

Output Example 1: Regular Expression Verification Example

Prompt:
Your task is to say whether two Regular Expression formulae are equivalent. The first formula
will appear right after [FORMULA 1] and the second after [FORMULA 2].
Give an explanation followed by a yes or no answer. The answer must show up at the end
with the format "[Answer]" followed by either a yes or no.
[FORMULA 1]: 100*
[FORMULA 2]: 1(0*)

∗

) are equivalent, let’s analyze
and 1(0
∗

Response:
To determine whether the two regular expressions 100
them:
### Explanation:
1. Formula 1: 100*
- This matches the character "1" followed by zero or more "0"s.
- It will match: "1", "10", "100", "1000", etc.
2.Formula 2: 1(0*)
- This matches the character "1" followed by zero or more "0"s (the same as Formula 1).
- It will also match: "1", "10", "100", "1000", etc.
### Key Observation:
- Both formulas describe the same set of strings: a "1" followed by zero or more "0"s.
- The use of parentheses in Formula 2 is purely for grouping and does not alter the matching
behavior.
### Conclusion:
The two regular expressions are equivalent.
[Answer]: yes

Output Example 2: First-Order Logic Verification Example

Prompt:
Your task is to say whether two First Order Logic formulae are equivalent. The first formula
will appear right after [FORMULA 1] and the second after [FORMULA 2].
Give an explanation followed by a yes or no answer. The answer must show up at the end
with the format "[Answer]" followed by either a yes or no.
[FORMULA 1]:
[FORMULA 2]:

pred8(p8, p7)

pred8(p8, p7)

pred4(x1))

pred4(x1))

x1.(
x1.(

∨ ¬

∀
∀

¬¬
¬

∨ ¬

Response:
The two formulas are equivalent.
Explanation: In both Formula 1 and Formula 2, the part

pred8(p8, p7) is equivalent to
pred8(p8, p7) due to the double negation elimination rule in logic. Therefore, both formulas
¬
convey the same meaning, as the presence or absence of a double negation does not affect the
truth value in this context.
[Answer]: Yes

¬¬

A more glaring reasoning error is found in Output Example 2, where ChatGPT fails to apply the
p. Our results convincingly showcase that LLMs cannot be
principles of logic where
used as verifiers even for straightforward statements such as the examples presented.

̸≡ ¬

¬¬

≡

p

p

M DATASET DIVERSITY

Fig. 9 and Fig. 9 provide additional details on the types of data present in the datasets packaged with
L. Users can generate dynamic datasets along these dimensions using the hyperparameters

uto

∀
mentioned in Table 1.

∃∨∧

32

1674
1675

1676
1677
1678
1679
1680
1681

1682
1683
1684
1685
1686
1687

1688
1689
1690
1691
1692

1693
1694
1695
1696
1697
1698

1699
1700
1701
1702
1703
1704

1705
1706
1707
1708
1709
1710

1711
1712
1713
1714
1715

1716
1717
1718
1719
1720
1721

1722
1723
1724
1725
1726
1727

Under review as a conference paper at ICLR 2025

To further provide additional statistics pertaining to the similarity of formulae in our dataset, especially
those where the formulae are otherwise equivalent but just use different vocabularies. For example,
the formula f = p1 can be represented via different propositions where p1 = It is raining in f1 and
something different in another formula f2 even though they canonically represent the same formula
f .

This allows to test robustness in LLM outputs. Nevertheless, the probability of such instances
decreases as the formula size increases. We have counted the total proporition of the dataset where
this occurs by replacing any variable from the vocabulary with an element of a vocabulary of size 1.
For example, all variables used in PL(12) dataset of our results are replaced by substituting those
variables with a vocabulary of only 1 proposition. Excess parentheses etc are preprocessed using
NLTK and removed before the substitution (e.g. ((p1)

p2) is simplified to p1

p2.

∧

∧

The k-SAT dataset contains 8550 unique samples and the propositional logic dataset contains 17.7k
samples constituting 85% and 90% of these datasets respectively.

N EVALUATION OF LLMS

Table 7 lists the models, their parameters (– if closed-source), and the exact model version used for
our experiments. The open-source models were loaded using NVIDIA A100 80GB GPUs whereas
we used the OpenAI API for the GPT family of models. We cover a diverse range of models in our
evaluation ranging from extremely small LMs with a few billion parameters (
1B) to LLMs with
L from the lens of generalization.
several billions of parameters. This allows the analysis of

uto

∼

∀

∃∨∧

Fig. 18 represents the syntactic compliance (
axis for each LLM. Similarly, Fig. 19 plots the Accuracy (
was used to plot the results in Fig. 3 and to compute the predictive power in Fig. 4.

A2) data from Fig. 5 for all the models with a separate
A3). Tables 9 – 14 provide the data that

§

§

Tables 15 – 18 list the example counts for each combination of class label and prediction for FOLIO(R;
NL) and FOLIO(R; FOL) and each label’s precision and recall rate. Tables 19 and 20 list the examples
counts for each combination of class label and prediction for LogiEval(R; PL) and LogieEval(R;
FOL).

N.1 CLAUDE EVALUATION

We evaluated Claude 3.0 Sonnet on just the 3-SAT, propositional logic, and regular expression
datasets due to the cost. Our results are shown in Figure 21 and show that Claude 3.0 Sonnet performs
similarly to GPT-4o with both having nearly perfect syntactic compliance and accuracy on 3-SAT.
Sonnet achieved the highest syntactic compliance and accuracy on propositional logic compared to
the other models. However the accuracy was only around 50% for expressions with more than 20
operators. Additionally, while being often syntactic compliant, Sonnet performed with low accuracy
on the regular expression dataset.

33

1728
1729

1730
1731
1732
1733
1734
1735

1736
1737
1738
1739
1740
1741

1742
1743
1744
1745
1746

1747
1748
1749
1750
1751
1752

1753
1754
1755
1756
1757
1758

1759
1760
1761
1762
1763
1764

1765
1766
1767
1768
1769

1770
1771
1772
1773
1774
1775

1776
1777
1778
1779
1780
1781

Under review as a conference paper at ICLR 2025

Table 7: The LLMs used in our evaluation. The label names represent the labels used in Fig. 18 and Fig. 19, |θ|
represents the total number of parameters, and the last column lists the exact version used (for reproducibility).

Label

|θ|

Version

ChatGPT
GPT-4o
GPT-4o-mini
GPT-4o1
Llama-3.2-1B-Instruct
Qwen-2.5-1.5B-Instruct
Phi-3.5-Mini-Instruct
Mistral-7B-Instruct-v0.2
Llama-3-8B-Instruct
Granite-3.0-8B-Instruct
LLama-3.1-8B-Instruct
Ministral-8B-Instruct-2410
Gemma-2-9B-IT
Phi-3-Medium-4k-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B-Instruct
Llama-3-70B-Instruct

GPT-3.5-turbo-0125
gpt-4o-2024-08-06
gpt-4o-mini-2024-07-18
o1-preview-2024-09-12
meta-llama/Llama-3.2-1B-Instruct

–
–
–
–
1B
1.5B Qwen/Qwen2.5-1.5B-Instruct
4B
7B
8B
8B
8B
8B
9B
14B
14B
34B
70B

microsoft/Phi-3.5-mini-instruct
mistralai/Mistral-7B-Instruct-v0.2
meta-llama/Llama-3-8B-Instruct
ibm-granite/granite-3.0-8b-instruct
meta-llama/Llama-3.1-8B-Instruct
mistralai/Ministral-8B-Instruct-2410
google/gemma-2-9b-it
microsoft/Phi-3-medium-4k-instruct
Qwen/Qwen2.5-14B-Instruct
01-ai/Yi-34B-Instruct
meta-llama/Llama-3-70B-Instruct

Table 8: Correlation data for FOLIO(R; NL). The ∀uto∃∨∧L data was averaged from the PL dataset with data
points with description complexity d ≤ 6. These values were used to compute the predictive power of ∀uto∃∨∧L
reported in Fig. 4.

Model

∀uto∃∨∧L Score

FOLIO(R; NL) Score

0.75
0.69
0.56
0.54
0.67
0.58
0.64
0.60
0.59
0.36
0.70
0.61
0.61
0.49
0.73
0.63

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.79
0.56
0.36
0.06
0.35
0.13
0.28
0.18
0.09
0.03
0.49
0.10
0.19
0.07
0.67
0.21

34

1782
1783

1784
1785
1786
1787
1788
1789

1790
1791
1792
1793
1794
1795

1796
1797
1798
1799
1800

1801
1802
1803
1804
1805
1806

1807
1808
1809
1810
1811
1812

1813
1814
1815
1816
1817
1818

1819
1820
1821
1822
1823

1824
1825
1826
1827
1828
1829

1830
1831
1832
1833
1834
1835

Under review as a conference paper at ICLR 2025

1836
1837

1838
1839
1840
1841
1842
1843

1844
1845
1846
1847
1848
1849

1850
1851
1852
1853
1854

1855
1856
1857
1858
1859
1860

1861
1862
1863
1864
1865
1866

1867
1868
1869
1870
1871
1872

1873
1874
1875
1876
1877

1878
1879
1880
1881
1882
1883

1884
1885
1886
1887
1888
1889

Figure 18: Syntactic compliance (
§

A2) of all models on the

35

uto

∀

∃∨∧

L datasets.

01PropositionalLogic(12)GPT-4o01GPT-4o-mini01ChatGPT01Mistral-7B-Instruct-v0.201Phi-3-Medium-4k-Instruct01LLama-3-8B-Instruct01Gemma-2-9B-IT01Granite-3.0-8B-Instruct01Llama-3.1-8B-Instruct01LLama-3.2-1B-Instruct01LLama-3-70B-Instruct01Ministral-8B-Instruct-241001Phi-3.5-Mini-Instruct01Qwen-2.5-1.5B-Instruct01Qwen-2.5-14B-Instruct0204001Yi-1.5-34BFOL(8,12)−S02040FOL(8,12)−E02040RegularExpression(2)02040#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepth§A2:SyntacticComplianceGPT-4oGPT-4o-miniChatGPTMistral-7B-Instruct-v0.2Phi-3-Medium-4k-InstructLLama-3-8B-InstructGemma-2-9B-ITGranite-3.0-8B-InstructLlama-3.1-8B-InstructLLama-3.2-1B-InstructLLama-3-70B-InstructMinistral-8B-Instruct-2410Phi-3.5-Mini-InstructQwen-2.5-1.5B-InstructQwen-2.5-14B-InstructYi-1.5-34BUnder review as a conference paper at ICLR 2025

Figure 19: Accuracy (
§

A3) of all models on the

36

1890
1891

1892
1893
1894
1895
1896
1897

1898
1899
1900
1901
1902
1903

1904
1905
1906
1907
1908

1909
1910
1911
1912
1913
1914

1915
1916
1917
1918
1919
1920

1921
1922
1923
1924
1925
1926

1927
1928
1929
1930
1931

1932
1933
1934
1935
1936
1937

1938
1939
1940
1941
1942
1943

uto

∀

∃∨∧

L datasets.

01PropositionalLogic(12)GPT-4o01GPT-4o-mini01ChatGPT01Mistral-7B-Instruct-v0.201Phi-3-Medium-4k-Instruct01LLama-3-8B-Instruct01Gemma-2-9B-IT01Granite-3.0-8B-Instruct01Llama-3.1-8B-Instruct01LLama-3.2-1B-Instruct01LLama-3-70B-Instruct01Ministral-8B-Instruct-241001Phi-3.5-Mini-Instruct01Qwen-2.5-1.5B-Instruct01Qwen-2.5-14B-Instruct0204001Yi-1.5-34BFOL(8,12)−S02040FOL(8,12)−E02040RegularExpression(2)02040#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepth§A3:AccuracyGPT-4oGPT-4o-miniChatGPTMistral-7B-Instruct-v0.2Phi-3-Medium-4k-InstructLLama-3-8B-InstructGemma-2-9B-ITGranite-3.0-8B-InstructLlama-3.1-8B-InstructLLama-3.2-1B-InstructLLama-3-70B-InstructMinistral-8B-Instruct-2410Phi-3.5-Mini-InstructQwen-2.5-1.5B-InstructQwen-2.5-14B-InstructYi-1.5-34BUnder review as a conference paper at ICLR 2025

1944
1945

1946
1947
1948
1949
1950
1951

1952
1953
1954
1955
1956
1957

1958
1959
1960
1961
1962

1963
1964
1965
1966
1967
1968

1969
1970
1971
1972
1973
1974

1975
1976
1977
1978
1979
1980

1981
1982
1983
1984
1985

1986
1987
1988
1989
1990
1991

1992
1993
1994
1995
1996
1997

∀

uto

(φ0) when evaluating
Figure 20: The number of positive and negative examples of φ1
GPT-4o on
L for each dataset (inner donuts). Additionally included is a breakdown of the
performance of each LLM when acting as the verifier (outer donuts). Included are all examples
containing 20 or fewer operators or, in the case of the regular expression dataset, CFG tree depth of 20
or fewer. Incompliant represents syntactically incompliant φ1 generated by GPT-4o for ground-truth
φ0 via (

≡ A ◦ I

)n(φ0)

∃∨∧

A ◦ I

Figure 21:
expression datasets. Dashed line is the accuracy.

∃∨∧

uto

∀

L results on Claude 3.0 Sonnet on the 3-SAT, propositional logic, and regular

37

ChatGPTksatplogicfolfol_humanregexGPT-4oPhiMistralLlama3Positive LabelsNegative LabelsTrue PositiveFalse NegativeIncompliant (Positive Label)True NegativeFalse PositiveIncompliant (Negative Label)0102030400.25.5.751§A1:SyntacticCompliance3–SAT(12)010203040PL(12)010203040RegularExpression(2)0.25.5.751§A2:Accuracy#ofOperators:∧,∨,¬(¬iscountedasanoperatoriﬀnotsucceededbyaterminal)CFGParseTreeDepthUnder review as a conference paper at ICLR 2025

Table 9: Correlation data for FOLIO(R; FOL). The ∀uto∃∨∧L data was averaged from the FOL dataset with
data points with description complexity d ≤ 6. These values were used to compute the predictive power of
∀uto∃∨∧L reported in Fig. 4.

Model

∀uto∃∨∧L Score

FOLIO(R; FOL) Score

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.79
0.56
0.36
0.06
0.35
0.13
0.28
0.18
0.09
0.03
0.49
0.10
0.19
0.07
0.67
0.21

0.71
0.67
0.51
0.51
0.62
0.52
0.59
0.56
0.56
0.36
0.66
0.56
0.53
0.45
0.71
0.61

Table 10: Correlation data for LogiEval(R; PL). The ∀uto∃∨∧L data was averaged from the PL dataset with
data points with description complexity d ≤ 30. These values were used to compute the predictive power of
∀uto∃∨∧L reported in Fig. 4.

Model

∀uto∃∨∧L Score

LogiEval(R; PL) Score

0.87
0.67
0.64
0.60
0.75
0.61
0.71
0.58
0.71
0.50
0.85
0.68
0.62
0.52
0.76
0.78

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.67
0.35
0.17
0.12
0.23
0.12
0.28
0.21
0.11
0.04
0.34
0.17
0.10
0.11
0.46
0.26

38

1998
1999

2000
2001
2002
2003
2004
2005

2006
2007
2008
2009
2010
2011

2012
2013
2014
2015
2016

2017
2018
2019
2020
2021
2022

2023
2024
2025
2026
2027
2028

2029
2030
2031
2032
2033
2034

2035
2036
2037
2038
2039

2040
2041
2042
2043
2044
2045

2046
2047
2048
2049
2050
2051

Under review as a conference paper at ICLR 2025

Table 11: Correlation data for LogiEval(R; FOL). The ∀uto∃∨∧L data was averaged from the FOL dataset with
data points with description complexity d ≤ 30. These values were used to compute the predictive power of
∀uto∃∨∧L reported in Fig. 4.

Model

∀uto∃∨∧L Score

LogiEval(R; FOL) Score

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.32
0.17
0.09
0.01
0.09
0.02
0.07
0.05
0.02
0.00
0.15
0.02
0.04
0.02
0.19
0.05

0.82
0.56
0.63
0.56
0.70
0.62
0.69
0.55
0.68
0.47
0.78
0.64
0.54
0.50
0.66
0.71

Table 12: Correlation data for FOLIO(A). The ∀uto∃∨∧L data was averaged from the FOL dataset with data
points with description complexity d ≤ 6. These values were used to compute the predictive power of ∀uto∃∨∧L
reported in Fig. 4.

Model

∀uto∃∨∧L Score

FOLIO(A) Score

0.48
0.47
0.38
0.23
0.37
0.18
0.35
0.16
0.26
0.00
0.47
0.26
0.21
0.12
0.42
0.37

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.82
0.58
0.40
0.07
0.38
0.15
0.32
0.21
0.10
0.03
0.53
0.11
0.22
0.08
0.71
0.24

39

2052
2053

2054
2055
2056
2057
2058
2059

2060
2061
2062
2063
2064
2065

2066
2067
2068
2069
2070

2071
2072
2073
2074
2075
2076

2077
2078
2079
2080
2081
2082

2083
2084
2085
2086
2087
2088

2089
2090
2091
2092
2093

2094
2095
2096
2097
2098
2099

2100
2101
2102
2103
2104
2105

Under review as a conference paper at ICLR 2025

Table 13: Correlation data for FOLIO(I). The ∀uto∃∨∧L data was averaged from the FOL dataset with data
points with description complexity d ≤ 6. These values were used to compute the predictive power of ∀uto∃∨∧L
reported in Fig. 4.

Model

∀uto∃∨∧L Score BLEU ROUGE METEOR BERT

FOLIO(I) Score

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-Medium-4k-Instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.71
0.49
0.27
0.04
0.26
0.08
0.21
0.12
0.06
0.02
0.39
0.07
0.12
0.05
0.57
0.14

0.14
0.13
0.19
0.08
0.12
0.04
0.10
0.15
0.09
0.00
0.12
0.11
0.05
0.09
0.07
0.12

0.42
0.41
0.47
0.31
0.39
0.18
0.34
0.41
0.31
0.06
0.40
0.36
0.22
0.33
0.26
0.39

0.64
0.61
0.62
0.51
0.58
0.35
0.53
0.58
0.51
0.15
0.60
0.55
0.41
0.49
0.45
0.58

0.71
0.73
0.76
0.64
0.70
0.50
0.63
0.72
0.64
0.36
0.70
0.67
0.55
0.65
0.55
0.72

Table 14: Correlation data for HumanEval (A). The ∀uto∃∨∧L data was averaged from the regex dataset with
data points with description complexity d ≤ 7. These values were used to compute the predictive power of
∀uto∃∨∧L reported in Fig. 4.

Model

∀uto∃∨∧L Score HumanEval (A) Score

0.92
0.88
0.74
0.45
0.75
0.63
0.68
0.62
0.63
0.35
0.80
0.77
0.71
0.57
0.81
0.73

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.66
0.44
0.36
0.20
0.45
0.07
0.28
0.21
0.19
0.03
0.33
0.13
0.36
0.12
0.45
0.13

40

2106
2107

2108
2109
2110
2111
2112
2113

2114
2115
2116
2117
2118
2119

2120
2121
2122
2123
2124

2125
2126
2127
2128
2129
2130

2131
2132
2133
2134
2135
2136

2137
2138
2139
2140
2141
2142

2143
2144
2145
2146
2147

2148
2149
2150
2151
2152
2153

2154
2155
2156
2157
2158
2159

Under review as a conference paper at ICLR 2025

Table 15: Count of examples in FOLIO(R; NL) for each combination of (T)rue, (F)alse, and (U)ncertain label
and predictions in that order. For example, TU is the number of times a LLM predicted a True label as Uncertain.

Model

TT

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct

1667
1500
1501
1301
1468
1400
1439
1415
1400
1407
1677
1577
1355
1470
1564
Yi-1.5-34B 1507

TF

125
187
281
205
153
244
94
109
174
235
101
242
164
345
132
125

TU

147
253
147
412
310
288
385
412
314
118
161
116
398
117
239
298

FT

178
162
366
200
222
272
231
304
267
931
263
358
223
615
215
240

FF

1133
1087
889
717
871
807
813
666
766
279
966
954
821
684
1020
894

FU

131
196
186
508
343
347
382
471
360
81
214
130
383
138
207
305

UT

246
255
620
525
310
477
378
382
435
1109
419
583
357
824
266
497

UF

419
488
562
387
289
413
289
316
352
235
319
532
359
477
276
346

UU

952
877
434
691
1009
717
934
919
781
111
881
503
890
309
1058
773

Table 16: Calculated precision and recall for each label in FOLIO (R;NL).

True Label

False Label

Uncertain Label

Model

Prec. Rec.

Prec. Rec.

Prec.

Rec.

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.80
0.78
0.60
0.64
0.73
0.65
0.70
0.67
0.67
0.41
0.71
0.63
0.70
0.51
0.76
0.67

0.68
0.62
0.51
0.55
0.66
0.55
0.68
0.61
0.59
0.37
0.70
0.55
0.61
0.45
0.71
0.65

0.79
0.75
0.62
0.50
0.61
0.57
0.57
0.46
0.55
0.22
0.67
0.66
0.58
0.48
0.71
0.62

0.77
0.66
0.57
0.43
0.61
0.53
0.55
0.51
0.54
0.36
0.70
0.67
0.53
0.55
0.70
0.56

0.59
0.54
0.27
0.43
0.63
0.45
0.58
0.57
0.50
0.08
0.54
0.31
0.55
0.19
0.66
0.48

0.86
0.77
0.78
0.68
0.76
0.72
0.75
0.73
0.74
0.80
0.86
0.81
0.71
0.76
0.81
0.78

41

2160
2161

2162
2163
2164
2165
2166
2167

2168
2169
2170
2171
2172
2173

2174
2175
2176
2177
2178

2179
2180
2181
2182
2183
2184

2185
2186
2187
2188
2189
2190

2191
2192
2193
2194
2195
2196

2197
2198
2199
2200
2201

2202
2203
2204
2205
2206
2207

2208
2209
2210
2211
2212
2213

Under review as a conference paper at ICLR 2025

Table 17: Count of examples in FOLIO(R; FOL) for each combination of (T)rue, (F)alse, and (U)ncertain label
and predictions in that order. For example, TU is the number of times a LLM predicted a True label as Uncertain.

Model

TT

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct

1596
1432
1500
1159
1405
1471
1378
1428
1449
1436
1661
1525
1291
1305
1648
Yi-1.5-34B 1513

TF

124
140
208
244
120
193
112
181
163
232
122
226
145
358
90
106

TU

218
367
227
521
393
249
408
317
305
127
149
180
449
255
194
271

FT

215
153
456
229
278
462
256
373
358
969
390
452
314
611
279
285

FF

1004
944
711
616
688
621
659
596
647
239
829
805
595
560
918
730

FU

224
348
266
575
457
332
489
458
409
96
224
185
503
256
241
350

UT

329
224
756
503
365
674
397
530
575
1142
576
692
466
829
377
476

UF

359
420
525
335
226
396
268
325
289
237
248
464
331
392
253
282

UU

932
976
338
760
1014
532
919
755
725
117
791
461
791
386
966
826

Table 18: Calculated precision and recall for each label in FOLIO(R; FOL).
Uncertain Label

False Label

True Label

Model

Prec. Rec.

Prec. Rec.

Prec.

Rec.

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct
Yi-1.5-34B

0.75
0.79
0.55
0.61
0.69
0.56
0.68
0.61
0.61
0.40
0.63
0.57
0.62
0.48
0.72
0.67

0.68
0.63
0.49
0.52
0.67
0.51
0.63
0.54
0.59
0.34
0.69
0.54
0.56
0.43
0.73
0.65

0.70
0.65
0.50
0.43
0.48
0.44
0.47
0.42
0.46
0.18
0.57
0.56
0.42
0.39
0.64
0.53

0.68
0.58
0.41
0.41
0.54
0.48
0.51
0.49
0.50
0.34
0.68
0.56
0.45
0.43
0.69
0.57

0.58
0.60
0.21
0.48
0.63
0.33
0.58
0.47
0.46
0.08
0.49
0.29
0.50
0.24
0.61
0.52

0.82
0.74
0.78
0.60
0.73
0.77
0.73
0.74
0.76
0.80
0.86
0.79
0.68
0.68
0.85
0.80

42

2214
2215

2216
2217
2218
2219
2220
2221

2222
2223
2224
2225
2226
2227

2228
2229
2230
2231
2232

2233
2234
2235
2236
2237
2238

2239
2240
2241
2242
2243
2244

2245
2246
2247
2248
2249
2250

2251
2252
2253
2254
2255

2256
2257
2258
2259
2260
2261

2262
2263
2264
2265
2266
2267

Under review as a conference paper at ICLR 2025

Table 19: Number of examples of true positives (TP), false positives (FP), true negatives (TN), and false
negatives (FN) for each LLM in LogiEval(R; PL). The counts for when the LLM was incompliant with our
prompt for positive (IP) and negative (IN) labels are also provided. Additionally, the calculated true positive rate
(TPR), true negative rate (TNR), precision, and F1 score for each LLM is shown.

Model

TP

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct

1724
1310
1348
1240
1558
1246
1464
1106
1523
985
1741
1350
1222
1085
1474
Yi-1.5-34B 1651

FP

56
116
260
187
197
209
217
168
242
250
142
161
180
281
72
193

TN

594
534
390
379
452
434
432
482
400
342
507
489
459
298
574
457

FN

251
665
625
640
411
715
497
869
430
820
223
621
719
582
486
321

IP

IN TPR TNR Prec.

F1

0
0
2
95
6
14
14
0
22
170
11
4
34
308
15
3

0
0
0
84
1
7
1
0
8
58
1
0
11
71
4
0

0.87
0.66
0.68
0.66
0.79
0.64
0.75
0.56
0.78
0.55
0.89
0.68
0.63
0.65
0.75
0.84

0.91
0.82
0.60
0.67
0.70
0.67
0.67
0.74
0.62
0.58
0.78
0.75
0.72
0.51
0.89
0.70

0.97
0.92
0.84
0.87
0.89
0.86
0.87
0.87
0.86
0.80
0.92
0.89
0.87
0.79
0.95
0.90

0.92
0.77
0.75
0.75
0.84
0.73
0.80
0.68
0.82
0.65
0.91
0.78
0.73
0.72
0.84
0.87

Table 20: Number of examples of true positives (TP), false positives (FP), true negatives (TN), and false
negatives (FN) for each LLM in LogiEval(R; FOL). The counts for when the LLM was incompliant with our
prompt for positive (IP) and negative (IN) labels are also provided. Additionally, the calculated true positive rate
(TPR), true negative rate (TNR), precision, and F1 score for each LLM is shown.

Model

TP

GPT-4o
GPT-4o-mini
ChatGPT
Mistral-7B-Instruct-v0.2
Phi-3-medium-4k-instruct
LLama-3-8B-Instruct
Gemma-2-9B-IT
Granite-3.0-8B-Instruct
Llama-3.1-8B-Instruct
LLama-3.2-1B-Instruct
LLama-3-70B-Instruct
Ministral-8B-Instruct-2410
Phi-3.5-Mini-Instruct
Qwen-2.5-1.5B-Instruct
Qwen-2.5-14B-Instruct

1627
1084
1346
1172
1449
1267
1355
1023
1466
968
1630
1304
1059
1013
1303
Yi-1.5-34B 1489

FP

57
95
177
159
139
139
118
102
198
255
116
161
140
220
89
156

TN

593
555
472
403
511
502
532
548
440
335
533
486
493
374
555
494

FN

IP

IN TPR TNR Prec.

F1

398
941
678
716
574
752
665
1002
538
853
392
708
922
775
707
534

0
0
1
137
2
6
5
0
21
204
3
13
44
237
15
2

0
0
1
88
0
9
0
0
12
60
1
3
17
56
6
0

0.80
0.54
0.67
0.62
0.72
0.63
0.67
0.51
0.73
0.53
0.81
0.65
0.53
0.57
0.65
0.74

0.91
0.85
0.73
0.72
0.79
0.78
0.82
0.84
0.69
0.57
0.82
0.75
0.78
0.63
0.86
0.76

0.97
0.92
0.88
0.88
0.91
0.90
0.92
0.91
0.88
0.79
0.93
0.89
0.88
0.82
0.94
0.91

0.88
0.68
0.76
0.73
0.80
0.74
0.78
0.65
0.80
0.64
0.87
0.75
0.67
0.67
0.77
0.81

43

2268
2269

2270
2271
2272
2273
2274
2275

2276
2277
2278
2279
2280
2281

2282
2283
2284
2285
2286

2287
2288
2289
2290
2291
2292

2293
2294
2295
2296
2297
2298

2299
2300
2301
2302
2303
2304

2305
2306
2307
2308
2309

2310
2311
2312
2313
2314
2315

2316
2317
2318
2319
2320
2321

