{"id":"6f0fc0df-fd58-475e-b459-888516af3365","arxiv_id":"2411.16718","paper_version":5,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"NeuS-V evaluates text-to-video alignment by converting prompts to temporal logic specifications and formally verifying a video automaton, and it correlates more strongly with human judgments than VBench.","lead":"This paper introduces NeuS-V, a metric that turns a video prompt into formal temporal logic and checks generated videos against it with a verification tool. It reports that current text-to-video models fail most temporally complex prompts, and that NeuS-V tracks human judgments of text-to-video alignment far better than existing quality metrics.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Equation (8) assumes all atomic propositions and all frame windows are conditionally independent, so the model-checked satisfaction probability is computed over a factored approximation of the video, not the video itself; the 5x human-correlation claim depends on this unvalidated factorization.","rationale":"The reader's weakest_assumption points at VLM calibration on static COCO images. I agree that is a risk, but the more precise and more damaging issue is Eq. (8): even perfectly calibrated per-proposition marginals do not determine the joint distribution over label configurations, and Algorithm 3 assumes a full factorization across propositions and across time windows. This is not a minor implementation detail; it defines what satisfaction probability is computed. The paper gives no evidence that the factored automaton agrees with the actual video, and the MSR-VTT robustness check (Table 2) only tests mean separation, not whether the automaton's probability model is faithful. The 5x correlation headline therefore inherits this unvalidated assumption. I would keep the reader's CONDITIONAL verdict, with the condition explicitly including a test of the Eq. (8) factorization. The proposed test is feasible because the authors already collect per-proposition VLM scores; adding human binary labels for a subset is the natural way to estimate the joint distribution.","tokens_in":21939,"tokens_out":5941,"duration_ms":57657,"concrete_test":"On a subset of the 160 prompts, collect per-window VLM marginals C_i^* and human binary labels for every proposition per window (or a second independently prompted VLM as a noisy oracle). Build two DTMCs: one with Eq. (8) product transitions and one with empirical joint transition frequencies of the observed label vectors per window. Compare the resulting satisfaction probabilities and their correlations with human text-to-video alignment scores. If the median absolute difference in satisfaction probability exceeds 0.1, or if the Gen-3 Pearson correlation drops from 0.479 toward the VBench baseline (0.089) when the empirical joint automaton is used, the factorization in Eq. (8) is load-bearing and the 5x claim is not established. Also report bootstrap confidence intervals for the Pearson coefficients in Figure 4.","verdict_should_be":"UNCHANGED","load_bearing_attack":"NeuS-V's automaton is not a representation of the observed video but of a product-of-Bernoulli approximation. In Eq. (8), the transition probability δ(q,q') is ∏_i (C_i^*)^{1{q'_i=1}}(1-C_i^*)^{1{q'_i=0}}, using only the marginal VLM confidence C_i^* for each proposition in a frame window. Algorithm 3 in Appendix 12 then attaches this same distribution from every previous state to every current state, so the next window's label configuration is independent of the previous window and each proposition is independent of all others. For generated video this is false: 'cyclist turns' is structurally dependent on 'cyclist signals turn'; an object that exists in one window usually persists into the next; and actions span multiple windows. Consequently P[AV |= Φ] computed by STORM is the satisfaction probability of a factored distribution, not of the actual video content. The ECDF calibration in Eq. (9) can rescale scores but cannot correct a wrong joint distribution. Section 6.2 ablates formal TL against VQA baselines but never tests this factorization, and Section 11.2 calibrates only per-proposition marginals on static COCO images. Since the headline 'over 5x' advantage in Section 6.1 is computed from scores produced by this approximation, the central empirical claim rests on an unvalidated independence assumption.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes NeuS-V, a neuro-symbolic metric for evaluating text-to-video alignment. It converts a text prompt into temporal-logic specifications via an LLM-based module (PULS), obtains per-proposition confidence scores from a VLM over frame windows, constructs a DTMC automaton of the video, and computes a satisfaction probability using the STORM probabilistic model checker. The satisfaction probability is then calibrated with an empirical CDF and averaged over four evaluation modes. The authors introduce a prompt suite of temporally extended prompts, benchmark four text-to-video models, compare against VBench and VQA-style baselines, and report that NeuS-V correlates with human text-to-video alignment ratings by 'over 5x' more strongly than existing metrics. They also report an MSR-VTT robustness experiment.","tokens_in":22254,"tokens_out":6501,"duration_ms":60102,"significance":"If the central empirical claim holds, NeuS-V would be a valuable addition to the T2V evaluation toolbox: it offers an interpretable, formal-verification-based score that targets temporal fidelity, a dimension neglected by quality-focused metrics such as VBench. The paper explicitly ships its benchmark, code, and dataset, and the use of a standard probabilistic model checker (STORM) makes the verification step machine-checkable and reproducible. The temporally extended prompt suite is a useful resource in itself. However, the headline 'over 5x' claim currently rests on small-scale human annotations without confidence intervals or significance tests, and on an unvalidated product-of-marginals independence assumption in the automaton construction. These issues need to be addressed before the empirical contribution can be considered established.","major_comments":[{"comment":"The transition probability δ(q,q') is defined as the product of per-proposition marginal VLM confidences for the target state, and Algorithm 3 assigns exactly this same distribution from every predecessor state to every successor state (lines 21-23). The resulting DTMC therefore models each frame window as an independent draw from a product-of-Bernoulli distribution over propositions. It does not represent conditional dependencies such as object persistence across windows, action preconditions, or the structural dependence between propositions like 'cyclist signals turn' and 'cyclist turns'. Since the satisfaction probability P[AV |= Φ] is computed over this factored approximation, the central claim in Section 6.1 rests on an unvalidated independence assumption. Please test this assumption, e.g., by comparing against a baseline that carries state across windows or by measuring violations of independence on a labeled video sample.","section":"Section 4.3, Eq. (8), and Algorithm 3 (Appendix 12)"},{"comment":"The 'over 5x' claim is based on point estimates of Pearson's r (e.g., 0.479 vs 0.089 for Gen-3) with no confidence intervals, no significance tests, and no adjustment for comparing two correlation coefficients computed on the same prompts. Appendix 13 reports only 20 annotators recruited via social media, with no inter-annotator agreement or demographic breakdown. A point-estimate ratio of 5x is not statistically established. Please provide bootstrap confidence intervals and a significance test for the difference between correlated correlations, and report annotation reliability (e.g., Krippendorff's alpha or Fleiss' kappa), ideally on a larger and more diverse annotator pool.","section":"Section 6.1, Figure 4"},{"comment":"The final score uses f_ECDF(P[AV |= Φ], D_m), where D_m is described only as 'the distribution of satisfaction probabilities of each evaluation mode from wide samples of synthetic videos.' The paper never defines how D_m is constructed, how large it is, whether it contains the test videos, or whether it is fit per prompt/theme/mode. Because this is a fitted mapping, the free distribution D_m is load-bearing for every reported score, including Table 1 and Figure 4. Please specify the estimation procedure, the train/test split, and the sensitivity of the reported correlations to the choice of D_m.","section":"Section 4.4, Eq. (9)"},{"comment":"The VLM confidence scores are calibrated using COCO Captions, a static-image dataset with positive/negative image-caption pairs. The propositions in NeuS-V, however, include actions and temporal relationships (e.g., 'cyclist signals turn', 'traffic light turns green') that appear only in video. The paper provides no evidence that token probabilities from InternVL2-8B are calibrated for these video-specific propositions, nor for the three-frame window used in the main experiments. Please validate or recalibrate on video data with proposition-level ground truth, or explicitly analyze how miscalibration propagates to the satisfaction probability.","section":"Section 11.2 and Eq. (6)"},{"comment":"The ablation replaces the TL/formal-verification stage with VQA-style yes/no questions, but it does not vary the automaton construction or the independence assumption. Therefore the ablation cannot establish that the formal verification step, rather than the specific VLM scoring or the factored automaton, is responsible for the improved correlation. An additional control should run NeuS-V's automaton and satisfaction computation against a non-formal baseline that uses the same per-frame scores in a simple logical conjunction or a hand-coded if-else check, to isolate the contribution of the formal machinery.","section":"Section 6.2"}],"minor_comments":[{"comment":"The paper states that the prompt suite contains 360 prompts (Section 5), but Section 6.1 and Appendix 13 consistently use 160 prompts (Table 5). Please reconcile this discrepancy and use one number throughout.","section":"Section 5 vs. Section 6.1 / Appendix 13"},{"comment":"The displayed TL specification appears to omit the implication and the 'eventually' consequent described in the surrounding text; as written it is a conjunction under □, not a formalization of the stated conditional. Please correct the formula so that it matches the prose.","section":"Eq. (1)"},{"comment":"InternVL2-8B is cited as reference [25], but the reference for InternVL2 appears to be [45] (OpenGVLab). Please check and correct the citation.","section":"Section 5, references"},{"comment":"The labeling function is written as λ : Q → 2^|P|; the intended codomain is presumably 2^P, the power set of atomic propositions. This is a notation typo that should be fixed.","section":"Section 3, preliminaries"},{"comment":"Several TL formulas in the prompt-suite tables are malformed or inconsistent, such as 'G ... U ...' constructs and the stray '¡' character in the lamp prompt. Please proofread the generated specifications, as they are central to the reproducibility of the benchmark.","section":"Tables 6 and 7"}],"recommendation":"major_revision","confidential_remarks":"The authors' prior work (NSVS-TL, reference [10]) provides much of the core verification machinery, so the editor may wish to ensure that the novelty claim for T2V evaluation is scoped carefully. The main empirical evidence comes from a small convenience-sample human study; if the authors cannot strengthen it with confidence intervals or a larger annotation effort, the 'over 5x' claim should be removed or heavily qualified. The approach is plausible, but the current manuscript needs additional validation before it can support the strength of its claims."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nThe thing to know: this is a genuine new application of formal verification to text-to-video evaluation, and the 160-prompt temporally extended suite is a useful resource. The headline claim—NeuS-V correlates over 5x better with human judgments than VBench—is not yet established. The direction is consistent across four models, which is reassuring, but the human data come from 20 annotators in a convenience sample, with no confidence intervals or significance tests, and comparing ratios of Pearson coefficients is a fragile way to quantify an advantage.\n\nWhat the paper does well: the pipeline is clean. PULS turns prompts into temporal-logic specifications, InternVL2-8B provides token-probability marginals for atomic propositions, the video is abstracted as a DTMC, and STORM computes the satisfaction probability. The formal checking step is standard and the ablation in Section 6.2 shows that the formal grounding adds something over plain VQA baselines. The MSR-VTT aligned/misaligned sanity check is a reasonable extra.\n\nThe soft spots are real but not disqualifying. The largest is the independence assumption in Eq. (8). The transition probabilities factor as a product of per-proposition marginals, and Algorithm 3 assigns that same factored distribution to every incoming state, so the next frame window is conditionally independent of the previous one and all propositions are independent. For video, that is false: objects persist across frames, actions have prerequisites, and a 'cyclist turns' is not independent of 'cyclist signals turn.' The paper never validates this factorization. The ECDF calibration can rescale scores, but it cannot correct a wrong joint distribution. Since the 5x correlation is computed from scores produced by this approximation, the central empirical claim rests on an unvalidated model.\n\nSecond, the calibration distribution D_m in Eq. (9) is never defined, and the VLM is calibrated on static COCO images but applied to synthetic video frames, a domain shift the paper does not investigate. Third, the human-evaluation section would need inter-annotator agreement and uncertainty bounds to support the strength of the claim.\n\nWho this is for: anyone building or evaluating T2V metrics, and formal-methods people interested in neuro-symbolic pipelines. I'd bring it to a reading group.\n\nRecommendation: send to peer review. The framework is worth referee time, and the authors can address the independence concern by testing a more expressive automaton or at least discussing the bias, reporting bootstrapped CIs for the correlations, specifying D_m, and releasing the code and data as promised. If those hold, this could become a useful metric. I would cite the framework, not the 5x number.","headline":"A genuinely new formal-verification application to T2V evaluation with a useful prompt suite, but the 5x correlation claim is not yet established due to unvalidated independence assumptions and small human annotation.","tokens_in":22782,"tokens_out":4158,"would_cite":true,"duration_ms":37028,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"NeuS-V converts text prompts into temporal-logic specifications and generated videos into automata, then formally verifies alignment, claiming over 5× higher correlation with human judgments than existing metrics.","keywords":["text-to-video evaluation","temporal logic","formal verification","neuro-symbolic","video automaton","discrete-time Markov chain","vision-language model calibration","temporal fidelity"],"falsifier":"Take a set of generated videos where a human checker confirms the VLM consistently mislabels an object or action (for example, a visible cyclist being scored as absent or a lane change scored as no movement), then compute NeuS-V scores and ask whether the metric's correlation with human text-to-video alignment ratings is significantly lower on those videos than on videos where the VLM labels are correct; a collapse in correlation would indicate the formal verification layer is only as good as the perception probabilities feeding it.","tokens_in":1655,"feed_emoji":"🎬","tokens_out":2338,"duration_ms":49015,"temperature":0.7,"pith_summary":"The paper introduces NeuS-V, an evaluation metric for text-to-video models that checks whether a generated video actually follows the temporal sequence described in a text prompt. It converts the prompt into a formal temporal-logic specification, turns the video into a discrete-time Markov chain automaton using vision-language-model confidence scores, and then applies probabilistic model checking to compute a satisfaction probability. The authors claim that this neuro-symbolic approach correlates over five times more strongly with human text-to-video alignment judgments than current visual-quality benchmarks like VBench. They also release a prompt suite of temporally extended scenarios and report that state-of-the-art video generators score poorly on it, arguing that temporal fidelity is a real, currently unmet requirement for safety-critical applications such as autonomous driving.","feed_headline":"Formal logic catches when AI videos ignore the prompt","feed_subtitle":"NeuS-V turns prompts into temporal-logic specs and checks videos against them, beating visual-quality benchmarks on human correlation.","key_machinery":"The load-bearing machinery is the video automaton: a discrete-time Markov chain $\\mathcal{A}_V = (Q, q_0, \\delta, \\lambda)$ where each state labels which atomic propositions from the prompt are true in a frame window, and transition probabilities $\\delta(q,q')$ are the product of calibrated VLM token probabilities (Eq. 8). This automaton converts a neural perception signal into a structured object that can be checked against the temporal-logic specification $\\Phi$ using the probabilistic model checker STORM; the PULS module (an LLM pipeline optimized with MIPROv2) performs the prompt-to-specification translation across four evaluation modes (object existence, spatial relationship, object-action alignment, overall consistency). The key move is that temporal operators such as UNTIL and EVENTUALLY are evaluated symbolically over the automaton rather than approximated by frame-level similarity.","core_discovery":"The central claim is that formal verification of a video against a temporal-logic specification yields a more human-aligned measure of text-to-video alignment than existing metrics that focus on visual quality or per-frame semantic similarity. Concretely, NeuS-V builds a video automaton $\\mathcal{A}_V$ as a discrete-time Markov chain whose states are truth assignments of atomic propositions extracted from the prompt, with transition probabilities computed as products of calibrated VLM confidence scores across frames. Probabilistic model checking then computes the satisfaction probability $P[\\mathcal{A}_V \\models \\Phi]$ against the temporal-logic formula $\\Phi$ produced by the PULS pipeline, and this probability is mapped through an empirical cumulative distribution to a final score. Across four video models (Gen-3, Pika, T2V-Turbo-v2, CogVideoX-5B), the reported Pearson correlations with human alignment annotations are roughly 0.48–0.62 for NeuS-V compared with near zero or negative values for VBench and simple VLM-based question-answering baselines, supporting the paper's stated 5× improvement in correlation.","pith_inferences":["A natural extension the authors leave implicit is using the automaton structure to trace which temporal operator first fails in a generated video, giving actionable feedback such as 'the UNTIL condition is violated at frame 40' for targeted re-prompting or model debugging.","The 5× improvement claim is contingent on the VLM calibration threshold tuned on COCO still images; a stress test that recalibrates on synthetic video frames or on frames with rare objects could reveal whether the advantage persists or partly reflects calibration choices.","Since the satisfaction probability is a continuous signal, NeuS-V could plausibly serve as a reward model for reinforcement-learning fine-tuning of video generators, closing the loop between evaluation and training on temporal fidelity."],"forward_implications":["If NeuS-V's correlation claim holds, it provides a practical way to rank text-to-video models on temporal adherence, complementing visual-quality leaderboards with a dimension that is currently under-measured.","The benchmark results imply that current video generators (including strong closed-source models) systematically fail at temporally extended prompts, often substituting panning and zooming for real event sequencing, which would motivate new training objectives and post-hoc reprompting pipelines.","The formal grounding means the metric returns not just a score but a verifiable satisfaction probability for each temporal-logic spec, which could be used as a filter to accept or reject generated videos before deployment in simulation or safety-critical systems.","On the MSR-VTT repurposed validation set, NeuS-V separates aligned from misaligned video-caption pairs by a larger margin than VBench, suggesting the approach generalizes beyond the authors' synthetic prompt suite to established video-captioning data.","The comparison against VLM-only VQA baselines shows that the same underlying vision models achieve higher human correlation when wrapped in temporal-logic verification, indicating the formal layer adds signal beyond raw neural perception."],"supporting_citations":[{"why":"VBench is the primary visual-quality benchmark that NeuS-V is compared against on human correlation and on MSR-VTT separation.","marker":"[23]"},{"why":"NSVS-TL supplies the prior neuro-symbolic video-understanding approach that NeuS-V extends to the evaluation setting.","marker":"[10]"},{"why":"COCO Captions is the dataset used to construct the calibration set for tuning the VLM false-positive threshold.","marker":"[7]"},{"why":"STORM is the probabilistic model checker used to compute the satisfaction probability of the video automaton against the temporal-logic specification.","marker":"[19]"},{"why":"InternVL2-8B is the vision-language model that produces the per-frame semantic confidence scores used in automaton construction.","marker":"[45]"},{"why":"MSR-VTT provides the repurposed validation data for testing whether NeuS-V can distinguish aligned from misaligned video-caption pairs at scale.","marker":"[52]"},{"why":"GPT-4 (and GPT-4o) is the LLM family powering the PULS prompt-to-proposition and prompt-to-TL translation modules.","marker":"[1]"},{"why":"DSPy with MIPROv2 is used to optimize the few-shot prompts and example selection for the PULS translation modules.","marker":"[30]"}],"fun_headline_variants":["Formal logic verifies AI video-prompt alignment","NeuS-V: Proven check on video-prompt fidelity","Temporal logic beats pixel metrics for video-prompt match","5x better correlation: formal verification for video models","Video models flunk temporal prompts, formal check finds"],"cache_read_input_tokens":24960,"weakest_assumption_plain":"The central claim collapses if a vision-language model's calibrated confidence scores, tuned on static COCO images, do not faithfully represent what is actually true in each frame of a generated video, because those scores directly determine the automaton's transition probabilities and hence the satisfaction probability.","fun_headline_variants_meta":{"raw":{"variants":["Formal logic verifies AI video-prompt alignment","NeuS-V: Proven check on video-prompt fidelity","Temporal logic beats pixel metrics for video-prompt match","5x better correlation: formal verification for video models","Video models flunk temporal prompts, formal check finds"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00028,"raw_usage":{"total_tokens":1690,"prompt_tokens":1006,"completion_tokens":684,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":622,"completion_tokens_details":{"reasoning_tokens":606}},"tokens_in":622,"tokens_out":684,"duration_ms":5517,"temperature":1.0,"reasoning_tokens":606,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T14:21:34.676495+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a set of generated videos where a human checker confirms the VLM consistently mislabels an object or action (for example, a visible cyclist being scored as absent or a lane change scored as no movement), then compute NeuS-V scores and ask whether the metric's correlation with human text-to-video alignment ratings is significantly lower on those videos than on videos where the VLM labels are correct; a collapse in correlation would indicate the formal verification layer is only as good as the perception probabilities feeding it.","supporting_citations":[{"cited_title":"Towards neuro- symbolic video understanding","cited_arxiv_id":null,"evidence_quote":"NSVS-TL supplies the prior neuro-symbolic video-understanding approach that NeuS-V extends to the evaluation setting."},{"cited_title":"Internvl 2.0: A suite of multimodal large lan- guage models for vision and language tasks","cited_arxiv_id":null,"evidence_quote":"InternVL2-8B is the vision-language model that produces the per-frame semantic confidence scores used in automaton construction."},{"cited_title":"Msr-vtt: A large video description dataset for bridging video and language","cited_arxiv_id":null,"evidence_quote":"MSR-VTT provides the repurposed validation data for testing whether NeuS-V can distinguish aligned from misaligned video-caption pairs at scale."},{"cited_title":"Joshi, Hanna Moazam, Heather Miller, Matei Zaharia, and Christopher Potts","cited_arxiv_id":null,"evidence_quote":"DSPy with MIPROv2 is used to optimize the few-shot prompts and example selection for the PULS translation modules."}],"review_version":1}