arXiv subjects

Haotian Deng

Publications and source records attributed to Haotian Deng.

18 recordsLinked to original sources

arXiv2026

Beyond Sensitive APIs: Detecting Access Control Flaws at Sensitive Callsites in Android Firmware

Existing studies of vulnerable pre-installed Android apps identify dangerous behavior by checking whether an app invokes an API from a predefined set of security-sensitive APIs. These sets usually exclude generic APIs to avoid false positives; unfortunately, this misses a class of vulnerabilities in which a generic API, such as a database read, appears benign in general but becomes security-sensitive when operating on protected data, yet is left without sufficient access control. While this class of vulnerabilities appears addressable via access control analysis, existing studies focus only on the presence of checks, not on whether those checks enforce sufficient protection for the operation at a given callsite. In this work, we propose Callix, which first assesses callsite sensitivity by jointly analyzing the invoked API functionality and the data involved in the operation, then recovers each security check on the execution path as an explicit security property, and finally introduces the notion of restriction context to decide whether these checks are sufficient for the identified sensitive operation. We evaluated Callix on 1,750 distinct pre-installed apps from the 10 top-tier Android vendors as of 2025. In total, Callix discovered 819 vulnerable paths across these vendors, 42.1% of which allow reading or modifying private user data through generic database operations. Manual validation of a random 60% sample shows a precision of 95.1%. Many of our findings have been confirmed and rewarded through vendor bug bounty programs.

cs.CR↗

arXiv2026

Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \in \{1,3,5,8\}$), achieving up to a $32\%$ relative gain and solving $82$ additional theorems on a $1{,}990$-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing $84\text{--}96\%$ of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches. This targeted repair successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.

cs.AI↗

arXiv2026

Can Vision-Language Models Stay Helpful When Facing Implicit Risks? Intent-Privilege OPSD for Efficient Safety-Helpfulness Alignment

Vision-Language Models (VLMs) remain vulnerable to cross-modal implicit risks: visual and textual inputs that appear benign in isolation can jointly elicit unsafe responses. Existing safety methods often require large preference datasets, costly multi-rollout training, or additional safeguards at inference time. They may also sacrifice helpfulness by directly refusing requests that could be answered safely. In this paper, we propose Intent-Privilege On-Policy Self-Distillation (OPSD), which leverages evidence-grounded intent as privileged supervision during training to help VLMs recognize implicit risks and provide safe, useful responses instead of blanket refusals. OPSD distills a teacher's intent-conditioned preferences over responses into a student using a single rollout per prompt; the student then responds without intent annotations or an additional safety module. With only 1,447 safety-specific examples - 95% fewer than standard preference datasets - OPSD reduces training time by 5x relative to multi-rollout GRPO-style training and average inference length by 7%. It attains the highest ratio for joint safety-helpfulness success, which measures the proportion of responses that are both safe and helpful, across all five evaluation groups. Remarkably, on pooled SIUO+HoliSafe, this success ratio rises from 43.9% to 53.5%. These results show that training-time intent supervision can improve both safety and helpfulness while substantially reducing data, training, and inference costs.

cs.CL↗

arXiv2026

Capture Now, Consume Later: Reachability Types with Flow-Sensitive Effects for Higher-Order Ownership Transfer

Higher-order impure programs routinely transfer or consume a resource through a closure: when one access path consumes the resource, it must be disabled through all remaining aliases---including those captured in closures---precisely at the point of consumption. We present a flow-sensitive type-and-effect system for reachability types that makes such ownership transfer sound in the presence of higher-order control flow. The key idea is simple: every computation can induce a use and/or a kill effect. The system statically tracks them, rejects any use of a killed resource. With reachability qualifiers and flow-sensitive effects, the system also derives on-demand uniqueness patterns compatible with higher-order impure functions. We illustrate the practicality of the system through numerous case studies such as a freezable counter, a destructive merge on unique linked lists, Rust-style swap on Box, recursive sum on unique linked lists, and use-once continuations. We formalize the system as the $\mathsf{F}_{\varepsilon <:}^{\diamondsuit}$ calculus, present its typing rules and operational semantics, and prove effect soundness, including multi-step preservation and preservation under parallel reduction. We mechanize all key results in Rocq.

cs.PL↗

arXiv2026

ShadowBlock: Efficient Dynamic Anonymous Blocklisting and Its Cross-chain Application

Online harassment, incitement to violence, racist behavior, and other harmful content on social media can damage social harmony and even break the law. Traditional blocklisting technologies can block malicious users, but this comes at the expense of identity privacy. The anonymous blocklisting has emerged as an effective mechanism to restrict the abuse of freedom of speech while protecting user identity privacy. However, the state-of-the-art anonymous blocklisting schemes suffer from either poor dynamism or low efficiency. In this paper, we propose $\mathsf{ShadowBlock}$, an efficient dynamic anonymous blocklisting scheme. Specifically, we utilize the pseudorandom function and cryptographic accumulator to construct the public blocklisting, enabling users to prove they are not on the blocklisting in an anonymous manner. To improve verification efficiency, we design an aggregation zero-knowledge proof mechanism that converts multiple verification operations into a single one. In addition, we leverage the accumulator's property to achieve efficient updates of the blocklisting, i.e., the original proof can be reused with minimal updates rather than regenerating the entire proof. Experiments show that $\mathsf{ShadowBlock}$ has better dynamics and efficiency than the existing schemes. Finally, the discussion on applications indicates that $\mathsf{ShadowBlock}$ also holds significant value and has broad prospects in emerging fields such as cross-chain identity management.

cs.CR↗

arXiv2026

Heisenberg-like critical behavior in the quasi-two-dimensional metallic ferromagnet LaCrSb3

LaCrSb3 is a material exhibiting both quasi-two-dimensional spin fluctuations and three-dimensional magnetic interaction characteristics. By measuring the isothermal magnetization of single-crystals and conducting a systematic critical behavior analysis, we clarify the critical properties of its ferromagnetic phase transition and the intrinsic magnetic interaction mechanism. Based on high-precision isothermal magnetization data measured in the vicinity of the critical point, the Curie temperature for the ferromagnetic-paramagnetic phase transition is determined to be TC = 126 K, with the critical exponents obtained as $β$ = 0.376, $γ$ = 1.417 and $δ$ = 4.76 via the self-consistent iterative method based on the Arrott-Noakes equation. The reliability of these critical exponents is verified by the Widom scaling law, the magnetic state scaling equation and other analyses. A comparison with theoretical models demonstrates that the critical behavior of the magnetic phase transition in this system basically belongs to the universality class of the three-dimensional Heisenberg model. This conclusion is further confirmed by the distance-dependent decay behavior of the exchange interaction J(r), revealing the dominant role of isotropic direct exchange interactions in this system. Finally, drawing on research findings of other quasi-two-dimensional magnetic materials, this work proposes that LaCrSb3 may exhibit finite-temperature magnetic order in the two-dimensional limit, thereby possessing important theoretical research significance and promising practical application prospects.

cond-mat.str-el↗

arXiv2026

Typestate via Revocable Capabilities

Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based constructs like Java's synchronized blocks offer ease of reasoning, but they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive approaches enable fine-grained control, but they require sophisticated typestate analyses and often burden programmers with explicit state tracking. In this work, we present a novel approach that unifies the ease of scoped reasoning with the expressiveness of imperative typestate management. Our design extends traditional flow-insensitive capability mechanisms to a flow-sensitive setting. In particular, we decouple capability lifetimes from lexical scopes, allowing functions to receive, revoke, or return capabilities in a flow-sensitive manner, building on existing mechanisms for the safety and ergonomics of scoped capability programming. We implement our approach as an extension to the Scala 3 compiler, leveraging path-dependent types and implicit resolution to enable concise, statically safe, and expressive typestate programming. Our prototype generically supports a wide range of patterns, including file operations, advanced locking protocols, DOM construction, and session types, showing that expressive and safe typestate management can be achieved with minimal extensions to an existing language with capability support.

cs.PL↗

arXiv2026

Local Intrinsic Dimension of Representations Predicts Alignment and Generalization in AI Models and Human Brain

Recent work has found that neural networks with stronger generalization tend to exhibit higher representational alignment with one another across architectures and training paradigms. In this work, we show that models with stronger generalization also align more strongly with human neural activity. Moreover, generalization performance, model--model alignment, and model--brain alignment are all significantly correlated with each other. We further show that these relationships can be explained by a single geometric property of learned representations: the local intrinsic dimension of embeddings. Lower local dimension is consistently associated with stronger model--model alignment, stronger model--brain alignment, and better generalization, whereas global dimension measures fail to capture these effects. Finally, we find that increasing model capacity and training data scale systematically reduces local intrinsic dimension, providing a geometric account of the benefits of scaling. Together, our results identify local intrinsic dimension as a unifying descriptor of representational convergence in artificial and biological systems.

cs.LG↗

arXiv2026

Understanding Generalization from Embedding Dimension and Distributional Convergence

Deep neural networks often generalize well despite heavy over-parameterization, challenging classical parameter-based analyses. We study generalization from a representation-centric perspective and analyze how the geometry of learned embeddings controls predictive performance for a fixed trained model. We show that population risk can be bounded by two factors: (i) the intrinsic dimension of the embedding distribution, which determines the convergence rate of empirical embedding distribution to the population distribution in Wasserstein distance, and (ii) the sensitivity of the downstream mapping from embeddings to predictions, characterized by Lipschitz constants. Together, these yield an embedding-dependent error bound that does not rely on parameter counts or hypothesis class complexity. At the final embedding layer, architectural sensitivity vanishes and the bound is dominated by embedding dimension, explaining its strong empirical correlation with generalization performance. Experiments across architectures and datasets validate the theory and demonstrate the utility of embedding-based diagnostics.

cs.LG↗

arXiv2026

Omni-fMRI: A Universal Atlas-Free fMRI Foundation Model

Self-supervised fMRI foundation models have shown promising transfer performance, yet most rely on predefined region-level parcellations that discard fine-grained voxel information and introduce atlas-dependent biases. We propose Omni-fMRI, an atlas-free foundation model that operates directly on voxel-level signals. To enable scalable pretraining on 49,497 fMRI sessions across nine datasets, Omni-fMRI introduces a dynamic patching mechanism that substantially reduces computational cost while preserving informative spatial structure. To support reproducibility and fair comparison, we establish a comprehensive benchmark suite spanning 11 datasets and a diverse set of resting-state and task-based fMRI tasks. Experimental results demonstrate that Omni-fMRI consistently outperforms existing foundation models, providing a scalable and reproducible framework for atlas-free brain representation learning. Code and logs are available.

cs.CE↗

arXiv2025

Rubric-Conditioned LLM Grading: Alignment, Uncertainty, and Robustness

Automated short-answer grading (ASAG) remains a challenging task due to the linguistic variability of student responses and the need for nuanced, rubric-aligned partial credit. While Large Language Models (LLMs) offer a promising solution, their reliability as automated judges in rubric-based settings requires rigorous assessment. In this paper, we systematically evaluate the performance of LLM-judges for rubric-based short-answer grading. We investigate three key aspects: the alignment of LLM grading with expert judgment across varying rubric complexities, the trade-off between uncertainty and accuracy facilitated by a consensus-based deferral mechanism, and the model's robustness under random input perturbations and adversarial attacks. Using the SciEntsBank benchmark and Qwen 2.5-72B, we find that alignment is strong for binary tasks but degrades with increased rubric granularity. Our "Trust Curve" analysis demonstrates a clear trade-off where filtering low-confidence predictions improves accuracy on the remaining subset. Additionally, robustness experiments reveal that while the model is resilient to prompt injection, it is sensitive to synonym substitutions. Our work provides critical insights into the capabilities and limitations of rubric-conditioned LLM judges, highlighting the importance of uncertainty estimation and robustness testing for reliable deployment.

cs.CL↗

arXiv2025

AutoICE: Automatically Synthesizing Verifiable C Code via LLM-driven Evolution

Automatically synthesizing verifiable code from natural language requirements ensures software correctness and reliability while significantly lowering the barrier to adopting the techniques of formal methods. With the rise of large language models (LLMs), long-standing efforts at autoformalization have gained new momentum. However, existing approaches suffer from severe syntactic and semantic errors due to the scarcity of domain-specific pre-training corpora and often fail to formalize implicit knowledge effectively. In this paper, we propose AutoICE, an LLM-driven evolutionary search for synthesizing verifiable C code. It introduces the diverse individual initialization and the collaborative crossover to enable diverse iterative updates, thereby mitigating error propagation inherent in single-agent iterations. Besides, it employs the self-reflective mutation to facilitate the discovery of implicit knowledge. Evaluation results demonstrate the effectiveness of AutoICE: it successfully verifies $90.36$\% of code, outperforming the state-of-the-art (SOTA) approach. Besides, on a developer-friendly dataset variant, AutoICE achieves a $88.33$\% verification success rate, significantly surpassing the $65$\% success rate of the SOTA approach.

cs.SE↗

arXiv2025

Treatment effects at the margin: Everyone is marginal

This paper develops a framework for identifying treatment effects when a policy simultaneously alters both the incentive to participate and the outcome of interest -- such as hiring decisions and wages in response to employment subsidies; or working decisions and wages in response to job trainings. This framework was inspired by my PhD project on a Belgian reform that subsidised first-time hiring, inducing entry by marginal firms yet meanwhile changing the wages they pay. Standard methods addressing selection-into-treatment concepts (like Heckman selection equations and local average treatment effects), or before-after comparisons (including simple DiD or RDD), cannot isolate effects at this shifting margin where treatment defines who is observed. I introduce marginality-weighted estimands that recover causal effects among policy-induced entrants, offering a policy-relevant alternative in settings with endogenous selection. This method can thus be applied widely to understanding the economic impacts of public programmes, especially in fields largely relying on reduced-form causal inference estimation (e.g. labour economics, development economics, health economics).

econ.EM↗

arXiv2025

Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)

Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches -- ownership systems, linear and affine types, uniqueness types, and lexical effect tracking -- impose global restrictions such as uniqueness or linearity, or rely on shallow syntactic analyses. These designs fall short with higher-order functions and shared mutable state. Reachability Types (RT) track aliasing and separation in higher-order programs, ensuring runtime safety and non-interference. However, RT systems face three key limitations: (1) they prohibit cyclic references, ruling out non-terminating computations and fixed-point combinators; (2) they require deep tracking, where a qualifier must include all transitively reachable locations, reducing precision and hindering optimizations like fine-grained parallelism; and (3) referent qualifier invariance prevents referents from escaping their allocation contexts, making reference factories inexpressible. In this work, we address these limitations by extending RT with three mechanisms that enhance expressiveness. First, we introduce cyclic references, enabling recursive patterns to be encoded directly through the store. Second, we adopt shallow qualifier tracking, decoupling references from their transitively reachable values. Finally, we introduce an escaping rule with reference subtyping, allowing referent qualifiers to outlive their allocation context. These extensions are formalized in the $\mathsf{F}_{<:}^{\circ}$-calculus with a mechanized proof of type soundness, and case studies illustrate expressiveness through fixpoint combinators, non-interfering parallelism, and escaping read-only references.

cs.PL↗

arXiv2025

Synthesizing Images on Perceptual Boundaries of ANNs for Uncovering Human Perceptual Variability on Facial Expressions

A fundamental challenge in affective cognitive science is to develop models that accurately capture the relationship between external emotional stimuli and human internal experiences. While ANNs have demonstrated remarkable accuracy in facial expression recognition, their ability to model inter-individual differences in human perception remains underexplored. This study investigates the phenomenon of high perceptual variability-where individuals exhibit significant differences in emotion categorization even when viewing the same stimulus. Inspired by the similarity between ANNs and human perception, we hypothesize that facial expression samples that are ambiguous for ANN classifiers also elicit divergent perceptual judgments among human observers. To examine this hypothesis, we introduce a novel perceptual boundary sampling method to generate facial expression stimuli that lie along ANN decision boundaries. These ambiguous samples form the basis of the varEmotion dataset, constructed through large-scale human behavioral experiments. Our analysis reveals that these ANN-confusing stimuli also provoke heightened perceptual uncertainty in human participants, highlighting shared computational principles in emotion perception. Finally, by fine-tuning ANN representations using behavioral data, we achieve alignment between ANN predictions and both group-level and individual-level human perceptual patterns. Our findings establish a systematic link between ANN decision boundaries and human perceptual variability, offering new insights into personalized modeling of emotional interpretation.

cs.CV↗

arXiv2025

Scale-Invariance Drives Convergence in AI and Brain Representations

Despite variations in architecture and pretraining strategies, recent studies indicate that large-scale AI models often converge toward similar internal representations that also align with neural activity. We propose that scale-invariance, a fundamental structural principle in natural systems, is a key driver of this convergence. In this work, we propose a multi-scale analytical framework to quantify two core aspects of scale-invariance in AI representations: dimensional stability and structural similarity across scales. We further investigate whether these properties can predict alignment performance with functional Magnetic Resonance Imaging (fMRI) responses in the visual cortex. Our analysis reveals that embeddings with more consistent dimension and higher structural similarity across scales align better with fMRI data. Furthermore, we find that the manifold structure of fMRI data is more concentrated, with most features dissipating at smaller scales. Embeddings with similar scale patterns align more closely with fMRI data. We also show that larger pretraining datasets and the inclusion of language modalities enhance the scale-invariance properties of embeddings, further improving neural alignment. Our findings indicate that scale-invariance is a fundamental structural principle that bridges artificial and biological representations, providing a new framework for evaluating the structural quality of human-like AI systems.

q-bio.NC↗

arXiv2025

Synthesizing Images on Perceptual Boundaries of ANNs for Uncovering and Manipulating Human Perceptual Variability

Human decision-making in cognitive tasks and daily life exhibits considerable variability, shaped by factors such as task difficulty, individual preferences, and personal experiences. Understanding this variability across individuals is essential for uncovering the perceptual and decision-making mechanisms that humans rely on when faced with uncertainty and ambiguity. We present a computational framework BAM (Boundary Alignment & Manipulation framework) that combines perceptual boundary sampling in ANNs and human behavioral experiments to systematically investigate this phenomenon. Our perceptual boundary sampling algorithm generates stimuli along ANN decision boundaries that intrinsically induce significant perceptual variability. The efficacy of these stimuli is empirically validated through large-scale behavioral experiments involving 246 participants across 116,715 trials, culminating in the variMNIST dataset containing 19,943 systematically annotated images. Through personalized model alignment and adversarial generation, we establish a reliable method for simultaneously predicting and manipulating the divergent perceptual decisions of pairs of participants. This work bridges the gap between computational models and human individual difference research, providing new tools for personalized perception analysis.

cs.AI↗

arXiv2015

iCellular: Define Your Own Cellular Network Access on Commodity Smartphones

Leveraging multi-carrier access offers a promising approach to boosting access quality in mobile networks. However, our experiments show that the potential benefits are hard to fulfill due to fundamental limitations in the network-controlled design. To overcome these limitations, we propose iCellular, which allows users to define and intelligently select their own cellular network access from multiple carriers. iCellular reuses the existing device-side mechanisms and the standard cellular network procedure, but leverages the end device's intelligence to be proactive and adaptive in multi-carrier selection. It performs adaptive monitoring to ensure responsive selection and minimal service disruption, and enhances carrier selection with online learning and runtime decision fault prevention. It is deployable on commodity phones without any infrastructure/hardware change. We implement iCellular on commodity Nexus 6 phones and leverage Google Project-Fi's efforts to test multi-carrier access among two top US carriers: T-Mobile and Sprint. Our experiments confirm that iCellular helps users with up to 3.74x throughput improvement (7x suspension and 1.9x latency reduction) over the state-of-art selection. Moreover, iCellular locates the best-quality carrier in most cases, with negligible overhead on CPU, memory and energy consumption.

cs.NI↗