Autonomous Evaluation of LLMs for Truth Maintenance and Reasoning Tasks
Authors: Rushang Karia
Daniel Richard Bramblett
Daksh Dobhal
Siddharth Srivastava
Venue: ICLR 2025 Poster (2025)
Keywords: Large Language Models
Logical Reasoning
Autoformalization
Informalization
Formal Translation
Truth Maintenance
Primary area: datasets and benchmarks
TL;DR: An automatic and scalable benchmark for evaluating LLMs for truth maintenance w.r.t. formal syntax.

Abstract: This paper presents AutoEval, 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. AutoEval 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 analysis shows that an LLM's performance on AutoEval is highly indicative of its 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.

Published as a conference paper at ICLR 2025
AUTONOMOUS EVALUATION OF LLMs FOR TRUTH MAINTENANCE AND REASONING TASKS
Rushang Karia', Daniel Bramblett, Daksh Dobhal, Siddharth Srivastava School Computing and Augmented Intelligence Arizona State University (rushang. karia, drbrambl, ddobhal, s siddharths) @asu. edu
ABSTRACT
This paper presents AutoEval, 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. AutoEval 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 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 analysis shows that an LLM's performance on AutoEval is highly indicative of its 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.
INTRODUCTION
Large Language Models (LLMs) have been demonstrated perform well in many natural language tasks involving formal languages such autoformalization converting natural language (NL)
to formal language (FL) such as source code, math etc., (Wu et al. 2022, Liang et al. 2023). informalization converting FL NL (e.g. code summarization), and reasoning using LLMs to perform sound reasoning or derive proofs. Although these methods have been successful in small-scale scenarios, LLM's effectiveness in maintaining factual accuracy or preserving which facts are true across translation remains unclear due to the difficulty in designing benchmarks that capture 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 their use of static datasets, e.g., HumanEval (Chen et al., 202T; Wu et 2022 Han al.) 2024), and/or metrics that are insufficienn/ncoopleet syntactic measures of evaluation (e.g. BLEU scores (Callison- Burch et al., (006). a result, existing methods provide misleading signals on the capabilities of LLM technology. One effective method to mitigate this problem in existing benchmarks creating new data (Xu et al. 20224)). This a tedious and expensive process since data generation requires expert annotators to hand-generate well-balanced datasets. While using LLMs as judges and/or metrics is promising research direction (Zheng et al., 2023; Shankar et al. 2024 Xu et al. 2024b Madaan et al. 2023), it is unknown whether LLMs can be used accurate verifers.
This paper addresses three key desiderata for benchmarking LLM capabilities in truth maintenance across NL and FL: (DI) Can dynamically generate diitt---istiitttion datasets without human annotators? (D2) How do we accurately assess an LLM's 's truth maintenance capabilities? (D3) Can we develop a benchmark predictive of LLM performance on formal translation and reasoning tasks?
Main contributions Our key contributions are as follows:
1. A new approach for automatic synthesis of grammars that are unlikely to be memorized during the LLM's training process ($D1).
test datasets using context-free
'These authors contributed equally.

---

Published as a conference paper at ICLR 2025
2. The utilization of formal verifiers such 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 ($D2).
3. Vuto3VAL: 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 performance other metrics across wide variety of tasks, such as first-order logic reasoning ($D3). Thus, our metric offers a scalable and efficient surrogate for evaluating new LLMs in tasks where other metries may be limited due the unavailability of new datasets, We also show that SOTA LLMs are unable to maintain truth effectively.
2 FORMAL FRAMEWORK
Large Language Models (LLMs) are non-linear functions represented by (billons of) parameters that, given set of input tokens ,',...,,In. typically from natural language NL, predict the output token 1 using the distribution ([ Fn, y1,... :,;0)) 0). The input tokens contain context (also known ctc). It is known that x significantly impacts the response quality yı..... Yn (Sahoo et al., 2024).
prompt) that provides the necessary information for the task (e.g., instructions, :
Propositional Logic is a branch of logic that utilizes propositions and logical operators (e.g.. con- junction: A, 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 V P2. If P is true and -pl is observed, then one can use the rules of inference to deduce that P2 true (Huth & Ryan 2004). Two sentences in propositional logic, P1 and P2, equivalent, P1 = P2. iff their truth values agree for all possible assignments. E.g., -(P A p2) = -pi V -p2 since VpI.P2 E {True, False) (True, False], -(p A p2) = P1 V pp2
First-order Logic (FOL) differs from propositional logic in that sentences are constructed using predicates, quantifiers, constants, symbols, and variables. A popular example is the syllogism, where, given two FOL. sentences Vx. Man(z) + Mortal (x)) and Man(Socrates), one can conclude that Morral(Socrates.. A FOL sentence F can be interpreted using a universe U, a substitution operator o, and an interpretation function I (Russell & Norvig 2020). Two FOL sentences, F1, F2, are equivalent, F. = F2, iff they are equivalent under all possible models. E.g., VV.. Man(x) = 3y. -Man(y).
A regular expression (regex) is a sequence of characters used to determine whether a particular string matches the pattern or language induced by the regex. For example, the regex 200) using Σ = {0, 1, matches all strings possible using Σ that begin with a two, followed by one more pairs of zeroes, and end with a one (Hopcroft et al.) 200T). Two regexes, R₁ and R2 are equivalent, R₁ R2, if they represent the same language. It is known that R1 R2 if their corresponding minimal deterministic finite automata, D1, D2, are isomorphic, i.e., D1 ~ D2 (Hopcroft et al.) 2001).
We refer to sentences (strings) in first-order and propositional logic (regexes) as formal language FL in this paper. We now provide a definition of (Auto/In) futoo///formaaiatiion in the context of LLMs.
Definition 2.1 (Autoformalization: A). Given an LLM L, a NL. N, FL F, string &b E NL, and context R', autoformalization A, is defiedd as using L to translate & to y = Ar (1), K') s.t. & E FL.
Definition 2.2 (Informalization: Z). Given an LLM L. a NL N. a FL F, a string E FL, and context K, informalization I, is defined as using L to translate yp to va Ir(s, H) s.t. vb NL.
Example One possible autoformalization of "Every human drinks coffee but some are not dependent on it" in FOL is [vz. Human(z) = Drinks(æ,, Coffee)] ^ By. Human(y) A -Dependentlly Coffee)). Ideally, informalization will be an inverse of autoformalizztion. Therefore, the FOL formula (vz. Human(x) = Drinks(æ, Coffee)) [3y. Human(y) ^ -Dependent(ig Coffee)] can be in- formalized to the sentence "Every human drinks coffee but some are not dependent on it".
We assume that the context k'' provided contains the prompt and any necessary vocabulary that is needed for the task (c.g., Human (z) represents that x is a human, etc.). We omit Ki, k', and L in the notation for A and I where they are clear from the context.
2

---

Published as a conference paper at ICLR 2025
Informalization and autoformalization non-etteriinistic functions. Therefore, it is possible that a different LLM (or the same LLM with a different seed) autoformalizes the same input text to a syntactically even semantically different output. E.g., the example above could be autoformalized to the semantically equivalent form: Vor. Human xt) = Drinks(I, Coffee) A AVy. Human(y) = Dependent(y: Coffee). Similarly, an L.LM can informalize differently. The example above could be informalized by the same LLM to "All humans drink coffee but some are not dependent on it". Thus, the informalization (autoformalization) of autoformalization (informalization) of string is possibly different from that string: As (Iz (p: re), f6) * up and (Az (v. x), # th. Given N+, let (A o I) (4o) refer to the sequence you + to + ... + Pn that obtained using an LLM L when starting with FL yo. where vh I(p):) and gi+t1 = A(tb).
While syntactic differences across (AoI) ((0)) operations may be acceptable, the ability of LLM to maintain semantic content across (Ao (po) for Fl. such as first-order logic, regular expressions, etc., is foundational and underlies many aspects of the capabilities of L.MSs surrounding reasoning. semantically accurate translation, etc. For programming, it has been shown that autoformalization accuracy indicative of the reasoning abilities of LLMs since they frame reasoning as generation of FL (Chen 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 LLM's ability preserve factual information or semantic truth across translations is indicative of its performance on related tasks.
Intuitively, truth maintenance captures LLM's ability preserve truth across translation; opera- tionally, it evaluates the ability of a system to be able to accurately invert its own translations. We say that LLM maintains truth in translation iff (AA ()"((p))))))))))()())) always leads to a fP, that semantically equivalent to Pou Recall that = denotes the semantic equivalence operator in FL. Formally,
Definition 2.3 (LLM Truth Maintenance). An LLM L maintains truth in translation iff Vipo, and for all sequences (A o (PP) obtained using L, Sr. = PPo.
In practice, we estimate the ability for truth maintenance through sampling-basse -based process. Naturally, LLMs may not autoformalize, reason, etc.. correctly due to issues like hallucination (Ji et al. 2023). etc. For the earlier example, the LLM could autoformalize by omitting the H umnnny (y) statement to -Dependent (y. Coffee)]. This seems innocuous
yield Vvr Human(r) + Drinks(æ: (z, Coffee)]\[S3 but changes the meaning since y no longer required to be human, and thus it interprets as "All humans drink coffee, but some element of the universe is not dependent on coffee." Such issues have profound implications synthesizing specifications and/or programs. Thus, an LLM must able to understand its own generated output across NL and FL, and it is imperative to create benchmark that can faithfully assess the truth maintenance of LLMs.
3 THE VUTOOVAL APPROACH FOR ASSESSING TRUTH MAINTENANCE
We now describe our approach, Vuto]VAL, for autonomously assessing an LLM's ability for truth maintenance. VutoEVAL provides dynamically generated datasets that can be scaled arbitrarily by systematically generating cattof-diitributton. well-balanced ground-truth data ($D1 Sec. [.. provides $D2 by using intrinsic LLM capabilities to automatically assess (A o (P))))) without requiring any labeled annotations and using formal verifiers rigorously check and guarantee the correctness of (A I)" (5Fo) without having to engage in an exhaustive search process.
3.1 AUTOMATIC EVALUATION OF TRUTH MAINTENANCE
We develop novel technique that can soundly assess truth maintenance without any human an- notations by evaluating ii + 1/2 > Pi++1 Our approach is based on the following intuition. Let I o0 - z be non-deterministic function that maps FL y to NL tb. Similarly, let A v + s be a non-determiiiitic function that maps NL 1b to FL sp In general, there are many possible correct informalizations (autoformalizations) of & E FL (w) E NL). Because I and A are non-deterministic functions, their inverses are thus not well-defined.
Our key observation is that if I and A come from the same system (e.g., an LLM), then we can evaluate that system's truth maintenance by composing I and A. Let y be any FL expression and let I. be an L.M. If T. preserves truth, then I[(p) will be accurate NI. representation of so and
3

---

Published as a conference paper at ICLR 2025
Formal Syntax
Vocabulary Uasabase
Clear D' Compxt
Generator
LLM L
L
Inpul Grammar:
Automatic
FL + Vocab
NL gha
Vocabulary
I(Poo
A(Pe)
FL 1p
Query 49) ?)
FL '00
Generation
Vocab
Ground-trufh Data and Context Generation
Informalization::
Autofommaizationnc A
Verification
Case 1 (Vocabulary is abstract)
Clear Lox Donaee
A conjunction of the propesitions p2, p1:
Po
LLM L
I(ps)
Vo
also expressed p and
A(va)
Ap:
Prover9
p2 by idempotence
Case 2 (Vocabulary is real-worid)
Ohesr Eo Conteet
P3 AP
I(ps)
The sun bright the day before whist it raining heavily today
491 = Aps A(Pb)
Pp (
True
It is raining
LLM L
Prover9
Pyi was sunny yesterday
(Vocabulary real-world)
An regular expression for email with characters separated by θ, ending .com
Oeee Eyy Conien
90 [a-z)+@(a-z]+..om
LLM L
I(ps)
A(vb)
WW@@W+.com
Prover9
Pn ?A
False
[nummbers not
Figure I: The vuto3VAL process for autonomous evaluation of LLM truth maintenance w.r.t. (AoI)"
A(1)(w) will be a semantically equivalent FL representation of v. Since v is an NL description, quite challenging check whether I(pp) is indeed an accurate representation of &p without human intervention. However, if preserves truth, sp A(I(s)) will be semantically equivalent to even if they are not syntactically identical. Thus, we only need to check & v For example, let PP = A Pl. tho I(p))) = "A conjunction of propositions Pl and p1 that can be simplified to pi using Idempotence." ", and أ = A( A(yu)) = Pı for sequence (AA I) (PP)). is challenging to check if dbu accurately represents (pu but it is easy to check if (Po (P1 using formal verifier.
Since VutoEVAL uses formal syntax o as input and produces formal syntax yp' as output, we can use yp". As result, VutO avoids brittle syntactic equivalence
formal verifiers to check whether checks and exhaustive tests of semantic equivalence that require evaluations of all possible truth valuations of formulas or executions of regexes.
We use the above insights to automatically assess LLM truth maintenance by using the same LLM L to represent I and A respectively. Fig. shows our overall assessment process. Briefly, we use context-fres grammar G to automatically generate ground-truth FL expression sPn. Next, we use vocabulary generation process generate context for (oo This can either use abstract terms or use NL elements for more human-like like scenarios ($D1). We then evaluate (AA o I. (vPo) by using L to first generate vho I[ypo, k) using context designed for informalization. The context of 7. is cleared (note that we only use the output of I(Pp))), and we use to generate و0 = A( k²) using context x' designed for autoformalization. We then use verifier (e.g.. Z3 (de Moura & Bjørner 2008), Prover9 (McCune (2010)) to assess if Poo = since both are elements of FL. If we can repeat the process by evaluating (A ( similarly.
Φ then
Consider case 2 in Fig. Vuto]vAL uses the grammar in Fig. to automatically generate a ground truth FL sentence as (P P1 A A2 Ap1 We can use any vocabulary to generate meaning for the propositions; P1 It is raining today, P2 It was sunny yesterday. Next, the LLM L is prompted with Prompt to perform informalization yielding NL t/o A(5oo) I. can perform any simplification or other paraphrasing necessary. For example, I. could informalize ?P above to tho = "The weather status was sunny yesterday whilst is raining today." Notice that the LLM-generated NL statement automatically reflects a simplification using the Commutative (a A b = b A a) and Idempotent (a A a = a) properties. Next, L is asked to autoformalize Yh without any context other than the vocabulary to use and prompt for autoformalization (App. [F). In this case, the LLM could return Pi A(*o) = pi A P2. We use a theorem prover such as Prover9 (McCune 2010) to show that PP 1i and thus assess L's truth maintenance capabilities w.r.t. (A (
Example:
4

---

Published as a conference paper at ICLR 2025
3.2 YUTOEVAL METRICS
VutoJVAL score When evaluating an LLM's truth-maintenance capabilities, it is crucial to consider the intended application, because performance FL strings of similar complexity typically indicates how the model will fare in practice. As such, VutoaVAL can be used in two distinct modes: parame- terized and calibrated VutoEVAL scores. The parameterized VutoavAL score computes performance with the descriptional complexity of FL. strings as parameter (e.g., the number of operators). The calibrated VutoEVAL score cat [D, d) is computed using all FL. strings from dataset D with complex- ity up to d, where there are equal number of examples for each complexity. In both modes, the score is computed as the fraction of FL strings in the corresponding dataset for which (A o I)* (fP1) = 4P1.
Bounding false positives in computation of VVAL scores A key advantage of the Vuto score is its robustness to different informalizations of the same FL. Thus, when VutoEvAL outputs that LLM maintains truth (AA I)" (PP) on FL Poo the intermediate NL I(wo) is a semantically equivalent translation of Po- We now bound the probability of false positives, i.e., cases where the LLM fails both autoformalizing and informalizing but yields an FL string equivalent to the original.
AL 10 be an execution of the Vuto3vAL process for (A o 2)² s.t. Ω0 = "Pi but vo is not an accurate representation of yoo We can derive the probability of VutoEvAL providing such false positives. Let pz be the probability with which informalizes an FL expression I(PPo) = th s.t. 4/ is an accurate representation of Pou Similarly, let P.A be the probability of autoformalizing Vnn A(Pn)) ff1 s.t. ( is semantically equivalent to vo. i.e. (0o = 9P Let pH be the probability that T. hallucinates F7. y01 by autoformalizing tho s.t. PP = Po given that the not an accurate representation of ypo
Ix(()))
Given an LLM L, let yo
It can be seen that for false positive to be outputted by VutoEVAL, the sequence Y0 + 1/ produces an incorrect NL description and the sequence tho - 4P autoformalizes incorrectly but hallucinates just right to yield Φ = sPo. The probability of such sequence corresponds to L making two mistakes, with the second mistake being such that generated an expression equivalent to Po- This can be expressed as (1 (1-pz)( pz) (1- PA)PH- For (AoI)"(pp) (yoo), this probability is (1- (1==))( since VALL computes (AA o I) (p.. if P = şo (Sec.3) 3.. As L.MM technology improves, we expect Pr, PA- 1 and pæ O. As result, the probability of false positives provided by VutoEVAL 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 (Sec. 4.
LLMs as verifiers score The llm-verifier score evaluates a given Ilm's ability to determine equivalence between FL strings. It is measured by using FL strings produced by a LLM from the VutoDvAL process. For each dataset and descriptional complexity, we compute an Fi score by comparing the evaluated LLM's equivalence predictions with the formal verifier's 's results. We use Chain-of Mhain-of-Thhuugh (CoTT) to allow LLMs to utilize their generated outputs to improve their reasoning (Wei et al. 2022).
Predictive power In addition to using calibrated and parameterized VutoEVAL scores for assessing the ability for truth maintenance, we propose new metric for evaluating the extent to which performance on a benchmark is indicative performance on other benchmarks:
Definition 3.1 (Predictive Power). Let L1 and L2 be language models evaluated on two benchmarks A and B with ranks ZA and BB. The predictive power of A over B is formally defined as (B) = Pr(L_ ZB Lz 1 Z Tz2)-
In practice, we compute predictive power as a sampling- based maximum maximum-likelihood estimate over multiple auto-generated datasets.
3.3 DYNAMIC DATASET GENERATION
We use context-free grammars (CFGs) (Hopcroft et al.) 2001) set of production rules over terminal and non-terminal symbols- - for dynamically generating datasets. An infix parse tree is obtained by repeatedly applying the rules, where the depth of this tree is often used to measure the descriptional complexity of a given string generated using the CFG (Csuhaj- Varjú & Kelemenová 1993). CFGs also can be used generate arbitrarily large amounts of data dynamically.
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, dynamic dataset
5

---

Published as a conference paper at ICLR 2025
SASAS
S - (+
S + FIVJ. S)
S (5)
- (PVPV P)
S S (-S)
F + (F (
S SEK
P
- 1
F (-F)
K + #/E
3-N3-NNF
Propositional Logic
(c) First-order Logic
(d) Regular Expression
Figure 2: CFGs (described in Sec. 3.3.1 used for synthesizing the datasets in VVI.
that only consists of k-CNF sentences propositional logic in the Canonical Normal Form (PP V V PP) A (P) v v... v PA) A where P/ {Pa. -P=) 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.
3.3.1 AUTO-GENERATED DATASETS
VuL is open-source] 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 that any newly developed LLM can be evaluated on by using Vuto3VAL out-of-the-box.
Our dataset generator (described in App. B takes user-provided CFG and vocabulary to dynamically generate user-controlled, diverse datasets up user-specified metric such as the number of operators. parse tree depth, etc. It is guaranteed to generate any representable string using the CFG (App. B) As result, users can easily generate CFGs and/or vocabularies.
datasets in VutoEVAL by simply providing
The Vuto core benchmark uses four CFGs (Fig. 2 for producing five datasets compromising FL strings. The 3-CNF(n) (Fig (b) and propositional logic PL.(n) (Fig.2b) CFGs replace the terminal by randomly selecting from a list of n propositions. First-order logic FOL(Mp, no) (Fig CFG replaces the terminal with predicates of the form p(v)..... Ux) where p is predicate name selected from a list of up predicates, 2/ is either an object o from a list of n. objects or is a free variable
E {01, ..) that is appropriately annotated within the scoping rules. Finally, the regular expression RE(n) (Fig. 2 CFG uses the vocabulary set Σ {O...., 11..
We provide 5 datasets with 2 generated from the FOL CFG and I each for the rest. We sampled 500 strings for each complexity level. The 3-CNF(12) dataset contains examples with up to 59 operators, totaling 100 strings. PL( contains examples with up 40 operators, for total of 20k strings. The RB(2) dataset contains examples with tree depth up to 40, also totaling ~20 strings.
The FOL datasets, FOL(8, 12)-S and FOL((8 12)-E, contain examples with up to 37 operators, for a total of 199 strings each. FOL(S, 12)-S uses auto-generated synthetic object and predicate names. Conversely, FOL 12) E uses verbs from VerbNet (Schuler) 2005) for predicate names and names from Faker (Faraglia 2024) for object names. Using more descriptive names allows for informalization to produce more abstract sentences that closely resemble the NL statements in SOTA autoformalization datasets. For example, a FL statement Boom( Richard)) A Exercise( Yolonda) yields a more natural NL statement: "Richard experiences a boom, and Yolonda engages in exercise".
While each dataset was generated in 10 separate pieces, each produced independently, our datasets contain ~85k unique examples. We also provide zero-shot and 2-shot prompts for each dataset, for a total dataset size ~1 70%: for off-the-shelf evaluation and continual assessment of any new L.M. Of these examples, ~85% of them are composed of unique CFG parse trees (trees obtained by sampling the CFG but not injecting the vocabularies). Expressions with the same parse tree but different vocabularies (e.g., P1 A P2 and p2 A P1) account for 10% of our dataset, providing a robust check against positional bias in the LLM. Additional information is presented in M
We use open- source libraries to robustly parse the L-M-generated output. We use the Natural Language Toolkit (NLTK) library (Bird 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,
'The code for this project is available at: httpp:://g/thub.ccmm///

---

Published as a conference paper at ICLR 2025
Prompt I: Informalization (Z) prompt for Fig. Case (other prompts available App. Fi
Your task is to convert a (Propositional Logic, First-order Logic) formula, appearing after [FORMULA], to 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 reconstruct the formula without having access 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 NI interpretations The objects in the universe (if any)
Objects:
Propositions:
The propositions in the universe and their NL interpretations (if any) The predicates in the universe and their NL interpretations (if any) Few-shot examples of the task (if any)
Predicates:
Examples:
Example Prompt
Your task...
Operators:
A represents conjunction, V represents disjunction,
Propositions: P1 It is raining, P2 was sumny yesterday
Formula: P1
Example Response: The sun was bright the day before whilst it is raining today.
we also use scripts to ensure that the informalization step does not copy elements of into NI. (e.g.. complete any parts of FL) that would otherwise make autoformalization trivial.
4 ASSESSMENT OF SOTA LLMS ON THE VUTOEVAL BENCHMARK
In this section we present evaluation of several SOTA LLMs using VutL, as well as an evaluation of Vuto3VAL as a benchmark for evaluating LLMs' reasoning and translation ability using the predictive power score. In particular,
the following assessment criteria for evaluating LLMs using Vuto (Al) Can LLMs produce FL translations that are syntactically compliant? (A2) Can LLMs maintain truth while translating FL? (A3) Can LLMs accurately verify whether two FL strings are logically equivalens? In addition, we use the following criterion to assess VutOEVAL itself: (A4) the performance on Vulo]AAL indicative of performance on other benchmarks?
4.1 EVALUATING LLMS USING AUTOEVAL
We assessed $A1 $A3 using 17 SOTA closed and open-source LLMs (Fig. For clarity, we plot select models, grey out the data from the others, and refer the reader to App. for comprehensive overview. We evaluated $A1 and $A2 using the parameterized Vuto=VAL score on our generated datasets. For $A3,, we calculated the LLMs as verifiers score for each descriptional complexity class by having each LLM verify the results produced by GPT-4o.
As stated in Sec. prompts are crucial for LLM performance. To ensure our results reflect LLM capabilities rather than the effect of poorly designed prompts, we conducted extensive prompt engineering and ensured that least one L.LM could achieve a parameterized Vuto-VAL score > 95% on the 3-CNF(12) dataset, which has constrained but representative grammar. Analysis on each LLM's performance on the 3-CNF(12) dataset is presented in App.
As shown in Fig 3 SOTA LLMs able to produce syntactically compliant formal syntax ($A1) for formal syntax with low descriptional complexity (e.g., few operators in logic). However, as the complexity increases, the ability of LLMs autoformalize their own informalizations diminishes. One surprising result here is that GPT-4o is less syntactically compliant for regexes than Phi and I.Lma-3, which much smaller models. This due GPT-4o often repeating token sequence

---

Published as a conference paper at ICLR 2025
ChatGPT GPT-4o
GPT-4o-mini (8L 12)-5
Phi3
Mistral
LLama3
Other LLMs (n 10)
Propositional L2g
10) 12)
Regular Expression
Syntactic Complance
88 b
Vuto Score
8 b
LLMs as Verifiers
Fi Score
b.
88
10
20
Operators: A. is counted operator iff succeeded terminal)
CFG Parse Tree Depth
Figure 3: Zero-shot Pass results from using Vuto to assess LLMs w.r.t $A1, $A2, $A3 on the packaged datasets (Sec. (Sec.3.3. 3.3.T The x-axis represents an increasing deseriptional complexity. The y-axis is each evaluated LLM's ss syntactic compliance
(Ist row), parameterized Vuto3VAL score (2nd row), and Fi score as a verifier (3rd row). Additional results (prompt calibration, few-shot, etc.) are included in Appendix.
when translating regex, resulting in hitting the token limit. For logic, we observed that LLMs often use the correct syntax but often misplace parentheses, creating malformed expressions.
Our analysis further shows, except on the 3-CNF(12) dataset used for prompt calibration, LLMs cannot maintain truth in FL translation ($A22 as the descriptional complexity increases. For translating logic expressions with more than 20 operators, none exceeded 50% accuracy in maintaining truth. This is concerning since formal specifications often have hundreds of operators. A common issue was misunderstanding the formal syntax's 's precedence and associativity rules. Misplaced operators led to quick verification failures. We provide an analysis of failing cases in App.
Moreover, with CoT prompting, LLMs cannot ($A3) for anything but toy expressions (low descriptional complexity), after which F1 scores fall sharply. For small FL strings, 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 verify correctly the Appendix (App. Fig.
accurate verifiers of logical equivalence
4.2 EVALUATING YUTOEVAL AS BENCHMARK
For assessing $44, used the same 17 LLMs evaluate the predictive power (Sec. of VutooVALL w.r. popular benchmarks: (a) (OLIO(R;(NL, FOL)) (Han et al. 2024), a popular logical reasoning benchmark with ground truth in both NL and FL; (b) FOLIO
evaluates if an LLM can
(auto/in) NL (FL) accurately; (c) LogiEval(R: FOL Patel et al. 2024) a reasoning benchmark with ground truth in propositional and first-order logic: (d) HumanEval(A (Chen et al.) 2021), a code autoformalization benchmark; (e) Big Bench Hard (BBH) (Suzgun et al.] (023). These benchmarks are contrasted in Sec. and example prompts of these benchmarks are included in A We ran 5 runs on each benchmark except BBH. For BBH, we use the reported numbers in the literature as scores for the models (sources included in App K. We measured the correlation between each benchmark's 's score and the calibrated Vuto VAL score (Fig. 4 which was calibrated based on the descriptional complexity of the examples found the benchmark. We also measured the calibrated VvLL. score's ' predictive power w.r.t these benchmarks (Fig 5)
As shown Fig. there a moderate- poddraate-to-stron to-strong positive correlation between LLM performance on VutoEvAL and other logic-based benchmarks on myriad of tasks such as autoformalization. logical reasoning, code generation, etc. The calibrated VutoIvaL score exhibits a strong, positive correlation (p > 0.7) with other static benchmarks FL-based tasks, as well reasoning tasks such as FOLIO. Notably, calculating the parameterized VutoEvAL score does not require annotatiin unlike these benchmarks. Similar results appear in LogiEval for propositional logic, though the FOL version shows only a moderate correlation (0.5 < p < 0.7). We traced this reduction to dataset imbalance, where 80% of samples from the positive class. Furthermore, the dataset is skewed
8

---

Published as a conference paper at ICLR 2025
Trend Line
Other Models
(n - 10)
CharGPT
GPT 4a
GPT 4o mini
Phi
Mistral
LLama
FOLIO (R; NL)
FOLIO (R: FOL)
LogiEval (R, PL)
LogiEval (R: FOL)
FOLIO (.4)
HumanEval (4)
6.39
Benchmark Score
010
600
001
0.0
.75-
.0
.25
5.
(FOLF.
12
300
FOL
121-222-- 6
Sud (LL(2) 201
Sa FOL(S
121- 201
5.
12)
Sayl (EE
.25
170
76
.25
76
Ca libiibated VutaEVAL Score
Figure 4: Correlation between scores on VutoEvAL and static benchmarks from the literature. The Pearson correlation coefficient (p) and the p-value (values S 0.05 are statistically significant) are annotated in the top left. The calibrated VutoEvAL score Send (D, d) use all strings in dataset D with descriptional complexity d Grey hexagons
bounded above, shown in the plots (App.
represent data from 10 other models.
towards lower difficulty. This leads to lower overall performance (and consequently correlation) of models like GPT-4o-mini that actually try to reason and provide no answers compared to models like LLama-3.1-80 which mostly answered yes.
Our results (Fig.5) show that an LLM's cal- ibrated VutL score is a strong predictor of its performance on FL-based benchmarks. Our metric also a more robust truth main- tenance measure than length-dependent, NL- based metrics like BLEU scores (Papineni et al. 2002). For example, changing the generated NL. & "he weather status was sunny yesterday and is raining today" to v/ ="the weather sta- tus was sunny yesterday and is not raining today" still achieves high BLEU( (/ 16) score of 0.74 (BLEU(r) (1b, 4) 1) but does not maintain truth. Even as a predictor for such metrics, VutoEVAL notably surpasses random-chance accuracy.
basbade metrics
Gos
0.86
0.85
Longth Dependent
0.11
0.78
Prosocau (X)
HumanbbullA) Accunncy
Logtbal(FOL) Accuntt
0.71
0.58
5
FOUOONN) Acorsty
FOUOLA) Acarag
BBH(R) Anurey
FOLIO/FO) Auseay
LigiEsu Auureyy
FQUoy)) METCOR
ROUGE
BERT
.25
Fouoor)
Faulor)
Fallor))
Benchmark (Annottaedd bars)
Figure 5: Predictive power of VutoTvAL w.r. other
benchmarks. Benchmark metries appear after the colon.
4.3 EVALUATING LARGE REASONING MODELS USING VUTOEVAL
Large Reasoning Models (LRMs) are LLMs that also perform some reasoning steps (e.g., search) a part of their generation process. We assessed two SOTA LRMs - OpenAl's ol (OpenAl 2024) and DeepSeek's s RI (DeepSeek 2024) on ŞA1 and $A2 using VuLoEVAL. Due to cost limitations, regenerated small dataset with 10 examples for each operator num- ber for approximately 400 total examples. Our results (Fig. () show that even SOTA LRMs can- maintain truth effectively in (A (poo).
OpenAt --- DaapSuok kt
Syntactic Compliance
PL(12)
FOL(S. 12)-E
SeepSteet
Score
-75
Vuto
-35
.25
Openl
10
20
30
10
10
20
30
10
# of Operators: A, V,
Figure 6: Applying VuLL with zero-shot prompts
to LRMs on a small dataset of 400 strings.
RELATED WORK
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 used by LoginNL (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. Although these techniques dynamic, they remain limited in generating interesting reasoning problems across different domains. In contrast, Vuto3VAL is multi-diimensional, offering five distinct datasets, multiple customization options, and the ability produce an infinite number of unique syntax trees.

---

Published as a conference paper at ICLR 2025
FOLIO (Han al., 2024) utilizes human experts to generate set of reasoning questions based on real-world text sources. They generate questions in both NL and FL 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 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 al.] (2023) through the HumanEval+ dataset that the test cases in HvaanEval are incomplete and can provide misleading rankings. StructuredRegex (Ye et al. 2020) used crowdsoure- ing for generating regex datasets. In contrast, Vuto3vAL requires no human annotations and utilizes formal verifiers for checking the truth maintenance and thus does not share such draw brawbacks.
FOLIO((A,I)) (Han al. 2024) tests the (ormaizinoooaaaizatiio abilities of LLMs by using hand- coded annotations of (NZ., FL) pairs. However, as noted by the authors, they cannot check truth maintenance effectively and rely on an inference engine to compute truth values for each conclusion. Vuto]vAL uses theorem provers to check equivalence and thus is sound in its accuracy evaluation.
MALLS Yang et al., 2024) 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-tuiing and not for evaluation. In contrast, VutoJVAL generraess correct FL and has 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 (002)) utilize formal verifiers to provide sound evaluation metrics but utilize hand-coded datasets that limit their use in evaluating newer LLMs unlike VutoEVAL.
Informalization Wu et al. (202)) and ProofNet (Azerbayev et al. (202)) use static datasets to evaluate LLM informalization capabilities. They use metries such as BLEU scores that are known to not be indicative of accuracy for FL-based tasks (Ren et al. 2020). Jiag et al. (2023) develop MMA, 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, VutoāVAL is autonomous and provides sound measures of LLM capabilities w.r.t. truth maintenance.
CONCLUSION
We introduced Vuto]VAL, new benchmark for autonomously assessing L.M truth maintenance in formal language translation. Vuto3vAL allows scalable data generation without human labeling and autonomously evaluates truth maintenance using formal verifiers to guarantce correctness. is easily extensible and provides several prepackaged datasets and dataset generators to assess new LLMs quickly. Furthermore, our evaluation indicates that SOTA LLMs and LRMs are not performant in this task. Finally, we show that our metric is predictive of performance on other formal- sarmal-language-asee tasks and thus can be used as a surrogate benchmark for evaluating future LLMs.
Broader Impact VutL provides robust framework for evaluating the suitability and safety of LLMs in FL-based tasks such as autoformalization and code generation. It also serves as a surrogate for estimating performance as LLMs emerge. Our work lays the foundation for developing autonomous evaluation techniques for LLMs in more flexible syntaxes, such as conversational Al.
Limitations and Future Work A limitation of our work is the use of formal verifiers: the equivalence problem for first-order logic is well known to be undecidable. We mitigate this by using an appropriate timeout and logging (only 0.66% of our results experienced timeout). This issue can be removed by using CFGs that generate decidable strings. An interesting application of VuLO is using generated evaluations as datasets for back-translation, thereby improving the autoformalization capabilities of models (Jiang et al. 2023). One interesting extension of our would be assessing truth maintenance in other applications (e.g.. image generation). Finally, using formal verifiers as callable tools for LLM is an intriguing extension of our benchmark, enhancing the assessment of SA3.
Threats to Validity Our results for paid APIs rely on the model checkpoints to be available. Due to cost limitations, results report pass @ scores. We do report the std. deviation across 10 runs on 10% of each dataset in App.[H] with similar conclusions. We assume that the verifier and parsing libraries sound. We mitigate this risk by using popular open-source tools like Prover9 and NLTK.
10

---

Published as a conference paper at ICLR 2025
ACKNOWLEDGEMENTS
This work was supported in part by the ONR grant N00014-23-1-2411 NSF grant IIS 1942856, the Open Al Researcher Access Grant, and Arizona State University's ' GPSA Jumpstart Research Grant. We acknowledge Research Computing at Arizona State University for providing computation resources that contributed to this paper's results.
ETHICS STATEMENT
Our work involves using LLMs for generating text. Naturally, it is imperative ensure that appropri- ate guardrails are in place to prevent offensive content from being generated and/or displayed. We do not any personally identifiable information in VutoEVAL.
REFERENCES
http://ggtttuubbcoom//o beg.dd/..icctss///tttom..om///// http//jaaackk//gggttee Q/rggdd 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. arXiv preprint urXiv:2302. 12433, 2023.
Satanjeev Banerjee and Alon Lavie. METEOR: An automatic metric for MT evaluation with improved correlation with human judgments. In Proc. ACL Workshop on Intrinsic and Extrinsic Evaluation Measures for Machine Translation and/or Sunmarization, pp. 65-72. Association for Computational Linguistics, 2005.
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 Ponde De Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained code. arXiv preprint arXiv:2107.0333 033374 2021.
Peter Clark, Oyvind Tafjord, and Kyle Richardson. Transformers as soft reasoners over language. In Proc. IJCAI, 2020.
Erzsébet Csuuhj-Varjj and Alica Kelemenová. Descriptional complexity of context-free grammar forms. Theoretical Computer Science, 1 11((2):277-28, 1993.
Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Z3: An efficient SMT solver. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
DeepSeek. Deepseek-rl: Incentivizing reasoning capability llms via reinforcement learning. httpsss/aaxxv..rrrraa//////////
2024. Accessed: 2025-01-22.
TJ Dunham and Henry Syahputra. Reactor mk. performances: Mmlu, humaneval and bbh test results. arXiv preprint arXiv:2406.10515, 2024.
Daniele Faraglia. Faker. httpp///ggthhbb.co///kkk//// 2024. Accessed: 2024-06- 01.
Clémentine Fourrier, Nathan Habib, Alina Lozovskaya, Konrad Szafer, and Thomas Wolf. Open Ilm leaderboard v2. https: open 11m leaderboarrrd 2024.
11m- leaderboard)
IBM Granite Team. Granite 3.0 language models, 2024.

---

Published as a conference paper at ICLR 2025
Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle-Solana Hannah Szabó, 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 Kryseinski, 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. In Proc. EMNLP, pp. 22017-22031, 2024.
Pengcheng He, Xiaodong I Liu, Jianfeng Gao, and Weizhu Chen. Deberta: Decoding-enhanced bert with disentangled attention. In Proc. ICLR, 2021.
J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley series in computer science. Addison-Wesley, 2001. ISBN 9780201441246.
Michael Huth and Mark Dermot Ryan. Logic in Computer Science Mooelling and Reasoning about Systems. Cambridge University Press, 2nd edition, 2004.
Douglas M. Jennewein, Johnathan Lee, Chris Kurtz, Will Dizon, Ian Shaeffer, Alan Chapman, Alejandro Chiquete, Josh Burks, Amber Carlson, Natalie Mason, Arhat Kobwala, Thirugnanam Jagadeesan, Praful Barghav, Torey Battelle, Rebecca Belshe, Debra McCaffrey, Marisa Brazil, Chaitanya Inumella, Kirby Kuznia, Jade Buzinski, Sean Dudley, Dhruvil Shah, Gil Speyer, and Jason Yalim. The Sol Supercomputer at Arizona State University. Practice and Experience in Advanced Research Computing. PEARC '23, pp. 296-301, New York, NY, USA, Jul 2023. Association for Computing Machinery. ISBN 9781 4704999399 doi: 10. 1451145/356995/ (t15699991.359999 33597573.
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-33 2023.
Albert Q Jiang, Wenda Li, and Mateja Jamnik, Multilingual mathematical autoformalization. arXiv preprint arXiv: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 Proc. ICRA, pp. 2023.
Chin-Yew Lin. ROUGE: A package for automatic evaluation of summaries. In Text Summarization Branches Out, pp. 74-81 81, Barcelona, Spain, July 2004. Association for Computational Linguistics.
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 Proc. NeurlPS, 2023.
Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self-feedback. In Proc. NeurlPS, 2023.
William McCune. Prover9 and Mace4. 2010.
http: / www.
unm www.ssss.wuuuuuuc...ooomooo www.n...bb.mmcccue//rreeeaaaae
Microsoft. Phi-3 technical report: A highly capable language model locally on your phone. https
7/arxiv.org htt.xxiwwrr///df//44.1111 14219 2024. Accessed: 2024-06-01.
MistralAI. Introducing the world's best edge models. https://mistraie newww
ministraux/) 2024. Accessed: 2024-11-22.
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 DolaraLezama, 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.
12

---

Published as a conference paper at ICLR 2025
OpenAl. http:////aaa..o//////////../.... 2023. Accessed: 2023-06-
01.
OpenAL. 2024-09-29.
-pt
https://openal htmpeenai.coo////aee www. /ndexx
2024. Accessed:
OpenAl. Introducing openai ol. hnttps://peeai..cmm
2024. Accessed: 2024-11-22.
Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. Logic-Im: Empowering large language models with symbolic solvers for faithful logical reasoning. In Proc. EMNLP, 2023.
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proc. ACL. pp. 311-318 2002.
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. In Proc. EMNLP, pp. 20856-20879, 2024.
Qwen2. Qwen 2.5. https:://wen2..rgg/
5/ 2024. Accessed: 2024-11-22.
Shuo Ren, Daya Guo, Shuai Lu, Long Zhou, Shujie Liu, Duyu Tang, Neel Sundaresan, Ming Zhou, Ambrosio Blanco, and Shuai Ma. Codebleu: method for automatic evaluation of code synthesis. arXiv preprint arXiv:2009. /002:99700.00977,, 2020.
Stuart Russell and Peter Norvig. Artificial Intelligence: Modern Approach. Pearson, 4th edition, 2020.
Pranab Sahoo, Ayush Kumar Singh, Sripama 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.07922 2024.
Abulhair Saparov and He He. Language models are greedy reasoners: systematic formal analysis of chain-of-the th-huhh.- In Proc. ICLR, 2023.
Karin Kipper Schuler. VerbNet: Broad- croee-coeerage, Comprehensive Verb Lexicon. PhD thesis, University of Pennsylvania, 2005. A713179808.
Shreya Shankar, JD Srinffrescu-Pereiirr Bjöm Hartmann, Aditya Parameswaran and Ian Arawjo.
Who validates the validators? Aligning llm-assisted evaluation of 11m outputs with human prefer- ences. In Proc. ACM Symposium User Interface Software and Technology, pp. 1-14, 2024.
Koustuv Sinha, Shagun Sodhani, Jin Dong, Joelle Pineau, and William L. Hamilton. CLUTRR: A diagnostic benchmark for inductive reasoning from text. In Proc. 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 Machine Learning Research, 2023. ISSN 2835-8856.
Mirac Suzgun, Nathan Scales, Nathanael Schärli, Sebastian Gehrmann, Yi Tay, Hyung Won Chung, Aakanksha Chowdhery, Quoe Le, Ed Chi, Denny Zhou, and Jason Wei. Challenging BIG-bench tasks and whether thain-of-thought can solve them. In Proc. ACI,, 2023.
Jidong Tian, Yitian Li, Wenqing Chen, Liqiang Xiao, Hao He, and Yaohui Jin. Diagnosing the first-order logical reasoning ability through LogicNLI. In Proc. 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 Proc. NewrlPS, 2022.
13

---

Published as a conference paper at ICLR 2025
Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Proc. NeurIPS, 2022.
Cheng Xu, Shuhao Guan, Derek Greene, and M-Tahar Kechadi. Benchmark data contamination of large language models: survey. arXiv preprint arXiv:2406.044 04244, 2024a.
Tengyu Xu, Eryk Helenowski, Karthik Abinav Sankararaman, Di Jin, Kaiyan Peng, Eric Han, Shaoliang Nie, Chen Zhu, Hejia Zhang, Wenxuan Zhou, et al. The perfect blend: Redefining rlhf with mixture of judges. arXiv preprint arXiv:2409. 2024b.
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. In Proc. ACL., pp- 9942-6959) 2024.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. Benchmarking multimodal regex synthesis with complex structures. In Proc. ACL, pp. 6081-6094, 2020.
Yi. 01-ai. http://////uunnnnnee....///////3 11-22.
2024. Accessed: 2024-
Weihao Yu, Zihang Jiang, Yanfei Dong, and Jiashi Feng. ReClor: A reading comprehension dataset requiring logical reasoning. Proc. ICLR, 2020.
Tianyi Zhang*, Varsha Kishore*, Felix Wu*, Kilian Q. Weinberger, and Yoav Artzi. Bertscore: Evaluating text generation with bert. In Proc. ICLR, 2020.
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng. Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging llm-as-a-judge with mt-bench and chatbot arena. Proc. NeurIPS, 2023.
Jin Peng Zhou, Charles E Staats, Wenda Li, Christian Szegedy, Kilian Q Weinberger, and Yuhuai Wu. Don't 't trust: Verify grounding LLM quantitative reasoning with autoformalization. In Proc. ICLR, 2024.
14

---

Published as a conference paper at ICLR 2025
A APPENDIX ORGANIZATION
The code used for this project can be found aljcctpss//gtttub..co/////a -aate//AAARRaAAA//Aaaa hasi//utoeval
The Appendix is organized follows. Appendix Appendix B provides the algorithm used for C discusses prompt tuning and validating our prompts on 3-CNE. D provides the parameters used when generating the five datasets discussed in the paper. Appendix provides additional information on our experimental setup, including the computational resources used. Oppendix(Fdiiseussees discusses the prompts and provides examples. Appendix G our detailed analysis of the empirical results from the main paper. Appendix discusses an experiment we ran evaluate the standard deviation error. Appendix iincludes additional results from zero-shot prompting experiments using other metrics for categorization. Appendix Seadixxxeee evvllates an experiment we performed comparing few-shot prompting compared zero-shot. Finally, Appendix K provides the experimental setup of the benchmarks we evaluated, data values and sources of scores collected, the calibrated Vuto3VAL scores used for comparison, and additional correlation results.
dataset generation. Appendix Appendix
H
B DATASET GENERATION
In this section, provide the algorithm for generating formal syntax (FS) expressions and show that can generate possible expressions from the grammar and vocabulary.
Our approach, VuLO generates datasets by constructing context-free grammar (CFG) tree using the grammars discussed in Section [.3.1 Since intractable to generate the full tree, we control the branching factor and randomly expand the branches of this tree generate formulac.
Algorithm Dataset Generation
1: Inputs: CFG G, vocabulary V, branching factor tree depth depth, sample count sample_count, and categorization metric m.
2: Outputs: set of FS expressions
3: N + {0: [None]]. + ()
4: for d 1,2....., depth do
5: N' + sampleN(N[d 11,dd11,,) 1),n)
6: for N2 do
7:
N To + generateNChildren(... WId += No Nr + -NUT,
8:
9:
end for
11: end for
12: M +- cattgertttEpeeessssuuaabbbt.ti
13: @ +)
14: for E (eys(M)
15: Mr + sampleCFGExpression((//////
16: PR buildFSExpreesioon((M.
17: Φ G
18:
end for Return: F
The dataset generation algorithm is shown in Algorithm I This algorithm constructs CFG tree by maintaining non-terminal nodes each tree level (A) and all the leaf nodes (Ni), where each terminal node represents a completed CFG expression (line 3). For generating nodes at certain level in the tree, n nodes from previous level are sampled (line 5). Fach node 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).
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, fixed number of CFG expressions corresponding to that value are sampled (line 15). Using the vocabulary, an FS expression constructed from each CFG expression (line 16). Consequently, the final dataset of FS expressions contains equal number for
15

---

Published as a conference paper at ICLR 2025
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 hyperparameter controlling the number of unique propositions for propositional logic. Similarly, for first-order logic, the number of unique variables, constants, and predicates also hyperparameters. Also, regular expressions have 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" arity. In the case of the arbitrary vocabulary, the arity for 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 is guaranteed to generate all possible formal syntax expressions that can be produced for a grammar and vocabulary. Let yp be an FS expression that can be constructed using the rules from CFG G and the vocabulary V. Note that yp corresponds to a CFG expression PCFF, derived by substituting the vocabulary with CFG symbols. Due to uniform selection, the probability of yo being generated from FCFG is greater than zero. Furthermore, the CFG expression represents leaf node in the CFG tree that can be reached by applying the CFG rules in specific sequence. Due to the random sampling of rules at each node, there a non-zero probability of generating this particular path in the tree. Thus, ço can be generated using the dataset generator algorithm.
C 3-CNF PROMPT CALIBRATION
In this section, we discuss the K-CNF results used calibration the prompts.
We tested several prompts for 3-CNF to verify that our prompts are sufficient to prompt the LLM correctly perform informalization and autoformalization. Additionally, we verified that the equivalence verification prompt prompted the L.Ms to give an accurate yes-or-no answer. The performance of all 14 LLMs 3-CNF for SAI, $A2, and $A3 are shown in Figure
ChatGPT
GPT-4o
GPT-Ao-mini
Phi3
Mistral
LLama3
Other LLMss (n 10)
3 (2)
1.00
Syntactic
Complance
0.75
0.50
0.25
0.00
1.00
LLMs Verifiers Yuto
Score
0.75
0.50
1.0
01 Score
0.25
0.00
of Operators: A, V. (- counted as an operator iff not succeeded by terminal)
Figure 7: Zero-shot Pass results (avg. over 10 batches, higher values better) for 3-CNF from using VutoEVAL to assess LLMs w.r.t $A1, $A2, $A3 (Sec. 3.3.1) on the packaged datasets. The x-axis is the # of operators.
The best-performing models we tested (GPT-4o and GPT-4o-mini) achieved nearly perfect syntactic compliance, accuracy, and equivalence verification even the number of operators increased. This proves that the prompts we used in our experiments are sufficient for prompting the model for performing the tasks for $A1, $A2, and SA3.
16

---

Published as a conference paper at ICLR 2025
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 LLMSs can verify two equivalent 3-CNF formulae as equivalent.
D DATASET GENERATION HYPERPARAMETERS
In T we provide the hyperparameters used to generate the five datasets.
Table 1: Hyperparameters used for producing the five datasets.
Parameter Type
Hyperparameter
Value
Description
depth
40
Maximum depth of the CFG tree.
General
200
Branching factor of produced CFG tree.
sample_count
50
Number of CFGS for each metric value to select.
free_ @ree_variable_pe prob
0.25
Probability of constant being placed by a variable.
max free saree_varibble,
Maximum number of unique variables.
First-Order Logic
vax_predicctte_arity
2
Maximum predicate arity.
min_prediccte_arit nun_objects num_predicates
Minimum predicate arity.
12
Number of unique constants. Number of unique predicates.
8
Propositional Logic
nun_propositions
12
Number unique propositions.
Regular Expression
a alphabet_size
2
Alphabet size.
E EXPERIMENTAL SETUP
In this section, we will provide the details of our experimental setup for generating the datasets and running VutoEvAL for evaluating each LLM's performance.
We ran our experiments using Python 3.10.13 with package versions shown in Table We also repackaged Prover9 (McCune 2010) to improve performance where this repackaged version can be found in our code base.
We generated five datasets using the dataset generation algorithm with the hyperparameters shown T the number of operators the categorization metric for all but regular expression, where we used CFG tree depth. We generated 10 batches for each dataset, resulting approximately 20k samples for each dataset with an equal distribution for each operator number.
Dataset Generation:
Table 2: Python package versions used for empirical evaluation.
Python Package
Version
openai
1.45.0
nltk
3.8.1
tqdm
4.66.4
Evaluating and Verification: The closed-source models (GPT- 3.5-turbo, GPT-4o, and GPT-4o-mini) were accessed using their API using temperature of 0. The open-source models LLama- I-SB-Instruct and --.-rll-vv.-------- on server with a 13th Gen Intel(R) Core(TM) 19-13900K and Nvidia RTX 4090 GPU using the model's default parameters with temperature of 1. Similarly, Phi-3-mediimm-4k-nnnte locally hosted on a server using Nvidia A100-XM4-80CS GPU,
anthropic
0.26.1
backoff
2.2.1
tiktoken
0.6.0
were locally hosted
transformers
4.41.1
Faker
25.2.0
networkx
3.3
was
Verification performed on AMD EPYC machine with 128 cores. The larger open-source
models, Yi-1.5-34B 1-33--Insttuct and Llama-3-700 Instrutt were run on Arizona State University's Sol
supercomputer (Jennewein et al. 2023
17

---

Published as a conference paper at ICLR 2025
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 the problem type and the vocabulary. For informalization, we prompt the model to produce just 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 non-synthetic grammar, we provide the predicate names and arity in the autoformalization prompt. Example informalization and autoformalization few-shot prompts for the first-order logic dataset are shown in Prompt the regular expression dataset are shown Prompt 4 and Prompt Example informalization and autoformalization zero-shot prompts for the propositional logic dataset are show in Prompt 6 and Prompt
2 and Prompt Example informalization and autoformalization few-shot prompts for
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-Th Chain-of-Thought prompting, the model is prompted to provide an explanation before giving a yes-or-no answer in a parsable format. Prompt [ gives an example of the prompt we used for verifying two first-order logic formulae.
G ANALYSIS OF MAIN PAPER RESULTS
In this section, we analyze the main empirical results the paper. Our results clearly show that current SOTA LLMs not performant in the truth maintenance task, which is why Vuto3VAL is needed. As the expression complexity increases, the syntactic compliance, accuracy, and ability verify equivalence diminishes. We describe some of the errors that cause the low accuracy for propositional logic, first-order logic, and regular expressions.
G.1 PROPOSITIONAL LOGIC RESULTS
Table 3: Examples of errors the evaluated LLMs made while evaluating Vuto3VAL for the proposi- tional logic dataset.
I(p))
(.4 (Ao (pp)
The natural description of the formula is: "It not the case that both proposition p11 and proposition p8 true."
(-pll A -p8)
(-(p11 Ap))
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."
(-p10 v7))
-p10 (-p9 p7))
Here is the natural description of the given formula: "The statement says that p3 is not true and p7 is also not true."
(-p3 A -p7)
(-p3 V -p7)
The formula states that either the proposition p2 is true the proposition p3 is true. Additionally, it specifies that the proposition p2 is not false.
(--12 v p3)
(p2 p3) A --p2
The formula describes a situation where the first proposition is false, the second proposition is true, and the third proposition false.
(-p2 A -p6)
(pp^g^
Informalization Errors: A common was the LLM failed deseribe 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 what propositions and operators
18

---

Published as a conference paper at ICLR 2025
Prompt 2: Few-Shov First- Ordder Logic Informalization Prompt
[TASK]
Your task is to convert 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 the vocabulary below.
[EXAMPLE 1]
(-p2 V V- -pp)
Disjunctive predicate logic expression consisting of three components: the negation of proposition labeled p2, the proposition pl, and again the negation of p2.
[EXAMPLE 2]
(--p2 A -(p3 V pl))
The expression asserts that p2 is not false while both p3 and pl are not true.
[VOCABULARY]
represents disjunction
represents conjunction
represents negation
( and ) represent parentheses propositions can be used verbatim predicates can be used verbatim
< >< x2 >
an represents universal quantification with xl... representing
free variables
æ1 ><
... an represents existential quantification with x1... representing
free variables
The objects are: p5, æ1
The parameterized predicates are: pred3(3p0, ?p1)
The free variables are: x1
[FORMULA]
drl pred3 (p5, 21)
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 Finally, we also observed hallucinations were the LLM attempted and failed to simplify the original formula (see example 4 in Table These interpretation errors resulted in the original meaning of the expression being lost.
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 describes >p A "p as predicate p "negated twice and combined" but failed to regenerate the original formula properly with this description.
Autoformalization Errors:
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 observed when not providing the predicate names and arity was the LLM rephrasing its explanation causing confusion when regenerating.
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 T).le Additionally, the L.MMs often messed up the predicate arity. Mistral often used and
Autoformalization Errors:
19

---

Published as a conference paper at ICLR 2025
Prompt 3: Few-Shot First-Order Logic Autoformalization Prompt
VOCABULARYY
Use V to represent disjunction
Use A to represent conjunction
Use represent negation
Use ( and ) to represent parentheses
Use y
list> to represent universal quantification
Use effre__variate list> to represent existential quantification
The
bistle consists of sequence of space separate free variables with the last variable immediately followed by period. Examples: (1) all x x2. (2) exists x4.
Use apredicate<<<prramie list>) to represent predicates (Names and parameters are provided in the description)
[TASK]
Your task interpret the natural language (NL) description of 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]
Disjunctive predicate logic expression consisting of three components: the negation of proposition labeled p2, the proposition pl, and again the negation of p2. (-p2 V pl V p2)
[EXAMPLE 2]
The expression asserts that p2 is not false while both p3 and pl are true. (7-22 A -p3 V pl))
[NL DESCRIPTION] For all objects labeled x1, the predicate pred3 holds true with parameters p5 and xl.
Table 4: Examples of errors the evaluated LLMs made while evaluating Vuto for the first-order
logic dataset.
I(p))
()())(
The formula states that is not the (pred8(p11) Apred8(p5) Apred6(p8)
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.
(-pred8(p10) A pred8(p5) (p5) Apred6(p8))
Here is the natural description of the given formula: "There exists an xl such that p4 is not an instance of pred2.
3r1. =p1.dpred2(p4)
Ez1. (pred())d
For all x1, it is not the case that (p5) is false.
Vzl. (pre-(pre)3( V v-pred3(p5)
There exists relationship between the
pred2(p3,p5)
objects p3 and p5 such that the predicate pred2 holds true for these objects.
3p3 p5. pre p5)
# operators with the variables, which was not needed for any formluae in VutoEVAL. Similarly, the L.MMs would often their own grammar instead of the provided in the prompt.
20

---

Published as a conference paper at ICLR 2025
Prompt 4: Few-Shov 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 so make sure to use the correctly account for scoping. You may terms verbatim 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 Iss.
[ORMULAJ
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 ''ss (01*)
[NL. DESCRIPTION]
The regex matches strings that start with the digit '0'.
G.3 REGULAR EXPRESSION RESULTS
Informalization Errors: Most of the emrors observed were the LLMs giving the wrong explanation,
for simple regular expressions. For example, GPT-4o often described e" as "one more
21

---

Published as a conference paper at ICLR 2025
Prompt 6: Zero-Shot Propositional Logic Informalization Prompt
[TASK]
Your task is to convert propositional logic formula, appearing after [FORMULA], to 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 correct names in your description. Explicitly describe the predicates. You may use terms verbatim as specified the vocabulary below.
(VOCABULARY]
represents disjunction
A represents conjunction
represents negation
( (and) ) represent parentheses propositions can be used verbatim The propositions are: p5, p12, p4
[FORMULA]
(p5 -p12 V -p4)
Prompt 7: Zero-Shot Propositional Logic Autoformalization Prompt
[TASK]
Your task is to interpret the natural language (NL) description of 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]
Use V to represent disjunction
Use A represent conjunction
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.
occurrences 'c"", where is a character from the alphabet (see example in Table For the other LLMs, it was quite common for the explanation to not give the actual character (see example 4 in T). Overall, we observed a higher likelihood of SOTA LLMS hallucinating on regular expressions compared to the other datasets.
The most common mistake when constructing a regular expression from natural language misplacing or adding it when it not needed (see example Table5). Finally, even though we explicitly prompted the LLMs to use just sometimes the LLM would use
Autoformalization Errors:
H STANDARD DEVIATION EVALUATION
In this section, we perform an empirical analysis the standard deviation of the syntactic compliance and accuracy of the VutoEvAL results. Due 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 Vuto 10 times the first batch of each dataset
22

---

The pattern consists of zero or occurrences of the Published as a conference paper at ICLR 2025
Prompt 8:
First-Order Logic Verification Prompt
Your task 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 yes no.
[Formula 1] Er1. (pr.:(ped)(p7)
[Formula 2] 3p7. 3p7.-pred5(p7)
Table 5: Examples of errors the evaluated LLMss made while evaluating with VutoTVAL for the regular expression dataset.
I(p))
o
The pattern consists of one or more occurrences of the digit "I" 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.
1"0
(1*)10
(1*)r0
((1))0)*
1*11* digit '1,, followed by exactly one occurrence of the digit '1' followed by zero or more occurrences of the digit I Zero or more occurrences of the character or group of characters before the asterisk.
1*1*1*
(1)*0
(+*
composed of 1974 propositional logic, 1900 first-order logic, and 1842 regular expressions examples. Additionally, we evaluated GPT-3.5-turbo (ChatGPT) with temperature Diarral-v.227--Instttu and Phi-3-medium--Kkinstteee deviation of each independent run of VutoEVAL and plotted the results in Figure
ALLam-3--B-Insstuue
We calculated the mean and standard
ChatGPT
Phi
Mistral
LLama3 FOL(8, 12)-E
3-CNF(12)
Propositional Logic(12)
FOL(S, 12)-5
Regular Expression
L.00-
Syntactic
Compliance
0.75
0.30
0.22
0.00
1.00-
Yuto3wnL
0.50
0.25
0.00
201
30
50
10
20
20
300
40
10
30
40
10
200
Operators: A,
counted operator iff succeeded by terminal)
CFG Parse Tree Depth
Figure 8: Average and standard deviation error of Zero-shot Pass results from using Yuto3vAL to assess LLMs w.r.t. ŠAI and $A2 (Sec. (.3.1I on the first batch of the packaged datasets. The x-axis represents an increasing order of descriptional complexity.
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
23

---

Published as a conference paper at ICLR 2025
better performing models having lower standard deviation. Overall, this experiment shows that the noise of non-deterministic text generation does not significantly impact VutoEVAL or our results and evaluations.
I ADDITIONAL ZERO-SHOT PROMPTING RESULTS
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 (A, V, -). For regular expressions, we have discussed the main paper that each regular expression represents a minimal deterministic finite automata (DFA) that is unique up to isomorphism. Therefore, the other categorization metrics for regular expressions the number of nodes V, the number of edges E, and the density of this minimal DFA. The density is calculated using [ where we discretize the value by rounding every tenth.
E
Densily VI(V
Imbalanced Dataset Labels Due to the datasets being created by sampling equal number of expressions for each number of operators, taking this dataset and evaluating in terms of the other metrics results in imbalanced dataset. To examine this effect, have created Figures 9 and I0 to perform an analysis of dataset imbalance on these other metrics.
For propositional and first-order logic, the dataset is actually quite balanced due 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 the extrema, the noise from the imbalanced data will be marginal.
The regular expression dataset is less balanced due 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.
Density
of Edges
of Nodes
Regular Expressio ()
05
0.1
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 12 14 and 15 the performance of each LLM over these other categorization metrics are shown. Across the board, we observe 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 similar behavior as the operator number. Propositional logic performance was concave w.r.t the number since it becomes easier describe expressions composed of exclusively A and V operators. A similar, but weaker pattern is observed the first-order logic results for the same reason. The negation operator not concave, showing how L.MSs struggle to handle multiple negation operators.
and V operators
24

---

Published as a conference paper at ICLR 2025
CFG Parse Tree Depth
# of Operators
# of Operators
# of Operators
Propositional Logic
13-15
16
46
19-21
25.27
26-30
37 39
12
36
FOLi8, 12)
19-21
22-24
40
37-39
10
10 12
FOLiS, 12)-E
19-2
22-24
40-42
18
35
20
34-36
15
Figure 10: Count 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 pic charts increase value counter-clockwise while going from lighter darker.
ChatGPT
GPT-4o
GPT-Mo-mini FOL(8, 12)-5
Phi3
Mistral
LLama3
Other LLMs = 10)
Propositional L1gic(12)
FOL(S, 12)-E
Regular Expression(2]
Compliance
1.00-
Syntacii
0.75
0.50
0.25
0.00
1.00-
YutoaNAL
0.75
Score
0.50
0.25
LLMs Verifiers
1.00-
V Score
0.75
0.50
10
20
30
40
10
20
30
40
10
20
30
40
0
10
20
30
40
CFG Parse Tree Depth
Figure 11: Zero-shot Pass @ results (avg. over 10 batches, higher values better) from using VutoEVAL to assess LLMs w.r.t. $A1, $A2, $A3 (Sec.B.3.1 on the packaged datasets. The x-axis the depth of the CFG tree to produce the formula.
For regular expressions, increasing the number of nodes and edges reduces accuracy and the ability to evaluate equality. Density does not seem to be factor, the dip at 0.1 can be associated with noise due to the lower number examples. Overall, these three metrics are much weaker factors in how well the LLM performs compared the CFG tree depth.
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 SA2.
25

---

Published as a conference paper at ICLR 2025
ChatGPT
GPT-4o
GPT-4o-mini
Phi3 FSL 12)-5
Mistral
LLama3
Other LLMs 10)
Propositional Log)c[12)
FOL(8,
Compliance
1.00
Syntactic
0.77
0.50
0.25
1.00
Yuto3
0.75
0.50-
0.25
0.00-
LLMs Verifies
89 Score
0.75
0.50
0.255
0.00
25
10
20
25
* Operators:
Figure 12: Zero-shot Pass results (avg. over 10 batches, higher values better) from using VAto assess LLMs w.r.t. $A1, $A2, $A3 (Sec.B.3.I)) on the packaged datasets. The x-axis is the number of and operators (A) in the expression.
ChatGPT
GPT-4o
GPT-4o-mini
Phi3
Mistral
LLama3
Other LLMs 10)
Propositional Logic(12)
FOL(S.
FOL(8, 12)
Compliance
1.00-
Syntactic
0.75
0.30
0.95
L.00-
LLMs Verifiers YutoJ
0.75
0.30
0.25
0.00
0.75
0.50
0:25
0.00
1b
20
25
# Operators:
Figure 13: Zero-shot Pass @ results (avg. over 10 batches, higher values better) from using VuLo assess LLMs w.r.t. $A1, SA2, $A3 (Scc.(3.3II) on the packaged datasets. The x-axis is the number of or operators (V) in the expression.
26

---

Published as a conference paper at ICLR 2025
ChatGPT
GPT-4o Propositional L1gic(12)
GPT-4o-mini
Phi3
Mistral
LLama3
Other LLMs = 10) FOL(8. -
FOL(S. 12)
Complince
1.00
Syntactic
0.77
0.50
0.25
0.00
1.00
LLMs Veriliers Yutoz VAL
0.75
Score
0..00
0.25
0.00
1.00-
(3 Score
0.75
0.50
0.00
12
# of Operators: (counted as an operator iff not succeeded by terminal)
Figure 14: Zero-shot Pass @ results (avg. over 10 batches, higher values better) from using Vuto to assess LLMs w.r.t. $AI, SA2, $A3 (S.c.3.3.I) on the packaged datasets. The x-axis is the number of negation operators (-) in the expression.
ChatGPT
GPT-4o
GPT-4o-mini
Phi3
Mistral
LLama3
Other LLMs (n
Compliance
1.00
Syntactic
0.75
0.50
0.25
1.00
LLMs Verfiers Yuto3
0.75
0.25
0.00
0.75
0.50
42 0.95
0.00
12
0.4
Nodes
of Edges
Density
Figure 15: Zero-shot Pass@ results (avg. over 10 batches, higher values better) from using VAL. to assess LLMs w.n.t. $A1, $A2, $A3 (S... on the packaged datasets. The x-axis the metric on the CFG tree to produce the regular expression formula.
27

---

Published as a conference paper at ICLR 2025
ChatGPT Propositional L2gic(12)
GPT-4o-mini
Mistral
LLama3
FOL(8, 12)-5
FOLÍ8, 12)-E
Regular Expression
Syntactcc
Compliance
0.75
0.50
0.00
0.25
1.00
Vato3
Score
0.95
0.75
10
# Operators: A, V, (n counted as an operator not succeeded by terminal)
CFG Parse Tree Depth
Figure 16: Syntactic compliance and accuracy difference of few-shot Pass@ compared to zero-shot Pass @1 1 results (avg. over 10 batches, higher values better) from using vutoEvAL to assess LLMs w.r.t $A1, $A2, $A3 SSc..3.3.1 on the packaged datasets. The x-axis represents the increasing order of descriptional complexity.
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 T6] the performance difference 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 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 AUTOEVAL PREDICTIVE POWER EVALUATION
For evaluating the correlation between LLM's performance Vuto and existing benchmarks and measuring the predictive power of VVLL, in Section 4.2 we evaluated on FOLIO (Han et al.
2024 Multi-LogiccEal (Patel et al. 2024). and HumanEval (Chen al. (222). In this section discuss these experiments and cite the sources of the HumanEval results along with evaluate the predictive power of Vuto]VAL.
In this section, we discuss the experimental setup for the benchmark, the sources used for LLM performance on other benchmarks, and the Vuto3VAL we used for evaluation. We also evaluate the FOLIO premise benchmark further based on the operator numbers in each premise.
K.1 FOLIO EXPERIMENTAL SETUPS
The FOLIO dataset is composed of premises and conclusion for each sample where the task is conclude whether the conclusion is true, false, 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 L.LM on their abilities to (1) informalize a first-order logic premise, (2) autoformalize 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.
For the FOLIO premise informalization and autoformalization experiments, the LLM was prompted using the same few-shot first-order logic prompt used by VutoEVAL where the example from the 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 that were able
28

---

Published as a conference paper at ICLR 2025
Prompt 9: FOLIO Premise Informalization Prompt
[TASK]
Your task is to convert 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]
Vz (Diinikk Regularlyl (z, fee) (-W oe o(x, ca. feine))) People regularly drink coffee, or they don't ton't want to be addicted to caffeine, or both.
[VOCABULAYY]
represents disjunction
represents conjunction
represents negation
+ represents implication and represent parentheses propositions can be used verbatim predicates be used verbatim
< æ1 >< x2 > < xn represents universal quantification with xl... representing
free variables
3 << æ1 >< x2
on represents existential quantification with xl... representing
free variables
The objects are: caffeine
The parameterized
predicates
are:
awarethatdrug(?p). ?p1).
wonttobeadddcceedoo (?p0, ?p1)
The free variables are: x
[FORMULA]
Vx. (=wonttobendddiceed(((. ea feine) + -wwrrthatdruggsr.cm feinne)
parse them into Prover9. Prompt and 10 shows example prompts using example premises come from the FOLIO dataset.
For evaluating the performance of each LLM on classifying whether the premises entailed the conclu- sion, the same prompt 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 Chain-of-Thouur prompting and prompt the model to provide the answer in parsable format. Prompt T1 and Prompt 12 are examples of these prompts using an example from the FOLIO dataset.
We evaluated the informalization results against the ground truth natural language representation using BLEU (Callison-Burch et | 2006), ROUGE (Lin) 2004), METEOR (Banerjee & Lavie (2005), and BERT Score (Zhang* et al. 2020). The model Saberta-xlarge-nne 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.
(He al. [002]) was used for
K.2 MULTI-LOGIEVAL EXPERIMENT SETUP
The task in Multi-LogicEVvll PPttel et al. 2024) is to answer 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 to provide the answer in a specific location to parse. Prompt [3 shows an example of this prompt using examples from the Multi-LogiiEval dataset.
Chain-of-Ti Thouuht prompting and prompt the LLM
29

---

Published as a conference paper at ICLR 2025
Prompt 10: FOLIO Premise Autoformalization Prompt
(VOCABULARY)
Use V to represent disjunction
Use A to represent conjunction
Use represent negation
Use ( and ) to represent parentheses
The objects are: caffeine
The parameterized predicates are: awarethatdrug((p), ?p1),
worlloheaddicledde The free variables are: x:
?p1)
[TASK]
Your task interpret the natural language (NL) description of 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 INL DESCRIPTION] tag.
[EXAMPLE 1]
People regularly drink coffee, or they don't want to be addicted to caffeine, or both. Vx(Drink Regularby(z; coffee fee) (-WantToBeAAddeteeeee (1, ca feine)))
[NL DESCRIPTION] No one who doesn't t want to be addicted to caffeine is unaware that caffeine is 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] True/False/Uncertiin based on the [PREMISES]. Use the following answer format:
Reasoning Steps:
Answer: True/FalseUnncertiin
[PREMISES]:
All people who regularly drink coffee are dependent on caffeine
People regularly drink coffee, or they don't itn't want to be addicted to caffeine, both.
No one who doesn't t want be addicted to caffeine unaware that caffeine is drug.
Rina is either student who is unaware that caffeine is drug, or she is not a student and is she aware that caffeine is drug.
Rina is either a student who depend caffeine, or she is not student and not dependent caffeine.
[CONCLUSION]]
Rina doesn't It want to be addicted to caffeine or is unaware that caffeine is a drug.
K.3 HUMANEVAL AND BIG BENCH HARD SCORE SOURCES
To evaluate the correlation and predictive power of Vuto against commonly used LLM bench- marks HumanEval (Chen et al. 2021) and Big Bench Hard (BBH) (Suzgun et al., (202)), we collected the performance scores of the LLMs evaulated on both benchmarks and report findings and sources in Table 6 We were unable to find any sources that evaluated GPT--0-mini on BBH.
K.4 COMPUTED CALIBRATED YUTOEVAL SCORE
To compare against the performance on different benchmarks in Section 4.2
we needed to calculate the calibrated performance of each LLM VutoEVAL for the relevant portions of the datasets. For example, there are few premises in the FOLIO dataset with more than operators meaning that the most accurate comparison would be to evaluate first-order logic dataset up the same number of
30

---

Published 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 Tmne/False/Uncertainn based on the [PREMISES]. Use the following answer format:
Reasoning Steps:
Answer: True/False/Uncertain
[PREMISES]:
dx Drinnkkeggulalllaa cof fee) - IsDependentOn(, feine))
Vx Drink Regularly(s (z, cef) (-WantTooee Addicled o(2, co. feine)))
vx -W antToBe Addicttd of,, feine) - -Awar e ehao Drugla, ca (rrerrrcaaaeeinee feine)
( (Student(rino) @ -wware DruggeTThaDDuurriinnn ca feine)
- (1s [LssependentOn(rine ca feine) @ Student(rina))
[CONCLUSION]:
oontToBe o(rina, ca feinc) V (~AwareThaatrrugrrinn ca feine)
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 '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, 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 HumanEval and Big Bench Hard (BBH) benchmarks. The values under the Computed column averaged over from experiments. Other results 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
BBH Score
Computed
(Online)
(Online)
ChatGPT
74.3
68 (OpenAl
2024
48.1
OOenAAl 2023
GPT-4o
91.8
90.2
OpenA
2024
83.1
Dunham & Syahputra
2024
GPT-4o-mini
88.3
87.2 OpenA
2024
L.ama-3.2-1B-Insttee
34.6
8.7
FForrrie et al.
2024
2.5-1.BBB Instruct
56.7
61.6
(wwen2
2024
19.8
Fourreer el a
2024
Phi-3.5-Mini Instrulnstruct
71.3
64.6
(Lu et al
2023
36.7
Fourrier et al
2024
Mistral-7B 7B-Insstuctt-O0.
44.5
42.1
(Liu
2025
24.0
Fourrerr
20224
LJama-3-8B-Insiee
62.8
61.6
LLu
202.
24.5
(Forrer
Granite-3.0-88 -iiee-3.---8---sttrree
62.2
64.6
Granite caam
2024
51.6
(Furriir ct ml
20224
Llama-3.1 1-8t-tnstruct
63.4
66.5
Microsoft
2024
63.4
(Mcrosoft
2024
76.8
76.8
MistralAT
2024
8.7
Fourner et al.
2024
Gemma-2-9B-IT
68.3
68.9
Qwen2
2024
42.1
Fourrer
2024
Phi-3-Medium-44-Ine
75.0
62.2
Microsoll
2024
49.4
Fourrer el al.
2024
Qwen-2.5 2.5-1-2..-1BB---- 14B-Instruct
80.5
83.5
(wenZ
2024)
48.4
Fourrier ct al
2024
Yi-1.5-34B-Innsie
72,6
75.2
YY 2024)
44.3
Fourrier et al
2024
Llama-3-70B 3-70B-Instruet Instruct
79.9
77.4
Liu et
2023
50.2
Fourreer al.
2024
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 Multil Multil.ogiEvas LogiEval, the number of
31

---

Published as a conference paper at ICLR 2025
ChatGPT FOLIO (A)
GPT-4 FOLIO (Z; BLEU)
LLama3 FOLIO (Z; ROUGE)
Mistral
Phi
-PT--o-mini FOLIO (Z; BERT)
FOLIO (7; ME METEOR)
Benchmark Score
6.00
0000
0.00
0.00
.75-
.25-
.25
.15
-15
.75
25
10
Vuto VAL Score
Figure 17: Correlation between the parameterized Vut. score and hoth autoformalization A and infor- malization I for FOLIO premises. Each point represents specific number of operators with arrows showing increasing complexity (number of operators). The trendline across all the points annotated with x, the Pearson correlation coefficient (p). and the p-value are annotated the top left.
operators is dictated by the depth of the rules, so we took the average of all first-order logic examples up 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 4.2 we evaluated the correlation of other benchmarks compared to VutoIVAL. For the FOLIO dataset, we were able to calculate the exact number of operators in each problem, allowing us 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 generated.
We plot these results Figure 17 with the Pearson correlation coefficient. Each figure shows a moderate strong correlation with statistically significant p-value of less than 0.05. As the compu- tational complexity increases, performance on VuLo autoformalization, and informalization decreases. The autoformalization correlation significantly stronger due 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 $A3, where we evaluate the performance of using a LLM to verify whether the formal syntax expression yp is equivalent to the one produced by GPT-4o after doing A I(p)) Figures 21 and 22 show the number of positive and negative examples. Additionally, it breaks down the performance of each LLM on each dataset.
The LLMs are clearly biased towards giving positive answers with high ratio 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 (AA o Z)" (1p) where Po = [FORMULA 1].
In the case of Output Example I can be clearly seen that ChatGPT failed to understand that the two formulae are different. In particular, was not able to correctly evaluate or reason that the second regular expression represents string that begins with followed by zero one O's. This is despite the LLM using a ofbain-ff-thought to help arrive at an answer.
A more glaring reasoning error is found in Output Example 2 where ChatGPT fails to apply the principles logic where --p = # <p. Our results convincingly showcase that LLMs cannot be used verifiers even for straightforward statements such the examples presented.
32

---

Published as a conference paper at ICLR 2025
Output Example 1: Regular Expression Verification Example
Prompt:
Your task is to say whether two Regular Expression formulac are equivalent. The first formula will appear right after [FORMULA 1] and the second after [FORMULA 2]. Give an explanation followed by or no answer. The answer must show up at the end with the format "[Answer]" followed by either yes no.
[FORMULA I]: 100*
[FORMULA 2]: I(0%)
Response:
To determine whether the regular expressions 100* and (0x) equivalent, let's analyze
them:
### Explanation:
1. Formula 1: 100*
-This matches the character "1" followed by zero or more "O"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 Formula 1). It will also match: "1", "10", "100", "1000", etc.
### Key Observation:
Both formulas describe the same set strings: a "I" followed by zero or more "O"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: Frstt-Ordrr Logic Verification Example
Prompt:
Your task is say whether two First Order Logic formulac equivalent. The first formula will appear right after [FORMULA 1] and the second after [FORMULA 2]. Give explanation followed by yes
answer. The answer must show up the end with the format "[Answer]" followed by either yes or no. [FORMULA I]: Vxl. (-1.(--pr) prppprrdssp (p8, p7) -predA(x1)) [FORMULA 2]: Vxl. (-pred--edS(p)) p7) V predA(al))
Response:
The two formulas are equivalent.
Explanation: In both Formula 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 absence of double negation does not affect the truth value in this context. [Answer]: Yes
M DATASET DIVERSITY
Fig. and Fig. provide additional details on the types of data present in the datasets packaged with Vuto VAL. Users can generate dynamic datasets along these dimensions using the hyperparameters mentioned in Table[]
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 pı be represented via different propositions where p1 It raining in fi and
33

---

Published as a conference paper at ICLR 2025
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 element of vocabulary of size 1. For example, all variables used PL((2) dataset our results are replaced by substituting those variables with vocabulary of only proposition. Excess parentheses
preprocessed using NLTK and removed before the substitution (e.g. ((P)) A P2) is simplified to pi A p2.
The k-CNF 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 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 OpenAl API for the GPT family of models. We cover diverse range of models in our evaluation ranging from extremely small LMs with a few billion parameters (~1B) LLMs with several billions of parameters. This allows the analysis of VutoEVAL from the lens of generalization.
Fig. represents the syntactic compliance (5A1) data from Fig. F for all the models with separate axis for each L.M. Similarly, Fig. 19 plots the Accuracy (GA2). Additionally, Fig. 20
20 plots the F1 score of using LLMS as verifiers (3A3). Tables 9 14 provide the data that was used to plot the results in Fig. and to compute the predictive power in Fig.
Tables list the example counts for each combination of class label and prediction for FOLIO(R; NL) and FOL FOL) and each label's precision and recall rate. Tables 19 and 20 list the examples
counts for each combination class label and prediction for LogiEval PL) and LogieEval(R; FOL).
N. CLAUDE EVALUATION
We evaluated Claude 3.0 Sonnet on just the 3-CNF, propositional logic, and regular expression datasets due the cost. Our results are shown Figure 23 and show that Claude 3.0 Sonnet performs similarly to GPT-4o with both having nearly perfect syntactic compliance and accuracy on 3-CNE 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.
34

---

Published as a conference paper at ICLR 2025
Table The LLMs used our evaluation. label names represent the used Fig. 18 and Fig.
represents the total number of parameters, and the last column lists the exact version used (for reproducibility).
Label
[0]
Version
ChatGPT
GPT-3.5-turbo--00
GPT-4o
gpt-4o-2024-09-03
GPT-4o-mini
gp2-40o-arr1222240000-1
GPT-4o1
01-prrvvlex-2222--3--2
Llama-3.2-IB-Instie
1B
Dwwn-2.5-115B-Insttre
1.5B
Phi-3.5-Mini-Insttuuc
4B
Mistral-7B-Inssrutt-00.2
Llama-3-8D-Inttruc
8B
8B
1--ma-3.1--B-Instruee
8B
Gemma-2-9B-IT
9B
googlaa/eemma222--111111
Phi-3-Mediumm444-nnsnuutt
14B
Owen-2.5-14B-Instru
14B
wver//peen2.55-14--nnttteeee
Yi-L.5-34B-Instie
34B
01-at/ta-34B-Instrut
LLama-3-70B-Insttee
neta-LLana//llaaa33-1000
Table Correlation data FOLIO(R; NL). Vuto data was averaged from dataset data
points with description complexity < 6. These values were used compute the predictive power Vuto reported in Fig
Model
VutoEVAL Score
FOLIO(R; NL) Score
GPT-4o
0.79
0.75
GPT-4o-mini
0.56
0.69
ChatGPT
0.36
0.56
Mistral-7B-Inee 2
0.06
0.54
Phi-3-mediim--k--intrruue
0.35
0.67
LLama-3--B-LLstree
0.13
0.58
Gemma-2-9B-I
0.28
0.64
Granite-3.0.e Siattte-.--8--Instttee
0.18
0.60
Llama-3, 1.1ma--..--B-mmme --8t-nsrttutt
0.09
0.59
LLama-3.2-11 3.2
0.03
0.36
LLama-3-70B-Instuu
0.49
0.70
Ministral-SB--nnstuue2-444
0.10
0.61
Phi-3.5-Mini-Instreee
0.19
0.61
Qwen-2.5-1.55
0.07
0.49
Dw5n-225-14BBB
Instruct
0.67
0.73
Yi-1.5-34B
0.21
0.63
35

---

Published as a conference paper at ICLR 2025
GPT-4b
Lama- 1hmm---1--B--iinn 1-8B-immtrutt
PH-S Meiislleiine
GPI 4omm
LLama 3-at-/rctruct
Instrct
-*-.
Minatrl-88-lnstuuettee
Y-1.5-946
Propositional (1)
FOL(8, 12)-5
FOL(8, 12)-E
Regular Expression
GPT-40
GPI -lomm
ChorPPT
0-
Mitts-PBhnttursa2?
Mii--Medum
LLamaa3 1arra-3----eeteee
Gomma 2-18-I7
Syntactic Compliance
+ Llama 1-B--iitttctt
m Amsnggn A/
LLama
3.70 Instect
Minit 2410
Mri-3.5 Miniinsruct
Queen 2 St-indtrct
Queen 5:148-hnerutt
20
20
10
# of Operators: A, V, (7 counted operator iff not succeeded by terminal)
CFG Parse Tree Depth
Figure 18: Syntactic compliance (GA1) all models on the VutoEVAL datasets.
36

---

Published as a conference paper at ICLR 2025
GPT-4b
Lima- 1-8B-immtruct
PH-- S-Miniletteee
GPI 4omm
LLama 3-at--rctruct
3.2-1-rrettuct
Instrct
-*-.
Minatrl-88-/rsttutte
Y-1.5-946
Propositional 12)
FOL(8, 12)-5
FOL(8, 12)-E
Regular Expression(
GPT-40
ChorGPT
Mitta-7Bhhetur-ah?
PhoS-Medum-deeeete
LLama-3 h-itt
Gomma 2-1B-I7
Grailed C- heee
Vuto3vAL Score
LLama-32.JBB Iutruct
LLama 3-70a-3-------
Miniz instrct 2410
Owee- 5-3 Instrcct
Hoge Yod 5-348
04
20
0
40
20
10
# of Operators: V, m (- counted operator iff not succeeded by terminal)
CFG Parse Tree Depth
Figure 19: Vuto3VAL Score ($A2) all models on the Vuto3VAL datasets.
37

---

Published as a conference paper at ICLR 2025
Gemma-2-4B-T
Miristra- Sinttra--B---ettm---111
ChardPT
Grarito 30 6B husnuct -.....
Ph. 25-35--Mi--ran Mii-irstrcct
GFT-4o
Y-L5.34B
1ima- 14B--mttrrtt
Qown-) 5-1 SR-Inetruct
Mistral-B--ie
Propositional Logie 12)
FOL(8, 12)-5
FOL(8, 12)-E
Regular Expression
Genma-2-ff-11
Liana 311 8B Instract
11ama-3 2u1B-brrrttt
Phi.3.5 Man-instuo
LLMs as Venliiers Fi Score
Queen
CIatGPT
GPT-4b
--- Pri3--Meuu-4e-alle
Mitral-B v0
0
40
20
10
# of Operators: A v. (- is counted as an operator not succerded by terminal)
CFG Parse Tree Depth
Figure 20: LLMs verifiers Fl score (5A3) for the GPT-4o results using the Vuto procedure of all models on the VVLL datasets.
38

---

Published as a conference paper at ICLR 2025
True Labels
True Positive
Non-compliant (True Label)
False Positive
False Labels
False Negative
True Negative
Non-compliant (False Label)
fol fol_human human
ksat
plogic
fol
regex
GPT-40
ChatGPT
Mistral
Phi3
Uamm33
Gemma2
Granite
Llama3.1
The number of positive and negative examples of (2 A I(yoo) when evaluating GPT-4o on vuto3VAL for each dataset (inner donuts). Additionally included 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 fewer. Non-compliant represents syntactically non-compliant responses when prompted to verify the equivalence.
Figure 21:
39

---

Published as a conference paper at ICLR 2025
True Labels
True Positive
Non-compliant (True Label)
False Positive
False Labels
False Negative
True Negative
Non-compliant (False Label)
fol homhhmma
ksat
plogic
fol
regex
Liamasi 2
Liarma3(708)
Ministral
Phi 5-mini
Owen2.5(1 (1 58)
Qwen2. 5(148)
Yr-15
Figure 22: Additional LLMs evaluate on $A3, where the number of positive and negative examples of (P1 o I(Po) when evaluating GPT-4o on VutoEVAL for each dataset (inner donuts). Additionally included is a breakdown of the performance of each LLM when acting as the verifier (outer donuts). Included all examples containing 20 fewer operators or, in the of the regular expression dataset, CFG tree depth of 20 or fewer. Non-compliant represents syntactically non-compliant responses when prompted to verify the equivalence.
40

---

Published as a conference paper at ICLR 2025
(12)
PL(12)
FOLÍS. 12)
Syntactic Compliance
Operators: A.V. (n counted as an operator ill not succeeded by a terminal)
CFG Parse Tree Depth
Figure 23: VutL results Claude 3.0 Sonnet the 3-CNF, propositional logic, and regular expression datasets. Dashed line is the accuracy.
Table Correlation data FOLIO(R; FOI.). The calibrated VuLo score was calculated from FOL. dataset with data points with description complexity d S 6. These values were used to compute the predictive power of VuLL reported in 5
Model
Vuto]vAL Score
FOLIO(R: FOL) Score
GPT-4o
0.79
0.71
GPT-4o-mini
0.56
0.67
ChatGPT
0.36
0.51
Mistral-7B-Inen -B-IInructt-oOO.
0.06
0.51
Phi-3 2al-3-medium-44 44-instruct
0.35
0.62
LLama-3-88 Instruct
0.13
0.52
Gemma-2 2--9-III
0.28
0,59
Granite-3 --n-------BB-n-ttuuctt
0.18
0.56
Ilama-3.1-80 -88t-rrtt
0.09
0.56
L.Lama-3.-1IB-Imss-
0.03
0.36
1amma-3-7BB-Instreee
0.49
0.66
Ministral-8B-Instruee 24110
0.10
0.56
0.19
0.53
Qwen-2.551.5B-Instte
0.07
0.45
Owen-2.5-14B-Inntn
0.67
0.71
Yi-1.5-34B
0.21
0.61
Table 10: Correlation data for LogiEval(R: PL). The calibrated VutoaVAL score was calculated from PL
dataset with data points with description complexity d I 30. These values were used to compute the predictive power of VutoEvAL reported in Fig.5
Model
VutoJVAL Score
LogiEval(R; PL) Score
GPT-4o
0.67
0.87
GPT-4o-mini
0.35
0.67
ChatGPT
0.17
0.64
Mistral-7BB -errall-BB-Instrrce
1B-IIntructt-0.2
0.12
0.60
thi-2-mediimm-4k-nnnteee
0.23
0.75
I.Lama-3-BB-Insrruct
0.12
0.61
Gemma-2-99--T
0.28
0.71
Granite-3.0k 3.ttte-33.--B-Inttttte
0.21
0.58
Llama-3.1-4 I-nssrurtt
0.11
0.71
LLama-3.2-1B 3.2stutInstruct
0.04
0.50
1.lama-3-70B-Instmee
0.34
0.85
Ministral-8PB -n-ttttttttnss
0.17
0.68
9hi-3.5-Mimi--mm
0.10
0.62
Qwen-2.5-1.50 1.B--1..B-Inssrrcc
0.11
0.52
1wen-2.5-14B-Instrru
0.46
0.76
Yi-1.5-34B
0.26
0.78
41

---

Published as a conference paper at ICLR 2025
Table 11: Correlation data for Logi FOL). The calibrated VutoDwaL score was calculated FOL dataset with data points with description complexity d I 30. These values were used to compute the predictive power of vuto3vAL reported in Fig.
Model
Vvt. Score
LogiEval(R; FOI.) Score
GPT-4o
0.32
0.82
GPT-44-mini
0.17
0.56
ChatGPT
0.09
0.63
Mistral- -B- 7B-Instruct-v0.2
0.01
0.56
Mhi-3-mediumm44
0.09
0.70
LLama-3-8B-Inee
0.02
0.62
Gemma-2-9B-IB
0.07
0.69
Granite-3 Franite-3.0-8B--1 3.-ssttnstttt
0,05
0.55
Llama- 3.1 8---tttuuctt
0,02
0,68
LLama-3.22 3.2--1B-Instuuteee
0.00
0.47
LLama-3-70BB 3-0-m----00-nnsttuc
0.15
0.78
0.02
0.64
Phi-3.5-Mini-Insteen
0.04
0.54
1.ee-225-1.5B--nnmt
0.02
0.50
Owen-2.5-14B-Instuee
0.19
0.66
Yi-1.5-34B
0.05
0.71
Table 12: Correlation data FOLIO(A), calibrated VutoEvAL score was calculated from the FOL dataset with data points with description complexity d These values were used to compute the predictive power of Vuto reported in 5
Model
VutoIvAL Score
FOLIO(A) Score
GPT-4o
0.79
0.41
GPT-4o-min
0.56
0.40
CharGPT
0.36
0.33
0.06
0.19
Phi-3-mediim--4--nntttee
0.35
0.32
LLama-3-8B- Instructt
0.13
0.16
Gemma-2-9B..
0.28
0.30
Branite-300-8B-Instii
0.18
0.14
Llama-3.1 1-8B-Instruct
0.09
0.23
0.03
0.00
LLama-3-70BB 3-00m-------Itttruee
0.49
0.40
Simistral-BB-Instrue--222
0.10
0.23
Mhi-3.5-MiniiInsttee
0.19
0.18
Qwen-2.5-1.50 1...srucB-
0.07
0.10
Qwen-2.5-144 1.Bstuutt
0.67
0.36
Yi-1.5-34B
0.21
0.31
42

---

Published as a conference paper at ICLR 2025
Table 13: Correlation data for FOLIO(Z). The Vuto3VAL data averaged from the FOL dataset with data
points with description complexity Σ 6. These values were used compute predictive power Vuto3vAL reported in Fig
FOLIO(I) Score
Model
YutoEvAL Score
BLEU
ROUGE
METEOR
BERT
GPT-4o
0.79
0.14
0.42
0.64
0.71
GPT-4o-mini
0.56
0.13
0.41
0.61
0.73
ChatGPT
0.36
0.19
0.47
0.62
0.76
Mistral- BB-aal-----nntttttttee
0.06
0.08
0.64
Phi-3-Medium-44 4k-Instruct
Meedium-4--lmm
0.35
0.12
0.39
0.58
0.70
LLama-3-8B-mm
3-B-a--BB-Instruct
0.13
0.04
0.18
0.35
0.50
Gemma-2-9B-I
0.28
0.10
0.34
0.53
0.63
Cranite-3.0-8B-Insttee
0.18
0.15
0.41
0.58
0.72
Llama-3.1 8B-Instruct
1aama-3.-8B-Insttuuet
0.09
0.09
0.31
0,51
0.64
0.03
0.00
0.06
0.15
0.36
LLLma-3-70B-Inssn
0.49
0.12
0.40
0.60
0.70
Ministral-AD--nnttrttt2224
0.10
0.11
0.36
0.55
0.67
Phi-3.5-Mini Instrunst
0.19
0.05
0.22
0.41
0.55
Qwen-2.5-1.35 1.5-srctBt
0.07
0.09
0.33
0.49
0.65
Qwen-2.5-14B-Imm
0.67
0.07
0.26
0.45
0.55
Yi-1.5-34B
0.21
0.12
0.39
0.58
0.72
Table Correlation data for HumanEval (A).. The VutoEVAL 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 VutoIVAL reported in Fig.
Model
VutoEvAL Score
HumanEval (AA) Score
GPT-4o
0.66
0.92
GPT-4o-mini
0.44
0.88
ChatGPT
0.36
0.74
Mistral- Beitral-BB--ae
TB-Instruct-v0.2
0.20
0.44
1in---medium----innnteee
0.45
0.75
LLamm-3-8B-Insseee
0.07
0.63
Gemma-2-9B.
0.28
0.68
Sonnite3.-0-8B-mma
0.21
0.62
Llama-3.1-88 1-8B-Instruct
0.19
0.63
3Laam-3.2-IB-IIstterr
0.03
0.35
LLLama3-770--Issruu
0.33
0.80
Ministral-SB--nsstruct--2
0.13
0.77
0.36
0.71
Qwen-2.5-1155
1-5--.5B-nnntrue
0.12
0.57
D.wen-2.5114--Ime Ins-Iutt
0.45
0.80
Yi-1.5-34B
0.13
0.73
43

---

Published 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 LLM predicted True label as Uncertain.
Model
TT
TF
TU
FT
FF
FU
UT
UF
UU
GPT-4o
1667
125
147
178
1133
131
246
419
952
GPT-44-mini
1500
187
253
162
1087
196
255
488
877
ChatGPT
1501
281
147
366
889
186
620
562
434
Cystral-7B-Instructt
1301
205
412
200
717
508
525
387
691
1468
153
310
222
871
343
310
289
1009
LLama-3-8B-nastrul
1400
244
288
272
807
347
477
413
717
Gemma-2-9B-IT
1439
385
231
813
382
378
289
934
Granite-3.0-88 3.0--88-nn-tttrrt
1415
109
412
304
666
471
382
316
919
Llama-3.1 3.1-8B 11-8B-Insse Instruct
1400
174
314
267
766
360
435
352
781
LLama-3.2 1aama-3..2-1B-ime Instruct
1407
235
118
931
279
81
1109
235
111
I.
1677
101
161
263
966
214
419
319
881
1577
242
116
358
954
130
583
532
503
2hi-3.5-MinniInstiee
1355
164
398
223
821
383
357
359
890
Qwen-2.S 2.5---2.-1..B--. --5--Instt
1470
345
117
615
684
138
824
477
309
Qwen-2.5-14B-Instnee
1564
132
239
215
1020
207
266
276
1058
Yi-1.5-34B
1507
125
298
240
894
305
497
346
773
Table 16: Calculated precision and recall for each label in FOLIO (R:NL).
True Label
False Label
Uncertain Label
Model
Prec.
Rec.
Pree.
Rec.
Prec.
Rec.
GPT-4o
0.80
0.86
0.68
0.79
0.77
0.59
GPT-4o-mini
0.78
0.77
0.62
0.75
0.66
0.54
ChatGPT
0.60
0.78
0.51
0.62
0.57
0.27
Mistral- -B-
77--Instruct-OO.
0.64
0.68
0.55
0.50
0.43
0.43
Phi-3-medium--kkinntttte
0.73
0.76
0.66
0.61
0.61
0.63
ALama-3-8B-Instruc
0.65
0.72
0.55
0.57
0.53
0.45
Gemma-2-9B-IT
0.70
0.75
0.68
0.57
0.55
0.58
Granite-3.00 B.aeee3..------ttttt
0.73
0.61
0.46
0.51
0.57
Llama-3. 1.1-aa3..-B-IIstttttt
0.67
0.74
0.59
0.55
0.54
0.50
-Lamm-332-11B In-ttrucct
0.41
0,80
0.37
0.22
0.36
0,08
1.Lama-3-70B-nsstee
0.71
0.86
0.70
0.67
0.70
0.54
-nnistal-8B--nssruce-22
0.63
0.81
0.55
0.66
0.67
0.31
Phi-3.5-Mini-Instrics
0.70
0.71
0.61
0.58
0.53
0.55
1wen-2.5-1.5B-Innse
0.51
0.76
0.45
0.48
0.55
0.19
Qwen-2.5-14B-IInttee
0.76
0.81
0.71
0.71
0.70
0.66
Yi-1.5-34B
0.67
0.78
0.65
0.62
0.56
0.48
44

---

Published as a conference paper at ICLR 2025
Table 17: Count of examples in FOLIO(R; FOL) for cach combination of (T)rue, (F)alse, and (U)nerttain label and predictions in that order. For example. TU is the number of times LLM predicted True label as Uncertain.
Model
TT
TF
TU
FT
FF
FU
UT
UF
UU
GPT-4o
1596
124
218
215
1004
224
329
359
932
GPT-4o-mini
1432
140
367
153
944
348
224
420
976
ChatGPT
1500
208
227
456
711
266
756
525
338
Bistral-7B-Instructt
1159
244
521
229
616
575
503
335
760
Thi-3-mediumm-4-innttte
1405
120
393
278
688
457
365
226
1014
LLama-3-8B-nnstrul
1471
193
249
462
621
332
674
396
532
Gemma-2-9B-IT
1378
112
408
256
659
489
397
919
Granite-3.0-88 3.8--8B-nn-tttrrtt
1428
181
317
373
596
458
530
325
755
Llama-3.1 3.1-8B11..B 11-8B-Insee Instruct
1449
163
305
358
647
409
575
289
725
1.-mma-3.2-1BIIsstti Instruct
1436
232
127
969
239
96
1142
237
117
1661
122
149
390
829
224
576
248
791
Ministral-8FP -0-tral--8--Isstmtt-244111
1525
180
452
805
185
692
464
2hi-3.5-MinniInsttee
1291
145
449
314
595
503
466
331
791
Qwen-2.S 2.5e--2.-1..B--. 1.5--Instret
1305
358
255
611
560
256
829
392
386
Qwen-2.5-14B-Instnee
1648
90
194
279
918
241
377
253
966
Yi-1.5-34B
1513
106
285
730
350
476
282
826
Table 18: Calculated precision and recall for each label in FOLIO(R; FOL).
True Label
False Label
Uncertain Label
Model
Prec.
Rec.
Prec.
Rec.
Prec.
Rec.
GPT-4o
0.75
0.82
0.68
0.70
0.68
0.58
GPT-4o-mini
0.79
0.74
0.63
0.65
0.58
0.60
ChatGPT
0.55
0.78
0.49
0.50
0.41
0.21
Mistral- -B- 77--Insrruct--O.
0.61
0.60
0.52
0.43
0.41
0.48
Phi-3-medium--kk-nntttee
0.69
0.73
0.67
0.48
0.54
0.63
ALama-3-8B-Instruc
0.56
0.77
0.51
0.44
0.48
0.33
Gemma-2-9B-IT
0.68
0.73
0.63
0.47
0.51
0.58
Granite-3.0- -..nite-3.0-8B.. 3.0-8B-Insttruuc
0.61
0.74
0.54
0.42
0.49
0.47
Llama-3. 1.1-aa3..-B-IIItttttt
0.61
0.76
0.59
0.46
0.50
0.46
-Lamm-332-11B In-ttructt
0.40
0,80
0.34
0.18
0.34
0.08
1.Lama-3-70B-nsstme
0.63
0.86
0.69
0.57
0.68
0.49
Ministral-8P -0--rra-----Istttu--241110
0.57
0.79
0.54
0.56
0.56
0.29
Phi-3.5-Mini-Instrice
0.62
0.68
0.56
0.42
0.45
0.50
Qwen-2.5-1.55 1.nn2..5-..SBInstrrre
0.48
0.68
0.43
0.39
0.43
0.24
Qwen-2.5-14B-Instee
0.72
0.85
0.73
0.64
0.69
0.61
Yi-1.5-34B
0.67
0.80
0.65
0.53
0.57
0.52
45

---

Published as a conference paper at ICLR 2025
Table 19: Number of examples of true positives (TP), false positives (FP), true negatives (TN), and falsc negatives (FN) for each LLM in LogiEval(R: PL). The counts for when the LLM was non-compliant with our prompt for positive (NP) and negative (NN) labels also provided. Additionally, the calculated true positive rate (TPR), true negative rate (TNR), precision, and score each LLM shown.
Model
TP
FP
TN
FN
NP
NN
TPR
TNR
Prec.
Fl
GPT-4o
1724
56
594
251
0
0
0.87
0.91
0.97
0.92
GPT-4o-mini
1310
116
534
665
0
0
0.66
0.82
0.92
0.77
ChatGPT
1348
260
390
625
2
0
0,68
0.60
0.84
0.75
1240
379
640
95
0.66
0.67
0.87
0.75
Phi-3-medium 44-instruct
1558
197
452
411
6
0.79
0.70
0.89
0.84
LLama-3-8B-Insiie
1246
209
434
715
14
7
0.64
0.67
0.86
0.73
Gemma-2-9B-II IT
1464
217
432
497
14
0.75
0.67
0.87
0.80
Granite-3.0-B--Instruc
1106
168
482
869
0
0.56
0.74
0.87
0.68
Llama-3.1-8B-Ime
1523
400
430
22
0.78
0.62
0.86
0.82
ALamm-3.2-IB-IIsttme
985
250
342
820
170
58
0.55
0.58
0.80
0.65
-Lama-3-70B-Instren
1741
142
507
223
11
0.89
0.78
0.92
0.91
1350
161
489
621
4
0
0.68
0.75
0.89
0.78
3.5- Instructt
1222
719
34
0.63
0.72
0.87
0.73
1085
281
298
582
308
71
0.65
0.51
0.79
0.72
Qwen-2.5-14pp
1474
72
574
486
15
4
0.75
0.89
0.95
0.84
Yi-1.5-34B
1651
193
457
321
3
0
0.84
0.70
0.90
0.87
Table 20: Number of examples of true positives (TP), false positives (FP), true negatives (TN), and false negatives (FN) for each L.I in LogiEval(R; FOI.). The counts for when the I.I.M non-compliant with our prompt for positive (NP) and negative (NN) labels also provided. Additionally, the calculated true positive rate (TPR), true negative rate (INR), precision, and score each LLM shown.
Model
TP
FP
TN
FN
NP
NN
TPR
TNR
Prec.
F1
GPT-4o
1627
57
593
398
0
0
0.80
0.91
0.97
0.88
GPT-4o-mini
1084
95
555
941
0
0
0.54
0.85
0.92
0.68
ChatGPT
1346
177
472
678
1
1
0.67
0.73
0.88
0.76
Mistral-7B-Inn 7B-Instruct-v0.2
1172
159
403
716
137
88
0.72
0.73
Phi-3-mediume 4k-uun---k-iittut
1449
139
511
574
2
0
0.72
0.79
0.91
0.80
1-ama-3-8B-nnstrul
1267
139
502
752
6
9
0.63
0.78
0.90
0.74
Gemma-2-9B-IT
1355
118
533
665
5
0
0.67
0.82
0.92
0.78
Granite-3.0-8B-Insttee
1023
102
548
1002
0
0
0.51
0.84
0.91
0.65
3lama-3,1-8B-IInst,
1466
198
440
538
12
0.69
0.80
LLama-3.22 3.2-1BBInnttrud
968
255
335
853
204
60
0.53
0.57
0.79
0.64
-Lamm--3-70B-Insee
1630
116
533
392
3
1
0.81
0.82
0.93
0.87
Ministral-SB -iiistral-B--Instuttt-2- Instruct-2410
1304
161
486
708
13
3
0.65
0.75
0.89
0.75
Phi-3.5-Miin 1.5--Mini-nntrrue
1059
140
493
922
44
17
0.53
0.78
0.67
Qwen-2.5-
1013
220
374
775
237
56
0.57
0.63
0.82
0.67
Qwwen22.5144B-Instte
1303
89
555
707
15
6
0.65
0.86
0.94
0.77
Yi-1.5-34B
1489
156
494
534
2
0
0.74
0.76
0.91
0.81
46


Reviews:
[{"review_id": "0yphJ8YL6J", "reviewer": "Reviewer_cakY", "summary": "The paper presents a new approach to evaluate and benchmark LLMs on formal syntax. The authors suggest using CFGs to generate synthetic data for testing the LLMs, they utilize formal verifiers to verify the logic.\n\nContributions:\n1. A new method to evaluate LLMs on formal syntax without using static datasets by generating synthetic data using CFGs and adding vocabulary using another LLM\n2. Their method has better indication of accuracy than other metrics for the LLM performance on various FOL.", "questions": "1. How diverse can the generated dataset be ?\n2. How do you ensure that duplicate data points won’t be there ? I.e data points with very close similarity or minute changes or only change in vocabulary while the logic statement is same \n3. Would love to know how LLMs with tools work as verfiers", "limitations": "", "rating": 8, "confidence": 4, "soundness": 4, "presentation": 4, "contribution": 4, "strengths": "1. LLMs can be now tested on dynamic data generated by this framework for Formal Syntax\n2. Their method has better indication of accuracy than other metrics for the LLM performance on various FOL. \n3. Very good experimentations , dataset size and presentation", "weaknesses": "1. Explanation on how the generated dataset is having diverse data points or quality is missing. \n\nUpdate: Rebuttal answered various points about this and mentioned they have added more information in appendix.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "fbMwchOty6", "reviewer": "Reviewer_JCXM", "summary": "The ∀UTO∃∨∧L method evaluates the ability of LLMs to maintain truthfulness in formal tasks by dynamically generating datasets, utilizing the models' automatic formal and informal processing capabilities, and using formal verifiers. This approach allows for automated, human-free evaluation and can be extended to any formal grammar category that uses syntax and accepts equivalence checks. The authors demonstrate the effectiveness of ∀UTO∃∨∧L as an evaluation framework through empirical studies, revealing the limitations of current state-of-the-art models in maintaining truthfulness in formal tasks. By comparing it with existing benchmarks, the article highlights the practicality and importance of ∀UTO∃∨∧L in evaluating LLMs.", "questions": "1. The article mentions using context-free grammars (CFGs) to generate datasets dynamically. How does this method ensure diversity and balance at different difficulty levels? Specifically in fields like logic and regular expressions, how does it ensure comprehensive coverage of various possible syntactic structures while maintaining a balanced sample size for each structure type?\n\n2. The article evaluates whether LLMs can act as verifiers to assess the equivalence of formal grammar expressions and finds that even the most advanced LLMs struggle with this role. In the evaluation process, in which types of logical structures or specific conditions do LLMs perform the worst? Are there specific logical structures or syntactic features that make it difficult for LLMs to accurately judge equivalence?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The article introduces the ∀UTO∃∨∧L benchmark as an innovative evaluation framework that can automatically assess the ability of large language models (LLMs) to maintain truthfulness in formal tasks. Its practicality lies in dynamically generating datasets, reducing the need for manual annotation, and providing an evaluation method without human intervention.\n2. The ∀UTO∃∨∧L framework is designed to be flexible, allowing it to be extended to any formal grammar category that uses syntax and accepts equivalence checks.\n3. The article demonstrates the correlation between the results of ∀UTO∃∨∧L and other existing benchmarks, indicating that ∀UTO∃∨∧L can serve as an effective alternative or complementary tool.", "weaknesses": "1. ∀UTO∃∨∧L relies on existing formal verifiers and parsing libraries to ensure evaluation accuracy. This means its reliability depends on the performance and accuracy of these tools, and any errors in them could affect the evaluation results of ∀UTO∃∨∧L.\n\n2. While ∀UTO∃∨∧L reduces the need for manual annotation, generating dynamic datasets and performing formal verification may require significant computational resources, especially for large-scale datasets and complex logical structures.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "5z28J1NpGh", "reviewer": "Reviewer_t14Z", "summary": "The paper introduces autoeval benchmark, designed for the autonomous evaluation of LLMs in formal tasks like truth maintenance and logical reasoning. The benchmark offers several features, such as dynamic dataset generation using CFGs and the use of formal verifiers to assess correctness. The authors argue that their approach mitigates common issues in existing benchmarks, like overfitting to static datasets, and provides a scalable method for evaluating LLMs without relying on human annotations. Empirical results show that performance on this benchmark correlates well with other established benchmarks.", "questions": "- Given that formal verifiers are central to your evaluation process, how do you handle cases where the verifier fails or produces ambiguous results? Are there fallback mechanisms in place?\n- Can your dynamic dataset generation approach be extended to more complex natural language tasks that do not rely on formal syntax? If so, how would this impact the scalability and performance of your evaluation framework?\n- What steps have you taken to ensure that your benchmark remains relevant as LLMs evolve? Specifically, how do you plan to update the benchmark as new models with different architectures or capabilities are developed?\n- In your empirical analysis, how many different LLMs were tested? It would be useful to know whether your results generalize across a broad range of models or are specific to a few.", "limitations": "", "rating": 5, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The use of CFGs to dynamically generate out-of-distribution datasets is a significant strength.\n- The use of formal verifiers to check the semantic equivalence of LLM outputs is a good method that avoids brittle syntactic checks. This allows for a more robust evaluation of truth maintenance across different formal syntaxes.", "weaknesses": "- While the paper focuses on formal tasks like truth maintenance and logical reasoning, it remains unclear how well the proposed benchmark generalizes to less structured or more complex natural language tasks. The reliance on formal verifiers may limit its applicability to broader LLM use cases, such as creative writing or conversational AI, where formal correctness is less critical.\n- Informalization, the process of converting formal syntax into natural language, is inherently ambiguous. The paper does not thoroughly address how it handles cases where multiple valid informalizations exist. This could lead to inconsistent evaluations when different LLMs produce semantically equivalent but syntactically different outputs.\n- Weak evidence for the robustness of this method. While the paper claims that performance on autoeval correlates well with other benchmarks, the empirical validation seems somewhat limited. I would suggest that the authors test their method on a larger set of models. The current correlation results, while promising, could be influenced by noise or outliers, especially given the relatively small number of models tested, they might not be robust enough to generalize across different architectures or configurations. By increasing the number of models tested (e.g., to 50+), the authors could reduce the impact of potential outliers and noise in the data.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)