arXiv subjects

Shan Lu

Publications and source records attributed to Shan Lu.

At least 19 recordsLinked to original sources

arXiv2026

Propagating construction-time knowledge quality into medical question answering: A framework grounded in clinical guidelines

Large language models have facilitated knowledge graph (KG) construction from clinical guidelines, but extracted triples vary in structural validity and evidential support. Meanwhile, graph-augmented question answering (QA) systems typically optimize query relevance during retrieval, with limited reuse of quality information produced during KG construction. This creates a disconnect between construction-time quality control and inference-time evidence use. We investigate whether construction-time triple quality can serve as a persistent signal for downstream evidence selection and presentation. We propose a quality-aware framework that models structural conformance (SchemaConf) and evidential support (EvidScore) as complementary dimensions and fuses them into a per-triple quality signal, Q(t). Rather than using quality solely for filtering, the framework retains Q(t) and derived quality tiers as graph attributes and propagates them into quality-weighted subgraph retrieval and tier-conditioned evidence prompting, while preserving passage-level provenance. Experiments on Chinese diabetes clinical guidelines show that the utility of the quality signal is distribution dependent. Under cross-version and cross-model shift, the fused Q(t) provides stronger triple-quality discrimination than either component alone (AUC 0.748 vs. 0.703 for EvidScore and 0.645 for SchemaConf). In guideline-grounded QA, propagating construction-time quality reduces required-knowledge omission from 16.3% to 5.3% and conflicting outputs from 16.3% to 2.7%, with an evidence-grounded precision of 81.6% and near-zero invalid citations. Blinded clinician ratings favor the full framework over no retrieval (4.68 vs. 4.21 on a five-point scale) and approach the oracle condition (4.80), while cross-generator experiments show consistent trends.

cs.AI↗

arXiv2026

Layered construction of Message-Wise Unequal Error Protection Codes

Conventional communication systems are mainly designed to reduce error rates and increase transmission rates, and therefore usually provide uniform protection to all transmitted messages. However, in intent-oriented applications, different messages may have different semantic meanings and importance levels, requiring different levels of reliability. This paper proposes a layered construction of message-level unequal error protection (UEP) codes for short-blocklength communication. Instead of appending an explicit protection tag to each codeword, the proposed method embeds the protection structure directly into the Hamming-distance structure of the codebook. By assigning larger minimum intra-level distances to higher-importance message groups and imposing suitable inter-level distance constraints, the proposed codebook provides differentiated error-correction capabilities while enabling reliable importance-level classification at the receiver. Theoretical conditions for correct group classification are derived, and simulations over AWGN and VLC-ISI channels show that the proposed scheme improves BER performance and group classification accuracy compared with a tag-based ECC baseline.

cs.IT↗

arXiv2026

Feasibility Study of VLC-Based Collective Perception for Vehicular Communication

This study explores the use of Visible Light Communication (VLC) in Collective Perception (CP), a technology that enables vehicles and infrastructure to share sensor information to help reduce traffic accidents. Recent advances in Vehicle-to-Everything (V2X) communication have spurred growing research interest in CP. However, in regions such as the United States and Japan, only 30 MHz of radio spectrum is allocated for V2X, which is insufficient to effectively support CP. In this paper, we propose integrating VLC into V2X systems to enhance CP, complementing the existing 5.9 GHz band for V2X communications. VLC can coexist with wireless systems that use radio waves, providing an additional optical channel for data exchange. To the best of the authors' knowledge, this is the first study to investigate VLC for CP. We evaluate the feasibility of VLC-based CP through three experiments. First, we measured the application-level delay of a VLC-based CP system in a stationary indoor environment. Next, we evaluated its communication range in a stationary outdoor setting. Finally, to assess robustness under realistic conditions, we conducted driving experiments at vehicle speeds up to 90 km/h. The results demonstrate that VLC-based CP is feasible and could serve as a promising solution to spectrum scarcity in the 5.9 GHz band for future V2X communications.

eess.SP↗

arXiv2026

Deep-Learning-Aided Successive Cancellation List Flip Decoding for Polar Codes

Polar codes are the first error-correcting code proven to achieve channel capacity based on infinite code length. The Successive Cancellation List Flip (SCLF) decoding algorithm was proposed by flipping an erroneous bit during the next decoding attempt. To identify the erroneous bits, the Log-Likelihood Ratio (LLR) is used to indicate the reliability of each decision bit. To improve the accuracy of the erroneous bit prediction, we propose deep-learning-aided (DL-aided) SCLF decoding algorithms. We first offer a stacked LSTM network that contains new features to train our models, which are able to improve the accuracy of the prediction of positions of erroneous bits. Then we separately train the stacked LSTM models to predict the position of both the first and second erroneous bits and whether to continue flipping. As a result, the DL-aided SCLF decoding algorithms based on the proposed stacked LSTM \mbox{flip-1} model, stacked LSTM \mbox{flip-2} model, and the stacked LSTM \mbox{continue-flipping} check (CFC) model are able to provide a better performance at a lower number of average decoding attempts when compared to other state-of-the-art decoding algorithms.

eess.SP↗

arXiv2026

Channel Modeling and LED Spot Detection for Dense Image-Sensor Visible Light Communication

High-density LED arrays enable high-speed transmission in image-sensor-based visible-light communication (VLC) systems. However, when optical spots become blurred and spatially overlapped due to focal shift, resolution limitations, or interference, severe inter-symbol interference (ISI) occurs, significantly degrading decoding performance. Furthermore, radial distortion introduces geometric deformation of the LED grid, while vignetting leads to incomplete and asymmetric spot shapes at the periphery, both of which further hinder reliable signal detection. Existing methods mitigate ISI by reducing LED transmission signaling density. This paper proposes a robust decoding framework that maintains full LED signaling density. We introduce a pilot-aided geometric recognition method that uses a PSF-constrained Hough transform and circle-center alignment refinement. \textbf{In addition, radial distortion correction and vignetting-aware compensation are incorporated to restore geometric consistency and suppress edge-related detection errors.} By leveraging prior structural knowledge from pilot frames, the system effectively separates overlapping LED signals under severe optical distortion. Experimental results on a real-world VLC testbed confirm that the proposed method achieves superior decoding accuracy and throughput compared to conventional Hough-based and low-density baseline methods. The results highlight its potential for high-efficiency VLC applications in interference-prone environments.

cs.IT↗

arXiv2026

VeriCache: Turning Lossy KV Cache into Lossless LLM Inference

The large size of the KV cache has become a major bottleneck for serving LLMs with increasing context lengths. In response, many KV cache compression methods, such as token dropping and quantization, have been proposed. However, almost all of these methods are inherently lossy-despite minimal accuracy degradation for short outputs, their outputs increasingly diverge from full-KV-cache outputs as more tokens are decoded, which leads to catastrophic failures in code generation and tool calling. We present VeriCache, the first inference framework that ensures the same output as full-KV-cache decoding but largely preserves the high decoding throughput of a range of KV cache compression algorithms. VeriCache uses the compressed KV cache to draft tokens, then verifies them against the full KV cache. While it may seem like just speculative decoding, VeriCache requires addressing a key system challenge to work-keeping the full KV cache out of GPU memory and minimizing the overhead of swapping it in for verification. The insight is two-fold: (1) compressed-KV decoding can be parallelized with full-KV swap, because one is HBM-bandwidth-bound and the other is PCIe/network-bound, and (2) the compressed KV cache often produces output similar to the full KV cache, allowing a long drafting horizon to amortize each full-KV swap. VeriCache applies to both long-context decoding and remote prefix caching, supports a broad family of token-dropping and quantization methods through a uniform compressor interface, and composes with traditional speculative decoding. Experimental results show that VeriCache achieves up to 4X higher throughput than full-KV inference while producing identical outputs.

cs.AR↗

arXiv2026

ISI Modeling and BER Performance for Rotating Light-Trail Image Sensor Communication

Image sensor communication (ISC) employing a propeller-LED transmitter encodes data along rotating light trails. We present an analytical framework that (i) constructs a single-LED, single-blink light trail model that maps optical power to pixel values, and (ii) integrates a probabilistic noise model to derive a closed-form bit-error rate (BER) using the $Q$-function. Trimodal pixel-value histograms motivate an adjacent-only inter-symbol interference (ISI) model in which the decision at segment $j$ depends on adjacent segments. Applying a hardest-pair midpoint threshold yields per-segment BER and a general BER after marginalization. We further provide practical sufficiency conditions under which adjacent-only ISI is adequate, and validate its tightness against Monte Carlo simulations and experimental results. Using the analytical BER, we select the control angle that maximizes throughput while satisfying a target BER reliability constraint.

cs.IT↗

arXiv2026

Real-world Latency Analysis of Vehicular Visible Light Communication with Multiple LED Transmitters and an Event-Based Camera

Event cameras offer high temporal resolution, low latency, and wide dynamic range, making them promising receivers for visible light communication (VLC) in vehicle-to-everything (V2X) applications. This work presents an event-camera-based VLC system addressing three key challenges: bandwidth saturation, multi-transmitter reception, and latency characterization. We adopt a positive-event-only mode and design a protocol that suppresses event generation while maintaining communication distance and a wide field of view. We also propose a method to identify multiple transmitters and demonstrate simultaneous reception from up to three LEDs. Finally, we evaluate end-to-end latency in real vehicular scenarios and show that the system meets cooperative perception requirements. These results demonstrate that event-camera-based VLC is a feasible complement to existing V2X technologies (e.g., RF).

cs.RO↗

arXiv2026

Nanvix: A Multikernel OS Design for High-Density Serverless Deployments

Serverless providers strive for high resource utilization by optimizing deployment density: how many applications can be deployed per host server. However, achieving high deployment density without compromising application performance or isolation remains an open challenge. High density can be achieved by sharing components across applications, yet applications from different tenants must be strongly isolated from each other due to the risk of side-channel attacks. Sharing components across applications from the same tenant, if done naively, can introduce contention on host resources thus negatively affecting application performance. We describe Nanvix, a new multikernel OS that disaggregates ephemeral execution state, unique per application invocation, from long-lived persistent state, shared among invocations from the same tenant. Applications in Nanvix execute inside a lightweight user VM running a micro-kernel that implements threads and memory, and forwards all I/O requests to a system VM. The system VM runs a macro-kernel with a rich set of device drivers and is shared among all invocations from the same tenant. Nanvix' split design achieves strong hypervisor isolation across tenants without sacrificing application performance, and reduces same-tenant contention by multiplexing all I/O requests to the system VM. Thanks to a system-wide co-design, Nanvix achieves order-of-magnitude lower application start up times with moderate I/O overheads. When replaying a production trace, Nanvix needs 20-100x fewer host servers compared to state-of-the-art systems, improving deployment density

cs.OS↗

arXiv2026

ExVerus: Verus Proof Repair via Counterexample Reasoning

Large Language Models (LLMs) have shown promising results in automating formal verification. However, existing approaches treat proof generation as a static, end-to-end prediction over source code, relying on limited verifier feedback and lacking access to concrete program behaviors. We present EXVERUS, a counterexample-guided framework that enables LLMs to reason about proofs using behavioral feedback via counterexamples. When a proof fails, EXVERUS automatically generates and validates counterexamples, and then guides the LLM to generalize them into inductive invariants to block these failures. Our evaluation shows that EXVERUS significantly improves proof accuracy, robustness, and token efficiency over the state-of-the-art prompting-based Verus proof generator.

cs.PL↗

arXiv2026

Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set

Large Language Models (LLMs) are widely used for code generation. However, the correctness of code generated by LLMs remains a concern. A potential remedy to this concern is to have LLMs generate formal correctness proofs along with such code. However, compared with code generation, code-proof generation requires much higher reasoning capability and has much less existing data to learn from. In this paper, we present VeruSyn, a data synthesis pipeline for Verus, a state-of-the-art verification tool for system software written in Rust. Through self-synthesis and tutorial-based synthesis, VeruSyn achieves much larger scale and Verus-feature coverage than previous data-synthesis techniques designed for Verus; VeruSyn also supplements its dataset with long-chain-of-thought (CoT) data through agent trajectory synthesis. With VeruSyn, we synthesize the largest set of Verus verified programs: 6.9 million Rust programs, each with a formal specification and a proof that it meets that specification. This dataset lets us create a fine-tuned Qwen2.5-Coder-32B-Instruct model with appealing cost-proof tradeoff compared with state-of-the-art commercial models like Claude Sonnet 4.5. It also significantly outperforms models like o4-mini and previously proposed research models.

cs.SE↗

arXiv2025

VeruSAGE: A Study of Agent-Based Verification for Rust Systems

Large language models (LLMs) have shown impressive capability to understand and develop code. However, their capability to rigorously reason about and prove code correctness remains in question. This paper offers a comprehensive study of LLMs' capability to develop correctness proofs for system software written in Rust. We curate a new system-verification benchmark suite, VeruSAGE-Bench, which consists of 849 proof tasks extracted from eight open-source Verus-verified Rust systems. Furthermore, we design different agent systems to match the strengths and weaknesses of different LLMs (o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5). Our study shows that different tools and agent settings are needed to stimulate the system-verification capability of different types of LLMs. The best LLM-agent combination in our study completes over 80% of system-verification tasks in VeruSAGE-Bench. It also completes over 90% of a set of system proof tasks not part of VeruSAGE-Bench because they had not yet been finished by human experts. This result shows the great potential for LLM-assisted development of verified system software.

cs.OS↗

arXiv2025

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.

cs.SE↗

arXiv2025

Performance Evaluation of an Integrated System for Visible Light Communication and Positioning Using an Event Camera

Event cameras, featuring high temporal resolution and high dynamic range, offer visual sensing capabilities comparable to conventional image sensors while capturing fast-moving objects and handling scenes with extreme lighting contrasts such as tunnel exits. Leveraging these properties, this study proposes a novel self-localization system that integrates visible light communication (VLC) and visible light positioning (VLP) within a single event camera. The system enables a vehicle to estimate its position even in GPS-denied environments, such as tunnels, by using VLC to obtain coordinate information from LED transmitters and VLP to estimate the distance to each transmitter. Multiple LEDs are installed on the transmitter side, each assigned a unique pilot sequence based on Walsh-Hadamard codes. The event camera identifies individual LEDs within its field of view by correlating the received signal with these codes, allowing clear separation and recognition of each light source. This mechanism enables simultaneous high-capacity MISO (multi-input single-output) communication through VLC and precise distance estimation via phase-only correlation (POC) between multiple LED pairs. To the best of our knowledge, this is the first vehicle-mounted system to achieve simultaneous VLC and VLP functionalities using a single event camera. Field experiments were conducted by mounting the system on a vehicle traveling at 30 km/h (8.3 m/s). The results demonstrated robust real-world performance, with a root mean square error (RMSE) of distance estimation within 0.75 m for ranges up to 100 m and a bit error rate (BER) below 0.01 across the same range.

cs.RO↗

arXiv2025

What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus

Proof-oriented programming languages (POPLs) empower developers to write code alongside formal correctness proofs, providing formal guarantees that the code adheres to specified requirements. Despite their powerful capabilities, POPLs present a steep learning curve and have not yet been adopted by the broader software community. The lack of understanding about the proof-development process and how expert proof developers interact with POPLs has hindered the advancement of effective proof engineering and the development of proof-synthesis models/tools. In this work, we conduct a user study, involving the collection and analysis of fine-grained source code telemetry from eight experts working with two languages, F* and Verus. Results reveal interesting trends and patterns about how experts reason about proofs and key challenges encountered during the proof development process. We identify three distinct strategies and multiple informal practices that are not captured final code snapshots, yet are predictive of task outcomes. We translate these findings into concrete design guidance for AI proof assistants: bias toward early specification drafting, explicit sub-goal decomposition, bounded active errors, and disciplined verifier interaction. We also present a case study of an F* proof agent grounded in these recommendations, and demonstrate improved performance over baseline LLMs

cs.SE↗

arXiv2025

The Role of Excitatory Parvalbumin-positive Neurons in the Tectofugal Pathway of Pigeon (Columba livia) Hierarchical Visual Processing

The visual systems of birds and mammals exhibit remarkable organizational similarities: the dorsal ventricular ridge (DVR) demonstrates a columnar microcircuitry that parallels the cortical architecture observed in mammals. However, the specific neuronal subtypes involved and their functional roles in pigeon hierarchical visual processing remain unclear. This study investigates the role of excitatory parvalbumin (PV+) neurons within the Ento-MVL (entoallium-mesopallium venterolaterale) circuit of pigeons underlying hierarchical moving target recognition. Electrophysiological recordings and immunofluorescence staining reveal that excitatory PV+ neurons originating from the entopallial internal (Ei) predominantly modulate MVL responses to varying visual stimuli. Using a heterochronous-speed recurrent neural network (HS-RNN) model, we further validated these dynamics, replicating the rapid adaptation of the Ento-MVL circuit to moving visual targets. The findings suggest that the fast-spiking and excitatory properties of PV+ neurons enable rapid processing of motion-related information within the Ento-MVL circuit. Our results elucidate the functional role of excitatory PV+ neurons in hierarchical information processing under the columnar organization of the visual DVR and underscore the convergent neural processing strategies shared by avian and mammalian visual systems.

q-bio.NC↗

arXiv2025

Distance Estimation in Outdoor Driving Environments Using Phase-only Correlation Method with Event Cameras

With the growing adoption of autonomous driving, the advancement of sensor technology is crucial for ensuring safety and reliable operation. Sensor fusion techniques that combine multiple sensors such as LiDAR, radar, and cameras have proven effective, but the integration of multiple devices increases both hardware complexity and cost. Therefore, developing a single sensor capable of performing multiple roles is highly desirable for cost-efficient and scalable autonomous driving systems. Event cameras have emerged as a promising solution due to their unique characteristics, including high dynamic range, low latency, and high temporal resolution. These features enable them to perform well in challenging lighting conditions, such as low-light or backlit environments. Moreover, their ability to detect fine-grained motion events makes them suitable for applications like pedestrian detection and vehicle-to-infrastructure communication via visible light. In this study, we present a method for distance estimation using a monocular event camera and a roadside LED bar. By applying a phase-only correlation technique to the event data, we achieve sub-pixel precision in detecting the spatial shift between two light sources. This enables accurate triangulation-based distance estimation without requiring stereo vision. Field experiments conducted in outdoor driving scenarios demonstrated that the proposed approach achieves over 90% success rate with less than 0.5-meter error for distances ranging from 20 to 60 meters. Future work includes extending this method to full position estimation by leveraging infrastructure such as smart poles equipped with LEDs, enabling event-camera-based vehicles to determine their own position in real time. This advancement could significantly enhance navigation accuracy, route optimization, and integration into intelligent transportation systems.

eess.IV↗

arXiv2025

Evaluation of Mobile Environment for Vehicular Visible Light Communication Using Multiple LEDs and Event Cameras

In the fields of Advanced Driver Assistance Systems (ADAS) and Autonomous Driving (AD), sensors that serve as the ``eyes'' for sensing the vehicle's surrounding environment are essential. Traditionally, image sensors and LiDAR have played this role. However, a new type of vision sensor, event cameras, has recently attracted attention. Event cameras respond to changes in the surrounding environment (e.g., motion), exhibit strong robustness against motion blur, and perform well in high dynamic range environments, which are desirable in robotics applications. Furthermore, the asynchronous and low-latency principles of data acquisition make event cameras suitable for optical communication. By adding communication functionality to event cameras, it becomes possible to utilize I2V communication to immediately share information about forward collisions, sudden braking, and road conditions, thereby contributing to hazard avoidance. Additionally, receiving information such as signal timing and traffic volume enables speed adjustment and optimal route selection, facilitating more efficient driving. In this study, we construct a vehicle visible light communication system where event cameras are receivers, and multiple LEDs are transmitters. In driving scenes, the system tracks the transmitter positions and separates densely packed LED light sources using pilot sequences based on Walsh-Hadamard codes. As a result, outdoor vehicle experiments demonstrate error-free communication under conditions where the transmitter-receiver distance was within 40 meters and the vehicle's driving speed was 30 km/h (8.3 m/s).

cs.RO↗