VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks
Authors: Yu Feng
Nathaniel Weir
Kaj Bostrom
Sam Bayless
Darion Cassel
Sapana Chaudhary
Benjamin Kiesl-Reiter
Huzefa Rangwala
Venue: ICLR 2026 Poster (2026)
Keywords: Neuro-symbolic methods
Large Language Models
Chain-of-Thought
Reasoning verification
Formal logic
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: LLMs can perform multi-step reasoning through Chain-of-Thought (CoT), but they cannot reliably verify their own logic. Even when they reach correct answers, the underlying reasoning may be flawed, undermining trust in high-stakes scenarios. To mitigate this issue, we introduce VeriCoT, a neuro-symbolic method that extracts and verifies formal logical arguments from CoT reasoning. VeriCoT formalizes each CoT reasoning step into first-order logic and identifies premises that ground the argument in source context, commonsense knowledge, or prior reasoning steps. The symbolic representation enables automated solvers to verify logical validity while the NL premises allow humans and systems to identify ungrounded or fallacious reasoning steps. Experiments on the ProofWriter, LegalBench-SARA, and BioASQ
datasets show VeriCoT effectively identifies flawed reasoning, and serves as a strong predictor of final answer correctness. We also leverage VeriCoT’s verification signal for (1) inference-time self-reflection, (2) supervised fine-tuning (SFT) on VeriCoT-distilled datasets and (3) preference fine-tuning (PFT) with direct preference optimization (DPO) using verification-based pairwise rewards, further improving reasoning validity and accuracy.

Published as a conference paper at ICLR 2026
VERICOT: NEURO-SYMBOLE
VALIDATION VIA LOGICAL CONSISTENCY CHECKS
Yu Feng", F Nathaniel Weir Kaj Bostrom , Sam Bayless Darion Cassel*, Sapana Chaudhary Benjamin Kiesl-Reiter Huzefa Rangwala* "University of Pennsylvania Amazon Web Services
ABSTRACT
LLMs can perform multi-step reasoning through -haiugh (CoT), but they cannot reliably verify their own logic. Even when they reach correct answers, the underlying reasoning may be flawed, undermining trust in high-stakes scenarios. To mitigate this issue, introduce VERICOT, a ncuro-symbolic method that extracts and verifies formal logical arguments from CoT reasoning. VERICOT formalizes each CoT reasoning step into first-order logic and identifies premises that ground the argument in source context, commonsense knowledge, or prior reasoning steps. The symbolic representation enables automated solvers to verify logical validity while the NL premises allow humans and systems to identify ungrounded or fallacious reasoning steps. Experiments on the ProofWriter, LegalBench-SARA, and BioASQ datasets show VERICOT effectively identifies flawed reasoning, and serves as strong predictor of final answer correctness. We also leverage VERICOT'S verification signal for (1) inference-time self-reflection, (2) supervised fine-tuning (SFT) on VERICOT-distillee datasets and (3) preference fine-tuning (PFT) with direct preference optimization (DPO) using verification-based pairwise rewards, further improving reasoning validity and accuracy.
INTRODUCTION
Chain-of- Thouuhh (CoT) (Wei et al., 2022) in natural language (NL) has emerged as a powerful technique for improving large language model (LLM) performance on tasks that require reasoning. LLMs like DeepSeek-R1 (DeepSeek AI, 2025) and OpenAl's ol (OpenAI, 2024b) demonstrate strong reasoning capabilities using COT. However, these models still frequently make logical errors in their reasoning chains, even when the final answer is correct (OpenAI, 2024a). For example, an LLM might generate the question answering (QA) CoT depicted in Figure 1, which leads to a correct answer, but an intermediate step might be false (e.g., "Charlie is most 15" instead of "at most 18"). When LLMs generate logically invalid CoT steps, it hinders their trust and usefulness, regardless of whether the final answers are correct. This issue is particularly critical in high- domains such as biomedical or legal reasoning, where users consider the accuracy of the reasoning path as important as that of the final answer. This behavior they predict text without an explicit mechanism for verifying the logical validity of the resulting semantics (Bender& & Koller, 2020; Ji al., 2023)
be attributed in part an inherent limitation of LMs:
Prior work has attempted to mitigate this through self-refinement of the model's output based on diverse feedback sources, such as dynamic retrieval of facts from external knowledge bases (Peng et al., 2023), a separate critic model (Paul et al., 2024), dynamic use of program execution (Chen et al., 2024; Olausson et al., 2024), or symbolic checking (Olausson et al., 2023; Ye et al., 2023; Ling et al., 2023; Pan et al., 2023; Quan et al., 2024a; Lalwani et al., 2025). However, these approaches do not ensure the logical validity of the entirety of an L.M'' output. The recently introduced Explanation- Refiner (Quan et al., 2024b) makes progress towards this goal by performing iterative autoformalization and refinement of NL explanations elicited from an LLM, guided by a theorem prover, for NLI task. However, there is yet be a verification method that simultaneously (1) applies over LLM Chain-of- Thought steps, (2) formalizes the context grounding of every reasoning step, and (3) improves LLM reasoner capabilities with respect to logical validity in domains other than code/math. To address these limitations, we introduce VERICOT: Symbolic Verification for
Work done during internship AWS

---

Published as a conference paper at ICLR 2026
Accii quall beneliss under and nosdl with powrt.
One's age is al most the cureet your minus their bitt year
Commonsense
A child qualiies 2025 They are under 21 and reside with a parent
Contect
Queetion:
Chorie was born in 2005 and lico with paront
Bob Dows Chucke quakly berelita in 202237
Charle in 2005 with parem
Autolormaizzation
Output NL Premises
Ingut Chein-ll-Though Steps
Logizai Implication
Cj Charle was born in 2005 and fivis with his parint Bob.
Ya:birtYYaun(cciliin) - 2005 A
Py birth birth (awrcherrii)) - 2005 A
LiveWiib(charlie bob) Parund/bul charlin)
LiveeWith Writh/chhrlinn bob) A Parent (bels, charli))
C3yy Charle most 16 2023
Psi age(chazile, a023) S 18
As Va age(a,9) S ym birthYear(e)
Cs:AA childi who is 18 or younger and lives with parent qualfiie..
Fy Vo. (age(s, 2023) s 18 ^ By LivesWith(sg)) A Paressio, ()) + Qualdies(s)
Ayy Ya.. (agelis, 2003) < 21 A By, Lives Livee/ath(a.3)))
Pareacly 1) - Qualibeess))
Cy: Therefore, qualries bonetis in 2023.
Fg Quadifioocchatile
VERIFIED: All sutolomaskzzd CoT steps implied
Output Logic Formula (Jrr)
Figure I: VERICOT verification of Chain-of-Thoughe for the SARA dataset (Holzenberger et al., 2020). Even if the final answer is correct, CoT that contains invalid step hurts user trust and raises questions of LLM faithfulness. As shown in $2.1. VERICOT autoformalizes each step of the COT into symbolic logie, producing formula that ensures each one follows logically from distilled list of NL premises, each of which it annotates with their source type (e.g. Commonsense or Context) If the CoT cannot be represented this way, it is unverifiable.
Chain-of-Thougghe a neuro-symholic algorithm that grounds and validates the logical consistency of Chain-of-Thought reasoning, identifying logical errors and making implicit premises explicit.
VERICOT maintains a growing set of first-order-lgiic (FOL) premises inferred from NL context. autoformalizes each CoT step into first-order-lgic formula, and uses a constraint solver to check whether it is logically entailed by the premises and previously formalized steps. If the step isn't entailed, VERICOT either autoformalizes sufficient set of supporting premises from available context (question text, documents, or common sense) or identifies reason why the step cannot be validated (e.g.. because premise could not be inferred from context, or because the step contradicts the inferred premises). Through this process, VERICOT provides multi-faceted feedback. It identifies whether a CoT can be represented in formal logic, how the CoT's steps are logically supported, and what underlying NL premises need to be accepted in order to accept the CoT's reasoning. To our knowledge, this is the first meuro-symbolic validator of CoT traces in non-math/ math/cooo domains.
Our evaluation demonstrates that VERICOT can detect ungrounded incorrect reasoning, and validdtttn is a strong predictor of final answer correctness, with validated CoT attaining higher precision than task-level accuracy ($3.3). Building on this verification capability, we leverage VERICOT to actively enhance an L.M's reasoning ($3.4). First, we use VERICOT for inference-tine self-reflection, where its validity-orienter feedback prompts the model to self-correct yielding an average 46% relative improvement in CoT verification pass rate and consistent 41 % relative gains in producing accurate and verifiable task outcomes across multiple datasets. Second, beyond inference- time correction, we build upon recent work using formal reasoning for RL verification (Leang et al., 2025) and use VERICOT to create high-fidelity dataset of verified CoT's for Supervised Fine-tuning (SFT) and as a source of pairwise reward signals for preference fine-tuning with direct preference optimization (DPO) (Rafailov al., 2024). These fine-tuning strategies improve the model's s ability to generate logically consistent CoTs by 18% (relative) while matching exceeding base task accuracy in less formal domains like biomedical and legal reasoning. We distill CoTs from a substantially stronger teacher model and retain only those that pass VERICOT's checks, yielding higher precision supervision than randomly sampled unfiltered traces when gold task labels are unavailable.
NEURO-S YYMBOIC CoT VERIFICATION ALGORITHM
Our goal is to validate the correctness of Chain-of- Thain-of-Thought reasoning by ensuring that individual reasoning steps can be translated into consistent firs-ordeer-lgiee formulas. We assume natural language context (which includes a question, an optional conversation history, and a source document with information relevant to the question) and CoT consisting of NL steps Ci,.... C..
given
As described in Alg. 1, VERICOT autoformalizes each step C₁ into a first-order logic formula F,, then uses constraint solver to determine whether F; be logically derived from our current.
2

---

Published as a conference paper at ICLR 2026
Algorithm 1: VERICOT Overview
1. Initialize: Set Po enrors
2. For each CoT step C. (i = ..).
(a) Autoformalization ($2.2): Formalize step C, into logic formula If C, cannot adequately expressed in our supported logic fragment or syntax errors persisted after multiple attempts:
erdors.add untranslatable)). Continue on to CoT step C.+1.
(b) Consistency check: If the formalized F; contradicts our established knowledge (Fi-1 F= -FF): errors.ad (i, contradiction).. Continue on next CoT step C.+1.
(c) Entailment check: If F; is logically implied by our established knowledge (F;-1 }= F:): set F, = F: U } and P. = P and continue on to next step C.+1- Otherwise, try to generate supporting premises:
(d) Premise generation ($2.3)) Generate premise P. to support F,. Check if P. is consistent with
established statements (Fi-1 / -P:)
Optional: Use LLM-as-judge evaluation ($2.4) to check that P: is attributable to source context.
still fails helps entail F (Fi-1 U (P3 }B} y F)): errors.add ungrounded)). ) set P; P.- (PP)) and F, Fi-1 (P.} (F) and continue on to next step C..1.
3. Return: Sets Pa, Fu, errors.
knowledge (Fi-1) or requires additional premises. We distinguish the following logical relationships
between new statement and our established knowledge:
Fi is entailed by Fi-1, meaning it necessarily follows from what we already know (Fi-1 |= F.),
F; is contradicted by F meaning it is inconsistent with what know (F F -Fi). is consistent with, but not entailed by, what we already know (F,-1 F,, Fi -Fi).
VERICOT identifies CoT as valid if infer consistent set of logical premises from the NL context that are sufficient to entail every step of the COT. If valid, VERICOT returns:
1. A self-consistent set of FOL premises P, where each premise P E P represents the formalization of an NL source (either from the provided context, or from common sense).
2. For each NL step C₁ FOL formula F; (the formalization of C₁) such that P F F.
If invalid, VERICOT identifies reasons for all steps that were not entailed. These reasons used as feedback signal for inference-time self-reflection or fine-tuning data distillation ($3.4):
1. Ungrounded: VERICOT could not identify a sufficient, non-contradictory set strengthening premises from context that would entail F; (c.g.. U (P.) F)).
Contradiction:
Existing statements contradict F, (e.g., L --F))
3. Untranslatable: C₂ could not be translated into the FOL subset supported by VERICOT, or syntax errors persisted after multiple attempts.
Logic formulas are encoded in SMT-LIB (Barrett et al., 2016), which supports fragment of first-order logic with theories including linear arithmetic, uninterpreted functions, and quantifiers. We use the SMT solver Z3 (de Moura & Bjørner, 2008) to perform the logical consistency and entailment checks described above. To build intuition, we first walk through a simplified example that demonstrates our approach on the CoT depicted in Figure 1.
2.1 EXAMPLE COT VERIFICATION
Step Infer premises from the user's question. For the first step, "Charlie was born 2005 and lives with his parent Bob," VERICOT autoformalizes it as follows (see $2.2):
F birth Year Year(charlie) charlie) 2005 A Lives With (charlie, bob) A Parent (bob, charlie)
P: be conjunction of multiple statements that then evaluated individually by L.MM-as-uude (82.4).
3

---

Published as a conference paper at ICLR 2026
At this initial point, the set Fu of previously established statements is empty, Fo / Fi. Since the current step's s statement cannot be derived from Fu. we check if supporting premises can be inferred from the provided context. Using an LLM, VERICOT is able to derive a supporting premise P from the question (in this case, P1 happens to be identical to Fi). We add Pi to our premise set Pı. confirm (via constraint solver) that Pi A Fo F Fi, and finally, add both (identical) statements Fi-
Step 2: Infer premises from common sense. For the second step, "Charlie is at most 18 years old in 2023," VERICOT autoformalizes it
P2 ==
2023) S 18
This statement cannot be derived from FI, which contains only information about Charlie's birth year and living situation, but no direct facts about his age. To bridge this gap, our premise generation approach (see $2.3) identifies commonsense assertion relating age to birth year: "Someone" age is at most the current year minus their birth year", autoformalized as:
P2 = Vr, y. age(x, 3) S y birth Year(x)
We can derive age( chharlee, 2023) < 18 from the combination of Fi and this new premise, so we obtain P2 by adding P2 to Pl. and we set F2 Fi U F2). Note that we reused the existing constant charlic and the predicate birth Year from our established vocabulary, introducing only the new predicate age as needed. Also note that if the step had made an incorrect claim like "Charlie at most 15," our verification would report the step inconsistent because P3 contradicts it.
Step 3: Infer premises from source document. For the third step, "A child who is 18 or younger and lives with parent qualifies," we formalize it as:
F3 = Vx. (age(s (z, 2023) S 18 A Fl. Lives With(a, y) A Parent(y, x)) - Qualifies
This universal statement cannot be derived from F2. However, the source document contains a stronger statement, which VERICOT autoformalizes as a new premise, "A child qualifies for benefits if they are under 21 and live with their parent", we formalize it as:
P3 = Vx. (age(z; (2. 2023) < A Fy. Lives With(x, y) A Parent x)) - Qualifies(s)
With P3 strengthened by adding P's to P2. we can derive P3 A F2 } F2, and so we update F3 U (P3, accordingly. Note that if this rule were not present in the source document or context, our verification would report the CoT step as ungrounded.
Step Conclusion. The last step, "Therefore, Charlie qualifies for benefits in 2023," formalizes as:
F1 =
This conclusion can now be derived from F3 without requiring additional premises: we know Charlie is at most 18 (hence under 21), lives with his parent Bob, and the qualification rule applies to all children meeting these criteria. Had the step wrongly said "Charlie does not qualify for benefits in 2023", we would have identified it as inconsistent with the reasoning trace.
Below we describe each modular component of VERICOT in more detail.
2.2 AUTOFORMALIZATION
Our autoformalization approach works in two stages, both using L.LMs to translate NI. into SMT-LIB. When attempting translate CoT step C; into its logical representation F,, the first stage uses an LLM prompt that includes the previously produced logical vocabulary as context. The LLM is prompted to generate structured, intermediate representation that combines SMT-LIB with metadata about which text in C, corresponds to which parts of the resulting F,, using only the variables and types already present in the vocabulary.
The second stage extends the vocabulary there are segments of the input text that the LLM deems relevant to the CoT's logical argument but cannot express with the existing vocabulary. In this stage, we use another LLM prompt to generate new SMT-LIB declarations (c.g., declare- fun, declare sort). The new declarations are added the vocabulary, and the first stage is attempted again. In our implementation, we allow this to repeat to three times before giving up (in which case the current step marked as untranslatable, or the current premise is discarded).
4

---

Published as a conference paper at ICLR 2026
In the following example, when VERICOT initially attempts to translate C2 ("Charlie is at most 18 years old in 2023") based on the available vocabulary. first reports that the vocabulary is insufficient, then extends it accordingly to translate C2 into F2:
Context: Charlic was born 2005 lives Bob.
Initial (Falling) LLM Translation Output Flt
Document: A child qualities for benefits they under 21 and live
with their parent.
CUEEENE year (assert false) cheee <22 UNTRAAGSLATABLE
COPTANGLACABLL
Question: Does Charlie qualify for benefits 2023?
Steps:
O1: "Charlic was born in 2005 and lives with parent Bob"
Cz. "Charlic is at most years old in 2023"
New Declarations Added to Vocabulary:
Previoudly Produced Vocabulary Fj:
current yeaz for celculation
Ideclare peeolare-comee arre-const current ago or person in given year iceclare-tun age_in, year year IFereon Intll Int]
Int]
: represents 5 person
(daclare-sort Person)
Chariic
IdecLare-censt cherlis Percon)
y specific pezson 868
Successful LLM Translation Output
idsclarc-ccact beb zerson!
eirth year
year 2023
(daciare-fun birth_vear (Person) Int)
ocerent_yeaz 2023) (se [age_in_yeax charlie ourzent_year) 18)
; whothor person 1190s with another person
chez age <28
ideclare-tun lives_xita (Zerson Ferson) Bool)
Successful autoformalization allows represent the step F2, but not necessarily ensure that is entailed by the growing logical formula, which is the focus of $2.3.
2.3 PREMISE GENERATION
Chain-of- Thaiughf-Thouuht steps aren't 't always directly implied by existing statements. Instead, they might rely on information from the context, like problem details ("Charlie is Bob's son") or support documents ("a child qualifies for benefits if they are under 21"),, or from common sense ("a father is a parent"). When a CoT step's 's formula F, is neither entailed nor contradicted by existing statements, VERICOT prompts LLM identify supporting premises from the context commonsense.
We attempt to build a premise formula P; that sufficient to entail F; as follows: We first generate multiple noncontradictory candidate NL premises and translate each of them into a logic formula using the autoformalization process from $2.2. We perform a round of premise regeneration the natural language meaning of any new declarations from this step is not captured in the generated premises. For each candidate premise p. we then check whether is consistent with the established statements (i.e., whether F;-1 p is satisfiable) and keep only those that Finally, conjoin all remaining candidate premises to form the final premise formula P..
2.4 LLM-AS-JUDGE PREMISE EVALUATION
VERICOT ensures that the CoT is FOL-representable and presents a list of inferred premises as one necessary basis for accepting the CoT's logic. However, has not verified that whether the premises themselves might be accepted. It may have enumerated the premise "the sky is purple" as necessary for accepting the COT, but this generally not an acceptable statement on its own. To provide greater assurance that the inferred premises are reliable, VERICOT uses LLM-as-Jun Ju-Judge approach (LLMaJ) to identify spurious premises after the premise generation process is complete. While the LLM generating premises in Alg. can produce confabulations omit relevant details, using L.MaJ reduces the likelihood that these errors go undetected.
We evaluate all premises using the LLMaJ approach. For premises inferred from source text, provide judge LLMs with both the source document and the NL version of the premise, prompting them to evaluate whether the premise is attributable to the source text. For premises inferred from common sense, we prompt judge LLMs to evaluate whether the premise is acceptable given the provided context and targeted reasoning step (omitting the attribution requirement).
3 EXPERIMENTS
Evaluation Models. We use Claude-3.5 3.iiee....-SSntettt V2 (Anthropic, 2024) through API calls as the executor of the proposed VERICOT. We fine-tune Q (Qwen Team, 2024).
5

---

Published as a conference paper at ICLR 2026
Method
Pass Rale
Precision
VCAR
Task Ace
ProofWriter
Category
Score
ER
14.8
83.3
12.3
75.8
DSB
10.0
96.1
9.5
74.8
Legalbench-SAAR
VERICOT-NoPPee
3.3
100
3.3
75.8
Grounded contextual premise
93.5
VERICOT
45.2
94.1
42.5
75.8
Acceptable commonsensse premise
83.9
BioASQ
Necessary commonsense premise
77.0
ER
1.5
80.0
1.2
81.4
BioASQ
DSB
5.9
72.2
4.2
75.7
VeRICoT-NoPPem
2.9
57.1
1.6
81.4
Grounded contextual premise
87.3
VERICOT
25.3
21.3
Acceptable commonsense premise
93.0
Necessary commonsense premise
81.1
Legalbench-S.ie
ProofWriter
ER
6.8
92.0
6.3
80.0
DSB VERICoT-NoPrem
4.8
94.1
4.5
77.7
Grounded contextual premise
96.4
0.6
50.0
0.3
80.0
Acceptable commonsense premise
90.5
VERICOT
15.2
87.0
13.2
80.0
Necessary commonsense premise
77.4
Table 1: Verification results across benchmarks. For each dataset, we report verification pass rate (%), verifier pre- cision (%), verified correct answer rate (VCAR, %), and task accuracy (%, i.c., correct answer rate). VERICOT consistently achieves the highest values across the main outcome metrics (pass rate and VCAR).
Table 2: Extended analysis of LLM-
as-Judge premise evaluation breakdown. The generated premises of all types are highly acceptable under LLMaJ.
3.1 DATASETS
We consider three datasets. ProofWriter (Tafjord al., 2021) contains small rulebases of facts and rules. Each rulebase has a set of questions which can either be proven true or false using proofs of var- ious depths. LegalBench (Guha al., 2023) is benchmark designed evaluate the legal reasoning capabilities of LLMs crowdsourced from legal professional; we use the SARA (Holzenberger et al., 2020) subset from LegalBench, which evaluates statutory reasoning in tax law. BioASQ (Nentidis et al., 2023; 2024) is series of annual open challenges focused on advancing biomedical semantic indexing and QA, specifically we use task b, which is biomedical QA with PubMed abstracts as context. Appendix Table 6 shows data statistics.
3.2 BASELINES
We compare VERICOT against three baselines using Claude-3.5-Somnet-Vy Explanation-Reffie (ER) (Quan al.. 2024b): an iterative formaaizaaiiinioonn and refinement approach guided by theorem prover, originally proposed for NLI tasks. In our adaptation, we treat the CoT steps as explanation, the question as the premise, and the model-generated answer as the hypothesis. Direct SMT Baseline (DSB): A direct formalization approach that decomposes reasoning steps with designated types and generates SMT-LIB expressions simultaneously via few-shot prompting. For reasoning steps based on document, background, or commonsense premises, only consistency check is applied: for inference steps, an entailment check is performed. VERICOT without Explicit Premise Generation VERICOT-NoPrent intermediate premises turned off. Verification is performed using the same check protocol as in the Direct SMT Baseline.
A variant of our VERICOT pipeline with generating
3.3 VERICOT AS AN EFFECTIVE VERIFICATION ALGORITHM
We first evaluate VERICOT as verification framework for CoT's, demonstrating that it achieves high verification performance by capturing larger proportion of verifiable reasoning with strong precision and introduces innovative mechanism for analyzing the premise grounding of reasoning steps.
Direct evaluation VERICOT. We evaluate verification methods using four complementary metrics: verification pass rate, verifier precision, verified correct answer rate (VCAR), and overall task accuracy. Following prior CoT-verification work such as Explanation-Retie 2024b), pass rate measures the fraction of godel-generated CoTs that verifier judges as valid, capturing verification coverage rather than task-solving ability. Precision captures the proportion of correct answers among verified CoTs, directly reflecting the reliability of VERICOT decisions.
(Quan et al.,

---

Published as a conference paper at ICLR 2026
Proportional Distribution of Outcome Scenarios
seffreflaciin
Proportional distribu- tion of outcome scenarios before and after self-reflection ($3.4) un- der VERICOT. Categories include successful verification (Valid) and failure cases: Contradiction, Un- grounded, Untranslatable as de- scribed in $2. Self-reflection sig- nificantly reduce errors.
Figure 2:
0.35
Prooottion
0.25
0.20
0.10
0.00
Valid
Contrediction
Ungrounded
Untranslatable
Dataset
Accurate Translation
Grounded Contextual
Acceptable Commonsense
Correct LLMaa
BioASQ 0.80
0.87
0.91
0.97
SARA
0.86
0,92
0.89
0,95
ProofWriter 0.87
0.95
0.95
1.00
Table 3: Evaluation of translation and premise quality across datasets. We report the proportion of accurate translations, grounded contextual premises, acceptable commonsense premises, and correct LLMal outcomes.
VCAR combines these two by quantifying the overall fraction of CoT's that are both verified and correct. The metric penalizes both the verifier that is too lenient (high pass rate, low precision) and the verifier that is overly selective and only accepts trivial cases (low pass rate, high precision). Finally, task accuracy corresponds to the final task-level correctness rate. As shown in Table 1, VERICOT achieves the highest pass rates across all benchmarks, leading the strongest verified correct answer rate. Importantly. its precision is consistently high, exceeding the final task accuracy, demonstrating that VERICOT-VV -aailidaadd CoTs provide a more reliable signal of correctness than the raw CoT's. These results highlight VERICOT as an effective and accurate verification algorithm that achieves broader coverage with better reliability.
Detailed analysis of instances that fail the VERICOT verification. We first conduct a quanti- tative analysis by presenting the proportional distribution of each possible outcome scenario under VERICOT before and after self-reflection (introduced below in $3.4). Ungrounded error is the most prominent, highlighting that CoT often overgenerates assumptions, producing reasoning steps that appear plausible but unsupported. Self-reflcction significantly increases the proportion of valid outcomes while reducing ungrounded and contradiction errors. The rate of translation-related erros remains largely unchanged. Additionally, corresponding to one type of failure case. For each example, we present the updated CoT along with its successful verification after self-reflection, as detailed $3.4.
provide three illustrative examples in $A.4, each
Quantitative analysis of NL premise quality. We present the results of VERICOT premise evaluation as described in $2.4. We use LLMaJ to assess the quality of the generated premises: (1) grounded contextual premise: whether contextual premise is correctly grounded in the source document or question, and (2) acceptable commonsense premise: whether commonsense premise reasonable given the context and the targeted reasoning step. In addition, we evaluate the necessity of each commonsense premise (necessary commonsense premise), i.e., whether support the corresponding reasoning step. The results in Table 2 confirm the high quality of premises identified by VERICOT. We present examples of different NL premises in Appendix A.3. A key strength of VERICOT is reliably locating reasoning steps in context or commonsense, making implicit premises explicit. For users to evaluate grounding, the challenge shifts from locating supporting premises to evaluating the quality of the premises that VERICOT has already identified shown in Appendix Tables 5, 6 and 7.
required to
Human Evaluation of VERICOT. We conduct human analysis by sampling 20 examples per dataset, evenly across the four labels: verifiable, ungrounded, untranslatable, and contradiction. We assess whether each logic translation is accurate, faithfully captures all necessary details, and
7

---

Published as a conference paper at ICLR 2026
Method
Pass Rate
APR
Precision
APrecision
VCAR
AVCAR
Task Accuracy
ProofWriter
ER
21.5
+6.7
80.2
-3.1
17.2
+4,9
75.8
DSB
12.3
+2.3
90.6
-5.5
11.1
+1.6
73.2
VERICOT CoT-NoPrem
30.7
+27.4
88.8
-11.2
27.3
+24.0
72.4
VERICOT-Base
60.1
+14.9
90.1
4.0
54.1
+11.6
74.1
VERICOT-W
60.6
+15.4
90.4
-3.7
+12.3
73.7
BioASQ
ER
3.8
42.3
84.6
+4.6
3.2
+2.0
81.4
DSB
8.5
+2.6
76.9
+4.7
6.5
+2.3
78.8
VERICoT-NoPrem
29.7
+26.8
+24.5
+22.6
79.8
VERICOT-Base
33.4
+8.1
86.3
+2.0
28.8
+7.5
82.0
VERICOT-W LLMaJ
36.9
+11.6
83.8
-0.5
30,9
+9.6
80.5
Legalbench-SARA
ER
+12.8
91.6
-0.4
18.0
+11.7
80.0
DSB VERICoT-NoPrent
9.0
+5.2
93.8
-0.3
8.4
+3.9
80.2
16.1
+15.5
84.2
+34.2
13.6
+13.3
80.3
VERICOT-Rase -Rase
25.2
+ +10.0
85.5
-1.5
21.6
+8.4
81.4
VERICOT-W LLMaJ
23.0
+7.8
85.5
-1.5
19.7
+6.5
81.0
Table 4: Verification results after self-reflection. In addition to the metrics in Table 1, we report absolute changes compared to pre-reflection (A). VERICOT-Ban
only verifier signals without LLMaJ evaluation, while VERICOT-W LLMaJ leverages the full set of signals for self-reflection. VERICOT(Base.w LLMaJ) achieves the strongest improvements (VCAR and accuracy) across all benchmarks while maintaining precision at similar or higher level compared to baselines.
Method
Pass Rate
Precision
VCAR
Task Accuracy
BioASQ
Qwen2.5-7B-Inssiee (direct)
22.8
83.1
18.9
77.4
SFT Random Distilled CoTs
22.9
85.7
19.6
78.5
SFT Verified CoTs
22.9
85,5
79.7
Verified CoTs DPO
26.8
83.5
22.3
79.4
ProofWriter
Qwen2.5-7B-Instiee (direct)
21.8
76.7
16.7
47.5
SFT Random Distilled CoT'
24.6
71.4
17.6
47.3
SFT Verified CoTs SFT Verified CoTs DPO
23.2
81.5
18.9
51.1
27.8
82.8
23.0
51.8
Table 5: SFT and DPO results on BioASQ and ProofWriter. We report pass rate (%), verifier precision (%), verified correct answer rate (VCAR, %), and task accuracy (%). Strategies include the base model (direct), fine-tuning with random distilled CoTs, verified CoTs, and DPO with verified CoTs.
preserves the correct logical relationships. We also evaluate the quality of the generated premises: (1) whether a contextual premise is correctly grounded source document or question, and (2) whether commonsense premise is acceptable and reasonable given the context and the targeted reasoning step. Finally, we check whether LLMaJ's judgments align with human annotations. As shown in Table 3, across all criteria. observe consistently high performance. The autoformalizer cxhibits a relatively low error rate, under 20%, which already quite strong for NL-to-FoL. translation. premises
LLMaJ decisions conducted a human analysis on the model's CoT decomposition. Across 60 examples (20 per dataset), we found that 96.7% of decompositions accurately preserved the information in the original COT.
aligned with human judgements 95-100% of the time. We also
3.4 APPLICATIONS OF VERICOT'S VERIFICATION SIGNALS
The verification signals produced by VERICOT provide structured feedback that improves CoT reasoning along three dimensions: user transparency, inference- time self-reflection, and fine-tuning. First, by formaainal CoTs and making premises explicit, VERICOT increases transparency, enabling users to directly and more effectively inspect the reasoning chain. Second, VERICOT supports self-reflection at inference time by exposing granular errors in faulty CoT's, thereby providing
8

---

Published as a conference paper at ICLR 2026
actionable signals that help correct COT. Third, the same structured signals can be incorporated into supervised tine-tuning and direct preference optimization (DPO) (Rafailov et al., 2024), guiding models toward producing more verifiable CoTs and ultimately achieving higher task accuracy.
Inference-time Self-reflection. We first evaluate whether VERICOT feedback can be used to guide models in producing better CoT's at inference time. Our process is as follows: if a CoT fails to pass the verification check, we prompt the model to self-correct its reasoning. We adopt two variants (Base, LLMaJ): Base uses only verifier signals without LLMaJ premise evaluation, while VERICOT-w LLMaJ leverages the full set of signals for self-reflection. Given all relevant information for every step, including the original reasoning steps, any added premises, the corresponding formalizations. errors, check results (with execution results and the model's 's parameter assignment), and optional I.LMJJ premise evaluation, the model prompted revise its CoT reasoning during inference. This generates an updated CoT, which is then re-evaluated.
Table 4 reports verification pass rates, verifier precision, verified correct answer rates (VCAR), and final task accuracy after self-reflection, together with the corresponding improvements relative to pre-reflection values (APR, Prrecision, and AVCAR). Across all benchmarks, VERICOT with self-reflection yields consistent gains in both coverage averagee + 12.33 +46b0ollue))+664499 +46.4% (relative)) and verified correct answer rate average (absoluttt +41.1% (relative)), indicating that refinement encourages the generation of reasoning that is more frequently verifiable and leads to correct answers. VERICOT achieves the highest absolute pass rates and verified correct answer rate, while maintaining similar level of precision and slightly better final task accuracy. These results highlight the effectiveness of VERICOT's verification signals in guiding self-reflection. We also report variant (w LLMaJ) that adds additional LLMaJ evaluation signal for self-reflection; however, it yields only a marginal improvement over the Base baseline. This is expected as the verifier results provide much more informative error signals.
Supervised Fine-tuning, To harness the benefits of verification for model improvement. we build high-fidelity datasets consisting of verified, logically consistent CoT examples (pass both verifier checks and LLMaJ evaluation) and apply them for supervised fine-tuning (SFT). We start from the Table 5 benchmarks different distillation strategies to evaluate the role of verification in data curation. Specifically, we compare (i) the baseline performance of Qwen2.5-775 7B-Insruuttt (ii) SFT with randomly sampled distilled CoTs, (iii) SFT with distilled CoTs that pass VERICOT verification. As shown in Table 5, requiring CoT's to pass verification (ii vs. iii) yields an average 3% improvement in final accuracy. This is because the verifier's higher precision ensures that verified CoT' contain a greater proportion of correct answers than randomly selected ones. This highlights VERICOT's signal as particularly valuable, as it can distill better data when gold answers are unavailable.
model and distill supervision signals from Claude-3.5-Someet-
Preference Fine-tuning. The verification signals from each reasoning step can further be utilized as pairwise reward signals during preference fine-tuning (PFT) with DPO enable more reliable CoT generation. We randomly resample CoTs for examples that initially pass VERICOT verification, keep those that fail in the new attempt, and then construct chosen/rejected CoT pairs, where the chosen/rejected one passes/fails verification. When applying DPO on top of SFT, we observed two key improvements across all datasets as shown in Table 5: the verification pass rate increased by 4.3% (an 18.4% relative improvement), while the verified correct answer rate improved by 3.4% (a 17.7% relative gain). This demonstrates that preference fine-tuning on data generated by VERICOT is especially helpful for generating verified CoTs because the pairwise reward signal provides stronger supervision signal to distinguish correct reasoning traces from incorrect ones.
RELATED WORK
Solver-based Verification of Natural Language Reasoning, The most relevant work to ours is Quan et al. (2024b), where a neuro-symbolic pipeline is introduced to formalize natural-language explanations (for natural language inference) into logical forms using LLMs, and then performs theorem- pereen--rooer-bbuse based verification and refinement of those explanations. While Quan et al. (2024b) focuses verifying and refining explanations post hoc for NLI tasks, our framework not only trans- lates and verifies each step of a CoT into first-order logic BB) but also grounds the reasoning chains in context and is tailored for multi-step reasoning beyond NLI explanations. Additionally, works like Ling et al. (2023) and Vacareanu et al. (2024) use LLMs to assess the logical consistency

---

Published as a conference paper at ICLR 2026
of each reasoning step, whereas method adds formal solver checks, context grounding, and correction, yielding more objective verification than LLM-only pipelines.
Solver-empowered Logical Reasoning in LLMs. Recent works have explored solver-assisted QA with LLMs (Pan et al., 2023; Poesia ct al., 2024; Ye et al., 2023; Kirtania et al., 2024; Ganguly et al., 2024; Arakelyan et al., 2025). Specifically, Pan et al. (2023) translates NL into logic and uses solvers with iterative repair; building on this, Kirtania et al. (2024) further uses the ability of LLMs to do pairwise comparisons, allowing the evaluation of the refinements suggested by the LLM; Ye et al. (2023) prompts LLMs to produce declarative constraints for SAT solving; Poesia et al. (2024) constrains LLM outputs via symbolic state tracking. Xu et al. (2024); Arakelyan al. (2025) propose symbolic Cty-l methods that generate formal reasoning steps to improve faithfulness to context and logical constraints without relying on external solvers. Ganguly et al. (2024) uses the L.IM to generate formal "thought program" in its intermediate JSON-based Domain-Speciffi Language (DSL), which serves as the verifiable logical representation of the reasoning step. All above works have LLMs generate solver code during reasoning with focus on task success, i.e., generating reasoning traces that are mostly NL but with verified components that help maximize benchmark performance. VERICOT, however, takes CoT as input and determines whether this reasoning is logically valid, imposing a strict constraint on the CoT's verifiability. We differ by combining context- grounded SMT-LIB translation with Rep-wise verification and using solver feedback for on-the-fly reasoning correction. Our RI setup is closest to Leang et al. (2025). They ground judgments in Lean's mathlib (math-focused) and demonstrate the effectiveness of "Theorem Prover-as-a-Jucee assa--Juge"" whereas VERICOT grounds statements in premises inferred from natural- language context, making it applicable across general NL domains.
Structured Explanation Generation for LLM Reasoning Our work relates to growing literature on surfacing the underlying premises and stepwise reasoning for task-specific conclusions. VERI- COT surfaces NL premises that, when formalized, provide directed, tree-like logical basis for symbolic conclusion; this similar to the fully NI. entailment tree structure (Dalvi et al., 2021; Bostrom et al., 2021) which uses NI. textual entailment as the "logical glue" between each layer of inferences. Versions of entailment tree- gec-generating algorithms such as Entailer (Tafjord et al., 2022), ADGV (Sprague et al., 2022), and NELLIE (Weir et al., 2024) map from task answers to entailment trees rooted in underlying conjunctive premises. Maieutic Prompting (Jung et al., 2022) produces related structures rooted in underlying arguments for/against believing recursive inferences.
5 LIMITATIONS
As both autoformalization and premise inference rely on LLMs, it is possible that either step can be incorrect (either by mis-translating the CoT into an unrepresentative formula, or by introducing a premise that is not well-founded). A formalization may be incorrect simply because the LLM used made mistake during translation, because the text to be translated fundamentally cannot be represented in the subset of SMT-LIB that we support. As a result, while VERICOT can prove that the formalization of the Chain-of-Thougle necessarily follows from the inferred premises, it cannot guarantee that the NL CoT or the premises are correct.
Potential future work includes: (1) reducing the number of LLM calls lower end-to-end latency of VERICOT: (2) improving robustness to autoformalization errors through tighter constraints and more explicit generation instructions, together with more effective translation-veriiiicttoo feedback; and (3) extending VERICOT to more complex domains that require richer reasoning structures, such as temporal or procedural reasoning.
6 CONCLUSION
In this paper, we present a neuro-symbolic framework that validates Chain-of-Thought reasoning by autoformalizing each intermediate step into first-order logic and grounding formal premises inferred from NL context or commonsense knowledge. Across the Proo/Writer, LegalBench-SARA. and BioASQ datasets, VERICOT reliably detects ungrounded or incorrect reasoning in CoT traces, which we show is strong predictor of final answer correctness. We further show that these verification signals can guide models to self-correct during inference and through supervised fine-tuning and preference fine-tuning for better CoT reasoning.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGMENTS
This work was conducted during Yu Feng's internship Amazon Web Services (AWS). We sincerely thank Nick Feng and Dan Roth for their valuable feedback, and we are also grateful to the ICLR reviewers and editors for their insightful and constructive comments.
REFERENCES
Anthropic. Introducing claude 3.5 sonnet. Anthropic press release, Claude.ai, June 20 2024. Accessed 2025-08-09.
Erik Arakelyan, Pasquale Minervini, Patrick Lewis, Pat Verga, and Isabelle Augenstein. FLARE:
Faithful logic-aided reasoning and exploration. In Christos Christoddoulpoollss, Tanmoy Chakraborty, Carolyn Rose, and Violet Peng (eds.), Proceedings of the 2025 Conference on Empir-
ical Methods in Natural Language Processing, pp. 23385-23403, Suzhou, China, November 2025. Association for Computational Linguistics. ISBN 979-8-89176-332-6
doi: 10. 10.18653/v1/2055. emnlp-maing 1193/.
emnlp-main. 1193, URL https: petttts::/aclaattin https///aaaattoooooo.ooo.o wttp:oyy...gg222/
Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www. SMT- COMT-LIB... L.I....... 2016.
Emily M. Bender and Alexander Koller. Climbing towards NLU: On meaning, form, and understand- ing in the age of data. In Dan Jurafsky, Joyce Chai, Natalie Schluter, and Joel Tetreault (eds.), Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp. 5185-5198, Online, July 2020. Association for Computational Linguistics. doi: 10. /0.18653/v1/2000 acl- cel-main.463, URL https: httppp///aaaaaaaaaeeee /at/aaaannttooooooo/oe org/ 2020 m
Kaj Bostrom, Xinyu Zhao, Swarat Chaudhuri, and Greg Durrett. Flexible generation of natural language deductions. Marie-Francine Moens, Xuanjing Huang, Lucia Specia, and Scott Wen- tau Yih (eds.), Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pp. 6266 6278, Online and Punta Cana, Dominican Republic, November 2021. Association for Computational Linguistics. doi: 10. 10.18853/v1/22 12233/11/222112 mmnlp-main.506. URL https: //aclanthology org 2021. emnlp-men main. 506/.
Xinyun Chen, Maxwell Lin, Nathanael Schärli, and Denny Zhou. Teaching large language models to self-debug. In The Twelfth International Conference on Learning Representations, 2024. URL net
ftttp:://opeereeee wwwprrvviee.nee/ooumth.e.. for.m?id-Kuut wiw.iidd-KKiiiiiii....
Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie. Hannah Smith, Leighanna Pi- patanangkura, and Peter Clark. Explaining answers with entailment trees. In
Moens, Xuanjing Huang, Lucia Specia, and Scott Wen-tau Yih (eds.), Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pp. 7358-7370, Online and Punta Cana, Dominican Republic, November 2021. Association for Computational Linguis- tics. doi: 10. 18653/v1/2021 het.:021...mmmmmami55.5.. URL BtLhttt::// http:////caaaahlllaao/// or2/2021. emm.pp-main mellp-maing 585/.
Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In TACAS, pp. 337-340, 2008.
DeepSeek AI. Deepseek-rl, https:: //ep. www.:/pdiaa.or///ll///eeeeee cessed: 2025-08-09
2025. Ac-
Debargha Ganguly, Srinivasan Iyengar, Vipin Chaudhary, and Shivkumar Kalyanaraman. PROOF OF THOUGHT Neurosymbolic program synthesis allows robust and interpretable reasoning. In The First Workshop on System-2 Reasoning at Scale, NeurIPS'24, 2024. URL https:// openreview.ner www.leww.eeefrrreeee fow.uorddumux-eer-eeed
d 333...
Neel Guha, Julian Nyarko, Daniel E. Ho, Christopher Re, Adam Chilton, Aditya Narayana, Alex Chohlas- Goohlas-Wood, Austin Peters, Brandon Waldon, Daniel Rockmore, Diego Zambrano, Dmitry Talisman, Enam Hoque, Faiz Surani, Frank Fagan, Galit Sarfaty, Gregory M. Dickinson, Haggai Porat, Jason Hegland, Jessica Wu, Joe Nudell, Joel Niklaus, John J Nay, Jonathan H. Choi, Kevin Tobia, Margaret Hagan, Megan Ma, Michael Livermore, Nikon Rasumov-Rahe, Nils
11

---

Published as a conference paper at ICLR 2026
Holzenberger, Noam Kolt, Peter Henderson, Sean Rehaag, Sharad Goel, Shang Gao, Spencer Williams, Sunny Gandhi, Tom Zur, Varun Iyer, and Zehua Li. Legalbench: A collaboratively built benchmark for measuring legal reasoning in large language models. In Thirty-seventh Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023. URL https::pp///...... http/ppppeevvveeeeeeeeeeeeeeeeee net. fonte/forrit forum? 2 dd=ggPQFXFRR.
Nils Holzenberger, Andrew Blair-Stanek, and Benjamin Van Durme. A dataset for statutory reasoning in tax law entailment and question answering. In Nikolaos Aletras, Ion Androutsopoulos, Leslic Barrett, Adam Meyers, and Daniel Preotiuc- Pietro (cds.), Proceedings of the Natural Legal Language Processing Workshop 2020 co-located with the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining (KDD 2020), Virtual Workshop, August 24, 2020, volume 2645 of CEUR Workshop Proceedings, pp. 31-38. CEUR-WS.org. 2020. URL https: / ceur ws. www/oooggoooooooooooooooooooo Vo1ooo41-65550 htppppp..pp..........
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 Comput. Surv., 55(12), March 2023. ISSN 0360-0300. doi: 10.1145/3571730. URL
https: /tl:://dooo www.i..rrg/le. /10 1141/15711177
Jaehun Jung, Lianhui Qin, Sean Welleck, Faeze Brahman, Chandra Bhagavatula, Ronan Le Bras, and Yejin Choi. Maieutic prompting: Logically consistent reasoning with recursive explanations. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pp. 1266- 1279, Abu Dhabi, United Arab Emirates, December 2022. Association for Computational Linguisties. doi: w0118653/v1/000 emolp-main.88 URL https:: / a a anthol org 2022. emn emmlp-ma in. 82/.
Shashank Kirtania, Priyanshu Gupta, and Arjun Radhakrishna. LOGIC-LM++: Multi-step refinement for symbolic formulations. In Bhavana Dalvi Mishra, Greg Durrett, Peter Jansen, Ben Lipkin, Danilo Neves Ribeiro, Lionel Wong, Xi Ye, and Wenting Zhao (eds.), Proceedings of the 2nd Workshop on Natural Language Reasoning and Structured Explanations (@ACL 2024), pp. 56-63, Bangkok, Thailand, August 2024. Association for Computational Linguistics. URL https: //aclanthology org/ 2024.0222.0 mww.e-1..6......
Abhinav Lalwani, Tasha Kim, Lovish Chopra, Christopher Hahn, Zhijing Jin, and Mrinmaya Sachan. Autoformalizing natural language to first-order logic: A case study in logical fallacy detection. In Kentaro Inui, Sakriani Sakti, Haofen Wang, Derek F. Wong, Pushpak Bhattacharyya, Biplab Banerjee, Asif Ekbal, Tanmoy Chakraborty, and Dhirendra Pratap Singh (eds.), Proceedings of the 14th International Joint Conference Natural Language Processing and the 4th Conference of the Asia-Paciffe Chapter of the Association for Computational Linguistics, pp. 132-147, Mumbai, India, December 2025. The Asian Federation of Natural Language Processing and The Association for Computational Linguistics. ISBN 979-8-89176-303-6 URL https:: //acl antho wetthooog logy. org/2025 findinggsiiinnte 1jcnlp.8/
Joshua Ong Jun Leang, Giwon Hong, Wenda Li, and Shay B Cohen. Theorem prover as a judge for synthetic data generation. In Wanxiang Che, Joyce Nabende, Ekaterina Shutova, and Mo- hammad Taher Pilehvar (eds.), Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume I: Long Papers), pp. 29941-29999999 Vienna, Austria, July 2025. Association for Computational Linguistics. ISBN 979-8-89176-251--1- doi: 10. 10.18653/v1/2025. acl-long. 1448. URL https: /aw.aaaananooooooccaaaaaaooollla org/ 2025 acl mocee-looge 1448/.
1448.
Zhan Ling, Yunhao Fang, Xuanlin Li, Zhiao Huang, Mingu Lee, Roland Mcmisevic, and Hao Su. Deductive verification of thain-of-thouuht reasoning. In Thirty-sevnnth Conference on Neural Information Processing Systems, 2023. URL https: http:///ppnneiieeeeeee net/ forum? idd= I5raM4CY22.
Anastasios Nentidis, Georgios Katsimpras, Anastasia Krithara, Salvador Lima López, Eulália Farré- Maduell, Luis Gasco, Martin Krallinger, and Georgios Paliouras. Overview of BioASQ 2023: The Eleventh BioASQ Challenge on Large-Scale Scale Biomedical Semantic Indexing and Question Answering. pp. 227-250. Springer Nature Switzerland, 2023, ISBN 9783031424489, doi: 10.10 978-3-031-424488 19. URL http:/ / /xx doi. org /ttg10...0 100...0.00//00 - 42448 9_ 9.
12

---

Published as a conference paper at ICLR 2026
Anastasios Nentidis, Georgios Katsimpras, Anastasia Krithara, Salvador Lima-Lópes Eulàlia Farré- Maduell, Martin Krallinger. Natalia Loukachevitch, Vera Davydova, Elena Tutubalina, and Geor- gios Paliouras. Overview of bioasq 2024: The twelfth bioasq challenge large-scale biomedical semantic indexing and question answering. In Lorraine Goeuriot, Philippe Mulhem, Georges Quénot, Didier Schwab, Giorgio Maria Di Nunzio, Laure Soulier, Petra Galuščáková, Alba Gareía Seco de Herrera, Guglielmo Faggioli, and Nicola Ferro (eds.), Experimental IR Meets Multilingual- ity, Multimodality, and Interaction, Cham, 2024. Springer Nature Switzerland, Springer Nature Switzerland. ISBN 1778---031-71908-4 doi: https:://oi..rrg/11.0/10000 000.0000000000000000002000000000 https: htt.//in..../..//////m/ springer com http//happtee/eeee 1011111----0111111110000-
0.1. URL
Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenen- baum, and Roger Levy. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing, pp. 5153-5176, Singapore, December 2023, Association for Computational Linguis- URL https: //tp://acllaaaae www.aaaaaaoooooooooooooooooooooa ogy orgg20233
tics. doi: amn1p-me 1..mainn.311 313//
Theo X. Olausson, Jeevana Priya Inala, Chenglong Wang, Jianfeng Gao, and Armando Solar-Lezama. Is self-repair silver bullet for code generation? In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024, 2024. URL https: / //openreview wwww..nee net/ fot://ooumm? d=GDGJRRnnRR.
OpenAl. Limitations of reasoning models. 2024a.
https: https://openaii /opeeai....ccco com/ index/
openai-ol-systent correct answers; Accessed: 2025-08-09.
Describes common reasoning errors despite
OpenAl. Openai ol system card.
openai-ol system--caddee 2024b. Accessed: 2025-08-09.
Liangming Pan, Alon Albalak, Xinyi Wang, and William Wang- Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Houda Bouamor, Juan Pino, and Kalika Bali (eds.), Findings of the Association for Computational Linguistics: EMNLP 2023, pp. -8244 Singapore, December 2023, Association for Computational Linguistics. doi: 10.18653/v1/2023 htt.:///....nnnnngeeemmppppp finniings--mnlp.245. findings-emnip 248/.
URL
2or.aaatooocay..r/22225 org/2023.
Debjit Paul, Mete Ismayilzada, Maxime Peyrard, Beatriz Borges, Antoine Bosselut, Robert West, and Boi Faltings. REFINER: Reasoning feedback on intermediate representations. In Yvette Graham and Matthew Purver (eds.), Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Pupers), pp. 1100-1126, St. Julian's s, Malta, March 2024, Association for Computational Linguistics. doi: 10.18653/v112000 1/22443/1002 67. URL https:
org/ 20042 eacl-long. 6
Baolin Peng, Michel Galley, Pengcheng He, Hao Cheng. Yujia Xie, Yu Hu, Qiuyuan Huang, Lars Liden, Zhou Yu, Weizhu Chen, and Jianfeng Gao. Check your facts and try again: Improving large language models with external knowledge and automated feedback, 2023. URL https: //arxiv. org abss 2302. 12813.
Gabriel Poesia, Kanishk Gandhi, Eric Zelikman, and Noah Goodman. Certified deductive reasoning with language models. Transactions on Machine Learning Research, 2024. ISSN 2835-8856. URL
https: wwwp//peevvveeeeeeeeeem/eeeieeee ew net/ / forum? ? d=yXnwrs2TT 2211 6.
Xin Quan, Marco Valentino, Louise Dennis, and Andre Freitas. Enhancing ethical explanations of large language models through iterative symbolic refinement. In Yvette Graham and Matthew Purver (eds.), Proceedings of the 18th Conference of the European Chapter of the Association for Computational Linguistics (Volume I: Long Papers), pp. 1-22, St. Julian's. s, Malta, March 2024a. Association for Computational Linguistics. doi: ht https: /a///aaannhhooooooo wwtp:///......//..... hac.2/22.....ooooo..oo...
URL
Xin Quan, Marco Valentino. Louise A. Dennis, and Andre Freitas. Verification and refinement of natural language explanations through I.M--ymmollc theorem proving. In Yaser Al-Onaizan,
13

---

Published as a conference paper at ICLR 2026
Mohit Bansal, and Yun-Nung Chen (eds.), Proceedings of the 2024 Conference Empirical Methods in Natural Language Processing, Pp. 2933-29535 Miami, Florida, USA, November 2024b. Association for Computational Linguistics. doi: 1/226/////102222.mmmmmmmmmma https:: //acl antho ogy- www.oogg...........ooo org/2024 emnlp-ma a i in. 12/.
URL
Qwen Team. Qwen2.5: A party of foundation models. Blog post; recommended citation for Qwen-2.5, September 2024. Includes Qwen2.5-7B and instruction
variants.
Rafael Rafailov, Archit Sharma, Eric Mitchell, Stefano Ermon, Christopher D. Manning, and Chelsea Finn. Direct preference optimization: Your language model is secretly reward model, 2024. URL
https: htttps:/arxiv..om wwt.//rgggaooooooo 2305. 18290.
Zayne Sprague, Kaj Bostrom, Swarat Chaudhuri, and Greg Durrett. Natural language deduction with incomplete information. In Yoav Goldberg. Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods in Natural Language Processing, pp. 8230-8258, Abu Dhabi, United Arab Emirates, December 2022. Association for Computational Linguistics. doi: 10. 112.3/////222..oo////o 2022. emnlp-main 564/.
URL https: htt///acaaaantttooooeeeee org/
Oyvind Tafjord, Bhavana Dalvi, and Peter Clark. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Chengqing Zong, Fei Xia, Wenjie Li, and Roberto Navigli (eds.). Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pp. 3621-363333 Online, August 2021. Association for Computational Linguisties. doi: 10.18653/ 1222021.indings-acl.333 URL https: / ac welllannoolllge 317/-
org/2021 orggg//202lgy.../2221 findi ind-nng--aee acl.
Oyvind Tafjord. Bhavana Dalvi Mishra, and Peter Clark. Entailer: Answering questions with faithful and truthful chains of reasoning. In Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (eds.), Proceedings of the 2022 Conference on Empirical Methods Natural Language Processing, pp- 1078-20933 Abu Dhabi, United Arab Emirates, December 2022. Association for Computational Linguistics. doi: 10. 1111865511122222 wwnwe-mainnnnnnmmm 134. URL https:ttpp.... / /aa/aalaanttt aclanthology org/ 2022. www.e-nnnlllamee maw...mmai....mmmmmmmmmmmmmmm 134//
Robert Vacareanu, Anurag Pratik, Evangelia Spiliopoulou, Zheng Qi, Giovanni Paolini, Neha Anna John, Jie Ma, Yassine Benajiba, and Miguel Ballesteros. General purpose verification for chain of thought prompting, 2024. URL ht /ttp//aavvvv..//////eee/eeeae..a org/ abs 2405 00204.
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi. Quoc Lc, and Denny Zhou. Chain of thought prompting elicits reasoning in large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL https: /pwprevienweeeeeeeoe net/ forum? id id=_violMesB_u.
Nathaniel Weir, Peter Clark, and Benjamin Van Durme. Nellie: A ncuro-symbolic inference engine for grounded, compositional, and explainable reasoning. 2024.
Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, and Wynne Hsu. Faithful log- ical reasoning via symbolic thaonhh.- In Lun-Wet Wei Ku, Andre Martins, and Vivek Srikumar (eds.), Proceedings of the 62nd Annual Meeting of the Association for Computa- tional Linguistics (Volume 1: Long Papers), pp. 93326-13365 Bangkok, Thailand, August 2024. Association for Computational Linguistics. doi: 10. 00.18653/v1/2024..o aww.:/2...l--ooo.7777 URL https://aclaatthh wwwp:/thhwhooooooooeeeoeeee acl- 720/.
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SatLM: Satisfiability language models using declarative prompting. In seirth- Conference on Neural Information Processing Systems, 2023. URL https:// wttp::////eeeeee..eeeeeeeeee fortt/form??? wtt.:orrwwmmmnoooeeeeeeoo d=TgW52L1P11.
14

---

Published as a conference paper at ICLR 2026
A APPENDIX
A.1
USE OF LARGE LANGUAGE MODELS (LLMS)
Large Language Models (L.LMs) used in the following scenarios:
Grammar Checking: we use Grammarly only for grammar checks, but this an Al-powered writing assistant.
Formatting Assistance: we use Claude 3.7 Sonnet to adjust figure and table formatting for consistency and readability.
No LLMs contributed to research ideation or drafting of substantive scientific content. The authors take full responsibility for all content presented in the paper.
A.2
DATA STATISTICS
Dataset
Train Size
Test Size
Description
ProofWriter
5000
400
Randomly sampled from the OWA-
Depth-5 and CWA-Depth-55 subsets. Contains only entailmen//contradicc tion labels (no "Unknown" answers). Source: https: httsss///hggggggaeseeee datasets hetess/eeemma/eaeeee Proofrriteeeee
BioASQ
5,049
340
Restricted to Task 12b: Test Results of Phase B.
LegalBench (SARA)
367
272 instances from SARA Entailment and 95 instances from SARA Numeric.
Table 6: Dataset statistics and descriptions.
A.3 EXAMPLES OF DIFFERENT PREMISES UNDER VERICOT
present two qualitative examples to demonstrate different type of generated premises. In the example in Appendix Fig. 3, all contextual premises are grounded and all commonsense premises acceptable and necessary. In the example in Appendix Fig. 4, all contextual premises are grounded and all commonsense premises are acceptable but unnecessary.
Question context
Output premise list
Question: Alice's taxable income for the year 2017 $25,561. How much taxes does Alice have pay for the year 2017 under Statute section I(a)()?
Document:
The is exactly 15% taxable income not over $36,900.
Context (partially omitted): Statute section ((a))): 15% taxable taxable
over $36,900.
Question:
Step-wise CoT:
Alice's taxable income for the year 2017
1. Statute specifies tax rate of 15% for taxable income not exceeding
$25,561.
$36,900.
2. Alice's taxable income $25,561.
Commonsense:
3. Since $25,561 < $36,900, Alice falls the 15% bracket.
The tax amount calculated by multiplying the taxable income by the percentage divided 100.
4. Tax $25.561 x 0.15 $3,834.15, rounding to $3,834.
5. Alice must pay 53,834.
2. The rounded tax amount exact tax amount munded nearest whole dollar, where with cents less than 50 round down and amounts with 50 cents or more round up.
Figure 3: Example from SARA: grounded reasoning and extracted premises.
A.4 EXAMPLES OF FAILURE CASES UNDER VERICOT
We present three illustrative cases of different types of errors, each of which, after relf-reflection. passes verification. Specifically,, these include (1) ungrounded example from ProofW riter as shown
15

---

Published as a conference paper at ICLR 2026
Question context
Output premise list
Question:
Based on the above information. the following statement tre, false, or unknown?
Charlie is blue.
Context:
Bob is big. Bob is nice. Bob smart. Charlie is nice, Dave nice. Erin is big. Erin blue. is furry. Erin quiet. Erin round. Brin is smart. All nice things big. All furry things hlue. Blue, furry
Document:
1. Charlic is nice.
things are quiet. If something is round and nice then is blue. If Bob is round then Bob is blue. Big. quiet things ure furry. If something is blue and furry then it is smart. If Charlie is nice and Charlie is big then Charlie quiet.
2. nice things big.
3. If Charlie nice and Charlie is big then Charlic
is quiet.
4. Big. quiet things are furry.
Step-wise CoT:
furry things are
1. Charlic is nice.
2. Since all nice things are big. and Charlic nice, Charlic must big.
Commonsense::
3. Since Charlic is both nice and big, and there is a rule stating "If Charlic nice and Charlie is big then Charlie quiet", Charlie must be quiet.
1. Being big is property that some things have and others don't.
2. Being quiet property that some things have and others don't.
4. Since Churlie is both big and quiet, and there is rule stating "Big. quiet things are furry". Charlic must be furry.
5. Since Charlic is furry, and there rule stating "All furry things
blue". Charlic must be blue.
6. Therefore, the statement "Charlie blue"
Figure 4: Example from ProofWriter: grounded reasoning and extracted premises for "Charlie is blue".
in Appendix Table 5 (refer to full details in A.4.1): the model initially is over-claiming. During self-reflection, however, it is able to identify the overclaimed portion, rephrase it appropriately, and thus generate a verified COT.
Quntiian contint
Outper premie Hbt
Chriget Lagic (Uett leo inporttntt snec)
Verticadion ruesl
dumment untertass The
Contret (portaaly uniitedi: The mouse cur the tigr..
rabli
The
ing relationaigs esta scorpe aepieitly steed wab
"so other
The mosse youn. The mahrr doee chose diper The
The matcoeatche
(Boea22
mosse hi.
(sc sexoo.
asseling a lig thes il vist decculle sulii.
4. sxreting tign
Step-nic
virbee Sger verrvish mose
Incteat land s1gert1305
lige. la mosse
and tiore is rule axcng thai if axnellig g vista foo aaosic then to excnc iillig
troomtiing
2. Stnce the monne cas the tiper and on other calng ruls-
Conmtsnesee
(foral3 antielet veaadl ccpec
conalage cear: escepi explanty stand
rale
The uosue and difieeett ande
conciuat the vasta
2. The nukki end liges ure diffeene uni- ruls
Incinal_yceita clgec souseil)
Sinc de visia
iss sontthng viala tacuu laa
oveilde the mouss beg
3. The rubea snd mone are diflove murza
Stece the mous Ne, and thre ts miee statue thx crechaie that
anattie tig bun van the rathi,
lopicll of the meno bikng hig wil aboua vidrng na canee
He mingivnonng
Figure 5: Highlights of an ungrounded example from Proofwriter before self-reflection.
(2) a contradiction example from BioASQ as shown in Appendix Table 6 (refer to full details in A.4.2): the reasoning contains a subtle logical flaw that is difficult to detect. Our VeriCoT framework successfully identifies this issue and prompts the model to explore alternative reasoning path during self-reflcction, ultimately resulting in a verified COT.
(3) untranslatable example from LegalBench-SANe SARA as shown in Appendix Table 7 (refer to full details in A.4.3): when the translation error is presented to the model for self-reflection, the model recognizes that the erroneous reasoning step unnecessary for the final solution. By removing this step, the model produces a verified COT.
16

---

Published as a conference paper at ICLR 2026
Quatinn contest
Outpat premise lstt
Output Lugic (Omit lew important une)
Virificaiin roult
Quettion: Connesic chantels be seal for dag adficryy
Grounded Contest:
Failed costrdiction. In sap the usions show macro pelyner mocecles > 1000 Da hut comesin hemshhrnncl only penni molecules 1000 Da. Thus. the milanik impossible.
Step-ntte Crr)
Contest unitted
is neribaanes thet molecules
1. Cousesin lemiciarne's ure chancels
(w) lasd EaCGerecinneccceenn di
ifeaall Meleculet shanoelgy
1. Consesas henickanals are chas- uels cell meuttrancs that cat allw molexals pao thoough are yor. of pop junciunn charnel.
Cunnesis
part
15059131
(apaazt (docaz) (in Mciepusnl)
Consesin beniclencle allow
un--ckkstive pascage melecalos up
3. Conneci herricarech alon for the mnn-adettie gaoage of molienskss sp
(apaact (docazs (te Chentell Holecs24))
6. The ability in deliver berg pulyraric
L0M0 Da.
Berapeetic masomolevales via the sap
land senosterolathaeoe
3. The junction channel pulyner therapeusic
junciion muse possides evideace for drig akiiary paicnial.
(Cnnmmarllaaaana 4)
autecule, which is evidence for drug deloory ponmiise.
Commonsensc:
IRRANSE
311
Inzzata Chantaly Koleczle))
4. Thersfor, moleculs, makes them highly atnacivve uaget la deliveins drasp.
molevale molecular
Trspenoonn yeortheropaat
Figure Highlights contradiction example from BioASQ before self-reflection.
Queliie conlest
Ouigut prenise list
Output Legic (Quif les ingectant ones)
Ya ilctiio result
Questio:: Detenise wheche the filosiis sutzrecats ur Estalinens,
Groundel in Contest:
Fail due to aetussaakiii..
cutlee statac Reply
3500 opplies to agrict-
casnent
Mep plaas
stat then arraaaaatra taher der fiom Feb it, 2017 to Sep 2nd 2017. Alke is Anei- zas empioger, Staereet: sectin 15065ak1 applice Alice employing
Contrst: Alic
exployed perfert cpi-
toys alice boto
LIB nles becass it
carsee mndoon under
your 2017.
Sepiemerr 2017. erstensed Allue's paynes of $3200 this work
cakid alice boo Letiiiadaaaaaaae
30576001 20530350113
proices porititty nibhr thas dofmitie vnsenen.
coxpect
Section 3306600() suiste vddresses agriodten
stusall to to mucsuit)
labor
(covered by, wwc.son, 2500c1 p111
purkormed
is loquetticslly apri
cuttera later
(covaced wwwpsyyetteceeeeeeee2 bob
sore
Ausricas employer agricol-
labe
jatidiecional inplicatoos. the
infermance abost irmitation.
emptoymeer 3008000)
scopo
Figure 7: Highlights of an untranslatable example from LegalBench-SARA before self-reflection.
17

---

Published as a conference paper at ICLR 2026
A.4.1 UNGROUNDED EXAMPLE FROM PROOFWRITER
Ungrounded example from ProofWriter
Reference information: The dog does not eat the rabbit. The mouse eals the liger. The mouse is green. The rabbit does not chase tiger. The rabbit cuts the dog. The rabbit young. The tiger something cats the tiger then the tiger visits the mouse. If the dog is young and the dog does not visit the mouse then the mouse does rabbit the rabbit does not visits the dkg. If something visits the rabiii and the rabbit is young them round. If something is round and visits the dog then it rabhit.
something visits the
then the mouse
If
rabbit. something green
something green
chases the figer. something hig
Question: Based on the above information, is the Jollowing statement true. Talse, or unknown? The mouse visits the rabbit.
True
Original CoT:
this step step.
1. First, lot's ideatity what we know about the mouse:
mouse eals tiger
The mouse is green
something visits the mouse then mouse big
2. Since the
the tiger and and other cating relationships exist except this explicilly stated, according the rule: "If somethiig cats the tiger then the riger visits the mouse"
Therefore, the tiger
mouse
3. Since the tiger visits the mouse, according to the rule:
"If sornething
mouse
hig"
Therefore, the mouse is big
4. Now, since the mouse big. according to the rule:
"If something hig then visits the rahbit"
Therefore, the mouse visits the rabbit
We directly conclude the Therefore, the statement "The mouse visits the rabbit" is TRLE.
rabbit based these logical steps.
VERICOT Output before self-reflection:
Decomposed CoT Steps
1. The mouse has three direct properties: the mouse eats the tiger, the mouse is green, and there is rule stating that if something visits the mouse then the mouse big
the tiger samethhin eats the tiger then the tiger visits the mouse, we can comclude that the tiger visits the mouse
2. Since mouse
other eating relationships exist except this explicitly stated, and there rule stating that if
3. Since the tiger visits the
and there mile stating that something visits the then the
big, conclude rabbit, we conclude mouse
that the mouse big
Since mouse big,
stating something big
visits the rabbit
5. The statement 'The mouse visits rabbit' is true based on the logical chain of the mouse being big and the rule about big things
visiting the rabbit
Step
Step Context: The mouse has three direct properties: the mouse cats the tiger, the mouse groen, there stating that if something visits the mouse then the mouse big.
18

---

Published as a conference paper at ICLR 2026
Schema
represents on animal entipy ddeolare-aort
constant repzesenting the mouse (declare-const Animal) constant reprasenting the tiger (declare-const ter Antmal)
if animal (declare-fun animal_eats (Anima) Animal) Bool) : (declare- animel big
ancther
animal green
(Animal: Bool)
7 true
(declare-fun animal_is_bit (Animal) Bool)
2 true if one animel viaits anothez
(declare-fun aninal_visite (Animal Animal] Bool)
Added premises
The mouse is green (occument)
(assert (enimal_ia_gzeen Le_geeen mouse)
The and tiger different animals (commonsense)
(assert (not (= mouse (iger))
7 mouse
tiger (document)
(assert (animal_eats mouse tiger))
something visita the mouse then mouse big (doccument) (assert [forall ((a Animal1)
(=> senimsl_visits mouse)
ianimal_is_big nousel)))
Step logic
eats Ligez
1 mouse green
if animal visits
then big
(assert (animel_eats mouse tiger))
(assert (animel_is_green mouse)
(assert [forall ((2 Animall)
(=> aanimal_visita mouse) tanimsl_is_big nousel))
Evaluation: Pass
Step 2
Step Context: Since mouse cats the tiger and no other eating relationships exist exoept this explicitly stated, and also there rule stating that something cats the tiger then the visits the mouse. we conclude that the tiger visits the mouse.
19

---

Published as a conference paper at ICLR 2026
Schema
(hone new)
7 Added premises
something eata the tiger then the tiger viaita the mouse (document) (assert [forall ((2 Animall)
(0> tanima _ eats tigeri
taninal_visita Liger mouse)]
Step logic
The
tiger and other eating relationshipe exist except those explicitly atated
mouse Liger if tiger Liger visita mouse (assert (animal_eats mouse tiger))
(assert [forall ((2
Amimal))
(animal _eats (and mouse) Liger))
(assert (and (snimal_eats
tiges!
(forall (Ta Animal)1
(=> janimel_eats tigez)
tanimel_visite tiger mouse))
coninal_vistsr tiger mouse)))
Evaluation: Ungrounded.
Reason:
"no other eating refationslips exist this explicitly stated" connot be grounded.
Step
Step Context: Since the tiger visits the mouse, and there is a rile stating that if something visits the mouse then the mouse is big, can conclude that the mouse is big.
Ochema
(none
Added premises
(none
Step logic
if ciger visits mouse and if any animal visits mouse then mouse is big (assert (w>
(and (snimal_visits tiger mouse)
(forall (a Animal)]
_iviiitt
(animsl_ie __g__ig_____gggg mouse) 1
(animal_is_be is___ig_________ mouse)))
Evaluation:
Step
Step Context: Since the mouse is big, and there rule stating that something is big then it visits the rabbit, conclude that mouse visits rabbit.
20

---

Published as a conference paper at ICLR 2026
Schema
constant reprasenting the rabbit (declare-ooe rabbit Animal)
Added premises
somathing is big then it visita the rabbit (oocument) (assert (forall Animalt)
(=> (animal_is bigbig a) canims__visite rabbitt)))
Step logic
big big visits rabbit mouse visits zabbit (assert (m>
(and (animal is big mouss)
(forall (1a An'ma 1)
(=> (animal_ie_biz a)
(animel_visite zabbit!)))
(aninal_vialie mouse rembit))
Evaluation: Pass
Step
Step Context: The statement 'The mouse visits the rabitt' true based on the logical chain of the mouse heing hig and the rule ahout things visiting the rabbit.
Schoma
(none new)
Added premises
(none new)
Step logio
mouse is big and big animais visit rabbit then mouse visits rabbit (assert
(and (aninal Sanimal_ia_ba la_big mouse) Animal)] (=> (an ma 1_____________ a)
(anima l_iisill_isttsssee rabbiti)))
(sminal_vieits rebbitt)
Evaluation: Pass
VERICOT Ouiput
Decompased Steps
1: From the reference information, know three direct facts about the mouse: the mouse cats the tiger, the mouse is green, and there
is rule stating that if something visits the mouse then the mouse big.
2: According the reference information rule "If something eats the tiger then the visits the mouse". and since know the
mouse eats the tiger, we can conclude that the tiger visits the mouse.
tiger mouse then the mouse big", we can conclude that the mouse is hig.
information something visits 4: reference information states something is big then it visits the rabbit", Since we have established that mouse is big.
3:
established
mouse,
applying this rule that the mouse visits the rabbit.
21

---

Published as a conference paper at ICLR 2026
5: Therefore, based logical starting from mouse cating the tiger. leading the tiger visiting mouse, making mouse big. and ending with the rule about big things visiting the rabbit, can conclude that the statement "The mouse visits the rabbit" irve.
Step
Step Context: From the reference information, we know three direct facts about the mouse: (1) The mouse cats the Liger, (2) Thee big.
green, (3) rule stating something visits
Schems
Zepresents animai entity (declare-sort Animal)
representing the (declare-const mouse Anima') : constant representing the tiger (declare-com) tiger Animal)
: true if one animal eats another (declare fun enimal_eats (Animal Animel) Bool)
7 true if an animel is green (declare-fun snimal_ia_grean (Animal) Bool) true if an animal is big
(declare sninal_is_ki (Animal) Bool)
true if ane animal visits another
(declare fun aninal vieits (Animal Animall Bool)
Added premises
7
is green (document)
(assert
(animal_ Sanimal_ta_grenn mouse))
: The mouse and tiger are different animala (commonsance) (assert (not
mouse tiger)))
The mouse eats the tiger (document)
: mouse eats tiger (assert
(aninal_ess _eats mouse tiger1)
If something visits the mouse then the mouse is big (docusent)
visits mouse then (assert
big
(forall
((o Animal))
(4>
fanimal visits mouse)
lanimal_is_big nousel))
Step logic
mooue eats tiger
; green
if animal visits mouse then mouse is big (assert
(animal_eats mouse tiger1)
(assert
(animal_ta_green mouse))
(assert
(forall
((a Animali)
(4>
lanimal_visite mouse)
fanimsl_is_hig mousell))
Evaluation: Pass
22

---

Published as a conference paper at ICLR 2026
Step
Step Context: According reference information "IF something eats riger tiger visits mouse', since know the mouse cats the tiger, conclude that the tiger visits the mouse.
Sohema
(none new)
Added premises
something eats the tiger then the tiger visits the mouse (document) tiger then tiger visits mouse (assert
((a Animal))
(=>
lanimol_eate tiger]
(animsl_visite tigez m)
Step logic
eats tiger tiger mouse if monse eats tiger then tiger visits mouse (assert
(forall
(ta Animali)
fanimal_ Lett tiger]
animal_viaite tiger mouse)
(assert
(0>
(animal tiger)
(animal_visita tiger mouse)
Evaluation: Pass
Step
Step Context:
Since have established that the tiger visits the and know from the reference information that 'If something visits the mouse then the mouse is big', we can conclude that the mouse is big.
Schema
new)
Added premises
new)
Step logic
if tigez visits then is big (assert
(animal_visite tiger mouse)
Lnimal_ia_bis mouse))
Evaluation:
23

---

Published as a conference paper at ICLR 2026
Step
Step Context: reference information states something is big visits rabbit'. Since we established mouse is big. applying this rule means that the mouse visits the rabbit.
Schema
constant reprasenting the rabbit
(declare-conat vabbit Animal)
Adddd promises
somethint big then visits the rabbit (document)
: if la big then viaits rabbit
(assert
(forall
((a Animal))
(2>
lanimsl_is_bae a)
canima_vvaiits rabbit))))
Step logic
if la big then visits rabbit
: mouse is big then mouse visits rabbit (assert
(forall
((a Animal))
(=>
aanimoliis_be
tanimal_visita raobiti)1)
(assert
(animal_is_bte mouse)
mnimal_visite mouse zabbit!))
Evaluation:
Step
Step Context: Therefore, making the mouse big, and ending with the rule about big things visiting the rabbit, we can conclude that the statement 'The mouse visits the rabbit' is true.
logical chain starting mouse eating tiger, leading tiger visiting mouse.
24

---

Published as a conference paper at ICLR 2026
Schema
(none new)
premises
(none new)
Stop logic
7 mouse ests tiger tiger visita mouse
tiger visits mouse as mouse 18 big 7 mouse big => mouse visits zabbit visits rabbit (assert
(snimal mouse tiger! Sanrral_vssise tiger mouse)))
(assert
(-3
(snimal_visise tiger mouse)
Sanima__ia_be mo
{=>
(antral _a__ral_ss_big mouse)
(aninal_visiis mouse rabbit))1
(assert
senimal_visite rabbit))
Evaluation: Pass
A.4.2 CONTRADICTION EXAMPLE FROM BIOASQ
Contradiction example from BioASQ
Question: Can Connexin hemi channels he used for drug delivery?
Gold Answer: Yes
Context:
The permeability of Cx43 channels small molecules and macromolecules makes them highly attractive lurgets delivering drugs directly into the cytoplasm. Cancer cells overespressing Cx43 may be more permeable and sensitive to chemotherapeuties In this context, certain channels lead transitory plasma membrane permeability changes, such pannexin, connexin bemichannels that channels in membranes that pass molecules. TRPVI- 1-4 and P2X7, which allow for the non-selective passage of molecules to 1,000
Gap junction channels, composed connexin proteins, provide mechanism for direct transfer of small molecuies across metnbranes, and recent evidence suggests that the trunsfer larger, polymer like molecules such as microRNAs may be possible. Collectively, these results reveal polymeric macromolecules junction route can be used for the delivery of macro polymeric therapeutic molecules, which provides evidence for drug delivery potential.
be delivered to cells gop junctions, suggesting that gap
Original CoT:
me break this down step by step.
understand
bemichannels
They are channels cell membranes that can allow molocules to through.
They are part of a gap junction.
2. Key characteristic connexin hemichannels:
They allow "non-oe selective passage of molecules up to 1,000 Da".
3. Evidence for drug delivery potential:
Gap junction route can transport various types of macro polymeric therapeutic moloculos.
drug delivery. The evidence strongly supports this, showing they can transport various types of therapeutic molecules, making them valuable targets for drug delivery applications.
Conclusion: Yes,
bemichannels
Decompased CoT
1. Connexin hemichannels are channels in cell membranes that allow molocules through and of gap junction chamnels.
2. Connexin hemichannels allow for the non-selective passage of motocules up 1,000 Da.
25

---

Published as a conference paper at ICLR 2026
3. The gap junction route can transport macro polymer therapeutic molecules, which evidence for drug delivery potcotial.
4. Therefore, Connexin hemi channels perieable to therspeutic macromolecules, makes them highly attractive targets for delivering drugs.
Step
Step Context: Connexin hemichannels channels in cell membranes that can allow molecules through and are of gap junction channels.
Schoma
representa molecuie
(declare-sort Mo ecule)
zepresenca
(declere-sort Channel)
: whether channel
connexin hemichannei
(declare-fan TsComnexinnem nRemmcchanel (Channel) Bool)
2 whecher channel a gap junction channel ideclare-fun tacoplunationthaamaa (Channal) Bool]
: whecher channel is located in a cell membrane
(declare IsInCellXembranee (Channel)
whecher an entity is considered a channe!
(declarc-fun Ischanne [Channel] Bool)
whether solecule can enter through channe! (declare fun CenEnte:Viahhaneel (Molecule Channel) Bool)
wbether channel is of another channel
(declare Cun Paztof (Channel Channel1 Bool)
Added promises ses
Connexin hemichanneis are channela in membranes that paas molecules (document)
(assert (forall (fe Channel))
(=> sxttomexxiniemichenne land (IsChannel c)
[isinCelltembrane
(exists ((n Molaculet) (ConEntervischannel m c)1))1)
Connexin hemichangeis (assert (forall (th Channel))
gap junction channels (document)
(=> (Lscommaxinkemmcchenn
texists (ig Channel)]
(LeiappuanctionChannee gl
(Partof h g)))))
Step logic
Connexin hemichanneis are channels in membranes that pass molecules Connexin hemichanneis are part gap junction channels
(assert (forall ((e Channe') ))
(=> IISComexiinfeeiichhenee
(and (IsChannel c)
[Msintelleembesne c)
lexists Molaculet) (ConthterVischannall c)1))
(assert (forall ((: Channel))
(=> [IcComexiineem
rexists (ig Channel)
(and (IsGapJanct www.ouannniinnneel........ gl
(Partoć gl)))))
Evaluation: Pass
Stop
Step Context: Connexin hemichannels allow for the non-selective passage of molecules 1,000 Da.
26

---

Published as a conference paper at ICLR 2026
Schema
returna the malecular weight of a malecule
(declare-Fun MolecularReight (Molecule)
Added promises
Connexin hemichennell aliow for the non-selective passage of molecules 1,000 Ga (document)
Molecule) Chansel)
(=> tand [1sComaxxinieeiicheane c)
iCenanterviachsneel c))
K= tooleculareeight m) 10CD))13
Step logic
If molecule cen encer via connexin channel, its weight must be <= 1000 (assert
Malecule) Channel)
(=> land Cetoonnexinteeechhmmna c)
|CanDnterVLaChaneell m c])
(Woleculerfleight 1000))11
Evaluation: Pass
Stop
Step Context: Gap junction transport polymer therapeutic molocules, which is evidence for drug delivery potential.
27

---

Published as a conference paper at ICLR 2026
Schema
whether a malacule 10 a mocro polymar therspoutic molecuie
(declare-fun www.rroolymehheereteti...o
(Kolecule) whetller channel has potential for drug delivery
(declare-fun aedurugpeliverypoeentiii
Bool)
Added premises
The ability to delr sacro polyseric therapeutle molecules via the gap junction route, which provides evidence for dzug delivezy potential (document) (assert
(forall (Ic Channel) In xolecule))
(-> (and ITsGaptunetionChanmeel
(and (CanEnterVBa ct
(CenBnteeVieChaaneel [Hasdrggpeeliverytcceetttt c}}1}}}
Any ma marco pytrere cherapentie molecule has so solecular we waigght > 1, 1,000 na commonsense)
(assert
(forall (im Molecule)
(bbleculareeight m) 1000)1))
Step logic
If gap junction channel tzansports lazge polymeric thecapeutic
macromolscules,
then it hag drug-delivery potential
(assert
(forall (1c Channell In Xolecule))
(-> (and [IsSapoanctionChaneee, arrsarreoolmmrrrrrrspossmmmmmoo
m))
(and (CanEnterVieChannee) = cl
(>> (Contnterriechaaneel
(#astrugDel ieatraggaliverryotontttia e))1))
Evalnatio:: Pass
Step 4
Step Context: Therefore, Connexin hemichannels are permeable to therapeutic macromokeculos, making them valuable targets delivering drugs.
28

---

Published as a conference paper at ICLR 2026
Schema
(hone new)
Added premises
(none new?
Step logic
Connexin hemichanneis are permeable to therapeutic macromolecules (assert
(exists (Tc Channell In Molecule))
(and
Tela::oooolmeeTheraapa como comolecule m) (CanEaterViaChamne c})))
7 Connexin hemichanneis are permeable to therapeutic macramolacnies, -> they are highly actractive drug-de ivery targeta (assert
(forall (1c Channel) In. Xolesule))
(-> (and ItsComnexinflenicchane c)
ilsyaccceealyeeefiiseeeeuiiiiiie (Cananterviachaneell el)
m)
[HadEruggh tarafrrrgnalllayyyoteeettalll c)1))
Evaluation: contradiction.
Reason: The axioms show macre-polymee molecules 1000 Da. but connexin bemichannels only permit molecules 2 1000 Da. Thus, the same molecule would need to both 1000 and 1000, which impossible.
Decompused CoT Steps
Connexin hemichannels are channels membranes
molecules to pass through part gap junction
chanaels.
2. Coonexin hemichanncls allow the non-selective passage of molocules up 1,000 Da.
3. Cx43 channels are permeable to both small molocules and macromnleeellss, makes them highly attractive targets for delivering drugs.
4. Since Cx43 connexin hemi channel and supports drug delivery, infer that connexin hemi channels be used for drug delivery.
Step
Step Context: connexin hemi channel channels membranes can molecules to pass through and part gap junction channels.
29

---

Published as a conference paper at ICLR 2026
Schema
represents molecuie
ddeolare-aort Mo_ecule)
represenca channei
(declare-sort Channel)
whother channel is connexin hemichannel
(declare-fun TaConnexi channel (Channel) Bool)
whether channel tonhhannel (Channal) Bool]
gap junction channel
(declare-fun TaCapJunetfonChanma,
whecher channel locaCed
(declare-fur IsinCellXembraze (Channel) Bool)
7 whether an enticy
(declare-fun Ischanne" [Channel] Bool)
: whecher selecule can enter through channel
(declare-fun ConRnterVizchameel (Mclecula Channel) Bool)
2 whecher one channel 18 part of another channe!
(declare
(Channel
7 premises
a*e.........
connexin hemnichaneei aze channels in membranes that pass molecules docunents)
(assert (forall (i Channel))
(=> [IsComexxinlemichheee
land (isChannel c)
[IsTnCel iMmmrrane
lexists ((n Moleculet) (CanEnterViaChamee e11))1)
Connexin hemichenneis
gap junction channels documents]
(assert (forall ((h Channei))
(=> (LsComaexinHemicchne
texists (ig Channel)]
(and (TsGapdunct inChannel gl
(PartOr ())1))
Step logic
Connexin channaaii are channels in mombranas that pass molecules (assert (forall (( Channel))
(=> IISComnexinlemiichann (and (isChannel c)
[1sIntell
(exists ((z Holeculet)
(CanEnterViaChannel m c))))
Connexin hemfchannalg are part of gap junct fon channels (assert (forall (th Channel))
(=> [IsComexiinlemichhnnn
texists (1g Channel)]
(and (TsGapdunct onChannel innhhannel
(Partoć h g))))))
Evaluation: pass
Stop
Step Context: Connexin hemi channels allow for the non-sclective passage of molecules 1,000 Da.
30

---

Published as a conference paper at ICLR 2026
Schema
returna the malecular weight of a malecule
ddeclare-Fun MolecularWeight (Molecule)
Added premises
Connexin heemichannels for the non-selective ve passage of moleculea up to
0,000
(assert (forall ((m Malecu's e) (o. Channel)]
[L5Conaaexinleencchannee c)
(Cananserviachamme..
K< (Molecular@oight m) 10CD))1)
Step logic
If drug can enter via connexin channel, its weight must be <e 1000 Molecule) Channel)
(assert
(=> land
IISComaexinnleenichannee c) (CanénterVieChanne-
[<- (MoleculacReight m) 10(0))1>
Evaluation: Pass
Step 3
Step Context: channels are permeable to small molocules and macromolccules, makes highly attractive targets delivering drugs.
31

---

Published as a conference paper at ICLR 2026
Schema
whether a channel is specifically connexin (Cx43)
ddeclare-fun TaCx43 (Channel) Bool)
whecller molecule is small solecule
(declaze-fun lesmalie (Molecule)
whother malecule 10 macromolecsle
(declare-fun TaMacromo whether channel is permeable
(Molecule) Bool]
given molecule
(declare-fun PerneableTo (Channel Molecule) Bool]
7 whecher
deliver drugs -eevellllevel, independent solecule)
feecler--fun CanDeliverDrug (Channell Bool)
Added premises
The permaability of Cx43 channels small molecules and macromoles ecules, makea them highly atcractive targets for delivering drugs directly into the cytopiass. (document) (assert
(forall (ie Channel] im Xolezula))
(+> (and (TsCX43 c)
(or (IoSnaliMolecule m)
(Lataccrmoleeulee
(and (CanEnterViaChanne (CanEntesVieChaanell
(Conueliverunue e()1))}
: Any large mecromelscule has molecular weight 1, 000 Da (commonsense) (assert
(forall (im Kolecule))
(1#Kacronolecule
(mblecula:wiight m) 1000)1))
Any small decromelecule has solecular weight <- 000 Da [commonsense)
(assert
(forall (im Nolecule))
(=> IIsSmal1Xclecule m)
[dolecularweight 10001))
Step logic
Combined: if is cx43 and m is small oz a macramolecule, then (1) permeates oz given permeabilicy, (assert
drugs.
(forall (te Channel] Im Molecule))
(=> (and (IsCx13 (or (LsSmalllelecule m)
leaMacromolecule
(and (Cananterviachannel
[=> (ConEnterVisCharnel c)
(CanDe LiverDrug el)1)))
Evaluation: Pass
Step 4
Step Context: Since Cx43 connexia hemi channel and supports drug delivery, infer that connexin hemi channels can be for drug delivery.
32

---

Published as a conference paper at ICLR 2026
Schema
(hone new)
Added premises
Cx43 channels are a cype of connexin chansel [Commoneense]
Cx43 is type of connexin temichannel
(assert (forall ((o Channe }
ISsComexiinleemichanne c)1)
: Cx43 supports drug delivery, (Document) (assert
(exists (1c Channel1)
(IsCx43
(CanbeliverOrug =1))
Step logic
Cx43 is a connexin hemz channel and supports drug delivery
(assert (e Channel))
(=> [1sUx43 c) channell c)1))
(assert
(exists (Ic Channel))
(and (IsCx43 c)
(CanDeliverOrug 211))
Every drug that Cx43 channei can deliver, can be fvered by some Connexia hemichannel.
(assert
(forall (t Channel))
(and (1stx43
Sennellivertipg c)
(exists ((h Channell)
(and axcComnexinleenichanee
(CanDelive:Urug h))))1)
Evaluation: Pass
A.4.3 UNTRANSLATABLE EXAMPLE FROM SARA
Untranslatable example
Reference information: Section 3306()X() applies agricultural labor.
Question: Determinn whether following statements are entailed under the stalute. Description Alice has puid $3200 to Bob agricultural labor done from Feb 1st, 2017 Sep 2nd, 2017. Allice American employer. Statement: Section 3306(c)( 1) applies to Alice employing Bob for the year 2017, Reply with either: Entailment, Contradiction.
Answer: Entailment
Original CoT:
Lei me solve this step by step.
First, let's identify the key elements in the statute:
statute in question Section 3300le)()).
Its primary subject is "agricultural labor".
Let's unalyze the given description of the situation:
Empploee:: Bob
Employer: Alice (an American employer)
Type
explicitly identified agricultural
Let's compare the situation to the statute's hasic scope:
statuto, Scction 3306leXI), spocifically and directly addresses agricultural labor.
The work performed by Bob agricultural labor.
33

---

Published as a conference paper at ICLR 2026
Therefore, the situation fälls squarely within fundamental subject matter this statutory section.
Important consideration:
"The that the work was performed un American employer raises polential jurisdictional or geugraphical questions.
Hawever, the provided statute fragment does contain information about geographical limitation.
Based on the basic provision:
Since the basic scope of this section.
agricultural
3306(eX explicitly covers agricultural labor, descrihed falls
VERICOT Ouiput before self-rellection:
Decomposed CoTI Steps
1. Section 3306(cX]) of the statule uidresses agricultural labur
2. The work performed Boh for Alice specifically agriculuura lahor
3. The basic scope Section 3306(cXI) covers all agricultural labor
emplayer there might jurisdictional implications, fragment provide information about geographical limitations
Alice
5. Bob's 's employment falls under the basic scope Section 3306(cX1)
Step
Step Context: Section 3306(c)(1) of the statute addresses agricultural labor
zepresents section of statute (deslare StatuteSectios)
; specific section 2306(e) (declare-const section_3306e 3306cl StatuteSection)
: whather section deals agricultural (declare-fun dea agutth_agrieuiturrll labor IStatnte3ection! Bool)
Add premises:
Section 3306(e) (1) applies to agricultural laber (document)
(assert
(deals htt.eaaaatt__errruuuuuuaaaa sect ion_3306c1)
Step Legic:
sec 3306ci abt agri labor (assert
Liteeeaattteerrrlluuuuaaaaa sect (306cl))
Evaluation: Pass
Stop
Step Context: The work performed Bob for Alice specifically agricultural labor
34

---

Published as a conference paper at ICLR 2026
schema: :
represents person
(declare-aort Person)
represencs Alice
(declare-const Person)
represents Bob
(declare-const Person)
whether performs agricultural labor
(declare-fun performs_avd aagaroslluuraa _ Labor (Person) Bool)
whecher person esploys
person
(declare- fun empleys (Person Person) Bool:
7 Add premises:
Alice employed Bob to perfers agriouitural labor from February 1st to Seplember 2nd, 2017, (document]
by Alice's payment $3200
7 Dotes encoded
pafd employer worker laborType amount starthate andhate (declare fun paid (Person Person laborType Int Int Int) Bool)
(assert
(employs alice bob)
(performs_age) (perfomss_grreeuluuue agrieulturall_aeet bobt
(paid alice bob agriou.tural_laber 3203 201 70201 20170902))1
Step logic:
performs agr! (assert
(and
beb!
(employs alice bob)))
Evaluation: Pass
Stop
Step Context: The basic scope of Section 3306(cX1) agricultural labor
35

---

Published as a conference paper at ICLR 2026
schema:
predicate: whather person's work is covered by 3306(c) (1)
(declare-fun covereod_ (Person! Bool)
Add premises:
persen performs laber, therefore anyone perform agricuiturol labor covered by Section (306 (1) (commonsense)
(forall (pp Perzon)
(=> cet.ommmgggscctturrell.
p)
(covered bt__byy__ss____eee cotattioonn3ooc pl)))
Step logic:
sec 3206ci covers agzi laboz
person does agei (assert
by see 3306c1
seotion_3306c1)
(assert
(forall (ip Person)
(per peerforme_egicculuuree. p)
byvered_bby_eection pl)))
Evaluation: Pass
Step
While Alice American employer and there might jurisdictional implications, fragment does provide information about goographical limitations
Context:
Schema
(none new)
Add premises: (none new)
Step logier
(none new)
Evaluation: Fail due Untranslatable
The phrase "there might be jurisdictional implication" cannot be rendered under SMI-1J8 rules becouse it expresses a possibility vather than definitive
Reason:
Stop
Step Context: Bob's employment falls under the basic scope of Section 3306(cX1)
36

---

Published as a conference paper at ICLR 2026
Schema:
(none
Add premises:
(none new)
Step logicr
aassert (soveree_by_.ccccioo..000 bob))
Evaluation:
VERICOT Output after self-reffee reflection:
Decompused CoT steps
1, Section 3306c))) explicitly applicd to agricultural labor shown statute text 'agricultural labor'.
2. Bob performed agricultural labor.
3. Since Bob's work qualifies as agriculiural labor, and Section 3306(c1(1) covers agricultural labor, Bob's employment falls under the basic scape of Section 3306(c)()..
Step
Step Context: Section 3306(e)( explicitly addresses agricultural labor, which means that any person who performs agricultural labor is covered by Section 3306(C)(1).
37

---

Published as a conference paper at ICLR 2026
Schema
represents statute sectich
ddellare-aort StatuteSect
represencs Lype of labor
(declere-sort Laborlype) represents person
(declare-sort Person)
specific
section (3)6(e) (1)
(declare-const poction_3066c StatuteSection)
: specific
type: agricultural
(declare-com const labor_agz Labor_agricultural LaborType)
7 whether section addresses labor type
(declare-fun
atttonnnddrasee__lbaa (Sta:uteSection labor"ype) Bool:
; whecher person perforsed labor type
(declare-fun performed labar (Parson laborTypal Bool)
whecher peraon's employment is covered by a scatute section emp-oyment_covered
ScatuteSection) Bool)
Added premises
Section (e) (1) explicitly epplies agricultural labor shown the statute text 'agricultural labor' (document)
(assert addreso
section_330fel Labes_opricuituall)
: persen performs laber, therefore anyone performing agricultoral covered by Section 3306 (1) (commonseese))
(assert
(forall (Ip person)
(=> ferrmeee__abbo lebor_agricullural)
[employment_coeeeed p section_310sci)
Step logle
Section (2) (1) explicitly addresses agricuiturai labor -> anyone who performed agricultural labor is covered
(assert bection__ddressee (assert
sestion_310fcl Labos_agricuutural))
(forall (Ip Person)
Iper subruuulic)l) (employment_covere) section_310sel))
Evaluation: Pass
Stop
Step Context: Bob performed agricultural labor.
38

---

Published as a conference paper at ICLR 2026
Schema
Bob performed agricultural labor.
(declare-conat Peraon)
Adddd promises
Alice has paid $3209 Bob for agricultursl labor done from Feb lst, 2017 sep 2nd, 2017. 7. (document)
Dates encoded TYYYNDD
paid employez worker laborTyce amount startDate endDate
(declare-fun paid (Person (declare-const. Alicc Person)
Labortype
Int). Bool)
(assert (performec_labor Bob labor abbor_agriculturall]
(assert (paió Alice Reb ano__aggriultural 3200 20170201 20170902)
Step logic
(assert (performec_ labor Rob ahor_agriculttun
Evahation:
Pass
Step
Step Context: Since Bob's work qualifies as agricultural labor, and Section 3306(c)( covers agricultural labor, Bob' employment falls under basic scope Section 33066cX().
Schema
Added premiser ses (none
Step logic aeseessan
dezive Bob's coverage
(assert (=> (and
[performed__aa
labor_agrioulturall
(forall (P Person))
(performed_iate labor sabor_agricultures
jemployment_coveeeeeee coverre boctiio__306el11
(emplcyment__cveeed) Bob sectior__336ee))
Evaluation: Pass
39


Reviews:
[{"review_id": "EjpkTo8ikG", "reviewer": "Reviewer_C6Nf", "summary": "This paper introduces VERICOT, a neuro-symbolic framework to validate the logical consistency of Chain-of-Thought (CoT) reasoning. It autoformalizes each CoT step into First-Order Logic (FOL) and uses an SMT solver (Z3) for verification. The authors claim their core novelty is a \"premise generation\" step, where an LLM infers and formalizes implicit commonsense or contextual premises to complete logical gaps. The resulting verification signal is then used for inference-time self-reflection, supervised fine-tuning (SFT), and direct preference optimization (DPO).", "questions": "To me, the core drawback to be fixed is that the paper must include a direct comparison against other neurosymbolic SMT-based CoT verifiers cited in the related work, namely SAT-LM (Ye et al., 2023), Logic-LM (Pan et al., 2023), Proof of Thought (Ganguly et al., 2024; 2025) and Logic-LM++ (Kirtania et al., 2024). On cursory browsing, current leaderboards for ProofWriter with Proof of Thought claim higher verified performance with GPT-5 than reported in your paper, and the SMT-LIB generation traces seem very similar. Without comparing against these techniques, the novelty and performance of VERICOT are unverified.", "limitations": "", "rating": 2, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "This paper tries to address the problem of verifying the step-by-step logical integrity of CoT, not just the final answer. The mechanism for generating implicit premises to fill logical gaps is multi-step beyond simple auto formalization. Verification, when it passes, is a high-precision signal, filtering incorrect reasoning and improving reliability over the base model. The authors demonstrate the utility for model improvement, using the verification signal for self-reflection and as a high-quality filter for SFT/DPO data. The error analysis (Ungrounded, Contradiction, Untranslatable..) is insightful and provides actionable feedback for the LLM self-reflection loop.", "weaknesses": "1. The system \"verifies\" an LLM-generated CoT against LLM-generated premises. This is an internal consistency check, not a sound grounding check. There is lots of literature about LLMs preferring their own outputs.  A human evaluation or ground truth is required to measure the error rate of the autoformalizer and the premise generator to prove the system isn't just \"consistently wrong.\"\n2. The low pass rate on LegalBench-SARA is concerning. Qualitative error analysis is needed to explain this failure.\n3. Writing could be improved for clarity. For example, Score in Tab 2 is not defined anywhere in the main text of the paper. Formatting errors are present, such as \\approx in Line 425.", "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": "IkU4mSJ9iQ", "reviewer": "Reviewer_D7eV", "summary": "The paper describes a system that provides a multi-step process for transforming a Chain of Thought into a formal argument, with the goals of grounding and validating individual steps in the CoT and identifying logical errors in the CoT. This process answers three questions: can the CoT admit of auto-formalization, are the steps in the CoT supported, and what premisses does the CoT rely upon. This approach accomplishes two objectives: inference-time checking of the correctness of a CoT, and providing examples of CoTs that are verified to be correct for use in the fine-tuning of a reasoning model.", "questions": "What specific technical advances would be required to achieve verification rates sufficient for practical use? Would a human-in-the-loop approach for handling untranslatable cases be viable?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The core innovation lies in combining LLM-based autoformalization with SMT solver verification using Z3, which provides formal guarantees about logical consistency within the formalized representation. This approach offers more rigor than purely LLM-based verification methods, while remaining more flexible than pure formal methods that require pre-specified logical frameworks.\n\nI see an analogy with the informal process of proof checking of a human-generated proof in informal and formal reasoning. The idea of using this to validate CoTs, and then using the validated CoT through fine tuning in a self-improving process is interesting. This concept\ndemonstrates practical versatility, and suggests a path toward increasingly reliable reasoning systems.", "weaknesses": "A fundamental concern is the circular dependency created by using LLMs for both autoformalization and premise generation, which are then employed to verify LLM outputs. This architectural decision introduces potential for systematic biases where the verifier may share failure modes with the system being verified. While the paper acknowledges this limitation, it doesn't adequately explore the implications or propose mitigation strategies. The system essentially asks LLMs to judge their own reasoning through a different lens, which may not catch errors that stem from fundamental misunderstandings encoded in the model family.\n\nThe presence of an \"untranslatable\" error category reveals a significant limitation in the approach's scope. Certain reasoning steps fundamentally cannot be represented in the supported first-order logic fragment, as illustrated by the LegalBench example where probabilistic statements like \"might be jurisdictional implications\" cannot be encoded. The paper reports these untranslatable rates but offers no strategies for handling such cases beyond marking them as failures, which limits the system's applicability to real-world scenarios where uncertainty or non-classical reasoning may be needed.\n\nThe reliance on LLM-as-judge evaluation for premise quality assessment introduces another layer of potential error and bias. While Table 2 reports high acceptance rates between 77% and 93%, these metrics don't guarantee that premises are actually correct or complete. The circular dependency problem resurfaces here, as LLMs evaluate premises generated by LLMs, potentially missing systematic errors or hallucinations.", "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": "z0hGuUI6hu", "reviewer": "Reviewer_MriA", "summary": "This paper augments CoT with generating verifiable first-order logic expressions, which can be used by a constraint solver, to verify the chains of thought being generated by LLMs. The paper spells out a careful procedure to do this (Section 2), which consists of generating a formal logical expression from each COT step ($C_i \\rightarrow F_i$), validating the formal expression, then generating premises to support the formal expression ($F_i \\rightarrow P_i$). \n\nThis procedure is especially nice in characterizing the unreliable CoT steps (ex: contradictions, ungrounded reasoning, etc.). \n\nThe authors then demonstrate the benefits of their procedure on a few benchmarks that rely on reasoning (ProofWriter, LegalBench, BioASQ). Augmenting VeriCOT does improve the reliability of the model's CoT steps (as measured by precision, pass rate), but does not seem to affect the end task accuracy much. \n\nThe authors study the effect of fine-tuning LLMs with VeriCOT. While simply applying SFT does not seem to make much of an effect, applying DPO (to favor correct VeriCOT steps vs. incorrect VeriCOT steps) does improve task accuracy, suggesting a better post-training recipe for domains that require multiple logical reasoning steps.", "questions": "What is the difference between updating $P_i$ with $P_i = P_{i-1}$ vs. $P_i = P_{i-1} \\cup \\{P_i\\}$?\n\nIn Table 4 - it doesn't seem like SFT-ing with VeriCOT makes much of a difference, unless DPO is applied. Any thoughts as to why?\n\nHow does VCAR combine precision and pass rate? It seems a bit odd to combine the two given that the two measures seem to have very different distributions. \n\nWhy do you think precision drops after self-reflection for ProofWriter?\n\nWhat results do you expect to see when VeriCOT is applied to \"unfaithful\" CoT, in which models justify their answers \"post-hoc\"? (https://arxiv.org/abs/2305.04388)", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "This paper provides an intuitive procedure to validate the reliability of CoT sequences. In particular, looking at the VeriCOT failure cases is a good way of uncovering common \"fallacies\" of model CoTs (e.g., contradictions, ungrounded reasoning). \n\nOverall, the paper makes a nice coherent, and well-scoped contribution to test the reliability of LLM's CoT steps.", "weaknesses": "From the brief description of the baseline methods being compared to, it sounds like VeriCOT isn't the first to incorporate FOL (or similar expressions that is conducive to do verification along the way) to validate and improve CoT. It would be helpful to explicitly spell out how VeriCOT differs from these other approaches.\n\nShould there be another baseline where the LLM-judge just verifies each natural language reasoning step (without the FOL counterparts) to isolate the effect of FOL steps? \n\nWhile VeriCOT seems to improve on precision and pass rate, it doesn't seem to affect task accuracy that much. Does this suggest that it's not so much the correctness of the CoT that matters, but instead something else like generation diversity? What are your thoughts on why this is? \n\nVeriCOT relies heavily on a LLM to correctly judge the generated premises as valid or invalid. How reliable are Claude's judgements for this?", "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": "ByJQGDzDBz", "reviewer": "Reviewer_37xu", "summary": "This paper introduces VERICOT, a neuro-symbolic method designed to verify reasoning trace of LLMs. \nThe methodology consists of two main components: 1. Autoformalization – translating each natural-language CoT step into a precise formal logic representation and 2. Verification – using automated constraint solvers to check whether the formal statement is logically consistent and entailed by explicitly identified premises. VERICOT demonstrates effectiveness across diverse tasks (ProofWriter, LegalBench, BioASQ), reliably detecting logical errors. Also, The authors also apply this methodology in two use cases—real-time self-reflection and constructing high-fidelity datasets—to actively improve LLM reasoning quality and task performance.", "questions": "The main questions are in the Weaknesses section.\n\nAdditionally, (This is not a drawback, but just a question:)\nCould this methodology also be applied to reasoning traces produced by reasoning-scaled models trained with reinforcement learning (RL), rather than CoTs generated purely through prompting?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 2, "presentation": 4, "contribution": 3, "strengths": "1. This paper deals with relatively unfamiliar concepts such as neuro-symbolic reasoning and first-order logic, yet it is written in a way that is easy for readers to follow. The authors also provide appropriate examples that effectively aid understanding.\n\n2. The overall approach of the paper is well thought out. Decomposing the CoT into atomic units, expressing them in a formal language, and verifying them is a promising direction for improving the interpretability of reasoning.\n\n3. The categorization presented in the paper is clear and logically sound.\n\n4. The two-step problem-solving process—formalization and premise generation—is well designed, and the authors effectively demonstrate the usefulness of their method through its applications in real-time inference and dataset generation.\n\n5. The paper makes appropriate use of the LLM-as-a-judge, relying on it only partially rather than excessively, and successfully leveraging its advantages.", "weaknesses": "1. Questions about the metrics presented in Table 1\n\n1-1. I have several questions regarding the metrics used in the experimental results shown in Table 1.\nThe Pass Rate measures whether a CoT trace is verifiable. Did each baseline method (ER or DSB) apply its own verification method, different from VeriCOT’s?\nIf so, I’m not sure a higher Pass Rate necessarily indicates a better verification method. Some verification methods can be very strict and reject even minor leaps in reasoning, while others may be more lenient and mark more traces as “pass.”\nWouldn’t it be better to apply a stricter verification method, along with the self-reflection mechanism shown in Section 3.4, to produce higher-quality CoTs?\n\n1-2. Related to the above, as I understand it, VCAR represents the proportion of test cases that satisfy both Pass Rate and Precision. If Pass Rate is high, then VCAR will naturally appear favorable. However, as mentioned in 1-1, if a high Pass Rate doesn’t necessarily mean a better verification process, doesn’t that also undermine the interpretive value of the VCAR metric?\n\n1-3. In my opinion, among all the metrics for CoT verification, Precision is the most important.\nThis is because we examine LLMs’ CoTs under the expectation that if their reasoning is logical and sound (even when we don’t know the ground truth), their final answer is likely correct.\nTherefore, Precision—the proportion of truly correct CoTs among those verified by a given method—seems the most meaningful and task-relevant metric.\nHowever, according to Table 1, VeriCOT does not achieve higher Precision than the baselines, and in the case of ProofWriter, its Precision is even lower than VeriCOT-NoPrem. The authors should provide a justification for this.\n\n1-4. What is the reason for the differences in Task Accuracy among methods? Were all methods evaluated on the same CoT samples?\n\n2. Since the proposed approach verifies CoTs through multiple rounds of LLM inference, it would be helpful to report the average verification cost per CoT (e.g., number of LLM calls, computation cost, etc.).\n\n3. Premise generation and premise evaluation—two core components of the proposed method—both rely on LLMs. Consequently, performance may vary greatly depending on which LLM is used. However, the experiments were conducted solely with Claude 3.5 Sonnet.\nIt seems essential to analyze how performance changes across LLMs with different capabilities.\nIf results vary by model, the authors should explain why; if they do not, an explanation for the stability would also be valuable.\n\n4. It would be helpful to include qualitative examples of the Commonsense type premises among the three types of NL Premises.\nThe classification in Table 2—Grounded contextual premise, Acceptable commonsense premise, and Necessary commonsense premise—is somewhat difficult to evaluate in terms of reliability.\nWhat exactly distinguishes something “acceptable” from “necessary”?\nA clearer analysis of what counts as a commonsense premise (and what does not) would strengthen the paper.\nSince the proposed method’s Pass Rate likely depends heavily on how well the model generates commonsense premises, this aspect deserves more attention.\n\n5. It seems that this paper assumes the CoT is already divided into individual steps, but an explanation of how the CoT steps were segmented would be necessary.\n\n\nOverall, the paper’s motivation, proposed solution, structure, and writing quality are excellent. However, I believe the experimental results are still insufficient to convincingly demonstrate the practical usefulness of the proposed method.", "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)