VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

LLMs can sound fluent but lack logical correctness: The paper demonstrates that despite Large Language Models producing grammatically smooth text, they frequently make logical errors in high-stakes domains, highlighting a critical gap between fluency and accuracy that existing evaluation methods miss.

Combining AI with formal logic tools improves reliability: VERGE uses a hybrid approach pairing LLMs with SMT solvers (automated logic verification systems) to check whether model outputs are logically consistent, providing formal guarantees where possible rather than relying solely on the model's own reasoning.

Pinpointing exact errors enables better corrections: Rather than simply telling an LLM "your answer is wrong," the framework identifies the precise subset of claims causing logical failures through Minimal Correction Subsets (MCS), allowing the system to provide targeted feedback that guides meaningful refinement rather than generic retry signals.

Different types of claims need different verification strategies: The framework recognizes that logical claims (e.g., mathematical statements) should be verified through formal solvers, while commonsense reasoning requires different approaches like LLM ensembles, avoiding one-size-fits-all verification that could miss domain-specific errors.

Formal verification moves beyond surface-level similarity: By checking logical equivalence rather than comparing text similarity, VERGE eliminates bias toward particular phrasings and ensures that different ways of expressing the same correct answer are recognized as equivalent, improving fairness in evaluation.