arXiv ScienceSearch

arXiv subjects

Zhiyi Wang

Publications and source records attributed to Zhiyi Wang.

17 recordsLinked to original sources

Beyond Time Series: Spatial Reasoning for Epidemic Forecasting via Multimodal Learning

Epidemic forecasting models typically rely on surveillance data reported over administrative regions, treating them as atomic units, thereby obscuring sub-regional spatial structure that shapes disease dynamics. We introduce a spatially structured multimodal epidemic forecasting setting that integrates region-level temporal surveillance data with spatially localized auxiliary signals that are misaligned in resolution and structure, reflecting realistic public health reporting constraints. Building on this formulation, we propose M-SPICE (Multimodal SPatIal Context for Epidemic Forecasting), a structure-aware spatiotemporal forecasting framework that performs joint reasoning over temporal disease dynamics and spatial context via attention-based multimodal fusion, allowing spatial signals to selectively condition temporal representations across forecast horizons. We evaluate our approach on real-world COVID-19, influenza, and influenza-like illness (ILI) forecasting tasks under realistic real-time evaluation protocols. Across all forecasting settings, our method consistently outperforms state-of-the-art multivariate time-series, multimodal, and epidemiological forecasting baselines while maintaining strong probabilistic forecasting performance. Finally, interpretability analyses reveal when, where, and how spatial signals are leveraged, highlighting settings in which purely temporal, region-aggregated models are most likely to fail.

cs.LG

A statistical study of the environmental age of core-collapse supernovae based on VLT/MUSE integral-field-unit spectroscopy

We aim to understand the progenitor channels of CCSNe via a statistical study of the ages of their environments. We compiled a large and minimally biased sample of 128 CCSNe discovered by untargeted wide-field transient surveys and with archival VLT/MUSE integral-field-unit spectroscopy. We measured the local H{\alpha} luminosity within a 300-pc aperture centered on the SN explosion site as an empirical proxy for the environmental age. We find that the mean local H$\alpha$ luminosities are ordered as II(P) $\approx$ IIb $\lesssim$ Ib $<$ Ic. The differences among Types~II(P), IIb and Ib are very small, if any. Type~Ic SNe are located in clearly younger environments than the other types. Our result suggests that Type Ic SNe have much younger and more massive progenitors than the other CCSN types and they likely originate from a distinct progenitor channel. The distinction between Types II(P), IIb and Ib SNe is insensitive to progenitor mass and mainly due to the different binary separation; in contrast, Type Ic SNe predominantly require much higher-mass progenitors accompanied by close companions with large mass ratios and/or much stronger stellar wind that depends sensitively on progenitor mass.

astro-ph.SR

Adapting SAM to Nuclei Instance Segmentation and Classification via Cooperative Fine-Grained Refinement

Nuclei instance segmentation is critical in computational pathology for cancer diagnosis and prognosis. Recently, the Segment Anything Model has demonstrated exceptional performance in various segmentation tasks, leveraging its rich priors and powerful global context modeling capabilities derived from large-scale pre-training on natural images. However, directly applying SAM to the medical imaging domain faces significant limitations: it lacks sufficient perception of the local structural features that are crucial for nuclei segmentation, and full fine-tuning for downstream tasks requires substantial computational costs. To efficiently transfer SAM's robust prior knowledge to nuclei instance segmentation while supplementing its task-aware local perception, we propose a parameter-efficient fine-tuning framework, named Cooperative Fine-Grained Refinement of SAM, consisting of three core components: 1) a Multi-scale Adaptive Local-aware Adapter, which enables effective capability transfer by augmenting the frozen SAM backbone with minimal parameters and instilling a powerful perception of local structures through dynamically generated, multi-scale convolutional kernels; 2) a Hierarchical Modulated Fusion Module, which dynamically aggregates multi-level encoder features to preserve fine-grained spatial details; and 3) a Boundary-Guided Mask Refinement, which integrates multi-context boundary cues with semantic features through explicit supervision, producing a boundary-focused signal to refine initial mask predictions for sharper delineation. These three components work cooperatively to enhance local perception, preserve spatial details, and refine boundaries, enabling SAM to perform accurate nuclei instance segmentation directly.

cs.CV

Object Reconstruction under Occlusion with Generative Priors and Contact-induced Constraints

Object geometry is key information for robot manipulation. Yet, object reconstruction is a challenging task because camera observations are partial due to occlusions. The scene may not offer the flexibility for a robot to alter its viewpoint to obtain a full observation of the object of interest. In this paper, we leverage two extra sources of information to reduce the ambiguity of vision signals under occlusion. First, generative models learn priors of the shapes of commonly seen objects, allowing us to make reasonable guesses of the unseen part of geometry. Second, contact information, which can be obtained from videos and physical interactions, provides sparse constraints on the boundary of the geometry. We combine the two sources of information through contact-guided 3D generation. The guidance formulation is inspired by drag-based generative image editing. We explore different guidance strategies and highlight the importance of short gradient paths for guided generation. Experiments on synthetic and real-world data show that our approach improves the object reconstruction compared to pure 3D generation and contact-based optimization methods.

cs.CV

Stellis: A Strategy Language for Purifying Separation Logic Entailments

Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, these rule statements are insufficient for describing automation strategies, which usually involve the alignment and elimination of corresponding memory layouts in specific scenarios. To overcome this limitation, we propose Stellis, a strategy language for purifying separation logic entailments, i.e., removing all spatial formulas to reduce the entailment to a simpler pure entailment. Stellis features a powerful matching mechanism and a flexible action description, enabling the straightforward encoding of a wide range of strategies. To ensure strategy soundness, we introduce an algorithm that generates a soundness condition for each strategy, thereby reducing the soundness of each strategy to the correctness of its soundness condition. Furthermore, based on a mechanized reduction soundness theorem, our prototype implementation generates correctness proofs for the overall automation. We evaluate our system on a benchmark of 229 entailments collected from verification of standard linked data structures and the memory module of a microkernel, and the evaluation results demonstrate that, with such flexibility and convenience provided, our system is also highly effective, which automatically purifies 95.6% (219 out of 229) of the entailments using 5 libraries with 98 strategies.

cs.SE

QCP: A Practical Separation Logic-based C Program Verification Tool

As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, their practical application to complex, real-world systems is often hindered by critical gaps in both automation and expressiveness. To address these difficulties, this paper presents \textbf{Qualified C Programming Verifier (QCP)}, a novel verification tool that integrates annotation-based automatic verification with interactive proving using Rocq. QCP employs symbolic execution and a separation logic entailment solver to automatically discharge many verification obligations, while deferring more complex obligations to Rocq for manual proof. Furthermore, QCP includes a VS Code extension designed to enhance proof efficiency and support a deeper understanding of both the program behavior and verification outcomes.

cs.PL

C*: Unifying Programming and Verification in C

Ensuring the correct functionality of systems software, given its safety-critical and low-level nature, is a primary focus in formal verification research and applications. Despite advances in verification tooling, conventional programmers are rarely involved in the verification of their own code, resulting in higher development and maintenance costs for verified software. A key barrier to programmer participation in verification practices is the disconnect of environments and paradigms between programming and verification practices, which limits accessibility and real-time verification. We introduce C*, a proof-integrated language design for C programming. C* extends C with verification capabilities, powered by a symbolic execution engine and an LCF-style proof kernel. It enables real-time verification by allowing programmers to embed proof-code blocks alongside implementation code, facilitating interactive updates to the current proof state. Its expressive and extensible proof support allows users to build reusable libraries of logical definitions, theorems, and programmable proof automation. Crucially, C* unifies implementation and proof code development by using C as the common language. We implemented a prototype of C* and evaluated it on a representative benchmark of small C programs and a challenging real-world case study: the attach function of pKVM's buddy allocator. Our results demonstrate that C* supports the verification of a broad subset of C programming idioms and effectively handles complex reasoning tasks in real-world scenarios.

cs.PL

DropEdge not Foolproof: Effective Augmentation Method for Signed Graph Neural Networks

The paper discusses signed graphs, which model friendly or antagonistic relationships using edges marked with positive or negative signs, focusing on the task of link sign prediction. While Signed Graph Neural Networks (SGNNs) have advanced, they face challenges like graph sparsity and unbalanced triangles. The authors propose using data augmentation (DA) techniques to address these issues, although many existing methods are not suitable for signed graphs due to a lack of side information. They highlight that the random DropEdge method, a rare DA approach applicable to signed graphs, does not enhance link sign prediction performance. In response, they introduce the Signed Graph Augmentation (SGA) framework, which includes a structure augmentation module to identify candidate edges and a strategy for selecting beneficial candidates, ultimately improving SGNN training. Experimental results show that SGA significantly boosts the performance of SGNN models, with a notable 32.3% improvement in F1-micro for SGCN on the Slashdot dataset.

cs.LG

Effect of vector meson spin coherence on the measurements of chiral magnetic effect in heavy-ion collisions

The chiral magnetic effect (CME) in heavy-ion collisions reflects the local violation of ${\cal P}$ and ${\cal CP}$ symmetries in strong interactions and manifests as electric charge separation along the direction of the magnetic field created by the wounded nuclei. The experimental observables for the CME, such as the $\gamma_{112}$ correlator, the $R_{\Psi_2}(\Delta S)$ correlator, and the signed balance functions, however, are also subject to non-CME backgrounds, including those from resonance decays. A previous study showed that the CME observables are affected by the diagonal component of the spin density matrix, the $\rho_{00}$ for vector mesons. In this work, we study the contributions from the other elements of the spin density matrix using a toy model and a multiphase transport model. We find that the real part of the $\rho_{1-1}$ component, $\mathrm{Re}\,\rho_{1-1}$, affects the CME observables in a manner opposite to that of the $\rho_{00}$. All three aforementioned CME observables show a linear dependence on $\mathrm{Re}\,\rho_{1-1}$ in the model calculations, supporting our analytical derivations. The rest elements of the spin density matrix do not contribute to the CME observables. The off-diagonal terms in the spin density matrix indicate spin coherence and may be nonzero in heavy-ion collisions due to local spin polarization or spin-spin correlations. Thus, $\mathrm{Re}\,\rho_{1-1}$, along with $\rho_{00}$, could play a significant role in interpreting measurements in search of the CME.

nucl-th

Assessing Phrase Break of ESL Speech with Pre-trained Language Models and Large Language Models

This work introduces approaches to assessing phrase breaks in ESL learners' speech using pre-trained language models (PLMs) and large language models (LLMs). There are two tasks: overall assessment of phrase break for a speech clip and fine-grained assessment of every possible phrase break position. To leverage NLP models, speech input is first force-aligned with texts, and then pre-processed into a token sequence, including words and phrase break information. To utilize PLMs, we propose a pre-training and fine-tuning pipeline with the processed tokens. This process includes pre-training with a replaced break token detection module and fine-tuning with text classification and sequence labeling. To employ LLMs, we design prompts for ChatGPT. The experiments show that with the PLMs, the dependence on labeled training data has been greatly reduced, and the performance has improved. Meanwhile, we verify that ChatGPT, a renowned LLM, has potential for further advancement in this area.

cs.CL

Fairness in the Assignment Problem with Uncertain Priorities

In the assignment problem, a set of items must be allocated to unit-demand agents who express ordinal preferences (rankings) over the items. In the assignment problem with priorities, agents with higher priority are entitled to their preferred goods with respect to lower priority agents. A priority can be naturally represented as a ranking and an uncertain priority as a distribution over rankings. For example, this models the problem of assigning student applicants to university seats or job applicants to job openings when the admitting body is uncertain about the true priority over applicants. This uncertainty can express the possibility of bias in the generation of the priority ranking. We believe we are the first to explicitly formulate and study the assignment problem with uncertain priorities. We introduce two natural notions of fairness in this problem: stochastic envy-freeness (SEF) and likelihood envy-freeness (LEF). We show that SEF and LEF are incompatible and that LEF is incompatible with ordinal efficiency. We describe two algorithms, Cycle Elimination (CE) and Unit-Time Eating (UTE) that satisfy ordinal efficiency (a form of ex-ante Pareto optimality) and SEF; the well known random serial dictatorship algorithm satisfies LEF and the weaker efficiency guarantee of ex-post Pareto optimality. We also show that CE satisfies a relaxation of LEF that we term 1-LEF which applies only to certain comparisons of priority, while UTE satisfies a version of proportional allocations with ranks. We conclude by demonstrating how a mediator can model a problem of school admission in the face of bias as an assignment problem with uncertain priority.

cs.GT

Assessing Phrase Break of ESL speech with Pre-trained Language Models

This work introduces an approach to assessing phrase break in ESL learners' speech with pre-trained language models (PLMs). Different with traditional methods, this proposal converts speech to token sequences, and then leverages the power of PLMs. There are two sub-tasks: overall assessment of phrase break for a speech clip; fine-grained assessment of every possible phrase break position. Speech input is first force-aligned with texts, then pre-processed to a token sequence, including words and associated phrase break information. The token sequence is then fed into the pre-training and fine-tuning pipeline. In pre-training, a replaced break token detection module is trained with token data where each token has a certain percentage chance to be randomly replaced. In fine-tuning, overall and fine-grained scoring are optimized with text classification and sequence labeling pipeline, respectively. With the introduction of PLMs, the dependence on labeled training data has been greatly reduced, and performance has improved.

cs.CL

Revealing atomistic mechanisms of gold-catalyzed germanium growth using molecular dynamics simulations

The vapor-liquid-solid (VLS) method is considered a plausible technique for synthesizing germanium (Ge) nanostructures (e.g. nanowires), which have a broad range of applications due to their unique electronic properties and intrinsic compatibility with silicon. However, crystallization failures and material defects are still frequently observed in VLS processes, with insufficient understanding of their underlying mechanisms due to instrumental limitations for high-resolution in-situ characterizations. Employing an accurate interatomic potential well fitted to the gold-germanium (Au-Ge) phase diagram, we performed molecular dynamics simulations for a systematic investigation on the Au-catalyzed growth process of Ge crystals. From the simulations, relationships were established between the overall Ge growth rate and several main synthesis conditions, including substrate crystallographic orientation, temperature and Ge supersaturation in liquid. The dynamical behaviors of Ge atoms near the liquid-solid growing interface were captured, from which the atom surface stability and exchange rate were estimated for quantifying the atomistic details of the growth. These interface properties were further linked to the surface morphologies, to explain the observed orientation-dependent growing modes. This study sheds new lights into the understanding of the VLS growth mechanisms of Ge crystals, and provides scientific guidelines for designing innovative synthesis methods for similar nanomaterials.

cond-mat.mtrl-sci

Approximate Core for Committee Selection via Multilinear Extension and Market Clearing

Motivated by civic problems such as participatory budgeting and multiwinner elections, we consider the problem of public good allocation: Given a set of indivisible projects (or candidates) of different sizes, and voters with different monotone utility functions over subsets of these candidates, the goal is to choose a budget-constrained subset of these candidates (or a committee) that provides fair utility to the voters. The notion of fairness we adopt is that of core stability from cooperative game theory: No subset of voters should be able to choose another blocking committee of proportionally smaller size that provides strictly larger utility to all voters that deviate. The core provides a strong notion of fairness, subsuming other notions that have been widely studied in computational social choice. It is well-known that an exact core need not exist even when utility functions of the voters are additive across candidates. We therefore relax the problem to allow approximation: Voters can only deviate to the blocking committee if after they choose any extra candidate (called an additament), their utility still increases by an $\alpha$ factor. If no blocking committee exists under this definition, we call this an $\alpha$-core. Our main result is that an $\alpha$-core, for $\alpha < 67.37$, always exists when utilities of the voters are arbitrary monotone submodular functions, and this can be computed in polynomial time. This result improves to $\alpha < 9.27$ for additive utilities, albeit without the polynomial time guarantee. Our results are a significant improvement over prior work that only shows logarithmic approximations for the case of additive utilities. We complement our results with a lower bound of $\alpha > 1.015$ for submodular utilities, and a lower bound of any function in the number of voters and candidates for general monotone utilities.

cs.GT

A free lunch from ViT:Adaptive Attention Multi-scale Fusion Transformer for Fine-grained Visual Recognition

Learning subtle representation about object parts plays a vital role in fine-grained visual recognition (FGVR) field. The vision transformer (ViT) achieves promising results on computer vision due to its attention mechanism. Nonetheless, with the fixed size of patches in ViT, the class token in deep layer focuses on the global receptive field and cannot generate multi-granularity features for FGVR. To capture region attention without box annotations and compensate for ViT shortcomings in FGVR, we propose a novel method named Adaptive attention multi-scale Fusion Transformer (AFTrans). The Selective Attention Collection Module (SACM) in our approach leverages attention weights in ViT and filters them adaptively to correspond with the relative importance of input patches. The multiple scales (global and local) pipeline is supervised by our weights sharing encoder and can be easily trained end-to-end. Comprehensive experiments demonstrate that AFTrans can achieve SOTA performance on three published fine-grained benchmarks: CUB-200-2011, Stanford Dogs and iNat2017.

cs.CV

The smallest spectral radius of bicyclic uniform hypergraphs with a given size

Identifying graphs with extremal properties is an extensively studied topic in spectral graph theory. In this paper, we study the log-concavity of a type of iteration sequence related to the $\alpha$-normal weighted incidence matrices which is presented by Lu and Man for computing the spectral radius of hypergraphs. By using results obtained about the sequence and the method of some edge operations, we will characterize completely extremal k-graphs with the smallest spectral radius among bicyclic hypergraphs with given size.

math.CO

On some properties of the $\alpha$-spectral radius of the $k$-uniform hypergraph

In this paper we show how the $\alpha$-spectral radius changes under the edge grafting operations on connected $k$-uniform hypergraphs. We characterize the extremal hypertree for $\alpha$-spectral radius among $k$-uniform non-caterpillar hypergraphs with given order, size and diameter. we also characerize the second largest $\alpha$-spectral radius among all $k$-uniform supertrees on $n$ vertices by two methods.

math.CO