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 solving, where modern instantiation-based techniques can fail when key ground terms and equalities are hidden by auxiliary variables, axiom guards, and nested array terms. We observe that many instances are largely driven by a small set of focal ground terms or constraints, similar to the backdoor sets in SAT solving. Building on this, we present LinguaArray, a framework where an LLM proposes a small Semantic Focus Set (ground terms/constraints), while a conventional SMT solver remains the sole proof engine and certifies all results. LinguaArray uses these LLM-suggested, solver-validated finite sets to significantly enhance solver capability, solving additional satisfiable and unsatisfiable instances that the backend alone fails to solve. It interacts within a finite time and then falls back to the backend solver to mitigate potential regressions. Evaluation on 1015 SMT-LIB instances across five logics under 1200s timeout (including LLM latency) shows that LinguaArray solves up to 69.1% of instances and increases solved-instance counts by 105%--397% over the corresponding backends.
Yuhang Dong, Min Xia, Jinghong Li, Yue Dai, Xinyue Wang, Shi Liang
Wind power forecasting models are often deployed as fixed temporal backbones, but the errors they make can vary across meteorological regimes such as cold waves, heat-and-calm periods, productive typhoon, and destructive storms. We present a guarded Agent-in-the-loop residual adaptation framework that leaves the temporal backbone unchanged and adapts only a small set of scene-conditioned residual experts. An Agent layer interprets external scene information, identifies the current regime, selects residual experts, and applies a correction only when recent observed errors support it. New experts enter the pool after they outperform their initializations on a validation set, keeping model growth under explicit control. Backbone-only and Agent-enhanced forecasts are compared at lead times of 4, 8, 12, 24, and 48 across nine time-series backbones. Across these runs, the guarded framework lowers both MAE and RMSE for all 45 backbone-horizon combinations, with average MAE reductions ranging from 11.21% to 20.26% across backbones. Online-selection baselines, component ablations, and routing analyses identify the roles of residual experts, scene-aware routing, and the online acceptance rule. Candidate-scene runs evaluate the promotion path under controlled conditions; long-term unattended deployment was not evaluated.
Yuhang Dong, Jinghong Li, Xinyue Wang, Yuanning Cui
Fact-verification benchmarks score the final label, while an interactive verifier must first decide whether the available evidence is sufficient. We focus on that intermediate Stop-or-Clarify Decision. Uncertainty alone is insufficient, because the benefit of another evidence-acquisition step is unknown before the step is taken. Sequential Experience-Adaptive Clarification (SEAC) wraps a fixed verifier with a lightweight evidence-acquisition policy. For each claim, SEAC retrieves evidence, runs the verifier, forms a label-free decision state, and combines stop risk with an observational clarification-utility estimate from earlier executed trajectories. Clarification is requested only when this score exceeds the action cost and decision threshold. On SciFact, LIAR, and FEVER, SEAC improves mean accuracy and macro-F1 over the compared fact-verification and active-retrieval baselines. Equal-budget and formula-level diagnostics support selective clarification as a contributor to the gain, while the small SciFact split leaves its paired improvement inconclusive.