SearcharxivSearch

arXiv subjects

Ran Wei

Publications and source records attributed to Ran Wei.

At least 19 recordsLinked to original sources

Scaling limit for the pinning model in correlated Gaussian environment beyond the $L^2$-regime

In this paper, we study the scaling limit of the pinning model in correlated Gaussian environment. The tail probability of the underlying renewal process of the model has a polynomial decay with exponent $\alpha>0$. The covariance of the Gaussian environment $\{\omega_n\}_{n\in\mathbb N}$ is given by $\text{Cov}_{\mathbb P}(\omega_n,\omega_m)\sim |n-m|^{2H-2}$ with $H\in(0,1)$. Assuming $\alpha\in(0,\frac12]$, $H\in(\frac12,1)$ and $\alpha+2H>2$, we show that the partition function of the disordered pinning model, under the appropriate scaling, converges in distribution to the $L^1$-solution of the fractional stochastic heat equation driven by Gaussian noise correlated in time and localized at the origin. In particular, it is known that the solution is not $L^2$-integrable when $\alpha<\frac12$.

math.PR

Contract-Aware Rescue of a Drifted Isabelle Development: The Double-Tank Case Study

Large language models can propose proofs for interactive theorem provers, but a successful build does not show the surrounding verification task was preserved. We study this problem in an Isabelle development of a sampled-data double-tank controller. The work began with nine theories and ten unfinished obligations, grew to a 16-theory build without sorry, oops, added axiomatisation, or oracle use, and accumulated 23 stable and 36 broken proof states. A retrospective audit found material changes in 16 of the 100 original declarations, including a weakened end-to-end assurance theorem that assumed three of the four requirements in its conclusion. We used CAPRI, a contract-aware proof-repair tool, to govern a reconstruction by combining Isabelle acceptance with an independent check of repository changes against machine-readable edit contracts. The reconstruction discharged all ten scoped obligations within the original nine-theory structure. A secondary replay by a co-author reproduced the R10 build, contract checks, control tests, and principal audit findings; independent replication remains future work. Operational end-to-end verification remains incomplete: we still need to connect operational executions to the reconstructed quantitative trace contract, a task requiring an extended contract.

cs.SE

CAPRI: Contract-Aware Proof Repair for Isabelle

We address the use of large language models (LLMs) to help discover Isabelle proofs. An Isabelle build establishes that the submitted theory is accepted, but not that an LLM changed only what the developer authorised. We present CAPRI, a contract-aware repair workflow in which Isabelle checks the proof and an independent checker enforces a machine-readable edit contract. Prompts, proposals, candidate repositories, diagnostics, verdicts, and hashes are retained for audit. We evaluate five workflows on twelve failed proofs from four developments, with three replicates per task and condition, giving 180 runs and 138 valid repairs. Of 144 terminal candidates accepted by Isabelle, six had modified protected text; all arose in iterative workflows that could edit a complete theory. A proof-body-only interface produced 29/36 valid repairs and no contract violations, compared with 31/36 for the corresponding full-theory workflow. One-shot repair produced 22/36, while a later prospectively frozen iterative workflow produced 32/36; these figures compare complete workflows rather than individual mechanisms. A separate post hoc OpenRouter campaign found no improvement in the designated Luna comparisons. A Sol configuration with matched demonstrations produced 33/36 repairs, compared with 29/36 in the frozen OpenAI Responses condition, but the difference was not statistically significant in a one-sided exact McNemar test ($p=0.0625$).

cs.SE

Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models

Software complexity is a long-standing challenge for system engineers. Model-Driven Engineering (MDE) addresses it by treating models as first-class artefacts, but a typical MDE process spans many tools and produces heterogeneous models of different system aspects, making traceability, maintenance, and change management difficult. We propose RADIANT, an engineering methodology that combines MDE with Multi-Agent Large Language Models (LLMs) for complete model-based system development, with a focus on safety-critical systems. From a carefully specified requirement model, RADIANT automatically generates heterogeneous models across engineering phases -- a concept model, a domain-specific modelling language, a conforming system model, and a behaviour model -- together with executable, element-level traceability links, on top of which it provides exact, automated change-impact analysis. Generated behaviour models are translated into CSP and formally verified (e.g.\ for deadlock freedom and convergence) with a counterexample-driven repair loop. Evaluating RADIANT across three LLMs, we find that the multi-agent decomposition reliably improves the \emph{syntactic validity} of the generated formal artefacts over a single-agent baseline -- and their \emph{executability} where the model's code generation permits -- while gains in semantic accuracy are model-dependent. A six-participant study shows an order-of-magnitude ($10$--$15\times$) reduction in development time, and the unmodified pipeline transfers to a second domain.

cs.SE

PalmClaw: A Native On-Device Agent Framework for Mobile Phones

Large Language Model (LLM) agents have moved beyond generating responses to executing multi-step tasks by calling tools, observing the results, and iteratively deciding the next action. Most agent systems run on desktops or servers, which support tool use and task automation. Mobile devices are also important agent environments because they are widely accessible and contain users' data, sensors, and daily-use applications. Existing mobile agents mainly operate smartphones through graphical user interface (GUI) actions such as tapping, swiping, and typing, which often form long, interface-dependent sequences, cannot directly access device capabilities, and make execution boundaries difficult to define. We present PalmClaw, an open-source agent framework that runs natively on mobile phones and manages the sessions, memory, skills, tools, and agent loop directly on the device. PalmClaw exposes device capabilities as device tools with explicit arguments, structured results, and clearly defined execution boundaries. This design enables agents to use mobile capabilities directly while keeping each action explicit and controlled. Experiments show an 11.5% relative improvement in task success and a 94.9% reduction in completion time over the strongest baseline, with lower setup burden and traces illustrating how execution boundaries are applied. Code is available at https://github.com/ModalityDance/PalmClaw.

cs.CL

Robust nuclear hyperpolarization of small molecules through intermolecular transfer of parahydrogen-derived polarization

The recent advent of hyperpolarization techniques, which can enhance NMR signals by several orders of magnitude relative to thermally polarized samples, has enabled applications traditionally out of reach due to the inherently low sensitivity of NMR techniques. However, a high barrier to entry remains, as most hyperpolarization approaches either require complex instrumentation or are applicable only to a relatively small set of molecules. Here we introduce PHIPNOE, a platform that directly addresses both limitations. PHIPNOE is based on parahydrogen-induced polarization (PHIP), which is well-established as a scalable route to hyperpolarization requiring minimal instrumentation, but has been mostly restricted to molecules that undergo specific chemical reactions. We overcome this barrier by tailoring PHIP to create highly polarized, highly concentrated solutions of one specific molecule, which acts as an intermediate source of polarization. This 'source molecule' then distributes polarization to a broad range of target molecules mixed into the solution, via the spin polarization-induced nuclear Overhauser effect (SPINOE). We investigate chemical influences on PHIPNOE, and develop a predictive model to estimate enhancement based on molecular mass and T1 relaxation times. A complete run from PHIP hyperpolarization to PHIPNOE polarization transfer and signal detection takes less than one minute, the approach does not require any modifications to the NMR spectrometer, and enhancements are repeatable across molecular classes. PHIPNOE thus enables applications including single-shot multidimensional NMR, real-time monitoring of dynamic processes, and, with 300-fold signal amplification demonstrated on a benchtop spectrometer, practical low-field NMR, where we show enhanced sensitivity in detecting per- and polyfluoroalkyl substances (PFAS).

physics.chem-ph

A Framework for Managing the Models of Engineered Quantum Systems

Quantum technologies are maturing into systems that classical engineering must build, verify and maintain. The model-driven community has begun to respond with quantum-aware pipelines and languages, and the domain models these produce must be synchronised with the heterogeneous models created and owned by other communities. We argue that existing synchronisation approaches are insufficient for engineered quantum systems. A quantum system description captures superposition and entanglement, which a model transformation could remove undetected, while every structural check passes. To address this, we present the Quantum Systems Model Management (QSysMM) Framework, which guides the construction and synchronisation of the models of a quantum system into a digital single source of truth. The framework features four concerns: ontological, abstraction, composition and exposure, each given the treatment that engineered quantum systems require. Within this framework, we propose a Quantum Systems Modelling Language (QSysML) on the SysML v2 technology stack, and we close with a proposal that matures this synchronisation core into full model management for quantum systems.

cs.SE

Model-Driven Digital Twin Framework for Quantum Networks

Quantum networks are advancing towards larger and more operational infrastructures, yet their evaluation remains fragmented across heterogeneous physical platforms, simulators, protocols, and architectural abstractions. Current digital-twin studies for quantum networks mainly realise isolated capabilities or application-specific solutions rather than reusable system-level twins. This paper argues that Model-Driven Engineering (MDE) can provide a systematic basis for integrating and evolving these heterogeneous artefacts. It derives requirements for design-time evaluation and runtime synchronisation, and proposes a progression of architectures from code-driven and domain-model-driven solutions to point-to-point and hub-and-spoke integration. A conceptual implementation case study illustrates this using SysML v2, QKD kit, an EMF-based controller, and SeQUeNCe. The work provides a foundation for adaptable and interoperable digital twins for quantum networks.

cs.SE

Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering

Vibe coding -- accepting LLM-generated source from natural-language intent with minimal review -- is fast and may be adequate for low-criticality consumer software. But for safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification: large language models (LLMs) provide no formal correctness guarantees, and existing remedies target verification-aware languages (Dafny, Verus, Lean) that are scarce in pretraining data and absent from industrial toolchains. This paper closes the gap. We present Forge (Formal method Oriented Refinement loop for GEnerated code): a closed-loop pipeline that guides vibe coding through formal verification using established Model-Driven Engineering (MDE) infrastructure. Through vibe coding, we generate Java source code; our pipeline then extracts -- via model transformations -- formal artefacts in three different formalisms, each checked by a complementary verifier: deductive verification (Dafny), Communicating Sequential Processes (CSP) refinement via the Failures-Divergences Refinement checker (FDR4), and theorem proving using Z-Machines in Isabelle; every verification failure becomes a structured correction prompt that drives the next code-generation iteration. The LLM is the draft generator, the MDE chain is the discriminator, and the developer never has to read the formal models. Empirically, we find that the pipeline produces standards-relevant verification evidence for LLM-generated Java -- a step toward certification.

cs.SE

Emotion in an active inference model of human driving

Active inference has emerged as a principled framework for modeling adaptive behavior by balancing goal-directed action with uncertainty reduction. It has been successfully applied across biological and artificial systems, including recent work on human driving. However, existing active inference models of driving have yet to address an important determinant of behavior in traffic: affective state, which significantly influences decision-making. Prior work in non-traffic domains has explored active inference agents in which emotions are represented along the axes of valence and arousal in the circumplex model. However, this work has been limited to simplified settings with discrete state spaces. In this work, we propose an expanded formulation of valence and arousal that can be extracted from a more complex active inference model of driving with continuous states. In particular, we condition affective estimates not only on the current state but also on predicted future outcomes. We evaluate the proposed approach in two interactive driving scenarios and show that the resulting emotion signals correspond to affective patterns reported in similar scenarios.

cs.AI

Resolving space-sharing conflicts in road user interactions through uncertainty reduction: An active inference-based computational model

Understanding how road users resolve space-sharing conflicts is important both for traffic safety and the safe deployment of autonomous vehicles. While existing models have captured specific aspects of such interactions (e.g., explicit communication), a theoretically-grounded computational framework has been lacking. In this paper, we extend a previously developed active inference-based driver behavior model to simulate interactive behavior of two agents. Our model captures three complementary mechanisms for uncertainty reduction in interaction: (i) implicit communication via direct behavioral coupling, (ii) reliance on normative expectations (stop signs, priority rules, etc.), and (iii) explicit communication. In a simplified intersection scenario, we show that normative and explicit communication cues can increase the likelihood of a successful conflict resolution. However, this relies on agents acting as expected. In situations where another agent (intentionally or unintentionally) violates normative expectations or communicates misleading information, reliance on these cues may induce collisions. These findings illustrate how active inference can provide a novel framework for modeling road user interactions which is also applicable in other fields.

cs.AI

Strix: Re-thinking NPU Reliability from a System Perspective

DNNs and LLMs increasingly rely on hardware accelerators, including in safety-critical domains, while technology scaling and growing model complexity make hardware faults more frequent. Existing system-level mechanisms typically treat the NPU as a monolithic unit, using coarse-grained replication that incurs prohibitive performance and hardware overheads, leaving a gap between reliability requirements and deployable solutions. To bridge this gap, we present Strix, a full-stack NPU reliability framework on an open-source SoC, spanning micro-architecture, ISA, and programming methods. Strix re-partitions the NPU along the system inference pipeline, identifies dominant failure modes, and attaches targeted safeguards, achieving sub-micro-second fault localisation, error detection, and correction with only 1.04$\times$ slowdown and minimal hardware overhead.

cs.AR

From Characterization to Microarchitecture: Designing an Elegant and Reliable BFP-Based NPU

Block Floating-Point (BFP) is emerging as an attractive data format for edge Neural Processing Units (NPUs), combining wide dynamic range with high hardware efficiency. However, its behavior under hardware faults and suitability for safety-critical deployments remain underexplored. Here, we present the first in-depth empirical reliability study of BFP-based NPUs. Using RTL-level fault injection on NPUs, our bit- and path-level analysis reveals pronounced heterogeneous vulnerabilities and shows conventional end-to-end check becomes ineffective under nonlinear block scaling. Guided by these insights, we design a fault-tolerant BFP-based NPU microarchitecture that aligns the BFP computational semantics with reliability constraints. The design uses a row/column-wise blocking strategy to decouple the fixed-point mantissa computations from the scalar exponent path, and introduces ultra-lightweight protection mechanisms for each. Experimental results demonstrate our design achieves near-dual modular redundancy reliability with only $3.55\%$ geometric mean performance overhead and less than $2\%$ hardware cost.

cs.AR

On a fractional stochastic heat equation arising from the disordered pinning model

We study the mild Skorohod solution to the following fractional stochastic heat equation on $\mathbb{R}$: \begin{equation} \begin{cases} \partial_t u(t,x)=-(-\Delta)^{\rho/2} u(t,x) +\beta u(t,x)\delta_0(x)\xi(t),\\ u(0,\cdot)=u_0(x), \end{cases} \end{equation} where $-(-\Delta)^{\rho/2}$ with $\rho\in(0,2]$ is the fractional Laplacian and $\xi$ is a Gaussian noise with covariance $\mathbb{E}[\xi(t) \xi(s)]=|t-s|^{2H-2}$ for $H\in(\frac12, 1]$. This equation with $\rho\in(1,2]$ arises naturally in the study of the disordered pinning model. We show that the equation admits a local $L^2$-solution when $\rho = 2$, whereas, for $\rho \in (0,2)$, any solution--if it exists uniquely--cannot be $L^p$-integrable for any $p > 1$. Moreover, inspired by the recent work of Quastel, Ramirez and Vir\'{a}g, we prove that the equation has a unique global $L^1$-solution whenever $\frac{1}{\rho}+1<2H$. We also establish the strict positivity of the solution. Our work partially fills the gap in the study of the Weinrib-Halperin prediction.

math.PR

scMRDR: A scalable and flexible framework for unpaired single-cell multi-omics data integration

Advances in single-cell sequencing have enabled high-resolution profiling of diverse molecular modalities, while integrating unpaired multi-omics single-cell data remains challenging. Existing approaches either rely on pair information or prior correspondences, or require computing a global pairwise coupling matrix, limiting their scalability and flexibility. In this paper, we introduce a scalable and flexible generative framework called single-cell Multi-omics Regularized Disentangled Representations (scMRDR) for unpaired multi-omics integration. Specifically, we disentangle each cell's latent representations into modality-shared and modality-specific components using a well-designed $\beta$-VAE architecture, which are augmented with isometric regularization to preserve intra-omics biological heterogeneity, adversarial objective to encourage cross-modal alignment, and masked reconstruction loss strategy to address the issue of missing features across modalities. Our method achieves excellent performance on benchmark datasets in terms of batch correction, modality alignment, and biological signal preservation. Crucially, it scales effectively to large-scale datasets and supports integration of more than two omics, offering a powerful and flexible solution for large-scale multi-omics data integration and downstream biological discovery.

q-bio.QM

Non-directed polymers in random environments with range penalties: the high dimensional case

We study a non-directed polymer model in random environments. The polymer is modeled by a simple symmetric random walk $S$ on $\mathbb{Z}^d$ with $d\geq2$, and the random environment is modeled by i.i.d. random variables whose tail probability decays polynomially. The interaction between the polymer and the random environment is captured by a Gibbs transform: at time $N$, the law of $S$ is tilted by the factor $\exp(\sum_{x\in\mathcal{R}_N}(\beta\omega_x-h))$, where $\mathcal{R}_N$ is the range of $S$ up to time $N$, $\beta\geq0$ is the inverse temperature, and $h\in\mathbb{R}$ is an external field. By appropriately tuning $\beta=\beta_N$ and $h=h_N$, we establish the phase diagram, analyze the fluctuations of $S$ under the Gibbs transform, and derive the scaling limits of the (logarithmic) partition function. This paper is a follow-up work of arxiv.org/abs/2101.05949. The main novelty and challenge arise from tuning the external field $h$, which brings in various range penalties, unlike in arxiv.org/abs/2101.05949, where $h$ is fixed and serves only as a centering term for the random environment.

math.PR

AXIOM: Learning to Play Games in Minutes with Expanding Object-Centric Models

Current deep reinforcement learning (DRL) approaches achieve state-of-the-art performance in various domains, but struggle with data efficiency compared to human learning, which leverages core priors about objects and their interactions. Active inference offers a principled framework for integrating sensory information with prior knowledge to learn a world model and quantify the uncertainty of its own beliefs and predictions. However, active inference models are usually crafted for a single task with bespoke knowledge, so they lack the domain flexibility typical of DRL approaches. To bridge this gap, we propose a novel architecture that integrates a minimal yet expressive set of core priors about object-centric dynamics and interactions to accelerate learning in low-data regimes. The resulting approach, which we call AXIOM, combines the usual data efficiency and interpretability of Bayesian approaches with the across-task generalization usually associated with DRL. AXIOM represents scenes as compositions of objects, whose dynamics are modeled as piecewise linear trajectories that capture sparse object-object interactions. The structure of the generative model is expanded online by growing and learning mixture models from single events and periodically refined through Bayesian model reduction to induce generalization. AXIOM masters various games within only 10,000 interaction steps, with both a small number of parameters compared to DRL, and without the computational expense of gradient-based optimization.

cs.AI

MERE: Hardware-Software Co-Design for Masking Cache Miss Latency in Embedded Processors

Runahead execution is a technique to mask memory latency caused by irregular memory accesses. By pre-executing the application code during occurrences of long-latency operations and prefetching anticipated cache-missed data into the cache hierarchy, runahead effectively masks memory latency for subsequent cache misses and achieves high prefetching accuracy; however, this technique has been limited to superscalar out-of-order and superscalar in-order cores. For implementation in scalar in-order cores, the challenges of area-/energy-constraint and severe cache contention remain. Here, we build the first full-stack system featuring runahead, MERE, from SoC and a dedicated ISA to the OS and programming model. Through this deployment, we show that enabling runahead in scalar in-order cores is possible, with minimal area and power overheads, while still achieving high performance. By re-constructing the sequential runahead employing a hardware/software co-design approach, the system can be implemented on a mature processor and SoC. Building on this, an adaptive runahead mechanism is proposed to mitigate the severe cache contention in scalar in-order cores. Combining this, we provide a comprehensive solution for embedded processors managing irregular workloads. Our evaluation demonstrates that the proposed MERE attains 93.5% of a 2-wide out-of-order core's performance while constraining area and power overheads below 5%, with the adaptive runahead mechanism delivering an additional 20.1% performance gain through mitigating the severe cache contention issues.

cs.AR