arXiv subjects

Ran Wei

Publications and source records attributed to Ran Wei.

At least 19 recordsLinked to original sources

arXiv2026

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↗

arXiv2026

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 $α>0$. The covariance of the Gaussian environment $\{ω_n\}_{n\in\mathbb N}$ is given by $\text{Cov}_{\mathbb P}(ω_n,ω_m)\sim |n-m|^{2H-2}$ with $H\in(0,1)$. Assuming $α\in(0,\frac12]$, $H\in(\frac12,1)$ and $α+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 $α<\frac12$.

math.PR↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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}(βω_x-h))$, where $\mathcal{R}_N$ is the range of $S$ up to time $N$, $β\geq0$ is the inverse temperature, and $h\in\mathbb{R}$ is an external field. By appropriately tuning $β=β_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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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↗

arXiv2026

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)=-(-Δ)^{ρ/2} u(t,x) +βu(t,x)δ_0(x)ξ(t),\\ u(0,\cdot)=u_0(x), \end{cases} \end{equation} where $-(-Δ)^{ρ/2}$ with $ρ\in(0,2]$ is the fractional Laplacian and $ξ$ is a Gaussian noise with covariance $\mathbb{E}[ξ(t) ξ(s)]=|t-s|^{2H-2}$ for $H\in(\frac12, 1]$. This equation with $ρ\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 $ρ= 2$, whereas, for $ρ\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ág, we prove that the equation has a unique global $L^1$-solution whenever $\frac{1}ρ+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↗

arXiv2026

On a pinning model in correlated Gaussian random environments

We consider a pinning model in correlated Gaussian random environments. For the model that is disorder relevant, we study its intermediate disorder regime and show that the rescaled partition functions converge to a non-trivial continuum limit in the Skorohod setting and in the Stratonovich setting, respectively. Our results partially confirm the Weinrib--Halperin prediction for disorder relevance/irrelevance.

math.PR↗

arXiv2026

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 $β$-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↗

arXiv2025

The critical disordered pinning measure

In this paper, we study a disordered pinning model induced by a random walk whose increments have a finite $(2+κ)$-th moment for some $κ>0$. It is known that this model is marginally relevant, and moreover, it undergoes a phase transition in an intermediate disorder regime. We show that, in the critical window, the point-to-point partition functions converge to a unique limiting random measure, which we call the critical disordered pinning measure. We also obtain an analogous result for a continuous counterpart to the pinning model, which is closely related to two other models: one is a critical stochastic Volterra equation that gives rise to a rough volatility model, and the other is a critical stochastic heat equation with multiplicative noise that is white in time and delta in space.

math.PR↗