Pith. sign in

REVIEW 3 major objections 3 minor 1 cited by

Real-Time Privacy Preservation for Robot Visual Perception

T0 review · 3 major / 3 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read A per-frame recurrence computes a provable lower bound on the probability that a live video stream keeps satisfying its privacy specification.

desk verdict A promising constant-time video abstraction for privacy specs, but the central recurrence is not a valid lower bound and the guarantee never responds to a detected face in the simplest case. read the letter →

arxiv 2505.05519 v1 pith:SI2QKIUR submitted 2025-05-08 cs.CV

Minkyu Choi , Yunhao Yang , Neel P. Bhatt , Kushagra Gupta , Sahil Shah , Aditya Rai , David Fridovich-Keil , Ufuk Topcu
show 1 more author
Sandeep P. Chinchali
This is my paper · ORCID
classification cs.CV
keywords privacy-constrainedvideostreamingconformalpredictiontemporallogicspecificationsabstractionprobabilisticguaranteerobotvisualperceptionreal-timeobjectconcealmentsafetyproperties
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

PCVS is a method for live video streams that conceals privacy-sensitive objects such as faces, license plates, and people while carrying a formal, per-frame probabilistic guarantee that the output still satisfies a user-written privacy specification. The paper's central claim is that a simple recurrence, multiplying the previous frame's guarantee by a term built from calibrated detection probabilities in the current frame, gives a valid lower bound on the probability that the whole frame sequence so far satisfies the specification. The abstraction compresses all past frames into two states, so the guarantee updates in constant time regardless of stream length. If the claim holds, privacy filtering for robots and cameras becomes a real-time, verifiable operation rather than an appeal to a detector's black-box accuracy.

What carries the argument

The central object is the video abstraction: a labeled Markov chain whose states are conjunctions of atomic propositions, such as person=true and face=false, plus two summary states recording whether the previous frames satisfied the specification. The abstraction's work is to collapse the entire history into one number, \(\mathrm{PG}_{k-1}\), so a new frame only adds transitions from the two summary states to the current frame's proposition states. Conformal calibration \(f_C\) supplies the per-detection probabilities, and Theorem 2 with Proposition 1 justifies multiplying the old bound by the sum over current-frame states that keep the trace out of the bad-prefix set. This product form is what makes per-frame, constant-time verification possible.

What would settle it

Run PCVS on a continuous, temporally ordered video in which the same person's face appears in many consecutive frames, and compare the empirical fraction of prefixes that satisfy the specification with the computed bound \(\mathrm{PG}_k\). Any sustained dip below \(\mathrm{PG}_k\) falsifies the lower-bound claim.

Watch

Extended reading notes

Core claim

On the paper's own terms, the discovery is that a privacy specification of the form \(\Phi = \square \tilde{\phi}\) can be monitored online by building a labeled Markov chain abstraction \(\mathcal{A}_k\) of the frames seen so far and computing \(\mathrm{PG}_k(\mathcal{A}_k \models \Phi) = \mathrm{PG}_{k-1}(\mathcal{A}_{k-1} \models \Phi) \times \sum_{\$\sigma$ \models \tilde{\phi}} \prod_{p \in \$\sigma$} f_C(M_{vl}(F_k, p))\), where \(f_C\) is a conformal-calibrated lower bound on the probability that the vision-language model correctly detects proposition \(p\) in frame \(F_k\). The authors prove, through a safety-property argument, that this product is a lower bound on the probability that the frame sequence satisfies the specification, and they show experimentally that the empirical satisfaction rate stays above the computed bound across several datasets.

Load-bearing premise

The recurrence treats each frame's detection outcomes as conditionally independent of all earlier frames and of one another, which real video streams with persistent people or faces typically violate.

Editorial extensions

If this is right

  • The per-frame guarantee stays constant-time as video grows, so privacy enforcement can run at frame rate on a robot's onboard CPU or GPU.
  • Users can specify privacy as temporal logic, such as "never show a face while a person is present," and PCVS chooses which objects to blur so the remaining detections satisfy the formula.
  • The computed number is a conservative, user-facing privacy score: if \(\mathrm{PG}_k\) stays above a threshold \(\lambda\), the frame is admitted; otherwise objects are blurred and the score recomputed.
  • Because only violating objects are concealed, non-sensitive features remain visible, and robot control policies such as stopping for pedestrians keep working with faces blurred.
  • Empirical satisfaction rates in the paper's evaluations consistently exceed the theoretical bounds, which is what the lower-bound claim predicts.

Reading between the lines

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

  • A direct implication the paper leaves implicit is that the product recurrence is only a valid lower bound if detections in successive frames are conditionally independent given the specification; for real streams where a person or face persists across many frames, the true probability could fall below the computed bound, so the guarantee should be read as conditioned on that independence.
  • One testable extension is to replace the per-frame product with a small stateful model of persistence, such as a Hidden Markov Model over object presence, which would preserve the recurrence structure while respecting temporal correlation.
  • The method's guarantee inherits the calibration set: if the robot moves to a new environment with different lighting or camera geometry, the lower bound needs recalibration to remain valid.
  • The paper's own stated limitation, no action-based specifications like "person eating," suggests a natural next step: use a second multi-frame action detector and add its calibrated output as another atomic proposition in the same abstraction.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 3 minor

Summary. The paper proposes PCVS, a real-time video privacy system. Given a temporal-logic privacy specification Φ over atomic propositions AP (e.g., □(person → ¬face)), a vision-language model scores each proposition in each incoming frame, a conformal calibration function f_C converts those scores into per-frame probability bounds, and Algorithm 1 builds a two-state Markov-chain abstraction of the frame history. The method then computes a probabilistic guarantee PG_k(A_k |= Φ) via Eq. (3), blurs objects when the guarantee falls below a user threshold λ, and otherwise releases the frame. Experiments on ImageNet-, COCO-, and UFPR-ALPR-based datasets report high privacy preservation success ratios, comparisons against GPT-4V and Video-LLaVA, real-robot demonstrations, and latency measurements intended to show real-time operation.

Significance. If the formal guarantee were valid, this would be a practically valuable contribution: a streaming privacy filter with a per-frame-updated probabilistic certificate, backed by real robot deployments and reproducible-looking empirical methodology. The system components, including the modular abstraction and the calibrated detector, are reasonable engineering choices, and the latency analysis is a useful practical result. However, the paper's central claim is the correctness of Eq. (3) as a lower bound on the probability that the frame sequence satisfies the privacy specification. As detailed below, Eq. (3) is not a valid probability bound even under the paper's own assumptions: it omits negated literals, uses non-normalized products, and makes an unstated and generally false independence assumption. Because the formal guarantee is the stated novelty that distinguishes this work from prior detection-and-blurring approaches, the manuscript's main scientific claim is not established.

major comments (3)
  1. [Section IV-A-c, Eq. (3); Algorithm 1 line 7] The recurrence in Eq. (3) is not a valid lower bound because the per-frame factor omits negated literals and is not normalized over the possible assignments. In Algorithm 1 line 7, each state σ is assigned probability prob = ∏_{p∈σ} f_C(Mvl(F_k,p)), with no factor for propositions not in σ and no normalization over all 2^AP assignments. Consider AP={face} and Φ=□¬face. The only satisfying positive assignment is σ=∅, whose empty product is 1, so Eq. (3) gives PG_k = PG_{k-1} for every frame no matter how confident the detector is that a face is present. If f_C(Mvl(F_k,face))=0.9, the actual probability that the current frame satisfies ¬face is at most 0.1, while the computed guarantee remains unchanged. Thus PG_k can lie far above the true probability; it is not a lower bound, and the guarantee fails exactly when it should respond to a detected privacy violation. A correct factor must include factors for negated propositions and must be a conditional probability of the current frame's assignment, normalized over all assignments.
  2. [Section IV-A-c, Eq. (3); Theorem 2 and Proposition 1] Even if the per-frame terms were correctly normalized, Eq. (3) would require the current frame's proposition assignment to be conditionally independent of the full previous frame history given safety; this assumption is neither stated nor proven. Theorem 2 and Proposition 1 justify multiplying a prefix safety probability by a per-state conditional factor only when the factor is conditional on the prefix, but Eq. (3) uses a factor that depends only on the current frame F_k and not on the previous history. In real video streams, detections are strongly autocorrelated: a person or face persists across many frames, so the conditional probability of the current frame's assignment given the previous frames differs substantially from its marginal probability. The synthetic evaluation datasets ED1 and ED2 are constructed by randomly inserting selected images into videos, which artificially enforces independence and therefore does not test the assumption that the formal guarantee relies on.
  3. [Section IV-A-b, Definition 2 and Algorithm 1] The abstraction constructed by Algorithm 1 does not satisfy Definition 2 of a labeled Markov chain because the transition function P is not stochastic. For example, with AP={face} and f_C(Mvl(F_k,face))=0.9, the transitions out of State 1 include the state σ=∅ with probability 1 (empty product) and the state σ={face} with probability 0.9, giving a total outgoing probability of 1.9, which violates the requirement ∑_{s'} P(s,s')=1. Consequently the trace-probability computation in Eq. (2), which multiplies transition probabilities along paths, is not well-defined for the abstraction produced by the algorithm.
minor comments (3)
  1. [Section VI-A, Privacy Preservation Success Ratio] The metric 'Number of p_i∈AP detected or concealed' counts detections even if those detections are not actually concealed, while the benchmarks are credited for detections alone; as a result, the empirical satisfaction rate does not directly measure the claimed formal guarantee of concealment.
  2. [Figure 2] The running example should be reconciled with Eq. (3): with AP={person,face} and the displayed values f_C(Mvl(F_k,face))=0.3 and f_C(Mvl(F_k,person))=1.0, the sum in Eq. (3) over positive satisfying assignments does not obviously equal 0.7, the factor used to obtain PG_k=0.56.
  3. [Section IV-A-a, Eq. (1)] The definition of the calibration function f_C would benefit from more precise notation: the density f_nc is defined on nonconformity scores 1-Mvl(x_i,y_i), but Eq. (1) integrates it up to c for c>0.5 and up to 1-c for c≤0.5 without a clear derivation of how these integrals become a function of the raw confidence c.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the probabilistic guarantee is a derived conditional-probability bound, the calibration input comes from external conformal prediction, and the empirical success metric is measured independently against ground truth.

full rationale

The paper's central derivation, Eq. (3), is presented as a theorem rather than as a restatement of its inputs. PG_k is defined operationally in Definition 1 and computed from the trace probability in Eq. (2); Theorem 2 and Proposition 1 are elementary conditional-probability steps that do not assume the conclusion. The only fitted input is the calibration function f_C, but it is learned from a separate calibration set using conformal prediction (Theorem 1, proof cited to Shafer and Vovk [22]), an external framework whose assumptions do not include the privacy guarantee being tested. The empirical Privacy Preservation Success Ratio counts ground-truth objects that are detected or concealed, so it is not constructed from PG_k; comparing the measured ratio to the bound is a genuine test. Self-citations ([7], [23], [31], [32]) appear in related-work discussion and do not carry the load of the derivation. Finally, the skeptic's objection that Eq. (3) omits negated literals and may not be a valid lower bound is a soundness/correctness concern, not a circularity concern: even if the equation is wrong, it is not equivalent to its inputs by construction. Accordingly, no circular step can be quoted, and the appropriate score is 0.

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

The derivation imports conformal prediction's exchangeability assumption without finite-sample guarantees, and Equation 3 imports an unstated independence assumption across frames and propositions. The calibration function f_C is fitted to a calibration set, so the bound is only as strong as that fit. The paper introduces no new physical entities; the video abstraction is a mathematical representation, not an invented entity.

free parameters (3)
  • Calibration density f_nc(z) and induced calibration function f_C = Not reported; estimated from an unspecified calibration set
    Section IV-A-a uses f_C(c) equal to an integral of f_nc over a confidence interval. The guarantee inherits this fitted density, and no estimator or calibration size is given.
  • Conformal error bound epsilon = Not reported in text
    Theorem 1 takes epsilon as a pre-defined error bound that determines c* and hence the calibration curve; no value or sensitivity analysis is provided.
  • Privacy threshold lambda = 0.80 in robot demonstrations
    The threshold decides when to blur more objects (Section IV, Figure 3). It is user-chosen, not fitted, but it shapes the reported operating behavior.
assumptions (5)
  • domain assumption Calibration frames and deployment frames are exchangeable and drawn from the same distribution.
    Invoked in Section IV-A-a through the phrase 'distributed identically to the task domain.' Live robot video from new scenes is not shown to satisfy this.
  • ad hoc to paper Detection outcomes across frames and across atomic propositions are conditionally independent.
    Equation 3 multiplies PG_{k-1} by a per-frame product; Algorithm 1 line 7 multiplies per-proposition probabilities. This independence is never stated or proven.
  • domain assumption The integral of the estimated density f_nc gives an exact lower bound for per-frame detection probability.
    Theorem 1 and Equation 1 treat f_C as exact despite estimating f_nc from a finite calibration set; no finite-sample guarantee is supplied.
  • domain assumption Blurring a detected object removes it from future detections so the recomputed abstraction reflects its absence.
    The blur-and-recompute loop in Section IV assumes the detector no longer reports the blurred object; this is not verified on blurred pixels.
  • standard math Standard safety-property semantics for temporal logic over finite prefixes apply.
    Definitions 2 and 3 and Theorem 2 use the Baier-Katoen safety-property framework, treated as background material.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Real-Time Privacy Preservation for Robot Visual Perception." pith.science (2026). https://pith.science/paper/SI2QKIUR

@misc{pith2026250505519,
  author       = {Pith},
  title        = {Pith review of: Real-Time Privacy Preservation for Robot Visual Perception},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SI2QKIUR}},
  note         = {Machine review of arXiv:2505.05519}
}
read the original abstract

Many robots (e.g., iRobot's Roomba) operate based on visual observations from live video streams, and such observations may inadvertently include privacy-sensitive objects, such as personal identifiers. Existing approaches for preserving privacy rely on deep learning models, differential privacy, or cryptography. They lack guarantees for the complete concealment of all sensitive objects. Guaranteeing concealment requires post-processing techniques and thus is inadequate for real-time video streams. We develop a method for privacy-constrained video streaming, PCVS, that conceals sensitive objects within real-time video streams. PCVS takes a logical specification constraining the existence of privacy-sensitive objects, e.g., never show faces when a person exists. It uses a detection model to evaluate the existence of these objects in each incoming frame. Then, it blurs out a subset of objects such that the existence of the remaining objects satisfies the specification. We then propose a conformal prediction approach to (i) establish a theoretical lower bound on the probability of the existence of these objects in a sequence of frames satisfying the specification and (ii) update the bound with the arrival of each subsequent frame. Quantitative evaluations show that PCVS achieves over 95 percent specification satisfaction rate in multiple datasets, significantly outperforming other methods. The satisfaction rate is consistently above the theoretical bounds across all datasets, indicating that the established bounds hold. Additionally, we deploy PCVS on robots in real-time operation and show that the robots operate normally without being compromised when PCVS conceals objects.

Figures

Figures reproduced from arXiv: 2505.05519 by the authors.

Figure 1
Figure 1. Pipeline of Privacy-Constrained Video Streaming: (Step 1) Given a privacy specification Φ, we define a set AP of atomic propositions describing privacy-sensitive ob￾jects. (Step 2) Given an incoming frame Fk from the video, the method uses a vision-language model (VLM) to detect sensitive objects in the frame. Each detection is associated with a confidence score from the VLM. The method calibrates a confidence score… view at source ↗
Figure 2
Figure 2. A running example on how to compute the proba [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. We present the demonstrations for indoor robot navigation (top left), ground robot navigation (top right), and urban [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (6 more)
Figure 4
Figure 4. Figure 4: A sample control policy for the ground robot. Each [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 6
Figure 6. Figure 6: The comparisons between our method and other [PITH_FULL_IMAGE:figures/full_fig_p006_6.png]
Figure 5
Figure 5. Figure 5: PCVS effectively maintains privacy in long￾horizon videos and complex privacy specifications. In Figure 5a, PCVS consistently preserves privacy, achieving an average Privacy Preservation Success Ratio of 0.97 across various video lengths. In Figure 5b, we show that PCV…
Figure 7
Figure 7. Figure 7: Effective privacy preservation in real-world driv￾ing scenes. We apply PCVS to driving scenes from the UFPR￾ALPR dataset and conceal privacy-sensitive objects such as license plates. The privacy preservation success ratio of PCVS is consistently above 0.8 [PITH_FULL_I…
Figure 8
Figure 8. Figure 8: Demonstrations on our method concealing license [PITH_FULL_IMAGE:figures/full_fig_p007_8.png]
Figure 10
Figure 10. Figure 10: Comparison between the verification time with and [PITH_FULL_IMAGE:figures/full_fig_p008_10.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. A Challenge to Build Neuro-Symbolic Video Agents

    cs.AI 2025-05 conditional novelty 3.0 of 10

    The paper issues a grand challenge to build neuro-symbolic video agents that search video, call tools, and generate video, using the authors' NSVS-TL and NeuS-V as starting points.

Reference graph

Works this paper leans on

33 extracted references · 23 canonical work pages · cited by 1 Pith paper

  1. [1]

    Principles of model checking

    Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT press, 2008

    2008

  2. [2]

    An introduction to first-order logic

    Jon Barwise. An introduction to first-order logic. In Studies in Logic and the Foundations of Mathematics , volume 90, pages 5–46. Elsevier, 1977

    work page 1977

  3. [3]

    Know where you’re uncertain when planning with multimodal foun- dation models: A formal framework

    Neel P Bhatt, Yunhao Yang, Rohan Siva, Daniel Mi- lan, Ufuk Topcu, and Zhangyang Wang. Know where you’re uncertain when planning with multimodal foun- dation models: A formal framework. arXiv preprint arXiv:2411.01639, 2024

    arXiv 2024

  4. [4]

    Privid: practical,{Privacy-Preserving} video analytics queries

    Frank Cangialosi, Neil Agarwal, Venkat Arun, Srinivas Narayana, Anand Sarwate, and Ravi Netravali. Privid: practical,{Privacy-Preserving} video analytics queries. In 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI 22) , pages 209–228, 2022

    work page 2022

  5. [5]

    Yolo-world: Real-time open-vocabulary object detection

    Tianheng Cheng, Lin Song, Yixiao Ge, Wenyu Liu, Xinggang Wang, and Ying Shan. Yolo-world: Real-time open-vocabulary object detection. arXiv preprint arXiv:, 2024

    work page 2024

  6. [6]

    Temporal sequence modeling for video event detection

    Yu Cheng, Quanfu Fan, Sharath Pankanti, and Alok Choudhary. Temporal sequence modeling for video event detection. In Proceedings of the IEEE conference on computer vision and pattern recognition , pages 2227– 2234, 2014

    work page 2014

  7. [7]

    Towards Neuro-Symbolic Video Understanding

    Minkyu Choi, Harsh Goel, Mohammad Omama, Yun- hao Yang, Sahil Shah, and Sandeep Chinchali. Neuro- symbolic video search. arXiv preprint arXiv:2403.11021, 2024

    work page Pith review arXiv 2024

  8. [8]

    Real- time privacy-preserving moving object detection in the cloud

    Kuan-Yu Chu, Yin-Hsi Kuo, and Winston H Hsu. Real- time privacy-preserving moving object detection in the cloud. In Proceedings of the 21st ACM international conference on Multimedia , pages 597–600, 2013

    work page 2013

Show all 33 references
  1. [9]

    Imagenet: A large-scale hierarchical image database

    Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In 2009 IEEE conference on computer vision and pattern recognition , pages 248–255. Ieee, 2009

    2009

  2. [10]

    A roomba recorded a woman on the toilet

    Eileen Guo. A roomba recorded a woman on the toilet. how did screenshots end up on facebook?, Mar 2024

    2024

  3. [11]

    Zooming into video conferencing privacy

    Dima Kagan, Galit Fuhrmann Alpert, and Michael Fire. Zooming into video conferencing privacy. IEEE Trans- actions on Computational Social Systems , 2023

    2023

  4. [12]

    Poggio, and Thomas Serre

    Hildegard Kuehne, Hueihan Jhuang, Est ´ıbaliz Garrote, Tomaso A. Poggio, and Thomas Serre. HMDB: A large video database for human motion recognition. In Dimitris N. Metaxas, Long Quan, Alberto Sanfeliu, and Luc Van Gool, editors, IEEE International Conference on Computer Visio...

    2011

  5. [13]

    Laroca, E

    R. Laroca, E. Severo, L. A. Zanlorensi, L. S. Oliveira, G. R. Gonc ¸alves, W. R. Schwartz, and D. Menotti. A robust real-time automatic license plate recognition based on the YOLO detector. In International Joint Conference on Neural Networks (IJCNN) , pages 1–10, July 2018. d...

    2018

  6. [14]

    Video-llava: Learning united visual representation by alignment before projection, 2023

    Bin Lin, Yang Ye, Bin Zhu, Jiaxi Cui, Munan Ning, Peng Jin, and Li Yuan. Video-llava: Learning united visual representation by alignment before projection, 2023

    2023

  7. [15]

    Belongie, Lubomir D

    Tsung-Yi Lin, Michael Maire, Serge J. Belongie, Lubomir D. Bourdev, Ross B. Girshick, James Hays, Pietro Perona, Deva Ramanan, Piotr Doll’a r, and C. Lawrence Zitnick. Microsoft COCO: common ob- jects in context. CoRR, abs/1405.0312, 2014. URL http://arxiv.org/abs/1405.0312

    2014 arXiv

  8. [16]

    Revamp 2 t: real-time edge video analytics for multicamera privacy-aware pedestrian tracking

    Christopher Neff, Mat ´ıas Mendieta, Shrey Mohan, Mo- hammadreza Baharani, Samuel Rogers, and Hamed Tabkhi. Revamp 2 t: real-time edge video analytics for multicamera privacy-aware pedestrian tracking. IEEE Internet of Things Journal , 7(4):2591–2602, 2019

    2019

  9. [17]

    Gpt-4 vision system card

    OpenAI. Gpt-4 vision system card. https://cdn.openai. com/papers/GPTV System Card.pdf, 2023. Accessed: [insert date of access]

    2023

  10. [18]

    Gemel: Model merging for{Memory-Efficient},{Real-Time} video an- alytics at the edge

    Arthi Padmanabhan, Neil Agarwal, Anand Iyer, Ganesh Ananthanarayanan, Yuanchao Shu, Nikolaos Karianakis, Guoqing Harry Xu, and Ravi Netravali. Gemel: Model merging for{Memory-Efficient},{Real-Time} video an- alytics at the edge. In 20th USENIX Symposium on Networked Systems De...

    2023

  11. [19]

    Chaos-cryptography based privacy preservation tech- nique for video surveillance

    Sk Md Mizanur Rahman, M Anwar Hossain, Hussein Mouftah, Abdulmotaleb El Saddik, and Eiji Okamoto. Chaos-cryptography based privacy preservation tech- nique for video surveillance. Multimedia systems , 18: 145–155, 2012

    2012

  12. [20]

    Faster r-cnn: Towards real-time object detection with region proposal networks

    Shaoqing Ren, Kaiming He, Ross Girshick, and Jian Sun. Faster r-cnn: Towards real-time object detection with region proposal networks. IEEE transactions on pattern analysis and machine intelligence , 39(6):1137– 1149, 2016

    2016

  13. [21]

    Temporal logic, volume 3

    Nicholas Rescher and Alasdair Urquhart. Temporal logic, volume 3. Springer Science & Business Media, 2012

    2012

  14. [22]

    A tutorial on confor- mal prediction

    Glenn Shafer and Vladimir V ovk. A tutorial on confor- mal prediction. Journal of Machine Learning Research , 9(3), 2008

    2008

  15. [23]

    S. P. Sharan, Minkyu Choi, Sahil Shah, Harsh Goel, Mohammad Omama, and Sandeep Chinchali. Neuro- symbolic evaluation of text-to-video models using formal verification, 2024. URL https://arxiv.org/abs/2411.16718

    2024 arXiv

  16. [24]

    Privacy- preserving ai-enabled video surveillance for social dis- tancing: Responsible design and deployment for public spaces

    Nehemia Sugianto, Dian Tjondronegoro, Rosemary Stockdale, and Elizabeth Irenne Yuwono. Privacy- preserving ai-enabled video surveillance for social dis- tancing: Responsible design and deployment for public spaces. Information Technology & People , 37(2):998– 1022, 2024

    2024

  17. [25]

    Grounding ltlf specifications in images

    Elena Umili, Roberto Capobianco, Giuseppe De Gia- como, et al. Grounding ltlf specifications in images. In Proceedings of the 16th International Workshop on Neural-Symbolic Learning and Reasoning , pages 45–63, 2022

    2022

  18. [26]

    Efficient privacy preserving video surveillance

    Maneesh Upmanyu, Anoop M Namboodiri, Kannan Sri- nathan, and CV Jawahar. Efficient privacy preserving video surveillance. In 2009 IEEE 12th international conference on computer vision , pages 1639–1646. IEEE, 2009

    2009

  19. [27]

    Yolov9: Learning what you want to learn using pro- grammable gradient information

    Chien-Yao Wang, I-Hau Yeh, and Hong-Yuan Mark Liao. Yolov9: Learning what you want to learn using pro- grammable gradient information. In European Confer- ence on Computer Vision , pages 1–21. Springer, 2025

    2025

  20. [28]

    A scalable and privacy-aware iot service for live video analytics

    Junjue Wang, Brandon Amos, Anupam Das, Padmanab- han Pillai, Norman Sadeh, and Mahadev Satyanarayanan. A scalable and privacy-aware iot service for live video analytics. In Proceedings of the 8th ACM on Multimedia Systems Conference, pages 38–49, 2017

    2017

  21. [29]

    Privacy-protecting video surveillance

    Jehan Wickramasuriya, Mohanned Alhazzazi, Mahesh Datt, Sharad Mehrotra, and Nalini Venkatasubramanian. Privacy-protecting video surveillance. In Real-Time Imaging IX, volume 5671, pages 64–75. SPIE, 2005

    2005

  22. [30]

    Formal methods: Practice and experience

    Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice and experience. ACM Comput. Surv., 41(4), oct 2009. ISSN 0360-0300. doi: 10.1145/1592434.1592436. URL https: //doi.org/10.1145/1592434.1592436

    2009

  23. [31]

    Specification-driven video search via foundation models and formal verification

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

    2023 arXiv

  24. [32]

    Fine- tuning language models using formal methods feedback: A use case in autonomous systems

    Yunhao Yang, Neel P Bhatt, Tyler Ingebrand, William Ward, Steven Carr, Atlas Wang, and Ufuk Topcu. Fine- tuning language models using formal methods feedback: A use case in autonomous systems. Proceedings of Machine Learning and Systems , 6:339–350, 2024

    2024

  25. [33]

    Minor privacy protection through real-time video processing at the edge

    Meng Yuan, Seyed Yahya Nikouei, Alem Fitwi, Yu Chen, and Yunxi Dong. Minor privacy protection through real-time video processing at the edge. In 2020 29th International Conference on Computer Communications and Networks (ICCCN) , pages 1–6. IEEE, 2020

    2020

Pith tools

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