Pith. sign in

REVIEW 5 major objections 5 minor 75 references

Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification

T0 review · 5 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2411.16718 v5 pith:YQGXG44I submitted 2024-11-22 cs.CV cs.AI

S P Sharan , Minkyu Choi , Sahil Shah , Harsh Goel , Mohammad Omama , Sandeep Chinchali This is my paper · ORCID
classification cs.CVcs.AI
keywords text-to-videoevaluationtemporallogicformalverificationneuro-symbolicvideoautomatondiscrete-timeMarkovchainvision-languagemodelcalibrationfidelity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

5 major / 5 minor

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.

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 (5)
  1. [Section 4.3, Eq. (8), and Algorithm 3 (Appendix 12)] 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.
  2. [Section 6.1, Figure 4] 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.
  3. [Section 4.4, Eq. (9)] 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.
  4. [Section 11.2 and Eq. (6)] 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.
  5. [Section 6.2] 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.
minor comments (5)
  1. [Section 5 vs. Section 6.1 / Appendix 13] 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.
  2. [Eq. (1)] 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.
  3. [Section 5, references] InternVL2-8B is cited as reference [25], but the reference for InternVL2 appears to be [45] (OpenGVLab). Please check and correct the citation.
  4. [Section 3, preliminaries] 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.
  5. [Tables 6 and 7] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: NeuS-V's headline correlation claim is an externally benchmarked empirical result, and the metric is an explicit function of its inputs rather than a fitted rename of the prediction target.

full rationale

The paper's central claim—that NeuS-V correlates 'by over 5x' with human text-to-video alignment ratings—is established empirically against external human annotations (Figure 4, Table 1), not derived from the definition of the metric. The pipeline is fully specified: PULS converts prompts to propositions and TL specifications (Eqs. 2-5), the VLM produces per-proposition token probabilities (Eq. 6), the video automaton is built explicitly (Eqs. 7-8 and Algorithm 3), STORM computes the satisfaction probability, and Eq. (9) applies an ECDF normalization. The fitted components are the VLM false-positive threshold calibrated on COCO captions (Section 11.2) and the ECDF distribution D_m; neither is fitted to the human alignment labels used for the headline correlation. The self-citations to [10] and [53] provide background for representing video as a DTMC, but the paper supplies its own construction and the correlation result does not reduce to those citations. The independence/product-form assumption in Eq. (8) is a modeling and validity concern—the skeptic's factorization critique—but it is not circular: it does not make the output equal to the input by construction. It is an empirically testable weakness, not a definitional equivalence. The under-specification of D_m is a missing-detail/data-leakage risk, not circularity. Overall, the derivation is self-contained and benchmarked externally, so no circular step is established.

Assumptions & free parameters 4 free parameters · 5 assumptions · 0 invented entities

The central claim rests on two learned stacks: an LLM stack that turns prompts into TL specifications and a VLM stack that labels video frames; both are treated as reliable without independent verification on synthetic video. The final score calibration introduces an empirical distribution D_m whose provenance is unspecified, and human correlation claims use a small convenience sample. No physical or ontological entities are introduced.

free parameters (4)
  • false-positive threshold gamma_fp = not reported numerically
    Chosen per VLM on the COCO Captions calibration set to maximize accuracy; maps raw VLM token probabilities to calibrated truth values (Sec. 11.2).
  • empirical satisfaction-distribution D_m = unspecified
    Final score is f_ECDF(P[AV |= Phi], D_m), a percentile mapping built from 'wide samples of synthetic videos'; if D_m includes the evaluated videos, the score is a fitted rank (Eq. 9).
  • optimized PULS few-shot prompts theta*_T2P and theta*_T2TL = not shipped in full form
    Selected via MIPROv2 and DSPy on DT2P|train and DT2TL|train; these prompts determine the TL specifications used for scoring.
  • frame window size w = 3
    Chosen by ablation; larger windows were not tested due to context limits (Table 3).
assumptions (5)
  • domain assumption VLM token probabilities faithfully estimate atomic proposition truth in video frames
    Central perception signal; calibrated on static COCO images, not on synthetic video with temporal events (Sec. 4.2, 11.2).
  • domain assumption LLM-based PULS produces TL specifications that preserve the prompt's intended temporal semantics
    No formal correctness guarantee; prompts optimized on a small training set (Sec. 4.1).
  • domain assumption Atomic propositions are conditionally independent, so transition probabilities factor as products
    Eq. (8) multiplies per-proposition probabilities; correlations between propositions such as cyclist signaling and turning are not modeled.
  • domain assumption Human annotations of text-to-video alignment are a valid ground truth
    20 annotators recruited from social media; no inter-annotator agreement or error bars reported (Sec. 13).
  • standard math DTMC and PCTL model checking semantics are sound
    Standard probabilistic model checking via STORM (Sec. 4.4).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification." pith.science (2026). https://pith.science/paper/YQGXG44I

@misc{pith2026241116718,
  author       = {Pith},
  title        = {Pith review of: Neuro-Symbolic Evaluation of Text-to-Video Models using Formal Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/YQGXG44I}},
  note         = {Machine review of arXiv:2411.16718}
}
read the original abstract

Recent advancements in text-to-video models such as Sora, Gen-3, MovieGen, and CogVideoX are pushing the boundaries of synthetic video generation, with adoption seen in fields like robotics, autonomous driving, and entertainment. As these models become prevalent, various metrics and benchmarks have emerged to evaluate the quality of the generated videos. However, these metrics emphasize visual quality and smoothness, neglecting temporal fidelity and text-to-video alignment, which are crucial for safety-critical applications. To address this gap, we introduce NeuS-V, a novel synthetic video evaluation metric that rigorously assesses text-to-video alignment using neuro-symbolic formal verification techniques. Our approach first converts the prompt into a formally defined Temporal Logic (TL) specification and translates the generated video into an automaton representation. Then, it evaluates the text-to-video alignment by formally checking the video automaton against the TL specification. Furthermore, we present a dataset of temporally extended prompts to evaluate state-of-the-art video generation models against our benchmark. We find that NeuS-V demonstrates a higher correlation by over 5x with human evaluations when compared to existing metrics. Our evaluation further reveals that current video generation models perform poorly on these temporally complex prompts, highlighting the need for future work in improving text-to-video generation capabilities.

Figures

Figures reproduced from arXiv: 2411.16718 by the authors.

Figure 1
Figure 1. Current generative video evaluation methods struggle with temporal fidelity. NeuS-Vconverts prompts into Temporal Logic specifications and formally verifies them against a video automaton. The upper video aligns with the prompt’s temporal sequencing, while the lower video, despite being visually appealing, fails to do so. Unlike VBench, NeuS-V effectively differentiates between them. Abstract Recent advancements in … view at source ↗
Figure 2
Figure 2. Video automaton from the running example. Above is an automaton of a video generated by the Gen-3 model con￾structed with a TL specification (See Eq. (1)). Every state qt from a frame F is labeled and has incoming and outgoing transition probabilities δ(q, q′ ) ∈ [0, 1]. For example, in frame F8, we have probabilities P(p4) = 0.8 and P(p5) = 0.9, where p4 repre￾sents the atomic proposition “cyclist turns”, and p5 re… view at source ↗
Figure 3
Figure 3. Spatio-temporal and semantic measurements be￾tween a text prompt and a video by NeuS-V. We first decompose the text prompt to TL specification Φ, then transform the synthetic video into an automaton representation AV . Finally, we calculate the satisfaction probability by probabilistically checking the extent to which AV satisfies Φ. 4. Methodology Given a synthetic video V from T2V model MT2V : T → V, where T is a … view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Correlation with Human Annotations. NeuS-V con￾sistently shows a stronger alignment with human text-to-video an￾notations (Pearson coefficients displayed at the top of each plot). Correlation with Human Annotations. We evaluate the selected video generation models usin…
Figure 6
Figure 6. Figure 6: Is Formal Language Important? VLMs without grounding in formal temporal logic lead to lower pearson coef￾ficients (in brackets) as compared to NeuS-V from [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Calibration Plots. We plot the accuracy vs threshold for all VLMs on our calibration dataset constructed from the COCO Caption dataset (top left). We plot the True Positive Rate (TPR) vs False Positive Rate (FPR) across all thresholds on the top right. Finally, the bot…
Figure 8
Figure 8. Figure 8: Tool for Annotating Videos. Subjects are instructed to disambiguate quality and alignment during annotation, scoring each from a range of 1 through 5 [PITH_FULL_IMAGE:figures/full_fig_p017_8.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

75 extracted references · 53 canonical work pages

  1. [1]

    Gpt-4 technical report

    Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ah- mad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. Gpt-4 technical report. arXiv preprint arXiv:2303.08774 ,

    arXiv

  2. [2]

    Llama 3.2: Revolutionizing edge ai and vision with open, customizable models

    Meta AI. Llama 3.2: Revolutionizing edge ai and vision with open, customizable models. Meta AI Blog , 2024. Available at https://ai.meta.com/blog/llama- 3 - 2 - connect - 2024 - vision - edge - mobile - devices/. 4, 3

    work page 2024

  3. [3]

    Principles of Model Checking

    Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. 3

    work page 2008

  4. [4]

    Align your latents: High-resolution video synthesis with la- tent diffusion models

    Andreas Blattmann, Robin Rombach, Huan Ling, Tim Dock- horn, Seung Wook Kim, Sanja Fidler, and Karsten Kreis. Align your latents: High-resolution video synthesis with la- tent diffusion models. In Proceedings of the IEEE/CVF Con- ference on Computer Vision and Pattern Recognition, pages 22563–22575, 2023. 2

    2023

  5. [5]

    Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions

    Andrea Brunello, Angelo Montanari, and Mark Reynolds. Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions. In 26th Inter- national Symposium on Temporal Representation and Rea- soning (TIME 2019), pages 17:1–17:19, Dagstuhl, Germany,

    work page 2019

  6. [6]

    Storybench: A multifaceted benchmark for continuous story visualization, 2023

    Emanuele Bugliarello, Hernan Moraldo, Ruben Villegas, Mohammad Babaeizadeh, Mohammad Taghi Saffar, Han Zhang, Dumitru Erhan, Vittorio Ferrari, Pieter-Jan Kinder- mans, and Paul V oigtlaender. Storybench: A multifaceted benchmark for continuous story visualization, 2023. 2

    work page 2023

  7. [7]

    Microsoft coco captions: Data collection and evaluation server

    Xinlei Chen, Hao Fang, Tsung-Yi Lin, Ramakrishna Vedan- tam, Saurabh Gupta, Piotr Doll ´ar, and C Lawrence Zitnick. Microsoft coco captions: Data collection and evaluation server. arXiv preprint arXiv:1504.00325, 2015. 3

    arXiv 2015

  8. [8]

    Nl2tl: Transforming natural languages to temporal log- ics using large language models, 2024

    Yongchao Chen, Rujul Gandhi, Yang Zhang, and Chuchu Fan. Nl2tl: Transforming natural languages to temporal log- ics using large language models, 2024. 4

    work page 2024

Show all 75 references
  1. [9]

    Measuring the quality of text-to-video model out- puts: Metrics and dataset

    Iya Chivileva, Philip Lynch, Tomas E Ward, and Alan F Smeaton. Measuring the quality of text-to-video model out- puts: Metrics and dataset. arXiv preprint arXiv:2309.08009,

    arXiv

  2. [10]

    Towards neuro- symbolic video understanding

    Minkyu Choi, Harsh Goel, Mohammad Omama, Yunhao Yang, Sahil Shah, and Sandeep Chinchali. Towards neuro- symbolic video understanding. In European Conference on Computer Vision, pages 220–236. Springer, 2025. 2

    2025

  3. [11]

    Sora detector: A unified hallucination detection for large text-to-video models

    Zhixuan Chu, Lei Zhang, Yichen Sun, Siqiao Xue, Zhibo Wang, Zhan Qin, and Kui Ren. Sora detector: A unified hallucination detection for large text-to-video models. arXiv preprint arXiv:2405.04180, 2024. 2

    2024 arXiv

  4. [12]

    Clarke, Orna Grumberg, and Doron A

    Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999. 3

    1999

  5. [13]

    Allen Emerson

    E. Allen Emerson. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, 1991. 3

    1991

  6. [14]

    Structure and content-guided video synthesis with diffusion models

    Patrick Esser, Johnathan Chiu, Parmida Atighehchian, Jonathan Granskog, and Anastasis Germanidis. Structure and content-guided video synthesis with diffusion models. In Proceedings of the IEEE/CVF International Conference on Computer Vision, pages 7346–7356, 2023. 2

    2023

  7. [15]

    Pytorchvideo: A deep learning li- brary for video understanding

    Haoqi Fan, Tullie Murrell, Heng Wang, Kalyan Vasudev Al- wala, Yanghao Li, Yilei Li, Bo Xiong, Nikhila Ravi, Meng Li, Haichuan Yang, et al. Pytorchvideo: A deep learning li- brary for video understanding. In Proceedings of the 29th ACM international conference on multimedia , ...

    2021

  8. [16]

    Tc-bench: Benchmark- ing temporal compositionality in text-to-video and image-to- video generation

    Weixi Feng, Jiachen Li, Michael Saxon, Tsu-jui Fu, Wenhu Chen, and William Yang Wang. Tc-bench: Benchmark- ing temporal compositionality in text-to-video and image-to- video generation. arXiv preprint arXiv:2406.08656, 2024. 2

    2024 arXiv

  9. [17]

    Nl2ltl – a python package for converting natural language (nl) instruc- tions to linear temporal logic (ltl) formulas

    Francesco Fuggitti and Tathagata Chakraborti. Nl2ltl – a python package for converting natural language (nl) instruc- tions to linear temporal logic (ltl) formulas. Proceedings of the AAAI Conference on Artificial Intelligence , 37(13): 16428–16430, 2024. 4

    2024

  10. [18]

    Videoscore: Building auto- matic metrics to simulate fine-grained human feedback for video generation, 2024

    Xuan He, Dongfu Jiang, Ge Zhang, Max Ku, Achint Soni, Sherman Siu, Haonan Chen, Abhranil Chandra, Ziyan Jiang, Aaran Arulraj, Kai Wang, Quy Duc Do, Yuansheng Ni, Bo- han Lyu, Yaswanth Narsupalli, Rongqi Fan, Zhiheng Lyu, Yuchen Lin, and Wenhu Chen. Videoscore: Building auto- m...

    2024

  11. [19]

    The probabilistic model checker storm

    Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, and Matthias V olk. The probabilistic model checker storm. CoRR, abs/2002.07080, 2020. 5

    2002 arXiv

  12. [20]

    Denoising dif- fusion probabilistic models

    Jonathan Ho, Ajay Jain, and Pieter Abbeel. Denoising dif- fusion probabilistic models. Advances in neural information processing systems, 33:6840–6851, 2020. 2

    2020

  13. [21]

    Make it move: Controllable image-to-video generation with text descrip- tions, 2022

    Yaosi Hu, Chong Luo, and Zhenzhong Chen. Make it move: Controllable image-to-video generation with text descrip- tions, 2022. 2

    2022

  14. [22]

    T2i-compbench: A comprehensive bench- mark for open-world compositional text-to-image genera- tion

    Kaiyi Huang, Kaiyue Sun, Enze Xie, Zhenguo Li, and Xihui Liu. T2i-compbench: A comprehensive bench- mark for open-world compositional text-to-image genera- tion. Advances in Neural Information Processing Systems , 36:78723–78747, 2023. 2

    2023

  15. [23]

    Vbench: Comprehensive bench- mark suite for video generative models

    Ziqi Huang, Yinan He, Jiashuo Yu, Fan Zhang, Chenyang Si, Yuming Jiang, Yuanhan Zhang, Tianxing Wu, Qingyang Jin, Nattapol Chanpaisit, et al. Vbench: Comprehensive bench- mark suite for video generative models. In Proceedings of the IEEE/CVF Conference on Computer Vision and P...

    2024

  16. [24]

    Logic in Computer Science: Modelling and Reasoning about Systems

    Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems . Cambridge Uni- versity Press, 2004. 3

    2004

  17. [25]

    Peekaboo: Interactive video generation via masked- diffusion, 2024

    Yash Jain, Anshul Nasery, Vibhav Vineet, and Harkirat Behl. Peekaboo: Interactive video generation via masked- diffusion, 2024. 2, 5

    2024

  18. [26]

    T2vbench: Benchmarking temporal dynamics for text-to- video generation

    Pengliang Ji, Chuyang Xiao, Huilin Tai, and Mingxiao Huo. T2vbench: Benchmarking temporal dynamics for text-to- video generation. In Proceedings of the IEEE/CVF Confer- ence on Computer Vision and Pattern Recognition (CVPR) Workshops, pages 5325–5335, 2024. 2, 6

    2024

  19. [27]

    T2vbench: Benchmarking temporal dynamics for text-to- video generation

    Pengliang Ji, Chuyang Xiao, Huilin Tai, and Mingxiao Huo. T2vbench: Benchmarking temporal dynamics for text-to- video generation. In Proceedings of the IEEE/CVF Con- ference on Computer Vision and Pattern Recognition, pages 5325–5335, 2024. 2

    2024

  20. [28]

    Stormpy - python bind- ings for storm, 2021

    Sebastian Junges and Matthias V olk. Stormpy - python bind- ings for storm, 2021. 5

    2021

  21. [29]

    Kemeny and J.L

    J.G. Kemeny and J.L. Snell. Finite Markov Chains. Springer,

  22. [30]

    Joshi, Hanna Moazam, Heather Miller, Matei Zaharia, and Christopher Potts

    Omar Khattab, Arnav Singhvi, Paridhi Maheshwari, Zhiyuan Zhang, Keshav Santhanam, Sri Vardhamanan, Saiful Haq, Ashutosh Sharma, Thomas T. Joshi, Hanna Moazam, Heather Miller, Matei Zaharia, and Christopher Potts. Dspy: Compiling declarative language model calls into self- impr...

    2023

  23. [31]

    Subjective-aligned dataset and metric for text-to-video qual- ity assessment, 2024

    Tengchuan Kou, Xiaohong Liu, Zicheng Zhang, Chunyi Li, Haoning Wu, Xiongkuo Min, Guangtao Zhai, and Ning Liu. Subjective-aligned dataset and metric for text-to-video qual- ity assessment, 2024. 2, 7

    2024

  24. [32]

    Evaluating and improving com- positional text-to-visual generation

    Baiqi Li, Zhiqiu Lin, Deepak Pathak, Jiayao Li, Yixin Fei, Kewen Wu, Xide Xia, Pengchuan Zhang, Graham Neu- big, and Deva Ramanan. Evaluating and improving com- positional text-to-visual generation. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recog...

    2024

  25. [33]

    Reward guided latent consistency distillation

    Jiachen Li, Weixi Feng, Wenhu Chen, and William Yang Wang. Reward guided latent consistency distillation. arXiv preprint arXiv:2403.11027, 2024. 2

    2024 arXiv

  26. [34]

    T2v- turbo: Breaking the quality bottleneck of video consis- tency model with mixed reward feedback

    Jiachen Li, Weixi Feng, Tsu-Jui Fu, Xinyi Wang, Sug- ato Basu, Wenhu Chen, and William Yang Wang. T2v- turbo: Breaking the quality bottleneck of video consis- tency model with mixed reward feedback. arXiv preprint arXiv:2405.18750, 2024. 6

    2024 arXiv

  27. [35]

    T2v- turbo-v2: Enhancing video generation model post-training through data, reward, and conditional guidance design.arXiv preprint arXiv:2410.05677, 2024

    Jiachen Li, Qian Long, Jian Zheng, Xiaofeng Gao, Robinson Piramuthu, Wenhu Chen, and William Yang Wang. T2v- turbo-v2: Enhancing video generation model post-training through data, reward, and conditional guidance design.arXiv preprint arXiv:2410.05677, 2024. 6, 7

  28. [37]

    Ground- ing complex natural language commands for temporal tasks in unseen environments

    Jason Xinyu Liu, Ziyi Yang, Ifrah Idrees, Sam Liang, Ben- jamin Schornstein, Stefanie Tellex, and Ankit Shah. Ground- ing complex natural language commands for temporal tasks in unseen environments. In Conference on Robot Learning (CoRL), 2023. 4

    2023

  29. [38]

    Fetv: A bench- mark for fine-grained evaluation of open-domain text-to- video generation, 2023

    Yuanxin Liu, Lei Li, Shuhuai Ren, Rundong Gao, Shicheng Li, Sishuo Chen, Xu Sun, and Lu Hou. Fetv: A bench- mark for fine-grained evaluation of open-domain text-to- video generation, 2023. 2

    2023

  30. [39]

    Evalcrafter: Benchmarking and eval- uating large video generation models

    Yaofang Liu, Xiaodong Cun, Xuebo Liu, Xintao Wang, Yong Zhang, Haoxin Chen, Yang Liu, Tieyong Zeng, Raymond Chan, and Ying Shan. Evalcrafter: Benchmarking and eval- uating large video generation models. In Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern R...

    2024

  31. [40]

    Evalcrafter: Benchmarking and eval- uating large video generation models, 2024

    Yaofang Liu, Xiaodong Cun, Xuebo Liu, Xintao Wang, Yong Zhang, Haoxin Chen, Yang Liu, Tieyong Zeng, Raymond Chan, and Ying Shan. Evalcrafter: Benchmarking and eval- uating large video generation models, 2024. 2, 7

    2024

  32. [41]

    Fetv: A bench- mark for fine-grained evaluation of open-domain text-to- video generation

    Yuanxin Liu, Lei Li, Shuhuai Ren, Rundong Gao, Shicheng Li, Sishuo Chen, Xu Sun, and Lu Hou. Fetv: A bench- mark for fine-grained evaluation of open-domain text-to- video generation. Advances in Neural Information Process- ing Systems, 36, 2024. 2, 6

    2024

  33. [42]

    Video-chatgpt: Towards detailed video understanding via large vision and language models

    Muhammad Maaz, Hanoona Rasheed, Salman Khan, and Fa- had Shahbaz Khan. Video-chatgpt: Towards detailed video understanding via large vision and language models. arXiv preprint arXiv:2306.05424, 2023. 2

    2023 arXiv

  34. [43]

    The Temporal Logic of Re- active and Concurrent Systems: Specification

    Zohar Manna and Amir Pnueli. The Temporal Logic of Re- active and Concurrent Systems: Specification . Springer- Verlag, 1992. 3

    1992

  35. [44]

    J.R. Norris. Markov Chains. Cambridge University Press,

  36. [45]

    Internvl 2.0: A suite of multimodal large lan- guage models for vision and language tasks

    OpenGVLab. Internvl 2.0: A suite of multimodal large lan- guage models for vision and language tasks. OpenGVLab Blog, 2024. Available athttps://internvl.github. io/blog/2024-07-02-InternVL-2.0/ . 4, 8, 3

    2024

  37. [46]

    Optimizing instructions and demonstrations for multi-stage language model programs, 2024

    Krista Opsahl-Ong, Michael J Ryan, Josh Purtell, David Bro- man, Christopher Potts, Matei Zaharia, and Omar Khattab. Optimizing instructions and demonstrations for multi-stage language model programs, 2024. 4

    2024

  38. [47]

    Data-efficient learning of natural language to linear temporal logic transla- tors for robot task specification, 2023

    Jiayi Pan, Glen Chou, and Dmitry Berenson. Data-efficient learning of natural language to linear temporal logic transla- tors for robot task specification, 2023. 4

    2023

  39. [48]

    Graph neural network (gnn) in image and video understanding using deep learning for computer vision applications

    P Pradhyumna, GP Shreya, et al. Graph neural network (gnn) in image and video understanding using deep learning for computer vision applications. In 2021 Second International Conference on Electronics and Sustainable Communication Systems (ICESC), pages 1183–1189. IEEE, 2021. 2

    2021

  40. [49]

    The lost melody: Empirical observations on text-to-video generation from a storytelling perspective, 2024

    Andrew Shin, Yusuke Mori, and Kunitake Kaneko. The lost melody: Empirical observations on text-to-video generation from a storytelling perspective, 2024. 2

    2024

  41. [50]

    T2v-compbench: A comprehen- sive benchmark for compositional text-to-video generation

    Kaiyue Sun, Kaiyi Huang, Xian Liu, Yue Wu, Zihan Xu, Zhenguo Li, and Xihui Liu. T2v-compbench: A comprehen- sive benchmark for compositional text-to-video generation. arXiv preprint arXiv:2407.14505, 2024. 2

    2024 arXiv

  42. [51]

    Towards a better metric for text-to-video generation

    Jay Zhangjie Wu, Guian Fang, Haoning Wu, Xintao Wang, Yixiao Ge, Xiaodong Cun, David Junhao Zhang, Jia-Wei Liu, Yuchao Gu, Rui Zhao, et al. Towards a better metric for text-to-video generation. arXiv preprint arXiv:2401.07781,

    arXiv

  43. [52]

    Msr-vtt: A large video description dataset for bridging video and language

    Jun Xu, Tao Mei, Ting Yao, and Yong Rui. Msr-vtt: A large video description dataset for bridging video and language. In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 5288–5296, 2016. 7

    2016

  44. [53]

    Specification-driven video search via foundation models and formal verification

    Yunhao Yang, Jean-Rapha ¨el Gaglione, Sandeep Chinchali, and Ufuk Topcu. Specification-driven video search via foundation models and formal verification. arXiv preprint arXiv:2309.10171, 2023. 2

    2023 arXiv

  45. [54]

    Cogvideox: Text-to-video diffusion models with an expert transformer

    Zhuoyi Yang, Jiayan Teng, Wendi Zheng, Ming Ding, Shiyu Huang, Jiazheng Xu, Yuanming Yang, Wenyi Hong, Xiao- han Zhang, Guanyu Feng, et al. Cogvideox: Text-to-video diffusion models with an expert transformer. arXiv preprint arXiv:2408.06072, 2024. 6, 7

    2024 arXiv

  46. [55]

    Celebv-text: A large-scale facial text-video dataset, 2023

    Jianhui Yu, Hao Zhu, Liming Jiang, Chen Change Loy, Wei- dong Cai, and Wayne Wu. Celebv-text: A large-scale facial text-video dataset, 2023. 2

    2023

  47. [56]

    Video-llama: An instruction-tuned audio-visual language model for video un- derstanding

    Hang Zhang, Xin Li, and Lidong Bing. Video-llama: An instruction-tuned audio-visual language model for video un- derstanding. arXiv preprint arXiv:2306.02858, 2023. 2, 4

    2023 arXiv

  48. [57]

    I2vgen-xl: High-quality image-to-video synthesis via cascaded diffusion models

    Shiwei Zhang, Jiayu Wang, Yingya Zhang, Kang Zhao, Hangjie Yuan, Zhiwu Qin, Xiang Wang, Deli Zhao, and Jingren Zhou. I2vgen-xl: High-quality image-to-video synthesis via cascaded diffusion models. arXiv preprint arXiv:2311.04145, 2023. 2

    2023 arXiv

  49. [58]

    Benchmarking aigc video quality assessment: A dataset and unified model, 2024

    Zhichao Zhang, Xinyue Li, Wei Sun, Jun Jia, Xiongkuo Min, Zicheng Zhang, Chunyi Li, Zijian Chen, Puyi Wang, Zhong- peng Ji, Fengyu Sun, Shangling Jui, and Guangtao Zhai. Benchmarking aigc video quality assessment: A dataset and unified model, 2024. 2, 7 Appendix Supplementary Material

    2024

  50. [61]

    Always Event A

    Temporal Logic Operation Example Given a set of atomic propositions P = {Event A, Event B}, the TL specification Φ = □ Event A (read as “Always Event A”) means that ‘Event A’ isTrue for every step in the sequence. Additionally, Φ = ♢ Event B (read as “eventually event b”) indi...

  51. [62]

    X i∈Ds max 0≤j≤k fT2P(Ds, i, j) # (17) DT2TL|train = arg max Ds⊂D′ T2TL,|Ds|=N

    Prompt Understanding via Temporal Logic Specification (PULS) In order to obtain Dtrain, we first begin with the larger dataset D with size B where D = DT2P ∪ DT2TL. DT2P and DT2TL are defined as the following: DT2P = {(Ti, Pi)}B i=1, DT2P ⊂ D, (11) DT2TL = {(Ti, Pi, Φi)}B i=1,...

  52. [63]

    Your output fields are:

    ‘input prompt’ (str): Input prompt summarizing what happened in a video. Your output fields are:

  53. [64]

    Overall Consistency

    ‘output propositions’ (str): A list of atomic propositions that correlate with the inputted prompt. For example, for a prompt such as ‘A person holding a hotdog is walking down to the street where many cars next to the huge truck’, the propositions are ‘person holds hotdog’, ‘...

  54. [65]

    person”, “car

    Vision Language Model Calibration In this section, we provide the implementation details to de- tect the existence of propositions obtained byPULS to label each frame in the synthetic video. First, we describe how VLMs conduct inference and then describe the methodol- ogy for ...

  55. [66]

    ‘input prompt‘ (str): Input prompt summarizing what happened in a video

  56. [67]

    Your output fields are:

    ‘input propositions‘ (str): A list of atomic propositions in the video. Your output fields are:

  57. [68]

    Overall Consistency

    ‘output specification’ (str): The formal specification of the event sequence. The response will be a linear temporal logic (LTL) formula made of the inputted propositions combined with LTL symbols. Each symbol can only be one of [‘AND’, ‘OR’, ‘NOT’, ‘UNTIL’, ‘ALWAYS’, ‘EVENTUA...

  58. [69]

    You must not include any other symbols, information, text, or justification in your answer or repeat Yes or No multiple times

  59. [70]

    Prompt 3

    For example, if the question is ’Is there a cat present in the Image?’, the answer must only be ’Yes’ or ’No’. Prompt 3. Semantic Detector VLM. Used to identify the atomic proposition within the frame by initiating VLM with a single frame or a series of frames. 11.2. False Pos...

  60. [71]

    dataset to calibrate the following open-source vision lan- guage models – InternVL2 Series (1B, 2B, 8B) [45] and LLaMA-3.2 Vision Instruct [2] – for NeuS-V. Given that each image-caption pair in the dataset is positive coupling, we construct a set of negative image-caption pai...

  61. [72]

    Calibration Plots

    Video Automaton Generation Function Given a calibrated score set (see Equation (20)) across all frames Fn (where n is the frame index of the video) and propositions in P, we construct the video automaton AV using the video automaton generation function (see Equa- 0.0 0.2 0.4 0...

  62. [73]

    Nature”, “Human & Animal Activities

    NeuS-V Prompt Suite Creating the Dataset: Our dataset is carefully designed to evaluate temporal fidelity and event sequencing in gen- erated videos. It spans four themes – “Nature”, “Human & Animal Activities”, “Object Interactions”, and “Driv- ing Data”, with each theme cont...

  63. [74]

    **Theme**: One of the following themes: Nature, Human and Animal Activities, Object Interactions, or Driving Data

  64. [75]

    Always,"

    **Complexity Level **: - **Basic (1 Operator) **: Use only **one temporal operator ** ("Always," "And," or "Until") in the prompt. - **Intermediate (2 Operators) **: Use **two temporal operators ** in a sequence. The prompt should clearly connect the events with each operator ...

  65. [76]

    Always"**: Describes an event that continuously occurs in the background or context. - **

    **Available Temporal Operators **: - **"Always"**: Describes an event that continuously occurs in the background or context. - **"And"**: Combines two events happening simultaneously or in coordination. - **"Until"**: Describes an event that occurs until another event starts. ...

  66. [2019]

    Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik. 4

  67. [2023]

    https://arxiv.org/abs/2304.08485. 4

    arXiv

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.