VERGE：面向可验证 LLM 推理的形式化精化与引导引擎

VERGE 是一个神经符号框架，将 LLM 与 SMT 求解器结合，通过迭代精化生成验证引导的答案：把 LLM 输出拆解为原子断言、自动形式化为一阶逻辑并用自动定理证明验证一致性。它引入多模型形式语义等价共识、按断言类型分流的语义路由，以及用最小修正子集（MCS）精确定位逻辑错误。在 GPT-OSS-120B 上，VERGE 在多个推理基准上收敛时平均性能较单次通过提升 18.7%。