Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays
Large language models can often identify useful semantic structure in formal artifacts, but their outputs cannot be trusted as proofs or solver decisions. We study whether LLMs can instead guide formal reasoning systems through a narrow, solver-verifiable interface. We instantiate this idea in quantified array SMT solv...
Kun-Hang Lv, Rui Han, Fuqi Jia et al.
· 0 citations