Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits

Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, but they fail silently. A generated model often runs and still formulates the wrong problem. This paper develops a theory of falsification-based verification for this setting. Every numeric quantity in the description is a typed slot, and a candidate model is tested only through solver calls on slot-transformed instances; no reference model or label is consulted. From duality, comparative statics, and polyhedral limit arguments we derive a battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange. Every test is sound, so a violation certifies unfaithfulness and the false-positive rate is zero by design. We characterize what such verification can never see, give conditions under which the canonical error classes are detected with certainty, and prove that no fixed-threshold perturbation tester is simultaneously sound and nontrivial. Experiments on 326 ground-truth models from NL4OPT and four benchmark families confirm the theory. The battery attains a 0.0% false-positive rate against 54.9% for a threshold tester, detects 70.0% of certified conditional-class mutants, convicts 40.4% of the mutants invisible to execution-accuracy scoring, and reproduces the predicted detectability pattern including its zeros.

CASP: Learning-Augmented Offline Approximation with Verifiable Certificates and Bounded-Loss PAC Guarantees

Machine-learned predictions can speed up offline NP-hard optimization, but asking a predictor what to do amounts to asking it to solve the problem, and committing an unchecked prediction forfeits every worst-case guarantee. CASP (Certificate-Augmented Solution Pruning) instead asks which parts of the search space may be ignored, and accepts each answer only after a sound polynomial-time verifier has checked it, so correctness never depends on prediction quality. We develop the learning theory of this design. The verifier makes the induced loss class uniformly bounded, so certificate parameters are learnable from $\tilde O(\varepsilon^{-2}\log K)$ samples ($K$ the maximum instance size), whereas the unverified commitment class admits no distribution-free rate and, under cost spread $R$, none below $Ω(R/\varepsilon^2)$. Filtering noisy predictions by verifiable confidence dominates the standard min-combiner, with a margin we compute in closed form, and the prediction stays useful even given the LP, because it breaks ties on degenerate optimal faces, where every symmetric LP policy, meaning one whose commitments depend on the instance only through the verifiable confidence values, provably stalls. Experiments on five problems test the theory's quantitative predictions. With trained predictors, unverified pruning loses up to $26%$ of the optimum under distribution shift, while the verified deployment of the same predictions loses nothing.

A Multi-level Distillation based Dense Passage Retrieval Model

Ranker and retriever are two important components in dense passage retrieval. The retriever typically adopts a dual-encoder model, where queries and documents are separately input into two pre-trained models, and the vectors generated by the models are used for similarity calculation. The ranker often uses a cross-encoder model, where the concatenated query-document pairs are input into a pre-trained model to obtain word similarities. However, the dual-encoder model lacks interaction between queries and documents due to its independent encoding, while the cross-encoder model requires substantial computational cost for attention calculation, making it difficult to obtain real-time retrieval results. In this paper, we propose a dense retrieval model called MD2PR based on multi-level distillation. In this model, we distill the knowledge learned from the cross-encoder to the dual-encoder at both the sentence level and word level. Sentence-level distillation enhances the dual-encoder on capturing the themes and emotions of sentences. Word-level distillation improves the dual-encoder in analysis of word semantics and relationships. As a result, the dual-encoder can be used independently for subsequent encoding and retrieval, avoiding the significant computational cost associated with the participation of the cross-encoder. Furthermore, we propose a simple dynamic filtering method, which updates the threshold during multiple training iterations to ensure the effective identification of false negatives and thus obtains a more comprehensive semantic representation space. The experimental results over two standard datasets show our MD2PR outperforms 11 baseline models in terms of MRR and Recall metrics.