AI RESEARCH
VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
arXiv CS.CL
•
ArXi:2601.20055v2 Announce Type: replace Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. Our approach decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. We.