SearcharxivSearch

arXiv subjects

Hyejin Han

Publications and source records attributed to Hyejin Han.

3 recordsLinked to original sources

TeachObs: A Human-Validated Benchmark for Multimodal Teaching Observation and Model Evaluation

Classroom videos contain observable teaching practices, but their pedagogical and visual signals are rarely organized in forms suitable for model evaluation. We present \textit{TeachObs}, a human-validated benchmark for multimodal teaching observation in classroom videos. \textit{TeachObs} includes 30 public lesson videos from eight countries divided into 5,158 fixed 15-second scenes. Seven researchers annotated each scene with 39 binary observation codes, covering 20 visual codes, such as gesture, board work, pointing, and visual materials, and 19 nonvisual codes, such as instruction, monitoring, questioning, feedback, and reflection. Gold segment labels are constructed using reliability- and prevalence-aware rules based on Krippendorff's alpha. In addition to segment-level labels, three expert raters produced lesson-level ratings and qualitative evaluations of instructional design, instructional delivery, learner response, learning materials, and lesson closure across the 30 lessons, with rater coverage detailed in the body. Using these two human reference layers, we evaluate five vision-capable frontier LLMs across three tracks - text-only segment coding, text + frame segment coding, and lesson-level coverage scored under an LLM-as-judge protocol - and find that no single model consistently outperforms others across all three tracks, that adding a mid-frame inflates both true and false attributions per scene, and that model evaluations over-rate procedurally clear lessons relative to expert raters. \textit{TeachObs} therefore supports both fine-grained annotation benchmarking and whole-lesson evaluation, showing where AI systems can assist classroom video analysis and where expert judgment remains necessary across varied subjects, classroom formats, and annotation difficulty levels.

cs.CL

Certifying the LTL Formula p Until q in Hybrid Systems

In this paper, we propose sufficient conditions to guarantee that a linear temporal logic (LTL) formula of the form p Until q, denoted by $p \mathcal{U} q$, is satisfied for a hybrid system. Roughly speaking, the formula $p \mathcal{U} q$ is satisfied means that the solutions, initially satisfying proposition p, keep satisfying this proposition until proposition q is satisfied. To certify such a formula, connections to invariance notions such as conditional invariance (CI) and eventual conditional invariance (ECI), as well as finite-time attractivity (FTA) are established. As a result, sufficient conditions involving the data of the hybrid system and an appropriate choice of Lyapunov-like functions, such as barrier functions, are derived. The considered hybrid system is given in terms of differential and difference inclusions, which capture the continuous and the discrete dynamics present in the same system, respectively. Examples illustrate the results throughout the paper.

eess.SY

Linear Temporal Logic for Hybrid Dynamical Systems: Characterizations and Sufficient Conditions

This paper introduces operators, semantics, characterizations, and solution-independent conditions to guarantee temporal logic specifications for hybrid dynamical systems. Hybrid dynamical systems are given in terms of differential inclusions -- capturing the continuous dynamics -- and difference inclusions -- capturing the discrete dynamics or events -- with constraints. State trajectories (or solutions) to such systems are parameterized by a hybrid notion of time. For such broad class of solutions, the operators and semantics needed to reason about temporal logic are introduced. Characterizations of temporal logic formulas in terms of dynamical properties of hybrid systems are presented -- in particular, forward invariance and finite time attractivity. These characterizations are exploited to formulate sufficient conditions assuring the satisfaction of temporal logic formulas -- when possible, these conditions do not involve solution information. Combining the results for formulas with a single operator, ways to certify more complex formulas are pointed out, in particular, via a decomposition using a finite state automaton. Academic examples illustrate the results throughout the paper.

eess.SY