VLM : 빠른 논문 리뷰 : NeuS-QA: Grounding Long-Form Video Understanding in Temporal Logic and Neuro-Symbolic Reasoning

NeuS-QA 학습 노트

---

용어 설명 (Terminology)

• NeuS-QA: 이 논문에서 제안하는 neuro-symbolic 파이프라인의 이름. 자연어 질문을 Temporal Logic으로 변환하고, video automaton을 구축하여 질문에 가장 적합한 비디오 segment를 VLM에 전달하는 시스템.
• LVQA (Long-Form Video Question Answering): 긴 비디오(수십 분 이상)에 대해 시간적 순서나 인과관계를 묻는 복잡한 질문에 답하는 task.
• Temporal Logic (TL): "A가 일어난 후 B가 발생한다"와 같이 이벤트의 시간적 순서나 관계를 형식적으로 표현하는 논리 언어. until, eventually, always 같은 연산자를 사용.
• Video Automaton: 비디오를 일련의 상태(프레임)와 상태 전이로 모델링한 것. 각 프레임(상태)은 특정 이벤트(atomic proposition)의 발생 여부를 라벨로 가짐. 이를 통해 비디오 내 이벤트의 흐름을 형식적으로 검증 가능.
• Model Checking: 주어진 Temporal Logic 명세(질문)를 Video Automaton(비디오)이 만족하는지 수학적으로 검증하는 프로세스.
• Neuro-Symbolic Reasoning: VLM과 같은 neural network의 인식 능력과 Temporal Logic과 같은 symbolic reasoning의 엄밀함을 결합한 접근 방식.

---

Purpose of the Paper

기존 Long-Form VQA 방식들의 근본적인 한계를 극복하고자 함.

• 기존 방식의 한계:
  1. Uniform Sampling (균일 샘플링): 비디오 전체에서 프레임을 무작위로 추출하여 VLM에 입력. 긴 비디오에서는 중요한 순간을 놓칠 확률이 높고, token 제한으로 인해 충분한 정보를 처리하지 못함.
  2. Heuristic Retrieval (휴리스틱 검색): 질문과 의미적으로 유사한 프레임을 검색. 그러나 이는 시간적 순서나 복잡한 인과관계를 고려하지 못하며, 검색 결과의 논리적 정합성을 보장할 수 없음.
• 이 논문의 접근 방식:
  • 질문의 논리적/시간적 구조를 명시적으로 모델링하고, 이를 만족하는 비디오 segment를 수학적으로 **검증(verify)**하여 찾아내는 새로운 접근법을 제시.
  • 이를 통해 VLM이 불필요하거나 오해의 소지가 있는 정보 없이, 질문에 가장 관련 있는 핵심 장면에만 집중하도록 만들어 VQA 성능을 향상시키는 것을 목표로 함.

---

Key Contributions & Novelty

• Key Contributions:
  • NeuS-QA Pipeline 제안: 자연어 질문을 Temporal Logic (TL) 명세로 자동 번역하고, 비디오를 automaton으로 변환한 뒤, model checking을 통해 질문의 논리를 만족하는 비디오 segment를 정확히 찾아내는 training-free, plug-and-play 프레임워크를 제안.
  • 질문의 논리적 구조화: 자연어 질문에 내포된 복잡한 시간적, 인과적 요구사항을 Temporal Logic이라는 형식 언어로 명확하게 표현.
  • 엄밀한 검증 기반 검색: Model checking을 통해 '감'이 아닌 수학적 검증을 거쳐 질문과 관련된 비디오 segment를 추출함으로써 검색의 정확성과 해석 가능성을 크게 높임.
• Novelty:
  • 단순히 neural network의 성능에만 의존하던 기존 LVQA와 달리, neuro-symbolic 접근법을 도입하여 VLM의 인식(perception) 능력과 formal logic의 추론(reasoning) 능력을 결합한 최초의 시도 중 하나.
  • 별도의 fine-tuning 없이 어떤 VLM에도 **모듈처럼 부착(plug-and-play)**하여 사용할 수 있어 범용성이 높음.

---

Experimental Highlights

• Datasets & Metrics: LongVideoBench와 CinePile 데이터셋을 사용하여 accuracy를 측정.
• Key Result 1: SOTA 성능 달성:
  • LongVideoBench에서 기존 VLM 및 structured reasoning 프레임워크들을 큰 폭으로 능가. 예를 들어 Qwen2.5-VL 모델에 NeuS-QA를 적용했을 때, 기본 모델(50.44%) 대비 약 10% 향상된 60.09%의 정확도를 달성.
• Key Result 2: Ground Truth를 능가하는 성능:
  • 놀랍게도, 사람이 직접 정답 구간이라고 표시한 ground truth segment를 VLM에 제공했을 때보다, NeuS-QA가 찾아낸 segment를 제공했을 때 VQA 정확도가 더 높게 나옴. 이는 NeuS-QA가 정답이 있는 직접적인 순간뿐만 아니라, 질문을 이해하는 데 필요한 **전후의 중요한 맥락(context)**까지 효과적으로 포착함을 시사.
• Key Result 3: Neuro-Symbolic의 중요성 입증:
  • Temporal logic과 automaton 부분을 제거하고 단순 VLM 프롬프팅으로 관련 segment를 찾게 했을 때, 정확도가 58.33%에서 40.09%로 급락. 이는 논리가 제거된 단순 검색은 효과가 없으며, NeuS-QA의 neuro-symbolic 피드백이 성능 향상의 핵심 요인임을 증명.

---

Limitations and Future Work

• Limitations:
  • "Neuro"와 "Symbolic" 간의 강한 의존성: Symbolic verifier는 완벽하지만, VLM("Neuro")이 비디오에서 특정 이벤트를 감지하지 못하면 Temporal Logic 명세가 만족되지 않아 전체 시스템이 실패(false negative)할 수 있음. 특히 시각적 단서가 미묘하거나, 가려지거나, 매우 짧게 나타날 때 취약.
• Future Work:
  • Agentic Neuro-Symbolic Systems: 한 번에 정답을 찾는 것을 넘어, 메모리, 계획, 중간 논리 표현을 사용하여 반복적으로 질문을 분해하고 추론하는 agent 시스템으로 확장하는 연구를 제안.
  • General-Purpose Video Automaton: 매번 질문마다 automaton을 생성하는 것은 비용이 많이 들므로, 미리 범용 video automaton을 구축해두고 여러 질문에 재사용하여 계산 비용을 절감하는 방안을 모색.

---

Overall Summary

NeuS-QA는 긴 비디오에 대한 복잡한 질문에 답하기 위해, 자연어 질문을 Temporal Logic이라는 형식 언어로 변환하고, model checking을 통해 비디오에서 해당 논리를 만족하는 정확한 구간을 찾아내는 neuro-symbolic 프레임워크이다. 이 접근법은 기존 방법들보다 월등히 높은 정확도를 보였으며, 심지어 사람이 직접 찾은 정답 구간을 VLM에 제공하는 것보다도 더 나은 성능을 기록했다. 이 연구는 VLM의 인식 능력과 formal logic의 엄밀함을 결합하여, 해석 가능하고 정밀한 Long-Form Video Understanding의 새로운 방향을 제시했다는 점에서 큰 의의를 가진다.

---

쉬운 설명 (Simple Explanation)

NeuS-QA는 똑똑하지만 가끔 엉뚱한 VLM에게 1시간짜리 영화를 통째로 보여주고 "주인공이 비행기에 앉은 뒤에 무엇을 집었어?"라고 묻는 대신, 먼저 똑똑한 조수(Temporal Logic)를 시켜 "주인공이 비행기에 탑승"하고 "자리에 앉는" 장면이 나오는 정확한 시간대(예: 35분 12초 ~ 36분 5초)를 찾아오게 하는 것과 같다. 그 후 VLM에게는 그 짧고 핵심적인 클립만 보여주며 질문하기 때문에, VLM은 헷갈리지 않고 훨씬 더 정확하게 "빨간 컵을 집었다"고 대답할 수 있다.

 

 

 

Abstract

Vision-language models(VLMs)는 single images나 short videos를 다루는 tasks에서 탁월하지만, complex multi-step temporal reasoning을 요구하는 Long Video Question Answering(LVQA)에서는 여전히 어려움을 겪고 있습니다.

단순히 frames를 uniformly sample하여 question과 함께 VLM에 입력하는 Vanilla approaches는 상당한 token overhead를 발생시킵니다. 이는 long videos에 대한 aggressive downsampling을 강제하여, models가 fine-grained visual structure, 미묘한 event transitions, 그리고 핵심적인 temporal cues를 놓치게 만듭니다.

Recent works는 heuristic approaches를 통해 이러한 한계를 극복하려 시도하지만, temporal relationships를 encoding하는 명시적인 mechanisms가 부족하며, sampled context가 실제로 question이 요구하는 compositional 혹은 causal logic을 encoding한다는 formal guarantees를 제공하지 못합니다.

이러한 foundational gaps를 해결하기 위해, 우리는 LVQA를 위한 training-free, plug-and-play neuro-symbolic pipeline인 NeuS-QA를 소개합니다.

NeuS-QA는 먼저 natural language question을 frame-level events 간의 temporal relationship을 model하는 logic specification으로 translate합니다. 그 다음, video의 frame-by-frame event progression을 model하기 위해 video automaton을 construct하고, 마지막으로 model checking을 employ하여 automaton을 specification과 비교함으로써 question의 logical requirements를 satisfy하는 모든 video segments를 identify합니다.

오직 이러한 logic-verified segments만이 VLM에 전달되므로, model을 modifying하거나 fine-tuning하지 않고도 interpretability를 개선하고, hallucinations를 줄이며, compositional reasoning을 가능하게 합니다.

LongVideoBench와 CinePile LVQA benchmarks에서의 Experiments는 NeuS-QA가 performance를 10% 이상, 특히 event ordering, causality, 그리고 multi-step reasoning과 관련된 questions에서 크게 향상시킴을 보여줍니다. 우리는 코드를 https://utaustin-swarmlab.github.io/NeuS-QA/ 에 open-source로 공개합니다.

 

1 Introduction

Video-language models(VLMs)의 최근 발전은 static images와 short video clips에 대한 visual question answering(VQA)에서 상당한 진전을 이끌어냈습니다. 그러나 real-world applications가 surveillance streams, egocentric vlogs, 그리고 movie scenes와 같은 longer-form content로 이동함에 따라, 사용자들은 점차 multiple events에 걸친 더 복잡하고, temporally grounded questions를 하고 있습니다. 예를 들어, Figure 1에 예시된 것처럼 1시간짜리 여행 브이로그를 보는 사용자는 다음과 같이 물을 수 있습니다: "남자가 비행기에 탑승해서 자리에 앉은 후, 무엇을 잡았는가?"

그러한 questions에 답변하는 것은 surface-level perception 이상을 요구합니다. 이는 ➊ entities와 그들의 interactions를 identify하기 위한 semantic grounding, ➋ sequence of events를 추적하고 해석하기 위한 temporal reasoning, 그리고 ➌ 이러한 temporally distinct sub-events를 query의 구조 및 의도와 일치하는 일관된 reasoning chain으로 통합하기 위한 compositionality를 필요로 합니다.

VLMs를 사용한 video question answering의 일반적인 전략은 video 전체에서 frames를 uniformly sample하는 것입니다. 이 방법은 short clips에는 충분하지만, video 길이가 늘어날수록 문제가 됩니다. visual input의 양이 급격히 증가하여 models가 token limits를 초과하거나 videos를 aggressive downsampling하게 만듭니다. 그렇게 함으로써, 그들은 video의 많은 부분을 건너뛰고 complex temporal queries에 답변하는 데 중요한 fine-grained visual details, 미묘한 event transitions, 그리고 핵심적인 temporal cues를 놓칠 위험이 있습니다.

Long-form videos는 종종 multiple scenes가 순차적으로 전개되는 narrative arc를 따르지만, 그에 대한 많은 questions는 이야기의 특정 부분에만 관련됩니다. Figure 1은 공항에 들어가는 것부터 하차하여 마침내 호텔 방에 체크인하기까지 남자의 전체 여정을 묘사하는 휴가 브이로그를 보여줍니다. 하지만 사용자의 query는 오직 기내 segment의 정보만을 필요로 합니다. 이것은 Long-form video question answering(LVQA)의 흔한 패턴입니다. content는 방대하지만, 대부분의 queries는 특정 temporal windows를 목표로 합니다.

따라서 uniform sampling의 자연스러운 대안은 query와 가장 관련 있는 작고 targeted segment에 model의 attention을 집중시키는 것입니다. 그러나 이는 핵심적인 과제를 제기합니다: 정답을 미리 알지 못한 상태에서 question과 semantically 그리고 temporally aligned된 올바른 segment를 어떻게 retrieve할 수 있을까요?

이를 해결하기 위해, 우리는 Temporal logic(TL)이 강력한 솔루션을 제공한다고 주장합니다. 이는 "until", "eventually", "always"와 같은 operators를 사용하여 구조를 기호적으로 나타냄으로써 events가 시간에 따라 어떻게 전개되는지 formalize할 수 있게 해줍니다. 이를 통해 question이 지칭하는 temporal patterns의 종류(예: 다른 사건 후에 발생하는 사건)를 정확하게 specify하고, 이러한 제약 조건을 만족하는 video segments를 체계적으로 filter하는 것이 가능해집니다.

이를 위해, 우리는 long-form videos에 대한 temporally complex questions에 정확하게 답변하기 위해 TL의 구조와 VLMs의 지각 능력을 결합한 neuro-symbolic pipeline인 NeuS-QA를 제안합니다. natural language로 된 question이 주어지면, NeuS-QA는 먼저 이를 원하는 sequence of events를 encode하는 TL specification으로 translate합니다. 그 다음 video로부터 개별 frames의 semantic propositions에 대한 scores를 할당하여 video automaton을 construct하고, 이 specification을 만족하는 video segments를 identify하기 위해 model checking을 적용합니다. 마지막으로, 검증된 이러한 segments에 대해 VLM에 query하여, model을 관련 없거나 오해의 소지가 있는 context에 노출시키지 않고 정확하고 temporally grounded 답변을 가능하게 합니다.

 

 

NeuS-QA: Introduction 핵심 정리 노트

Target Audience: LVQA(Long Video Question Answering) 및 Neuro-symbolic approaches 연구자

1. Problem Statement: LVQA의 본질적 한계

• Current Status: 기존 VLMs는 static images나 short video clips에서는 강력하지만, surveillance streams나 movies 같은 Long-form content에서는 성능이 저하됨.
• Challenges in LVQA: 단순 인식이 아닌 다음 세 가지 능력이 필수적임.
  1. Semantic grounding: Entities와 interaction 식별.
  2. Temporal reasoning: Sequence of events의 추적 및 해석.
  3. Compositionality: 시간적으로 분리된 sub-events를 coherent reasoning chain으로 통합.
• Limitation of Uniform Sampling:
  • 긴 비디오에서 frames를 uniformly sample하는 방식은 Token limits 문제에 직면함.
  • 이를 피하기 위해 aggressive downsampling을 수행하면, fine-grained visual details, subtle event transitions, key temporal cues를 소실하여 Reasoning 실패를 유발함.

2. Key Insight & Approach

• Observation: Long-form videos는 긴 narrative arc를 가지지만, 실제 User Query는 특정 temporal windows에 국한된 정보를 요구함. (e.g., 1시간 브이로그 중 '비행기 내부' 사건만 질문)
• The Core Dilemma: 정답을 모르는 상태에서 어떻게 Question과 Semantically/Temporally aligned된 올바른 segment를 Retrieve 할 것인가?
• Solution: Temporal Logic (TL)
  • Events의 구조를 기호적(symbolically)으로 표현(operators: until, eventually, always)하여 Temporal patterns를 명시.
  • 이를 통해 단순 키워드 매칭이 아닌, 논리적 흐름에 맞는 segment를 systematic filtering 가능.

3. Proposed Method: NeuS-QA (Neuro-symbolic Pipeline)

TL의 구조적 강점과 VLMs의 지각 능력을 결합한 Training-free Pipeline 제안.

• Step 1: Specification Translation
  • Natural language question $\rightarrow$ Desired sequence of events를 encode하는 TL specification으로 변환.
• Step 2: Automaton Construction
  • Video로부터 개별 frames의 semantic propositions에 대한 scores를 할당하여 Video automaton 생성.
• Step 3: Model Checking (Verification)
  • Automaton에 Model checking을 적용하여 TL specification을 만족하는 Video segments를 식별.
• Step 4: Targeted VLM Query
  • 검증된(Verified) Segments만을 VLM에 입력하여 답변 생성.
  • Effect: Irrelevant context 노출을 최소화하여 Hallucination 방지 및 High-precision reasoning 달성.

---

쉬운 설명 : NeuS-QA가 필요한 이유

"1시간짜리 영화를 다 보여주는 대신, 질문에 딱 맞는 장면만 찾아서 보여주자!"

우리가 챗GPT 같은 AI에게 "이 1시간짜리 여행 영상에서 남자가 비행기 탔을 때 뭘 먹었어?"라고 물어본다고 가정해 봅시다.

1. 기존 방식 (비효율적):
2. AI는 1시간짜리 영상을 다 볼 수 없으니(용량 문제), 듬성듬성 스킵하면서 봅니다. 그러다 보면 정작 '비행기 식사 장면'이 스킵되어 "모르겠습니다"라고 하거나 엉뚱한 답을 내놓습니다.
3. 이 논문의 접근 방식 (NeuS-QA):
   • 질문 분석: "비행기 탑승"이라는 사건이 발생하고 $\rightarrow$ 그 상태가 유지되는 동안(until) $\rightarrow$ "무언가를 먹는 행위"를 찾아라.
   • 장면 검색: 영상 전체에서 '비행기'가 나오는 구간을 먼저 논리적으로 찾아냅니다. (이때 수학적인 '시간 논리(Temporal Logic)'를 사용해서 아주 정교하게 찾습니다.)
   • 답변: 딱 그 '비행기 구간'만 잘라서 AI에게 보여주며 "여기서 뭐 먹었는지 맞춰봐"라고 시킵니다.
4. AI에게 영상을 무작정 보여주기 전에, 탐정처럼 질문을 논리적으로 분해합니다.

결론:

영상 전체를 대충 훑어보는 게 아니라, 질문의 논리(순서, 인과관계)를 먼저 파악해서 정확한 구간만 콕 집어 AI에게 보여주기 때문에, 긴 영상에서도 훨씬 똑똑하게 대답할 수 있습니다.

 

 

 

2 Related Works

Video Question Answering. Early VQA systems는 일반적으로 convolutional 및 recurrent networks, encoder-decoder pipelines, 또는 video features에 대한 attention mechanisms를 사용하여 entire videos를 encode하는 fully supervised architectures에 의존했습니다. 그러나 이러한 models는 longer videos로의 scalability가 부족했고 limited visual-linguistic reasoning에 의해 제약받았습니다.

VLMs의 등장은 stronger generalization과 함께 diverse domains에 걸쳐 zero-shot VQA를 가능하게 했습니다. 그러나 이러한 models는 일반적으로 entire video에서 sample된 fixed set of frames를 consuming하여 작동하므로, complex temporal structures를 가진 long-form videos를 처리하는 능력이 제한됩니다. Global frame pooling이나 simple attention mechanisms에 대한 의존은 multi-event sequences가 제시될 때 종종 irrelevant하거나 diluted context로 이어져, degraded performance를 초래합니다.

Global frame sampling의 한계를 해결하기 위해, recent state-of-the-art (SOTA) approaches는 가장 relevant video segments를 identify하고 condition하는 retrieval-augmented strategies를 채택합니다. Irrelevant context를 줄이는 데는 효과적이지만, 이러한 methods는 종종 coarse heuristics나 textual summarization에 의존하며, 이는 visual fidelity를 희생하고 formal structure가 부족합니다. 대조적으로, NeuS-QA는 temporal logic을 사용하여 frame selection을 guide함으로써, video content의 더 interpretable하고 precise grounding을 산출합니다.

Symbolic Representations for Video. Symbolic representations는 robotics, autonomous vehicles, generative models, 그리고 structured neural networks와 같은 분야 전반에 걸쳐 탐구되었습니다. Vision의 맥락에서, symbolic methods는 long-form understanding을 지원하기 위해 사용되었지만; 이들은 일반적으로 latent-space embeddings에 의존하여 interpretability를 희생합니다. Yang et al.과 Choi et al.은 structured reasoning을 가능하게 하기 위해 videos를 formal models로 나타내는 방향으로 나아갑니다. NeuS-QA는 유사한 철학을 따르며, interpretable하고 temporally grounded analysis를 가능하게 하기 위해 videos를 verifiable automata로 modeling합니다.

 

NeuS-QA: Related Works 핵심 정리 노트

Target Audience: LVQA(Long Video Question Answering) 및 Neuro-symbolic 연구자

1. Limitations of Existing VQA Approaches

• Early Supervised Architectures (CNN/RNN based):
  • Longer videos에 대한 Scalability 부족 및 제한적인 visual-linguistic reasoning 능력.
• Modern VLMs (Zero-shot):
  • Sampling Strategy: 전체 비디오에서 고정된 frames를 sampling하는 방식.
  • Critical Flaw: Multi-event sequences에서 context가 희석(diluted)되거나 무관한 정보가 섞여 성능 저하 발생. Global pooling 방식은 복잡한 시간 구조(temporal structures)를 파악하지 못함.
• Recent SOTA (Retrieval-Augmented):
  • 관련된 segments를 찾아내는 방식이나, Coarse heuristics 또는 Textual summarization에 의존함.
  • Problem: Text 요약 과정에서 Visual fidelity(시각적 정확도)가 손실되고, 엄밀한 Formal structure가 결여됨.
  • NeuS-QA Contribution: Heuristics 대신 **Temporal Logic (TL)**을 사용하여 Frame selection을 가이드함. $\rightarrow$ Precision & Interpretability 확보.

2. Symbolic Representations in Vision

• Previous Approaches:
  • Robotics 등 타 분야에서 활발했으나, Vision 분야에서는 주로 Latent-space embeddings에 의존하는 방식이었음.
  • Problem: Latent space는 해석이 불가능하여(Sacrificing interpretability) 검증이 어려움.
• NeuS-QA Approach:
  • Videos를 모호한 임베딩이 아닌, 검증 가능한 Automata (Verifiable automata)로 모델링함.
  • 이를 통해 블랙박스 방식이 아닌, Structured reasoning이 가능한 해석 가능한 분석(Interpretable analysis)을 구현함.

---

쉬운 설명 : 기존 AI들은 영상을 어떻게 봤을까?

"대충 훑어보거나(SOTA), 요약본만 읽거나(Summarization) vs 논리적으로 따져보기(NeuS-QA)"

이 논문이 나오기 전까지, 긴 비디오에 대한 질문을 해결하는 AI들의 방식은 다음과 같은 한계가 있었습니다.

1. 초창기 모델들:
2. 영상을 처음부터 끝까지 다 외우려고 했습니다. 영상이 길어지면 머리가 터져서(메모리 부족) 포기했습니다.
3. 최신 유행하는 모델들 (Retrieval-augmented):
   • 문제점: 글로 요약하는 과정에서 '남자의 표정이 미묘하게 변했다' 같은 시각적 디테일(Visual fidelity)이 다 사라져 버립니다.
4. "중요해 보이는 장면만 뽑아서 보자"는 전략입니다. 하지만 그 장면을 뽑는 기준이 "대충 키워드가 비슷하면 가져와" 수준이거나, **"영상 내용을 글로 요약한 뒤 그 글을 읽고 판단"**하는 방식이었습니다.
5. NeuS-QA의 차별점:
   • 기존 방식이 "비행기 나오는 장면 대충 다 가져와"라면,
   • NeuS-QA는 **"비행기 탑승 이벤트가 시작된 직후부터, 자리에 앉기 전까지의 구간을 정확히 잘라와"**라고 명령합니다.
   • 또한, 알 수 없는 숫자 덩어리(Latent embedding)로 영상을 처리하던 기존 방식과 달리, **오토마타(Automata)**라는 검증 가능한 구조를 만들어 "왜 이 장면을 선택했는지" 사람이 이해할 수 있게 만듭니다.
6. "대충 감으로" 장면을 고르는 게 아니라, **수학적인 논리(Temporal Logic)**를 사용합니다.

 

 

 

3 Preliminaries

우리의 접근 방식을 설명하기 위해, running example을 소개하는 것으로 시작합니다. Video가 주어졌을 때, 우리가 "여자가 그래놀라 위에 뜨거운 물을 붓고 요거트를 그릇에 숟가락으로 넣은 후, 무엇을 토핑으로 올리는가?"라고 묻는다고 가정해 봅시다.

Temporal Logic. Temporal Logic (TL)은 logical 및 temporal operators의 조합을 통해 events의 진행을 묘사하는 데 사용되는 formal language입니다. TL에서, 개별 events는 atomic propositions, 즉 True 또는 False로 평가되는 진술들로 표현됩니다. 이러한 propositions는 AND($\wedge$), OR($\vee$), NOT($\neg$), IMPLY($\implies$)와 같은 logical operators뿐만 아니라 ALWAYS($\square$), EVENTUALLY($\diamond$), NEXT($X$), UNTIL($U$)과 같은 temporal operators를 사용하여 결합됩니다.

우리의 running example로 돌아가서, 우리는 atomic propositions의 집합 $P$와 그에 상응하는 TL specification $\phi$를 다음과 같이 정의합니다:

$$P = \{ \text{woman pours hot water over granola}, \text{woman spoons yogurt into bowl}, \text{woman places topping} \}$$

$$\phi = (\text{woman pours hot water over granola} \wedge \text{woman spoons yogurt into bowl}) \wedge \diamond \text{woman places topping}$$

이 specification은 여자가 먼저 그래놀라 위에 뜨거운 물을 붓고, 그릇에 요거트를 추가하며, 결국 마지막에 어떤 토핑을 추가하는 query를 encode합니다.

Video Automaton. 우리는 video를 각 state가 sampled frame에 해당하고 transitions가 temporal progression을 포착하는 stochastic finite-state automaton으로 표현합니다. Videos는 고유한 temporal structure를 가진 discrete frames의 finite sequence이므로, 우리는 그것들을 discrete-time Markov chain으로 model합니다.

공식적으로, video automaton $A_V$는 튜플로 정의됩니다:

$$A_V = (Q, q_0, \delta, \lambda), \quad (1)$$

여기서 $Q$는 states의 finite set이고, $q_0 \in Q$는 initial state이며, $\delta : Q \times Q \rightarrow [0, 1]$은 $\delta(q_i, q_j)$가 state $q_i$에서 state $q_j$로 transition할 확률을 제공하는 transition function이고, $\lambda : Q \rightarrow 2^{|P|}$는 각 state에 atomic propositions 집합을 할당하는 labeling function입니다. 이 구조는 frames의 sequences를 labeled paths로 취급함으로써 video에 대해 TL formulas가 verify될 수 있게 합니다.

Formal Verification. Formal verification을 통해, 우리는 video automaton이 주어진 TL specification을 satisfy하는지 평가합니다. 우리는 automaton $A_V$를 통과하는 path $\pi$를 모든 $i \ge 0$에 대해 $\delta(q_i, q_{i+1}) > 0$인 states의 infinite sequence $\pi = q_0q_1q_2 \dots$로 정의합니다. 각 path는 trace—path를 따라 states에 할당된 label sets의 sequence, $\text{trace}(\pi) = \lambda(q_0)\lambda(q_1)\lambda(q_2)\dots$로 표기됨—를 유도합니다. 이 trace는 Figure 2에 예시된 바와 같이 시간에 따른 observable propositions의 진행을 포착합니다. 우리는 satisfaction probability $P[V \models \phi]$를 compute하기 위해 probabilistic model checking을 적용하여, video trace가 TL specification을 얼마나 잘 satisfy하는지 정량화합니다. 이는 video 내의 event sequences를 identify하기 위한 formal하고 interpretable framework를 제공합니다.

 

NeuS-QA: Preliminaries 핵심 정리 노트

Target Audience: Formal Verification 및 Neuro-symbolic Video Understanding 연구자

1. Problem Formulation: Logic-based Query Decomposition

• Goal: Natural Language Query를 수학적으로 검증 가능한 형태인 **Temporal Logic(TL)**으로 변환하여 Event의 순서와 조건을 명시함.
• Temporal Logic (TL) Components:
  • Atomic Propositions ($P$): 개별 Event가 발생했는지 여부 (True/False).
  • Logical Operators: AND($\land$), OR($\lor$), NOT($\neg$), IMPLY($\implies$).
  • Temporal Operators:
    • ALWAYS ($\square$): 항상 성립.
    • EVENTUALLY ($\diamond$): 언젠가 발생함.
    • NEXT ($X$): 바로 다음 시점.
    • UNTIL ($U$): 특정 조건 만족 전까지 유지.
• Example Specification ($\phi$):$\phi = (\text{Action}_A \land \text{Action}_B) \land \diamond \text{Target\_Action}$
• $\rightarrow$ 단순 키워드 매칭이 아닌, Sequence와 Causality를 논리식으로 정의.
• Query: "여자가 A 행동을 하고 B 행동을 한 뒤, 토핑으로 무엇을 올리는가?"

2. Video Representation: Stochastic Finite-State Automaton

• Modeling Approach: Video를 연속적인 이미지 나열이 아닌, Discrete-time Markov Chain으로 모델링함.
• Formal Definition ($A_V$):
  • $Q$: Finite set of states (각 State는 Sampled Frame에 대응).
  • $q_0$: Initial state.
  • $\delta$: Transition function ($Q \times Q \rightarrow [0, 1]$). Frame 간의 시간적 진행 확률.
  • $\lambda$: Labeling function ($Q \rightarrow 2^{|P|}$). 각 Frame(State)에 감지된 Atomic Propositions 할당.
• Video Automaton $A_V = (Q, q_0, \delta, \lambda)$
• Key Insight: Video를 Automaton으로 변환함으로써, Frame sequence를 Labeled Path로 취급하여 수학적 검증이 가능해짐.

3. Formal Verification via Model Checking

• Trace Definition: Automaton을 통과하는 Path $\pi$에서 관측된 Label들의 sequence ($\text{trace}(\pi)$).
• Probabilistic Model Checking:
  • 단순히 Yes/No를 판별하는 것이 아니라, Satisfaction Probability $P[V \models \phi]$를 계산.
  • 즉, Video Trace가 주어진 TL Specification($\phi$)을 얼마나 잘 만족하는지 정량화(Quantifying)함.
  • 이를 통해 Formal하고 Interpretable한 Event Sequence 식별 프레임워크를 제공.

---

쉬운 설명 : 비디오를 수학 문제로 바꾸는 법

"비디오는 보드게임판, 질문은 게임 규칙"

이 섹션은 AI가 비디오를 이해하기 위해 문제를 '수학적'으로 정의하는 기초 작업을 설명합니다.

1. 질문을 '규칙'으로 번역하기 (Temporal Logic):
   • 우리가 "밥 먹고 나서 물 마셨어?"라고 묻는 것을 컴퓨터에게는 프로그래밍 코드처럼 규칙을 짜줍니다.
   • "이벤트 A(밥 먹음)가 발생함" AND "그 이후 언젠가($\diamond$)" "이벤트 B(물 마심)가 발생함".
   • 이렇게 하면 "물 마시고 밥 먹은" 경우(순서 틀림)를 정확히 걸러낼 수 있습니다.
2. 비디오를 '보드게임판'으로 만들기 (Video Automaton):
   • 비디오의 각 장면(Frame)을 보드게임의 '칸(State)'으로 만듭니다.
   • 각 칸에는 꼬리표(Label)가 붙어 있습니다. (예: 1번 칸='요리 중', 2번 칸='먹는 중')
   • 시간이 흐르는 것을 주사위를 굴려 다음 칸으로 이동하는 확률 게임(Markov Chain)으로 봅니다.
3. 검증하기 (Verification):
   • 이제 보드게임 말(Player)이 비디오라는 판 위를 지나갑니다.
   • 말이 지나온 길(Trace)을 보니 "요리 중 $\rightarrow$ 먹는 중" 순서로 꼬리표가 붙어 있습니다.
   • 아까 정해둔 규칙(밥 $\rightarrow$ 물)과 비교해서 **"이 경로가 규칙을 따를 확률이 몇 %인가?"**를 계산합니다. 이것이 바로 NeuS-QA가 정답 구간을 찾아내는 핵심 원리입니다.

 

 

4 Methodology

 

우리는 natural language query를 기반으로 video에서 temporally grounded scenes of interest를 추출하여 vision-language models를 guide하는 NeuS-QA의 개요를 제시합니다.

NeuS-QA는 먼저 question에 답변하는 데 필요한 key events와 semantics를 identify합니다. 그 다음 이들은 expected structure와 ordering of events를 encode하는 temporal logic specification으로 formalized됩니다. Video의 어떤 부분이 이 specification을 satisfy하는지 evaluate하기 위해, 우리는 VLM에 의해 predicted된 frame-level propositions를 나타내는 states를 가진 automaton을 construct합니다. VLM이 consecutive video segments를 iteratively process함에 따라, 우리는 frames에 relevant propositions를 label하고 automaton을 incrementally build합니다. 그런 다음 Formal verification이 이 automaton에 적용되어 query를 satisfy하는 sequences를 identify하고, 최종적인 set of frames of interest를 산출합니다. 우리는 이 과정을 Algorithm 1에 개략적으로 설명합니다.

LQ2TL: Question to Temporal Logic. LQ2TL은 spatial 및 temporal relationships를 모두 capture하는 prompting strategies를 사용하여 natural language questions를 TL specifications로 translating하기 위한 structured two-shot framework를 제공합니다. Question $q$가 주어지면, LQ2TL은 query 내의 key objects, actions, 그리고 relationships에 해당하는 set of atomic propositions $P = {p_1, p_2, \dots, p_n}$을 extract합니다. 이 extraction은 semantic 및 event-level coverage를 보장하기 위해 신중하게 선택된 few-shot examples가 포함된 optimized prompts에 의해 guided됩니다. Propositions가 identified된 후, LQ2TL은 query의 temporal structure를 formal operators에 mapping하고 extracted propositions를 그에 따라 linking하여 TL specification $\phi$를 construct합니다. 결과적인 propositions와 specification은 Section 3에 자세히 설명되어 있습니다.

Automaton Representation of Video. LQ2TL로부터 얻은 TL specification $\phi$가 주어지면, 우리는 event-based atomic propositions에 grounded된 discrete-time Markov chain automaton $A_V$를 incrementally build하여 video의 formal representation을 construct합니다. Empty automaton $A_{V,0}$ (L3)에서 시작하여, 우리는 size $\kappa$의 frame windows $F_t$ (L5)로 video를 process하며, 시간에 따른 identified events의 evolution을 capture하는 probabilistic state-based model을 build합니다.

각 frame sequence $F_t$에 대해, system은 vision-language model $M_{\text{prop}}(p_i, F_t)$ (L7)를 사용하여 proposition $p_i \in P$가 존재할 likelihood를 나타내는 probabilistic detections $Z_{t,p_i} \in [0, 1]$를 compute합니다. 이 값들은 semantic assessments의 reliability를 개선하기 위해 held-out validation set(Appendix 참조)을 사용하여 calibrated된 model의 Yes/No logits로부터 derived됩니다. Cumulative detections $Z_{0:t}$와 current automaton state $A_{V,t-1}$에 기반하여, 우리는 transition builder $\Theta(A_{V,t}, P, Z_{0:t})$ (L8)를 통해 automaton을 update합니다. 이 automaton은 video 전체에 걸쳐 event-based propositions의 temporal progression을 incrementally model합니다.

Formal Verification for Scenes of Interest. 우리는 TL specification $\phi$가 satisfied되는 모든 time intervals를 identify하기 위해 formal verification을 사용합니다. 이 과정은 video automaton에 대한 rigorous temporal analysis를 가능하게 하기 위해 확립된 model-checking techniques를 employ합니다 (L9).

각 timestep $t$에서, current automaton $A_{V,t}$가 주어지면, 우리는 satisfaction probability를 다음과 같이 compute합니다:

$$P_t = P[A_{V,t} \models \phi] = \mu(V, \phi). \quad (2)$$

이 satisfaction probability는 STORM model checker를 통해 implement된 probabilistic model checking을 사용하여 computed됩니다. 이 과정은 $\mu(\cdot)$가 $A_{V,t}$의 state labels와 transition probabilities를 analyze하여 specification $\phi$가 satisfied될 가능성을 assess하는 Probabilistic Computation Tree Logic(PCTL) framework 하에서 operate합니다.

Stable하고 calibrated signal을 얻기 위해, 우리는 raw satisfaction probabilities를 per-frame detection scores로 map하는 smoothing function $F_b(\cdot)$를 apply합니다. 이는 다음과 같이 정의됩니다:

$$F_b(c) = \frac{1}{1 + e^{-\gamma(c-\tau)}}, \quad (3)$$

여기서 $c$는 raw satisfaction probability이고, $\tau$는 confidence threshold이며, $\gamma$는 sigmoid curve의 steepness를 control합니다. 이 transformation은 정의된 confidence threshold 미만의 noise를 suppress하면서 high-confidence detections를 preserve합니다. Threshold $\tau$ 주변의 transition의 steepness를 modulating함으로써, 이 function은 smooth하고 interpretable confidence curve를 produce합니다. Output은 high temporal precision으로 query-relevant events를 capture하는 minimal satisfying interval (예: frames 615 $\rightarrow$ 820)을 산출합니다.

Temporal Extension. 우리는 robust question answering을 위한 complete temporal context를 보장하기 위해 identified interval을 extend합니다 (L13). Context window extension process는 interval을 fixed 또는 learned temporal window $\alpha, \beta$만큼 forward 및 backward로 extend하여 comprehensive understanding을 위해 sufficient temporal context가 preserved되도록 보장합니다. 우리는 query $q$ 내의 "before" 및 "after"와 같은 temporal keywords에 따르는 event lead-up 및 aftermath periods를 고려하기 위해 VLM을 leverage합니다. Final extended window는 question answering을 위한 VLM의 filtered input이 되며, optimal performance를 위해 temporally focused이면서도 contextually complete video segment를 제공합니다. Temporal extension은 L14에 formalized되어 있습니다.

Vision Language Model Answering. Final stage는 VLM prompting을 통해 accurate responses를 generate하기 위해 이 temporally filtered video segment를 context로 사용합니다.

 

 

---

NeuS-QA: Methodology 핵심 정리 노트

Target Audience: Neuro-symbolic 구현 및 VLM 파이프라인 설계 연구자

1. Core Pipeline Overview (Algorithm 1)

• Input: Natural Language Query + Long Video
• Process:
  1. Query $\rightarrow$ Logic Specification (LQ2TL)
  2. Video $\rightarrow$ Automaton Construction (Frame-level proposition detection)
  3. Automaton + Logic $\rightarrow$ Formal Verification (Interval Identification)
  4. Interval $\rightarrow$ Temporal Extension (Context padding)
• Output: Temporally focused video segment $\rightarrow$ Final VLM Answer

2. Component Details

• LQ2TL (Logic Translation):
  • Method: Structured two-shot prompting.
  • Task: Query에서 Key objects/actions를 추출하여 Atomic Propositions $P$ 정의 후, 이를 Temporal Logic Specification $\phi$로 매핑.
• Automaton Construction (Incremental):
  • Model: Discrete-time Markov Chain Automaton $A_V$.
  • Detection: VLM ($M_{\text{prop}}$)을 사용하여 각 Frame window $F_t$마다 Proposition 존재 확률 $Z_{t, p_i}$ 계산.
  • Calibration: Yes/No logits를 사용하며 held-out set으로 보정(Calibrated)하여 신뢰성 확보.
• Formal Verification (The Filter):
  • Technique: Probabilistic Model Checking (STORM checker 사용, PCTL framework).
  • Metric: Satisfaction Probability $P_t = P[A_{V,t} \models \phi]$.
  • Smoothing ($F_b(c)$): Sigmoid function을 적용하여 Noise(Low probability)를 억제하고 High-confidence detection만 남김. $\tau$ (threshold)와 $\gamma$ (steepness)로 제어.
• Temporal Extension (Robustness):
  • Issue: 탐지된 구간이 너무 타이트하면 문맥이 잘릴 수 있음.
  • Solution: 앞뒤로 $\alpha, \beta$ 윈도우만큼 구간을 확장(Extension). 특히 "before/after" 같은 키워드가 있을 때 VLM을 활용해 전후 맥락(lead-up/aftermath)을 포함시킴.

---

쉬운 설명 : AI 탐정의 수사 기법 4단계

"범인을 찾기 위해 몽타주를 그리고, CCTV를 돌려본 뒤, 확실한 증거 구간만 확보한다."

이 섹션은 NeuS-QA가 실제로 어떻게 작동하는지 4단계로 설명합니다.

1. 몽타주 그리기 (LQ2TL):
   • 사용자의 질문("범인이 차를 타고 도망간 뒤 어디로 갔나?")을 AI가 이해할 수 있는 '수사 지침서(논리식)'로 바꿉니다.
   • 지침서 내용: "차를 탄다(Event A)" $\rightarrow$ "이동한다(Event B)" $\rightarrow$ "내린다(Event C)" 순서로 된 장면을 찾아라.
2. CCTV 분석 및 지도 만들기 (Automaton):
   • 긴 비디오를 조금씩 잘라서(Frame windows) VLM에게 보여줍니다.
   • VLM은 각 장면마다 "여기 차가 있나요? (Yes/No)", "내리고 있나요? (Yes/No)"를 판단하여 확률 점수를 매깁니다.
   • 이 점수들을 모아 시간 흐름에 따른 '사건 지도(Automaton)'를 만듭니다.
3. 검증 및 구간 확정 (Formal Verification):
   • 아까 만든 '수사 지침서'와 '사건 지도'를 대조합니다.
   • 수학적인 검증 도구(Model Checker)를 돌려서 지침서와 정확히 일치하는 시간대를 찾아냅니다. 이때 잡음(애매한 구간)을 없애기 위해 특별한 함수(Sigmoid)로 점수를 깔끔하게 다듬습니다.
4. 앞뒤 맥락 확보 (Temporal Extension):
   • 범인이 내리는 딱 그 1초만 보여주면 전후 사정을 모르니, 앞뒤로 5초씩 더 붙여줍니다(Extension).
   • 특히 "도망가기 전" 같은 말이 있으면 앞부분을 더 넉넉히 챙깁니다.
   • 이렇게 완성된 '핵심 요약 영상'만 최종적으로 AI에게 보여주며 답을 하게 합니다.

 

 

 

 

 

 

 

 

 

 

 

 

 

주인장 이해

 

 

질문 -> 쿼리 분해

프레임 별로 각 쿼리에 대한 확률 * 이전 프레임의 시간 적으로 이전 쿼리 확률을 곱한 확률을 기록 t=0에서는 시간적으로 이전 쿼리 확률은 1로 봄.

그렇게 모든 프레임에 대해서 확률값을 매김.

거기에 스무딩을 걸고 노이즈를 없애고 기준치를 넘는 구간에 앞뒤 패딩을 주어 잘라냄.

그 잘라낸 구간을 모두 합쳐서 인풋으로 사용.

 

 

 

네, 이제 완벽합니다.

사용자 님이 정리하신 문장이 NeuS-QA의 핵심 알고리즘을 가장 정확하고 깔끔하게 요약한 것입니다.

제가 헷갈리게 했던 복잡한 과정들을 다 걷어내면, 결국 사용자 님이 말씀하신 이 한 줄의 수식 논리로 귀결됩니다.

1. "프레임 별로 각 쿼리에 대한 확률 × 이전 프레임의 이전 쿼리 누적 확률"
   • 이게 바로 아까 제가 길게 설명했던 오토마톤의 상태 전이(State Transition) 핵심 수식입니다.
   • (지금 소금일 확률) × (1초 전까지 양파를 찾았을 확률) = (지금 소금 단계까지 완료했을 확률)
2. "t=0에서는 시간적으로 이전 쿼리 확률은 1로 봄"
   • 시작 상태() 초기화(Initialization)를 정확히 짚으셨습니다.​
3. "스무딩 -> 패딩 -> 자르기 -> 합쳐서 인풋"
   • 후처리(Post-processing) 및 VLM 입력 과정까지 정확합니다.

지금 정리하신 그 내용이 정답입니다.