arXiv subjects

Yuwei Liu

Publications and source records attributed to Yuwei Liu.

13 recordsLinked to original sources

arXiv2026

KaPilot: LLM-Assisted Generation of Kani Specifications for Unsafe Rust Verification

Rust's ownership and type system provide strong memory safety guarantees, but unsafe code still presents memory safety risks. Formal verification is crucial for ensuring memory safety, but writing precise specifications for unsafe Rust is challenging and largely manual. Large language models (LLMs) have shown promise in generating formal specifications but are often code-centric, prone to inheriting implementation flaws, and lack systematic quality assessment. In this paper, we present KaPilot, a multi-agent framework for automatically generating specifications to verify unsafe Rust memory safety using Kani. The process begins with lightweight program analysis and proof harness generation. The SafetyReq agent extracts a concise, refined list of safety requirements from the target Rust function's documentation, which guides the SpecGenerate agent in producing initial specifications that specify memory safety concerns. Then, the specifications are iteratively refined through a generate-precheck-verify loop involving SpecGenerate, SpecPrecheck, and SpecVerify agents, which assess quality and feed errors back. By executing this loop multiple times, KaPilot generates a set of candidate specifications. Finally, the shuffle-and-implication strategy is applied to systematically determine the best specification from these candidates. We evaluated KaPilot on 54 unsafe Rust functions with ground truth and 70 without. KaPilot achieved 88.9% and 71.4% specification generation success, respectively, with 57.4% of generated specifications equivalent to or stronger than the ground truth. Compared with AutoSpec, KaPilot produces 14.8% more verifiable specifications and 25.9% more equivalent-or-better specifications.

cs.SE↗

arXiv2026

HarnessLLM: Rust Verification Harness Generation with Large Language Models

Rust's ownership model and type system offer strong memory safety guarantees, but unsafe code and runtime panics still present significant risks. Formal verification is essential to ensure memory safety, but developing verification harnesses remains a challenging and manual task. Although large language models (LLMs) have shown strong performance in various code analysis tasks, directly applying them to harness generation often results in inaccurate API invocations, inefficient nondeterministic data generation, and fabricated fixes. In this paper, we present HarnessLLM, an automated workflow that leverages LLMs to generate verification harnesses for Rust code directly from existing test suites. HarnessLLM automatically extracts calling scenarios from test cases, generates nondeterministic arguments based on dependency analysis, and incrementally synthesizes harnesses. It then iteratively refines the harnesses, preserving critical code regions and reporting fabricated types or functions to LLMs for correction. In our evaluation on 9 real-world Rust codebases, HarnessLLM extracted 294 calling scenarios from 494 test cases with 94.66% precision and generated harnesses for all scenarios in an average of 145 seconds each. It outperformed the existing approach, Autoharness, which succeeded on only 41% of those scenarios. Finally, 6 real-world memory safety bugs were detected using the generated harnesses, demonstrating the practical utility of our approach in verification. To our knowledge, this is the first work to use LLMs for generating harnesses aimed at memory safety verification in real-world Rust projects.

cs.SE↗

arXiv2026

KVerus: Scalable and Resilient Formal Verification Proof Generation for Rust Code

Formal verification provides the highest assurance of software correctness and security, but its application to large-scale, evolving systems remains a major challenge. While large language models (LLMs) have shown promise in automating proof generation, they often fail in real-world settings due to their inability to handle complex cross-module dependencies or changes in the codebase or the verification toolchain. We identify the fundamental problem as the Semantic-Structural Gap: LLMs operate on semantic code patterns, whereas formal verification is governed by rigid structural dependencies, a disconnect that leads to brittle, unsustainable proofs. To bridge this gap, we propose a new paradigm of self-adaptive verification and present KVerus, a retrieval-augmented system for Verus-based Rust verification that can adapt to an evolving software environment. KVerus constructs a dynamic knowledge base of code metadata, lemma semantics, and toolchain specifics. By combining dependency-aware program analysis, semantic lemma indexing, and error-driven self-refinement, it can navigate intricate cross-file dependencies to synthesize proofs and automatically repair proofs when faced with common evolutionary changes. Across three single-file benchmarks, KVerus verifies 80.2% of tasks, outperforming the state-of-the-art AutoVerus (56.9%) and degrades less than AutoVerus under breaking Verus updates. On three repository-level benchmarks with cross-file dependencies, KVerus achieves a 51.0% success rate, compared to 4.5% for a multi-round prompting baseline. Finally, on the Asterinas Rust OS kernel, KVerus produces upstream-accepted proofs that verify 23 previously unverified functions (21.0% of proof code) in the memory-management module. KVerus represents a significant step towards making formal verification a scalable and sustainable practice for modern, security-critical software.

cs.SE↗

arXiv2026

Pressure-Induced Superconducting-like Transition in the $\it d$-wave Altermagnet Candidate CsV$_2$Se$_2$O

Altermagnetism generates exchange-type spin splitting without net magnetization and, in its $\it d$-wave form, resembles the angular symmetry of unconventional $\it d$-wave superconductivity. Whether this correspondence bears directly on superconducting instabilities in real correlated materials remains open. Here we study the quasi-two-dimensional vanadium oxychalcogenide CsV$_2$Se$_2$O (CVSO), a square-net $\it d$-wave altermagnet candidate, through combined experimental and theoretical investigation of its lattice structure, electronic structure and transport properties. At ambient pressure, CVSO is a weakly insulating parent state with a density-wave-like anomaly near 100 K, and its bulk properties are most consistent with a G-type compensated antiferromagnetic background. Under compression, the density-wave-like feature is suppressed, the magnetoresistance evolves from predominantly negative to positive, and a superconducting-like resistive downturn emerges below about 3 K. This low-temperature anomaly is reproducible across samples and pressure media, and is suppressed by magnetic field. Room-temperature X-ray diffraction reveals no symmetry lowering, whereas does show a pronounced compressibility anomaly over the same pressure range. CVSO thus reveals a pressure-tuned phase diagram in which a reconstructed weakly insulating parent state gives way to strange-metal-like transport and superconducting-like behavior, echoing broader phenomenology associated with unconventional superconductors, including cuprates and nickelates.

cond-mat.supr-con↗

arXiv2026

Deception by Design: A Temporal Dark Patterns Audit of McDonald's Self-Ordering Kiosk Flow

Self-ordering kiosks (SOKs) are widely deployed in fast food restaurants, transforming food ordering into digitally mediated, self-navigated interactions. While these systems enhance efficiency and average order value, they also create opportunities for manipulative interface design practices known as dark patterns. This paper presents a structured audit of the McDonald's self-ordering kiosk in Germany using the Temporal Analysis of Dark Patterns (TADP) framework. Through a scenario-based walkthrough simulating a time-pressured user, we reconstructed and analyzed 12 interface steps across intra-page, inter-page, and system levels. We identify recurring high-level strategies implemented through meso-level patterns such as adding steps, false hierarchy, bad defaults, hiding information, and pressured selling, and low-level patterns including visual prominence, confirmshaming, scarcity framing, feedforward ambiguity, emotional sensory manipulation, and partitioned pricing. Our findings demonstrate how these patterns accumulate across the interaction flow and may be amplified by the kiosk's linear task structure and physical context. These findings suggest that hybrid physical--digital consumer interfaces warrant closer scrutiny within emerging regulatory discussions on dark patterns.

cs.HC↗

arXiv2025

Muscle Synergy Patterns During Running: Coordinative Mechanisms From a Neuromechanical Perspective

Running is a fundamental form of human locomotion and a key task for evaluating neuromuscular control and lower-limb coordination. In recent years, muscle synergy analysis based on surface electromyography (sEMG) has become an important approach in this area. This review focuses on muscle synergies during running, outlining core neural control theories and biomechanical optimization hypotheses, summarizing commonly used decomposition methods (e.g., PCA, ICA, FA, NMF) and emerging autoencoder-based approaches. We synthesize findings on the development and evolution of running-related synergies across the lifespan, examine how running surface, speed, foot-strike pattern, fatigue, and performance level modulate synergy patterns, and describe characteristic alterations in populations with knee osteoarthritis, patellofemoral pain, and stroke. Current evidence suggests that the number and basic structure of lower-limb synergies during running are relatively stable, whereas spatial muscle weightings and motor primitives are highly plastic and sensitive to task demands, fatigue, and pathology. However, substantial methodological variability remains in EMG channel selection, preprocessing pipelines, and decomposition algorithms, and direct neurophysiological validation and translational application are still limited. Future work should prioritize standardized processing protocols, integration of multi-source neuromusculoskeletal data, nonlinear modeling, and longitudinal intervention studies to better exploit muscle synergy analysis in sports biomechanics, athletic training, and rehabilitation medicine.

q-bio.QM↗

arXiv2025

Spatial Policy: Guiding Visuomotor Robotic Manipulation with Spatial-Aware Modeling and Reasoning

Vision-centric hierarchical embodied models have demonstrated strong potential. However, existing methods lack spatial awareness capabilities, limiting their effectiveness in bridging visual plans to actionable control in complex environments. To address this problem, we propose Spatial Policy (SP), a unified spatial-aware visuomotor robotic manipulation framework via explicit spatial modeling and reasoning. Specifically, we first design a spatial-conditioned embodied video generation module to model spatially guided predictions through the spatial plan table. Then, we propose a flow-based action prediction module to infer executable actions with coordination. Finally, we propose a spatial reasoning feedback policy to refine the spatial plan table via dual-stage replanning. Extensive experiments show that SP substantially outperforms state-of-the-art baselines, achieving over 33% improvement on Meta-World and over 25% improvement on iTHOR, demonstrating strong effectiveness across 23 embodied control tasks. We additionally evaluate SP in real-world robotic experiments to verify its practical viability. SP enhances the practicality of embodied models for robotic control applications. Code and checkpoints are maintained at https://plantpotatoonmoon.github.io/SpatialPolicy/.

cs.RO↗

arXiv2024

Low-Rank Adaptation of Time Series Foundational Models for Out-of-Domain Modality Forecasting

Low-Rank Adaptation (LoRA) is a widely used technique for fine-tuning large pre-trained or foundational models across different modalities and tasks. However, its application to time series data, particularly within foundational models, remains underexplored. This paper examines the impact of LoRA on contemporary time series foundational models: Lag-Llama, MOIRAI, and Chronos. We demonstrate LoRA's fine-tuning potential for forecasting the vital signs of sepsis patients in intensive care units (ICUs), emphasizing the models' adaptability to previously unseen, out-of-domain modalities. Integrating LoRA aims to enhance forecasting performance while reducing inefficiencies associated with fine-tuning large models on limited domain-specific data. Our experiments show that LoRA fine-tuning of time series foundational models significantly improves forecasting, achieving results comparable to state-of-the-art models trained from scratch on similar modalities. We conduct comprehensive ablation studies to demonstrate the trade-offs between the number of tunable parameters and forecasting performance and assess the impact of varying LoRA matrix ranks on model performance.

cs.LG↗

arXiv2024

Interpretable Vital Sign Forecasting with Model Agnostic Attention Maps

Sepsis is a leading cause of mortality in intensive care units (ICUs), representing a substantial medical challenge. The complexity of analyzing diverse vital signs to predict sepsis further aggravates this issue. While deep learning techniques have been advanced for early sepsis prediction, their 'black-box' nature obscures the internal logic, impairing interpretability in critical settings like ICUs. This paper introduces a framework that combines a deep learning model with an attention mechanism that highlights the critical time steps in the forecasting process, thus improving model interpretability and supporting clinical decision-making. We show that the attention mechanism could be adapted to various black box time series forecasting models such as N-HiTS and N-BEATS. Our method preserves the accuracy of conventional deep learning models while enhancing interpretability through attention-weight-generated heatmaps. We evaluated our model on the eICU-CRD dataset, focusing on forecasting vital signs for sepsis patients. We assessed its performance using mean squared error (MSE) and dynamic time warping (DTW) metrics. We explored the attention maps of N-HiTS and N-BEATS, examining the differences in their performance and identifying crucial factors influencing vital sign forecasting.

cs.LG↗

arXiv2024

Improved Lower Bounds for Approximating Parameterized Nearest Codeword and Related Problems under ETH

In this paper we present a new gap-creating randomized self-reduction for parameterized Maximum Likelihood Decoding problem over $\mathbb{F}_p$ ($k$-MLD$_p$). The reduction takes a $k$-MLD$_p$ instance with $k\cdot n$ vectors as input, runs in time $f(k)n^{O(1)}$ for some computable function $f$, outputs a $(3/2-\varepsilon)$-Gap-$k'$-MLD$_p$ instance for any $\varepsilon>0$, where $k'=O(k^2\log k)$. Using this reduction, we show that assuming the randomized Exponential Time Hypothesis (ETH), no algorithms can approximate $k$-MLD$_p$ (and therefore its dual problem $k$-NCP$_p$) within factor $(3/2-\varepsilon)$ in $f(k)\cdot n^{o(\sqrt{k/\log k})}$ time for any $\varepsilon>0$. We then use reduction by Bhattacharyya, Ghoshal, Karthik and Manurangsi (ICALP 2018) to amplify the $(3/2-\varepsilon)$-gap to any constant. As a result, we show that assuming ETH, no algorithms can approximate $k$-NCP$_p$ and $k$-MDP$_p$ within $\gamma$-factor in $f(k)n^{o(k^{\varepsilon_\gamma})}$ time for some constant $\varepsilon_\gamma>0$. Combining with the gap-preserving reduction by Bennett, Cheraghchi, Guruswami and Ribeiro (STOC 2023), we also obtain similar lower bounds for $k$-MDP$_p$, $k$-CVP$_p$ and $k$-SVP$_p$. These results improve upon the previous $f(k)n^{\Omega(\mathsf{poly} \log k)}$ lower bounds for these problems under ETH using reductions by Bhattacharyya et al. (J.ACM 2021) and Bennett et al. (STOC 2023).

cs.CC↗

arXiv2023

Vital Sign Forecasting for Sepsis Patients in ICUs

Sepsis and septic shock are a critical medical condition affecting millions globally, with a substantial mortality rate. This paper uses state-of-the-art deep learning (DL) architectures to introduce a multi-step forecasting system to predict vital signs indicative of septic shock progression in Intensive Care Units (ICUs). Our approach utilizes a short window of historical vital sign data to forecast future physiological conditions. We introduce a DL-based vital sign forecasting system that predicts up to 3 hours of future vital signs from 6 hours of past data. We further adopt the DILATE loss function to capture better the shape and temporal dynamics of vital signs, which are critical for clinical decision-making. We compare three DL models, N-BEATS, N-HiTS, and Temporal Fusion Transformer (TFT), using the publicly available eICU Collaborative Research Database (eICU-CRD), highlighting their forecasting capabilities in a critical care setting. We evaluate the performance of our models using mean squared error (MSE) and dynamic time warping (DTW) metrics. Our findings show that while TFT excels in capturing overall trends, N-HiTS is superior in retaining short-term fluctuations within a predefined range. This paper demonstrates the potential of deep learning in transforming the monitoring systems in ICUs, potentially leading to significant improvements in patient care and outcomes by accurately forecasting vital signs to assist healthcare providers in detecting early signs of physiological instability and anticipating septic shock.

cs.LG↗

arXiv2023

Revealing unusual bandgap shifts with temperature and bandgap renormalization effect in phase-stabilized metal halide perovskite thin films

Hybrid organic-inorganic metal halide perovskites are emerging materials in photovoltaics, whose bandgap is one of the most crucial parameters governing their light harvesting performance. Here we present the temperature and photocarrier density dependence of the bandgap in two phase-stabilized perovskite thin films (MA0.3FA0.7PbI3 and MA0.3FA0.7Pb0.5Sn0.5I3) using photoluminescence and absorption spectroscopy. Contrasting bandgap shifts with temperature are observed between the two perovskites. Using X-ray diffraction and in situ high-pressure photoluminescence spectroscopy, we show that thermal expansion plays only a minor role in the large bandgap blueshift, which is attributed to the enhanced structural stability of our samples. Our first-principles calculations further demonstrate the significant impact of thermally induced lattice distortions on the bandgap widening. We propose that the anomalous trends are caused by the competition between static and dynamic distortions. Additionally, both the bandgap renormalization and band filling effects are directly observed for the first time in fluence-dependent photoluminescence measurements and are employed to estimate the exciton effective mass. Our results provide new insights into the basic understanding of thermal and charge-accumulation effects on the band structure of hybrid perovskite thin films.

cond-mat.mtrl-sci↗

arXiv2023

Antiferromagnetic $\alpha$-MnTe: Molten-Salt-Assisted Chemical Vapor Deposition Growth and Magneto-Transport Properties

Antiferromagnetic (AF) materials are attracting increasing interest of research in magnetic physics and spintronics. Here, we report controllable synthesis of room-temperature AF $\alpha$-MnTe nanocrystals (N\'eel temperature ~ 307 K) via molten-salt-assisted chemical vapor deposition method. The growth kinetics are investigated regarding the dependence of flake dimension and macroscopic shape on growth time and temperature. The high crystalline quality and atomic structure are confirmed by various crystallographic characterization means. Cryogenic magneto-transport measurements reveal anisotropic magnetoresistance (MR) response and a complicated dependence of MR on temperature, owing to the subtle competition among multiple scattering mechanisms of thermally excited magnetic disorders (magnon drag), magnetic transition and thermally populated lattice phonons. Overall positive MR behavior with twice transitions in magnitude is observed when out-of-plane external magnetic field ($B$) is applied, while a transition from negative to positive MR response is recorded when in-plane $B$ is applied. The rich magnetic transport properties render $\alpha$-MnTe a promising material for exploiting functional components in magnetic devices.

cond-mat.mtrl-sci↗