arXiv subjects

Jian Xiang

Publications and source records attributed to Jian Xiang.

8 recordsLinked to original sources

arXiv2026

ProofPatch: Reviewing Lean Statements and Keeping the Reviews Valid as Formalizations Evolve

The kernel of the Lean proof assistant checks that a proof establishes its statement. Whether the statement says what was intended is left to human reviewers. This is the old problem of validating a specification, and it grows more pressing as language models write formal statements in bulk and agents edit formal developments continuously. We present ProofPatch, a tool that helps reviewers judge Lean statements and keeps their judgments valid while the development changes. A reviewer can ask the kernel targeted questions about a statement, such as whether a hypothesis is needed or whether a counterexample exists. Each decision is stored with fingerprints of the statement as Lean elaborated it and of the definitions it depends on, and any declaration can be pinned so that a patch changing it is blocked, whether a person or an agent built on a large language model (LLM) wrote the patch. Working on elaborated terms rather than source text is the central design choice: notation and formatting changes leave a decision intact, and a changed definition reaches every theorem that uses it. On 229 pairs of consecutive revisions of Mathlib, Lean's mathematics library, ProofPatch sends 118 of 12,898 synthetic decisions back for review. Every text-based alternative misses at least 38 of these or sends back at least 13 times as many. On 1,527 labeled statements, kernel evidence flags unfaithful ones with precision 0.88 to 0.96, and in 344 runs of an LLM agent no change to a pinned statement got through.

cs.LO↗

arXiv2026

DSR-Net: Learning Dynamic Skeletal Relations for 3D Human Pose Estimation

3D human pose estimation requires accurate modeling of motion-dependent skeletal structures and inter-joint dependencies. Existing methods typically rely on fixed skeletal topologies in Graph Convolutional Networks (GCNs) or implicitly capture joint relations through attention mechanisms, limiting their adaptability to diverse motion patterns. To address this issue,we proposeDSR-Net, a dynamic structural representation learning framework for 3D human pose estimation. Specifically, a Dynamic Skeletal Relation (DSR) module is introduced to learn adaptive inter-joint dependencies beyond predefined skeletal connections. Based on the learned relations, a hierarchical relation-aware fusion strategy is developed to facilitate effective interaction between structural and temporal representations. In addition, a lightweight Residual Skeletal Recalibration Module (RSRM) is designed to enhance the stability of structure-aware features with minimal computational overhead. Extensive experiments on Human3.6M and MPI-INF-3DHP demonstrate that DSR-Net achieves MPJPEs of 37.9 mm and 14.9 mm, respectively, consistently improving over strong baselines. The results validate the effectiveness of dynamic skeletal relation modeling for robust 3D human pose estimation.

cs.CV↗

arXiv2026

Where Does Detection Fail? A Residual-Evidence Diagnostic Workflow for Industrial Control Systems

Residual-based anomaly detectors for industrial control systems (ICS) convert model residuals into anomaly scores and alarms, but final detection metrics provide little guidance on which component to examine when performance is poor. We present a retrospective diagnostic workflow built around covariance-normalized residual energy (CNRE), a measurement based on squared Mahalanobis distance. The workflow evaluates whether the normal reference still describes the evaluation recording, whether attacks separate from normal operation under a specified reference, and how scoring and alarm rules use fixed residuals. Across fifteen detector--dataset pairs spanning five detectors on SWaT, WADI, and HAI, reference updates improve attack--normal separation in some cases but degrade it in others. A retrospective policy that updates the reference only when recommended by a label-free screening rule increases mean AUC from 0.751 with no update and 0.759 with unconditional updating to 0.809. On the twelve non-GDN pairs, which did not inform the screening boundaries, the corresponding AUC is 0.805, compared with 0.759 and 0.747. Rescoring CNRE under a fixed reference reproduces most of the AUC gain from a reference update on WADI, but not on SWaT. A detailed GDN case study further connects the diagnostic stages. Normal-only adaptation reduces normal prediction error by 27.3\%, yet its effect on attack separation depends on the reference protocol. With residuals fixed, improved score ranking also does not guarantee that normal-calibrated alarms preserve their nominal false-positive rate. Together, these results support diagnosing reference fit, attack evidence, and alarm calibration separately when selecting intervention stages and interpreting their effects.

cs.CR↗

arXiv2026

Dual-stream Spatio-Temporal GCN-Transformer Network for 3D Human Pose Estimation

3D human pose estimation is a classic and important research direction in the field of computer vision. In recent years, Transformer-based methods have made significant progress in lifting 2D to 3D human pose estimation. However, these methods primarily focus on modeling global temporal and spatial relationships, neglecting local skeletal relationships and the information interaction between different channels. Therefore, we have proposed a novel method,the Dual-stream Spatio-temporal GCN-Transformer Network (MixTGFormer). This method models the spatial and temporal relationships of human skeletons simultaneously through two parallel channels, achieving effective fusion of global and local features. The core of MixTGFormer is composed of stacked Mixformers. Specifically, the Mixformer includes the Mixformer Block and the Squeeze-and-Excitation Layer ( SE Layer). It first extracts and fuses various information of human skeletons through two parallel Mixformer Blocks with different modes. Then, it further supplements the fused information through the SE Layer. The Mixformer Block integrates Graph Convolutional Networks (GCN) into the Transformer, enhancing both local and global information utilization. Additionally, we further implement its temporal and spatial forms to extract both spatial and temporal relationships. We extensively evaluated our model on two benchmark datasets (Human3.6M and MPI-INF-3DHP). The experimental results showed that, compared to other methods, our MixTGFormer achieved state-of-the-art results, with P1 errors of 37.6mm and 15.7mm on these datasets, respectively.

cs.CV↗

arXiv2024

Measuring Robustness in Cyber-Physical Systems under Sensor Attacks

This paper contributes a formal framework for quantitative analysis of bounded sensor attacks on cyber-physical systems, using the formalism of differential dynamic logic. Given a precondition and postcondition of a system, we formalize two quantitative safety notions, quantitative forward and backward safety, which respectively express (1) how strong the strongest postcondition of the system is with respect to the specified postcondition, and (2) how strong the specified precondition is with respect to the weakest precondition of the system needed to ensure the specified postcondition holds. We introduce two notions, forward and backward robustness, to characterize the robustness of a system against sensor attacks as the loss of safety. To reason about robustness, we introduce two simulation distances, forward and backward simulation distances, which are defined based on the behavioral distances between the original system and the system with compromised sensors. Forward and backward distances, respectively, characterize upper bounds of the degree of forward and backward safety loss caused by the sensor attacks. We verify the two simulation distances by expressing them as modalities, i.e., formulas of differential dynamic logic, and develop an ad-hoc proof system to reason with such formulas. We showcase our formal notions and reasoning techniques on two non-trivial case studies: an autonomous vehicle that needs to avoid collision and a water tank system.

eess.SY↗

arXiv2021

Relational Analysis of Sensor Attacks on Cyber-Physical Systems

Cyber-physical systems, such as self-driving cars or autonomous aircraft, must defend against attacks that target sensor hardware. Analyzing system design can help engineers understand how a compromised sensor could impact the system's behavior; however, designing security analyses for cyber-physical systems is difficult due to their combination of discrete dynamics, continuous dynamics, and nondeterminism. This paper contributes a framework for modeling and analyzing sensor attacks on cyber-physical systems, using the formalism of hybrid programs. We formalize and analyze two relational properties of a system's robustness. These relational properties respectively express (1) whether a system's safety property can be influenced by sensor attacks, and (2) whether a system's high-integrity state can be affected by sensor attacks. We characterize these relational properties by defining an equivalence relation between a system under attack and the original unattacked system. That is, the system satisfies the robustness properties if executions of the attacked system are appropriately related to executions of the unattacked system. We present two techniques for reasoning about the equivalence relation and thus proving the relational properties for a system. One proof technique decomposes large proof obligations to smaller proof obligations. The other proof technique adapts the self-composition technique from the literature on secure information-flow, allowing us to reduce reasoning about the equivalence of two systems to reasoning about properties of a single system. This technique allows us to reuse existing tools for reasoning about properties of hybrid programs, but is challenging due to the combination of discrete dynamics, continuous dynamics, and nondeterminism. To evaluate, we present three case studies motivated by real design flaws in existing cyber-physical systems.

cs.CR↗

arXiv2019

Time-dependent generator coordinate method study of mass-asymmetric fission of actinides

Low-energy positive and negative parity collective states in the equilibrium minimum, and the dynamics of induced fission of actinide nuclei are investigated in a unified theoretical framework based on the generator coordinate method (GCM) with the Gaussian overlap approximation (GOA). The collective potential and inertia tensor, both at zero and finite temperature, are computed using the self-consistent multidimensionally constrained relativistic mean field (MDC-RMF) model, based on the energy density functional DD-PC1. Pairing correlations are treated in the BCS approximation with a separable pairing force of finite range. A collective quadrupole-octupole Hamiltonian characterized by zero-temperature axially-symmetric deformation energy surface and perturbative cranking inertia tensor, is used to model the low-lying excitation spectrum. The fission fragment charge distributions are obtained by propagating the initial collective states in time with the time-dependent GCM+GOA that uses the same quadrupole-octupole Hamiltonian, but with the collective potential and inertia tensor computed at finite temperature. The illustrative charge yields of $^{228}$Th, $^{234}$U, $^{240}$Pu, $^{244}$Cm, and $^{250}$Cf are in very good agreement with experiment, and the predicted mass asymmetry is consistent with the result of a recent microscopic study that has attributed the distribution (peak) of the heavier-fragment nuclei to shell-stabilized octupole deformations.

nucl-th↗

arXiv2017

Interpreted Formalisms for Configurations

Imprecise and incomplete specification of system \textit{configurations} threatens safety, security, functionality, and other critical system properties and uselessly enlarges the configuration spaces to be searched by configuration engineers and auto-tuners. To address these problems, this paper introduces \textit{interpreted formalisms based on real-world types for configurations}. Configuration values are lifted to values of real-world types, which we formalize as \textit{subset types} in Coq. Values of these types are dependent pairs whose components are values of underlying Coq types and proofs of additional properties about them. Real-world types both extend and further constrain \textit{machine-level} configurations, enabling richer, proof-based checking of their consistency with real-world constraints. Tactic-based proof scripts are written once to automate the construction of proofs, if proofs exist, for configuration fields and whole configurations. \textit{Failures to prove} reveal real-world type errors. Evaluation is based on a case study of combinatorial optimization of Hadoop performance by meta-heuristic search over Hadoop configurations spaces.

cs.LO↗