arXiv subjects

Haoyu Li

Publications and source records attributed to Haoyu Li.

At least 73 records · Page 4Linked to original sources

arXiv2025

WEST: LLM based Speech Toolkit for Speech Understanding, Generation, and Interaction

In this paper, we present WEST(WE Speech Toolkit), a speech toolkit based on a large language model (LLM) for speech understanding, generation, and interaction. There are three key features of WEST: 1) Fully LLM-based: Standing on the shoulders of giants by reusing mature architectures, ecosystems (e.g., Hugging Face), and methods (e.g., sequence packing) from large models. 2) Full-stack: Supports tasks such as recognition, synthesis, understanding, dialogue, and multimodal capabilities, with extensibility to incorporate open-source models. 3) Simple and Stupid: A simple and stupid speech toolkit that everyone can Touch. In addition, WEST provides two types of recipes, models, and experimental results. The first is entirely based on open-source models and open-source data, allowing users to fully reproduce the experiments in this paper and serving as a verification system or minimal system baseline. The second is trained on massive data, offering superior performance so the user can directly apply it out of the box. WEST is publicly avilable at https://github.com/wenet-e2e/west/

cs.CL↗

arXiv2025

Two-Stage Learning of Stabilizing Neural Controllers via Zubov Sampling and Iterative Domain Expansion

Learning-based neural network (NN) control policies have shown impressive empirical performance. However, obtaining stability guarantees and estimates of the region of attraction of these learned neural controllers is challenging due to the lack of stable and scalable training and verification algorithms. Although previous works in this area have achieved great success, much conservatism remains in their frameworks. In this work, we propose a novel two-stage training framework to jointly synthesize a controller and a Lyapunov function for continuous-time systems. By leveraging a Zubov-inspired region of attraction characterization to directly estimate stability boundaries, we propose a novel training-data sampling strategy and a domain-updating mechanism that significantly reduces the conservatism in training. Moreover, unlike existing works on continuous-time systems that rely on an SMT solver to formally verify the Lyapunov condition, we extend state-of-the-art neural network verifier $α,\!β$-CROWN with the capability of performing automatic bound propagation through the Jacobian of dynamical systems and a novel verification scheme that avoids expensive bisection. To demonstrate the effectiveness of our approach, we conduct numerical experiments by synthesizing and verifying controllers on several challenging nonlinear systems across multiple dimensions. We show that our training can yield region of attractions with volume $5 - 1.5\cdot 10^{5}$ times larger compared to the baselines, and our verification on continuous systems can be up to $40-10{,}000$ times faster compared to the traditional SMT solver dReal. Our code is available at https://github.com/Verified-Intelligence/Two-Stage_Neural_Controller_Training.

cs.LG↗

arXiv2025

LLMartini: Seamless and Interactive Leveraging of Multiple LLMs through Comparison and Composition

The growing diversity of large language models (LLMs) means users often need to compare and combine outputs from different models to obtain higher-quality or more comprehensive responses. However, switching between separate interfaces and manually integrating outputs is inherently inefficient, leading to a high cognitive burden and fragmented workflows. To address this, we present LLMartini, a novel interactive system that supports seamless comparison, selection, and intuitive cross-model composition tools. The system decomposes responses into semantically aligned segments based on task-specific criteria, automatically merges consensus content, and highlights model differences through color coding while preserving unique contributions. In a user study (N=18), LLMartini significantly outperformed conventional manual methods across all measured metrics, including task completion time, cognitive load, and user satisfaction. Our work highlights the importance of human-centered design in enhancing the efficiency and creativity of multi-LLM interactions and offers practical implications for leveraging the complementary strengths of various language models.

cs.HC↗

arXiv2025

DFUSE: Strongly Consistent Write-Back Kernel Caching for Distributed Userspace File Systems

Cloud platforms host thousands of tenants that demand POSIX semantics, high throughput, and rapid evolution from their storage layer. Kernel-native distributed file systems supply raw speed, but their privileged code base couples every release to the kernel, widens the blast radius of crashes, and slows innovation. FUSE-based distributed file systems flip those trade-offs: they run in user space for fast deployment and strong fault isolation, yet the FUSE interface disables the kernel's write-back page cache whenever strong consistency is required. Practitioners must therefore choose between (i) weak consistency with fast write-back caching or (ii) strong consistency with slow write-through I/O, a limitation that has kept FUSE distributed file systems out of write-intensive cloud workloads. To this end, we present DFUSE, the first distributed FUSE file system that delivers write-back kernel caching and strong consistency. DFUSE achieves this by offloading userspace consistency control to the kernel driver, allowing coordinated access to the kernel's page cache across nodes. This design eliminates blind local cache updates and ensures cluster-wide strong consistency without compromising performance. In our evaluation, DFUSE achieves up to 68.0% higher throughput and 40.4% lower latency than the existing write-through design of FUSE-based distributed file systems.

cs.OS↗

arXiv2025

Construction of blowup solutions for Liouville systems

We study the following Liouville system defined on a flat torus \begin{equation} \left\{ \begin{array}{lr} -Δu_i=\sum_{j=1}^n a_{ij}ρ_j\Big(\frac{h_j e^{u_j}}{\int_Ωh_j e^{u_j}}-1\Big),\nonumber \\ u_j\in H_{per}^1(Ω)\mbox{ for }i\in I=\{1,\cdots,n\}\nonumber, \end{array} \right. \end{equation} where $h_j\in C^3(Ω)$, $h_j>0$, $ρ_j>0$ and $u=(u_1,..,u_n)$ is doubly periodic on $\partialΩ$. The matrix $A=(a_{ij})_{n\times n}$ satisfies certain properties. One central problem about Liouville systems is whether multi-bubble solutions do exist. In this work we present a comprehensive construction of multi-bubble solutions in the most general setting.

math.AP↗

arXiv2025

Local uniqueness and non-degeneracy of blowup solutions for regular Liouville systems

We study the following Liouville system defined on a compact Riemann surface $M$, \begin{equation} -Δu_i=\sum_{j=1}^n a_{ij}ρ_j\Big(\frac{h_j e^{u_j}}{\int_Ωh_j e^{u_j}}-1\Big)\mbox{ in }M\mbox{ for }i=1,\cdots,n,\nonumber \end{equation} where the coefficient matrix $A=(a_{ij})_{n\times n}$ is nonnegative, $h_1, \ldots, h_n$ are positive smooth functions, and $ρ_1, \ldots, ρ_n$ are positive constants. For the blowup solutions, we establish their uniqueness and non-degeneracy based on natural assumptions. The main results significantly generalize corresponding results for single Liouville equations \cite{BartJevLeeYang2019,BartYangZhang20241,BartYangZhang20242}. To overcome several substantial difficulties, we develop certain tools and extend them into a more general framework applicable to similar situations. Notably, to address the considerable challenge of a continuum of standard bubbles, we refine the techniques from Huang-Zhang \cite{HuangZhang2022} and Zhang \cite{Zhang2006,Zhang2009} to achieve extremely precise pointwise estimates. Additionally, to address the limited information provided by the Pohozaev identity, we develop a useful Fredholm theory to discern the exact role that the Pohozaev identity plays for systems. The considerable difference between systems and a single equation is also reflected in the location of blowup points, where the uncertainty of the energy type of the blowup point makes it difficult to determine the sufficiency of pointwise estimates. In this regard, we extend our highly precise pointwise estimates to any finite order. This aspect is drastically distinct from analyses of single equations.

math.AP↗

arXiv2025

Gradient-based multi-focus image fusion with focus-aware saliency enhancement

Multi-focus image fusion (MFIF) aims to yield an all-focused image from multiple partially focused inputs, which is crucial in applications cover sur-veillance, microscopy, and computational photography. However, existing methods struggle to preserve sharp focus-defocus boundaries, often resulting in blurred transitions and focused details loss. To solve this problem, we propose a MFIF method based on significant boundary enhancement, which generates high-quality fused boundaries while effectively detecting focus in-formation. Particularly, we propose a gradient-domain-based model that can obtain initial fusion results with complete boundaries and effectively pre-serve the boundary details. Additionally, we introduce Tenengrad gradient detection to extract salient features from both the source images and the ini-tial fused image, generating the corresponding saliency maps. For boundary refinement, we develop a focus metric based on gradient and complementary information, integrating the salient features with the complementary infor-mation across images to emphasize focused regions and produce a high-quality initial decision result. Extensive experiments on four public datasets demonstrate that our method consistently outperforms 12 state-of-the-art methods in both subjective and objective evaluations. We have realized codes in https://github.com/Lihyua/GICI

cs.CV↗

arXiv2025

Reverse Engineering User Stories from Code using Large Language Models

User stories are essential in agile development, yet often missing or outdated in legacy and poorly documented systems. We investigate whether large language models (LLMs) can automatically recover user stories directly from source code and how prompt design impacts output quality. Using 1,750 annotated C++ snippets of varying complexity, we evaluate five state-of-the-art LLMs across six prompting strategies. Results show that all models achieve, on average, an F1 score of 0.8 for code up to 200 NLOC. Our findings show that a single illustrative example enables the smallest model (8B) to match the performance of a much larger 70B model. In contrast, structured reasoning via Chain-of-Thought offers only marginal gains, primarily for larger models.

cs.SE↗

arXiv2025

Dual-Stage Safe Herding Framework for Adversarial Attacker in Dynamic Environment

Recent advances in robotics have enabled the widespread deployment of autonomous robotic systems in complex operational environments, presenting both unprecedented opportunities and significant security problems. Traditional shepherding approaches based on fixed formations are often ineffective or risky in urban and obstacle-rich scenarios, especially when facing adversarial agents with unknown and adaptive behaviors. This paper addresses this challenge as an extended herding problem, where defensive robotic systems must safely guide adversarial agents with unknown strategies away from protected areas and into predetermined safe regions, while maintaining collision-free navigation in dynamic environments. We propose a hierarchical hybrid framework based on reach-avoid game theory and local motion planning, incorporating a virtual containment boundary and event-triggered pursuit mechanisms to enable scalable and robust multi-agent coordination. Simulation results demonstrate that the proposed approach achieves safe and efficient guidance of adversarial agents to designated regions.

cs.RO↗

arXiv2025

KNighter: Transforming Static Analysis with LLM-Synthesized Checkers

Static analysis is a powerful technique for bug detection in critical systems like operating system kernels. However, designing and implementing static analyzers is challenging, time-consuming, and typically limited to predefined bug patterns. While large language models (LLMs) have shown promise for static analysis, directly applying them to scan large systems remains impractical due to computational constraints and contextual limitations. We present KNighter, the first approach that unlocks scalable LLM-based static analysis by automatically synthesizing static analyzers from historical bug patterns. Rather than using LLMs to directly analyze massive systems, our key insight is leveraging LLMs to generate specialized static analyzers guided by historical patch knowledge. KNighter implements this vision through a multi-stage synthesis pipeline that validates checker correctness against original patches and employs an automated refinement process to iteratively reduce false positives. Our evaluation on the Linux kernel demonstrates that KNighter generates high-precision checkers capable of detecting diverse bug patterns overlooked by existing human-written analyzers. To date, KNighter-synthesized checkers have discovered 92 new, critical, long-latent bugs (average 4.3 years) in the Linux kernel; 77 are confirmed, 57 fixed, and 30 have been assigned CVE numbers. This work establishes an entirely new paradigm for scalable, reliable, and traceable LLM-based static analysis for real-world systems via checker synthesis.

cs.SE↗

arXiv2025

Joint decoding method for controllable contextual speech recognition based on Speech LLM

Contextual speech recognition refers to the ability to identify preferences for specific content based on contextual information. Recently, leveraging the contextual understanding capabilities of Speech LLM to achieve contextual biasing by injecting contextual information through prompts have emerged as a research hotspot.However, the direct information injection method via prompts relies on the internal attention mechanism of the model, making it impossible to explicitly control the extent of information injection. To address this limitation, we propose a joint decoding method to control the contextual information. This approach enables explicit control over the injected contextual information and achieving superior recognition performance. Additionally, Our method can also be used for sensitive word suppression recognition.Furthermore, experimental results show that even Speech LLM not pre-trained on long contextual data can acquire long contextual capabilities through our method.

eess.AS↗

arXiv2025

3DTTNet: Multimodal Fusion-Based 3D Traversable Terrain Modeling for Off-Road Environments

Off-road environments remain significant challenges for autonomous ground vehicles, due to the lack of structured roads and the presence of complex obstacles, such as uneven terrain, vegetation, and occlusions. Traditional perception algorithms, primarily designed for structured environments, often fail in unstructured scenarios. In this paper, traversable area recognition is achieved through semantic scene completion. A novel multimodal method, 3DTTNet, is proposed to generate dense traversable terrain estimations by integrating LiDAR point clouds with monocular images from a forward-facing perspective. By integrating multimodal data, environmental feature extraction is strengthened, which is crucial for accurate terrain modeling in complex terrains. Furthermore, RELLIS-OCC, a dataset with 3D traversable annotations, is introduced, incorporating geometric features such as step height, slope, and unevenness. Through a comprehensive analysis of vehicle obsta cle-crossing conditions and the incorporation of vehicle body structure constraints, four traversability cost labels are generated: lethal, medium-cost, low-cost, and free. Experimental results demonstrate that 3DTTNet outperforms the comparison approaches in 3D traversable area recognition, particularly in off-road environments with irregular geometries and partial occlusions. Specifically, 3DTTNet achieves a 42\% improvement in scene completion IoU compared to other models. The proposed framework is scalable and adaptable to various vehicle platforms, allowing for adjustments to occupancy grid parameters and the integration of advanced dynamic models for traversability cost estimation.

cs.RO↗

arXiv2025

MFA-KWS: Effective Keyword Spotting with Multi-head Frame-asynchronous Decoding

Keyword spotting (KWS) is essential for voice-driven applications, demanding both accuracy and efficiency. Traditional ASR-based KWS methods, such as greedy and beam search, explore the entire search space without explicitly prioritizing keyword detection, often leading to suboptimal performance. In this paper, we propose an effective keyword-specific KWS framework by introducing a streaming-oriented CTC-Transducer-combined frame-asynchronous system with multi-head frame-asynchronous decoding (MFA-KWS). Specifically, MFA-KWS employs keyword-specific phone-synchronous decoding for CTC and replaces conventional RNN-T with Token-and-Duration Transducer to enhance both performance and efficiency. Furthermore, we explore various score fusion strategies, including single-frame-based and consistency-based methods. Extensive experiments demonstrate the superior performance of MFA-KWS, which achieves state-of-the-art results on both fixed keyword and arbitrary keywords datasets, such as Snips, MobvoiHotwords, and LibriKWS-20, while exhibiting strong robustness in noisy environments. Among fusion strategies, the consistency-based CDC-Last method delivers the best performance. Additionally, MFA-KWS achieves a 47% to 63% speed-up over the frame-synchronous baselines across various datasets. Extensive experimental results confirm that MFA-KWS is an effective and efficient KWS framework, making it well-suited for on-device deployment.

eess.AS↗

arXiv2025

Safe Domains of Attraction for Discrete-Time Nonlinear Systems: Characterization and Verifiable Neural Network Estimation

Analysis of nonlinear autonomous systems typically involves estimating domains of attraction, which have been a topic of extensive research interest for decades. Despite that, accurately estimating domains of attraction for nonlinear systems remains a challenging task, where existing methods are conservative or limited to low-dimensional systems. The estimation becomes even more challenging when accounting for state constraints. In this work, we propose a framework to accurately estimate safe (state-constrained) domains of attraction for discrete-time autonomous nonlinear systems. In establishing this framework, we first derive a new Zubov equation, whose solution corresponds to the exact safe domain of attraction. The solution to the aforementioned Zubov equation is shown to be unique and continuous over the whole state space. We then present a physics-informed approach to approximating the solution of the Zubov equation using neural networks. To obtain certifiable estimates of the domain of attraction from the neural network approximate solutions, we propose a verification framework that can be implemented using standard verification tools (e.g., $α,\!β$-CROWN and dReal). To illustrate its effectiveness, we demonstrate our approach through numerical examples concerning nonlinear systems with state constraints.

eess.SY↗

arXiv2025

From Macro to Micro: Probing Dataset Diversity in Language Model Fine-Tuning

Dataset diversity plays a pivotal role for the successful training of many machine learning models, particularly in the supervised fine-tuning (SFT) stage of large language model (LLM) development. Despite increasing recognition of its importance, systematic analyses of dataset diversity still remain underexplored. To address this gap, this work presents a systematic taxonomy of existing diversity-control strategies, which primarily focus on the instruction component, operating at either macroscopic (entire instruction semantics) or mesoscopic levels (instruction units), and furthermore introduces a novel analysis of microscopic diversity within the response component, specifically analyzing the statistical distribution of tokens in SFT training samples. In the experimental evaluation, we construct fixed-size datasets (e.g., 10,000 samples each) from a corpus of 117,000 open-source SFT samples, incorporating six distinct diversity-control strategies spanning macro-, meso-, and microscopic levels applied to both instructions and responses. We then fine-tune LLMs on these datasets to assess the six diversity-control strategies. Results reveal that while macroscopic and mesoscopic strategies lead to higher performance with increasing diversity, the microscopic strategy in responses exhibits both a stronger correlation between model performance and the degree of diversity and superior performance with maximum diversity across all strategies. These findings offer actionable insights for constructing high-performance SFT datasets.

cs.CL↗

arXiv2025

Masked Self-distilled Transducer-based Keyword Spotting with Semi-autoregressive Decoding

RNN-T-based keyword spotting (KWS) with autoregressive decoding~(AR) has gained attention due to its streaming architecture and superior performance. However, the simplicity of the prediction network in RNN-T poses an overfitting issue, especially under challenging scenarios, resulting in degraded performance. In this paper, we propose a masked self-distillation (MSD) training strategy that avoids RNN-Ts overly relying on prediction networks to alleviate overfitting. Such training enables masked non-autoregressive (NAR) decoding, which fully masks the RNN-T predictor output during KWS decoding. In addition, we propose a semi-autoregressive (SAR) decoding approach to integrate the advantages of AR and NAR decoding. Our experiments across multiple KWS datasets demonstrate that MSD training effectively alleviates overfitting. The SAR decoding method preserves the superior performance of AR decoding while benefits from the overfitting suppression of NAR decoding, achieving excellent results.

cs.SD↗

arXiv2025

A New Approach to Inspect Weakly Coupled Logistic Systems and their Asymptotic Behavior

We consider the weakly coupled elliptic system of logistic type, \begin{equation}\label{LS} \begin{cases} -Δu &=λ_1 u- |u|^{p-2}u+ β|u|^{\frac{p}{2}-2}u |v|{^{\frac{p}{2}-1}}v\mbox{ in }Ω, -Δv & =λ_2 v- |v|^{p-2}v+β|u|^{\frac{p}{2}-1}u|v|^{\frac{p}{2}-2}v \mbox{ in }Ω, \ \ u,v &\in H_0^1(Ω), \end{cases} \tag{$LS$} \end{equation} where $Ω\subset\mathbb{R}^N$ is a bounded domain with $N\geq 2$, $2< p < 2^*$, and $λ_1(Ω)< λ_1 \leq λ_2$. We say the system is competitive if $β<0$ and cooperative if $β>0$, for $β\in \mathbb{R}$. We prove the existence and multiplicity of solutions to the problem \eqref{LS} in alternative variational frameworks, depending on the range of the parameter $β.$ We do not rely on bifurcation or degree theory, which have been used in the literature for logistic-type problems. Instead, the novelty is to obtain min-max type solutions by exploiting the different geometry of the functional associated with the logistic problem. In case $N\geq 2$ and suitable values of $p$, we extend the existence results, for all $β$ in the whole line, and possibly for the classical case $N=3$ and $p=4$. Furthermore, we analyze the asymptotic behavior of such solutions as $β\to 0$ or $β\to \pm \infty.$} \bigskip \newline \textsc{Key words: Logistic System, Ground State Solution, Linking structure, seminodal Solution.}{\small}

math.AP↗

arXiv2025

Neural Contraction Metrics with Formal Guarantees for Discrete-Time Nonlinear Dynamical Systems

Contraction metrics are crucial in control theory because they provide a powerful framework for analyzing stability, robustness, and convergence of various dynamical systems. However, identifying these metrics for complex nonlinear systems remains an open challenge due to the lack of scalable and effective tools. This paper explores the approach of learning verifiable contraction metrics parametrized as neural networks (NNs) for discrete-time nonlinear dynamical systems. While prior works on formal verification of contraction metrics for general nonlinear systems have focused on convex optimization methods (e.g. linear matrix inequalities, etc) under the assumption of continuously differentiable dynamics, the growing prevalence of NN-based controllers, often utilizing ReLU activations, introduces challenges due to the non-smooth nature of the resulting closed-loop dynamics. To bridge this gap, we establish a new sufficient condition for establishing formal neural contraction metrics for general discrete-time nonlinear systems assuming only the continuity of the dynamics. We show that from a computational perspective, our sufficient condition can be efficiently verified using the state-of-the-art neural network verifier $α,\!β$-CROWN, which scales up non-convex neural network verification via novel integration of symbolic linear bound propagation and branch-and-bound. Built upon our analysis tool, we further develop a learning method for synthesizing neural contraction metrics from sampled data. Finally, our approach is validated through the successful synthesis and verification of NN contraction metrics for various nonlinear examples.

math.OC↗