arXiv subjects

Shihao Xia

Publications and source records attributed to Shihao Xia.

15 recordsLinked to original sources

arXiv2026

ImagineUAV: Aerial Vision-Language Navigation via World-Action Modeling and Kinodynamic Planning

Vision-language navigation (VLN) for UAVs demands grounding free-form instructions into 6-DoF flight under partial observability. While Vision-Language-Action (VLA) models excel at semantic reasoning, they suffer from brittleness due to geometric inconsistency and dynamics mismatch. To address this, we propose ImagineUAV, an imagination-driven framework leveraging cascaded world-action modeling. Instead of direct regression, ImagineUAV employs a latent video diffusion model to generate instruction-conditioned future observations, explicitly imagining environmental evolution, from which 6-DoF motions are inferred via an action extractor. A kinodynamic planner then refines these estimates into collision-free trajectories. Additionally, a step-distilled inference pipeline ensures real-time execution. With only 1.3B parameters, ImagineUAV outperforms prior VLN and VLA baselines on benchmarks and real-world flights, validating the practicality of imagination-driven aerial navigation.

cs.RO↗

arXiv2026

M2K: Making the Model-Kernel Interface Explicit for Reliable CUDA Kernel Verification

Large language model (LLM) inference systems rely on CUDA kernels for core GPU computations, yet the interface between models and kernels is implicit and poorly specified. Models and kernels evolve independently and often make incompatible assumptions about tensor shapes and input sizes, leading to subtle memory bugs in CUDA kernels. These bugs can crash inference services, corrupt model weights, or be exploited by remote adversaries. Existing techniques either incur prohibitive runtime overhead, require specialized hardware, or fail to handle dynamic tensor shapes and variable kernel launch configurations, leaving the CUDA memory bugs largely unaddressed. This paper presents M2K, a fully automated framework that makes the model-kernel interface explicit and leverages it to detect memory bugs in CUDA kernels used in LLM inference systems. M2K consists of two components. HFProbe traces model execution without GPU hardware, classifies kernel arguments into model-fixed and user-variable, and emits symbolic constraints that capture the interface. cuKLEE then performs symbolic execution on CUDA kernels to pinpoint memory bugs under the interface constraints, modeling tensors as disjoint memory regions and treating thread identifiers symbolically to scale to thousands of threads. In the evaluation, M2K discovers 181 previously unknown bugs in real LLM inference systems, while producing only nine false positives, demonstrating its effectiveness.

cs.PL↗

arXiv2026

SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each defining a set of rules governing contract behavior. Violating these rules can cause serious security issues and financial losses, signifying the importance of verifying ERC compliance. Today's practices of such verification include manual audits, expert-developed program-analysis tools, and large language models (LLMs), all of which remain ineffective at detecting ERC rule violations. This paper introduces SymGPT, a tool that combines LLMs with symbolic execution to automatically verify smart contracts' compliance with ERC rules. We begin by empirically analyzing 132 ERC rules from three major ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, SymGPT instructs an LLM to translate ERC rules into a domain-specific language, synthesizes constraints from the translated rules to model potential rule violations, and performs symbolic execution for violation detection. Our evaluation shows that SymGPT identifies 5,783 ERC rule violations in 4,000 real-world contracts, including 1,375 violations with clear attack paths for financial theft. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.

cs.AI↗

arXiv2026

Doc2Spec: Synthesizing Formal Programming Specifications from Natural Language via Grammar Induction

Ensuring that API implementations and usage comply with natural language programming rules is critical for software correctness, security, and reliability. Formal verification can provide strong guarantees but requires precise specifications, which are difficult and costly to write manually. To address this challenge, we present Doc2Spec, a multi-agent framework that uses LLMs to automatically induce a specification grammar from natural-language rules and then generates formal specifications guided by the induced grammar. The grammar captures essential domain knowledge, constrains the specification space, and enforces consistent representations, thereby improving the reliability and quality of generated specifications. Evaluated on seven benchmarks across three programming languages, Doc2Spec outperforms a baseline without grammar induction and achieves competitive results against a technique with a manually crafted grammar, demonstrating the effectiveness of automated grammar induction for formalizing natural-language rules.

cs.PL↗

arXiv2025

Quantum Coherence as a Thermodynamic Resource Beyond the Classical Uncertainty Bound

Thermodynamic uncertainty relations (TURs) establish a fundamental trade-off between current precision and entropy production in nonequilibrium systems, yet the role of genuine quantum coherence in these bounds remains unresolved. Here we develop a general framework that explicitly incorporates quantum coherence into TURs for Markovian open quantum systems. By combining the quantum Cram\'er-Rao inequality with a Dyson series expansion of the parametrically deformed Lindblad dynamics, we derive a generalized TUR containing a coherence-sensitive correction that naturally separates classical and quantum contributions. The coherent term originates from the off-diagonal components of the nonequilibrium steady-state density matrix and systematically relaxes the classical precision-dissipation bound, allowing enhanced current precision without additional entropy production. Applying our theory to a three-level quantum maser, we demonstrate that steady-state coherence enables precision beyond the classical limit over a broad parameter regime while remaining consistent with the generalized bound. Our results identify quantum coherence as a genuine thermodynamic resource and provide a unified framework bridging classical and quantum uncertainty relations.

quant-ph↗

arXiv2025

Geometric Bound for Trade-off Relation in Quantum Tricycle

We establish a finite-time quantum tricycle driven by an external field and investigate its thermodynamic performance in the slow-driving regime. By developing a perturbative expansion of heat with respect to operation time, we capture the dynamics of heat exchange processes beyond the quasistatic limit. Within a geometric framework, we derive fundamental bounds on trade-offs between the cooling rate, coefficient of performance, and dissipation, governed by the thermodynamic length and trajectory geometry in control space. Our findings unveil intrinsic limits to the performance of quantum thermal machines and highlight the role of geometry in shaping finite-time thermodynamics. This work advances the fundamental understanding of quantum thermodynamic processes and offers guiding principles for the design of next-generation quantum technologies.

quant-ph↗

arXiv2025

How to Save My Gas Fees: Understanding and Detecting Real-world Gas Issues in Solidity Programs

The execution of smart contracts on Ethereum, a public blockchain system, incurs a fee called gas fee for its computation and data storage. When programmers develop smart contracts (e.g., in the Solidity programming language), they could unknowingly write code snippets that unnecessarily cause more gas fees. These issues, or what we call gas wastes, can lead to significant monetary losses for users. This paper takes the initiative in helping Ethereum users reduce their gas fees in two key steps. First, we conduct an empirical study on gas wastes in open-source Solidity programs and Ethereum transaction traces. Second, to validate our study findings, we develop a static tool called PeCatch to effectively detect gas wastes in Solidity programs, and manually examine the Solidity compiler's code to pinpoint implementation errors causing gas wastes. Overall, we make 11 insights and four suggestions, which can foster future tool development and programmer awareness, and fixing our detected bugs can save $0.76 million in gas fees daily.

cs.SE↗

arXiv2025

Theoretical bound of the efficiency of learning

A unified thermodynamic formalism describing the efficiency of learning is proposed. First, we derive an inequality, which is more strength than Clausius's inequality, revealing the lower bound of the entropy-production rate of a subsystem. Second, the inequality is transformed to determine the general upper limit for the efficiency of learning. In particular, we exemplify the bound of the efficiency in nonequilibrium quantum-dot systems and networks of living cells. The framework provides a fundamental trade-off relationship between energy and information inheriting in stochastic thermodynamic processes.

cond-mat.stat-mech↗

arXiv2025

SC-Bench: A Large-Scale Dataset for Smart Contract Auditing

There is a huge demand to ensure the compliance of smart contracts listed on blockchain platforms to safety and economic standards. Today, manual efforts in the form of auditing are commonly used to achieve this goal. ML-based automated techniques have the promise to alleviate human efforts and the resulting monetary costs. However, unlike other domains where ML techniques have had huge successes, no systematic ML techniques have been proposed or applied to smart contract auditing. We present SC-Bench, the first dataset for automated smart-contract auditing research. SC-Bench consists of 5,377 real-world smart contracts running on Ethereum, a widely used blockchain platform, and 15,975 violations of standards on Ehereum called ERCs. Out of these violations, 139 are real violations programmers made. The remaining are errors we systematically injected to reflect the violations of different ERC rules. We evaluate SC-Bench using GPT-4 by prompting it with both the contracts and ERC rules. In addition, we manually identify each violated rule and the corresponding code site (i.e., oracle) and prompt GPT-4 with the information asking for a True-or-False question. Our results show that without the oracle, GPT-4 can only detect 0.9% violations, and with the oracle, it detects 22.9% violations. These results show the potential room for improvement in ML-based techniques for smart-contract auditing.

cs.CR↗

arXiv2024

Semi-Markov Processes in Open Quantum Systems. III. Large Deviations of First Passage Time Statistics

In a specific class of open quantum systems with finite and fixed numbers of collapsed quantum states, the semi-Markov process method is used to calculate the large deviations of the first passage time statistics. The core formula is an equation of poles, which is also applied in determining the scaled generating functions (SCGFs) of the counting statistics. For simple counting variables, the SCGFs of the first passage time statistics are derived by finding the largest modulus of the roots of this equation with respect to the $z$-transform parameter and then calculating its logarithm. The procedure is analogous to that of solving for the SCGFs of the counting statistics. However, for current-like variables, the method generally fails unless the equation of pole is simplified to a quadratic form. The fundamental reason for this lies in the nonuniqueness between the roots and the region of convergence for the joint transform. We illustrate these results via a resonantly driven two-level quantum system, where for several counting variables the solutions to the SCGFs of the first passage time are analytically obtained. Furthermore, we apply these functions to investigate quantum violations of the classical kinetic and thermodynamic uncertainty relations.

cond-mat.stat-mech↗

arXiv2024

Performance optimization of a finite-time quantum tricycle

We establish a finite-time external field-driven quantum tricycle model. Within the framework of slow driving perturbation, the perturbation expansion of heat in powers of time can be derived during the heat exchange processes. Employing the method of Lagrange multiplier, we optimize the cooling performance of the tricycle by considering the cooling rate and the figure of merit, which is the product of the coefficient of performance and cooling rate, as objective functions. Our findings reveal the optimal operating region of the tricycle, shedding light on its efficient performance.

quant-ph↗

arXiv2024

Efficiency bounds for bipartite information-driven thermodynamic systems

This study introduces a novel approach to derive a lower bound for the entropy production rate of a subsystem by utilizing the Cauchy-Schwarz inequality. It extends to establishing comprehensive upper and lower bounds for the efficiency of two subsystems. These bounds are applicable to a wide range of Markovian stochastic processes, which enhances the accuracy in depicting the range of energy conversion efficiency between subsystems. Empirical validation is conducted using a two-quantum-dot system model, which serves to confirm the effectiveness of our inequality in refining the boundaries of efficiency.

cond-mat.stat-mech↗

arXiv2024

AuditGPT: Auditing Smart Contracts with ChatGPT

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each containing a set of rules to guide the behaviors of smart contracts. Violating the ERC rules could cause serious security issues and financial loss, signifying the importance of verifying smart contracts follow ERCs. Today's practices of such verification are to either manually audit each single contract or use expert-developed, limited-scope program-analysis tools, both of which are far from being effective in identifying ERC rule violations. This paper presents a tool named AuditGPT that leverages large language models (LLMs) to automatically and comprehensively verify ERC rules against smart contracts. To build AuditGPT, we first conduct an empirical study on 222 ERC rules specified in four popular ERCs to understand their content, their security impacts, their specification in natural language, and their implementation in Solidity. Guided by the study, we construct AuditGPT by separating the large, complex auditing process into small, manageable tasks and design prompts specialized for each ERC rule type to enhance LLMs' auditing performance. In the evaluation, AuditGPT successfully pinpoints 418 ERC rule violations and only reports 18 false positives, showcasing its effectiveness and accuracy. Moreover, AuditGPT beats an auditing service provided by security experts in effectiveness, accuracy, and cost, demonstrating its advancement over state-of-the-art smart-contract auditing practices.

cs.CR↗

arXiv2023

Theoretical bound of the efficiency of learning with coarse-graining

A thermodynamic formalism describing the efficiency of information learning is proposed, which is applicable for stochastic thermodynamic systems with multiple internal degree of freedom. The learning rate, entropy production rate (EPR), and entropy flow from the system to the environment under coarse-grained dynamics are derived. The Cauchy-Schwarz inequality has been applied to demonstrate the lower bound on the EPR of an internal state. The inequality of EPR is tighter than the Clausius inequality, leading to the derivative of the upper bound on the efficiency of learning. The results are verified in cellular networks with information processes.

cond-mat.stat-mech↗

arXiv2023

Performance improvement of a fractional quantum Stirling heat engine

To investigate the impact of fractional parameter on the thermodynamic behaviors of quantum systems, we incorporate fractional quantum mechanics into the cycle of a quantum Stirling heat engine and examine the influence of fractional parameter on the regeneration and efficiency. We propose a novel approach to control the thermodynamic cycle that leverages the fractional parameter structure and evaluates its effectiveness. Our findings reveal that by tuning the fractional parameter, the region of the cycle with the perfect regeneration and the Carnot efficiency can be expanded.

quant-ph↗