Aug 2026· 2026 12th International Conference on Big Data and Information Analytics (BigDIA)· pp. 160-167· 0 citations· 24 references
Abstract
Constrained resource-task assignment(RTA) is a foundational problem in operations research and engineering decision support. Turning a natural-language assignment description into a correct optimization model and executable solver code requires expertise in both application semantics and mathematical programming. Large language models (LLMs) offer a promising way to automate this process, but they often misread specialized terminology, omit indispensable constraints, and return numerically valid yet semantically infeasible solutions. Existing self-correction methods mainly rely on code-execution errors and therefore fail to detect formulation-level faults when the solver runs successfully. We present RTA-Verifier, a plug-and-play dual-side verification framework for trustworthy LLM-based constrained assignment modeling. A distillation agent first extracts a multi-level modeling structure, including the problem class, assignment variant, low-level constraints, and explicit exclusions. A structure-side verifier then back-translates the generated model and checks whether it faithfully matches the extracted reference, while a solution-side verifier interprets the numerical solution in application-level terms and detects semantic contradictions that are invisible to the solver. The resulting comments guide a focused refinement step. On a published constrained-assignment benchmark with standard and hard splits, RTA-Verifier achieves 80.0% and 67.8% accuracy, improves code executability and numerical-output reliability, and remains effective across different backbone LLMs.
SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification, is introduced, and Z3 checks domain cross-feasibility and global objective-order preservation for mixed-integer linear formulations, while dReal provides tolerance-aware feasibility/range and $\epsilon$-argmin checks for con...
Formal hardware information-flow verification (IFV) provides strong guarantees against secret-dependent timing and control behavior, but often scales poorly on realistic RTL. We identify two recurring proof barriers in self-composed IFV: implementation complexity, where proof-hard datapath logic dominates even though t...
Liangtao Dai, Yimin Gao, Melika Morsali et al.· 0 citations
This work proposes VPID, a multi-agent framework for generating complex Verilog that achieves monotonic functional improvement and introduces an experience-guided refinement strategy that distills historical waveform mismatches into constraints, guiding the targeted debugging for the unverified ports.
Hong-Guang Wang, Jiaming Guo, Rui Zhang et al.· Proceedings of the Thirty-Fi...· 0 citations
Large language models (LLMs) increasingly generate executable optimization code, yet evaluations often rank programs by objective value, overlooking deployment-relevant properties such as validity under structural constraint changes, failure localization, repairability, and component compatibility. We introduce GenSE-S...
Achraf Ghorbel, Nourchène Elleuch Ben Ayed, Keletso J. Letsholo et al.· IEEE Access· 0 citations
Zero-knowledge virtual machines (zkVMs) enable verifiable execution of general-purpose programs by translating virtual machine semantics into algebraic constraints over execution traces. The correctness of these constraints is critical: a single incorrect constraint can admit forged proofs (under-constrained) or reject...
The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerate legacy code, repair feedback in prompts alone does not prevent subsequent candidates from repeating the same errors. We introduce Certific...
Piyush Jha, A. Ghosh, Vijay Ganesh· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.