← Back to all news
arXiv AI By Kunhang Lv, Rui Han, Fuqi Jia, Yuhang Dong, Feifei Ma, Jian Zhang

Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays

Read the original on arXiv AI →

The paper introduces LinguaArray, a framework that uses large language models (LLMs) to suggest a small set of focal ground terms or constraints—called a Semantic Focus Set—in quantified array SMT solving. The LLM’s suggestions are then verified by a conventional SMT solver, which remains the sole source of proof. Experiments on 1,015 SMT-LIB instances show that LinguaArray solves up to 69.1% of cases and increases the number of solved instances by 105%–397% compared to the backends alone.

Machine-generated by The Flow from the publisher's headline and feed description — not written or checked by a human. The full article lives at arXiv AI.

Related stories

arXiv AI
Oct 19

Repairing LLM-Generated Specifications with Deterministic Diagnosis

The paper introduces DRAGO, a framework that repairs formal specifications generated by large language models (LLMs) using deterministic, formalism‑specific diagnosis instead of ungrounded LLM critiques. DRAGO selectively rewrites specifications only when the diagnosed error weight decreases, reducing regressions from 11.8% to 1.3% and improving answer accuracy by 12.9 percentage points over zero‑shot formalization and 8.7 percentage points over LLM‑diagnostic repair across five benchmarks. Additionally, the authors identified and corrected rendering defects in Planetarium that caused half of its floor‑tile split instances to be inconsistent with reference formalizations.

By Giovanni Vaccarino, Emanuele La Malfa, Dehai Min, Hanrong Zhang, Pier Luca Lanzi, Lu Cheng, Michael J. Wooldridge, Philip S. Yu, Sara Bernardini
llmsbenchmarks
More like this →
arXiv AI
Aug 20

SMTrap: Cost-Effective DoS Attacks Against Large Reasoning Models via SMT Conflict Guidance

The paper introduces SMTrap, a cost‑effective denial‑of‑service attack framework for large reasoning models that does not rely on model feedback or GPU resources. It uses conflict counts from an SMT solver to guide the creation of inference‑heavy constraint satisfaction problem queries, exploiting the models’ backtracking search to induce long output trajectories. Experiments on seven state‑of‑the‑art models show SMTrap achieves DoS effects several times stronger than existing methods, and the authors also present a mitigation tool that reduces token usage.

By Jian Yang, Zhenqi Feng, Zhaoyang Yu, Zhaoxin Fan, Kejian Wu, Xiaofeng Wang, Zheng Zhu, Jianjun Huang, Wei You, Bin Liang
benchmarks
More like this →