Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays.

arXiv:2610.39435v1 Announce Type: new Abstract: 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