arXiv subjects

Yufeng Li

Publications and source records attributed to Yufeng Li.

At least 55 records · Page 3Linked to original sources

arXiv2024

TIUP: Effective Processor Verification with Tautology-Induced Universal Properties

Design verification is a complex and costly task, especially for large and intricate processor projects. Formal verification techniques provide advantages by thoroughly examining design behaviors, but they require extensive labor and expertise in property formulation. Recent research focuses on verifying designs using the self-consistency universal property, reducing verification difficulty as it is design-independent. However, the single self-consistency property faces false positives and scalability issues due to exponential state space growth. To tackle these challenges, this paper introduces TIUP, a technique using tautologies as universal properties. We show how TIUP effectively uses tautologies as abstract specifications, covering processor data and control paths. TIUP simplifies and streamlines verification for engineers, enabling efficient formal processor verification.

cs.LO↗

arXiv2024

Convolutional neural network classification of cancer cytopathology images: taking breast cancer as an example

Breast cancer is a relatively common cancer among gynecological cancers. Its diagnosis often relies on the pathology of cells in the lesion. The pathological diagnosis of breast cancer not only requires professionals and time, but also sometimes involves subjective judgment. To address the challenges of dependence on pathologists expertise and the time-consuming nature of achieving accurate breast pathological image classification, this paper introduces an approach utilizing convolutional neural networks (CNNs) for the rapid categorization of pathological images, aiming to enhance the efficiency of breast pathological image detection. And the approach enables the rapid and automatic classification of pathological images into benign and malignant groups. The methodology involves utilizing a convolutional neural network (CNN) model leveraging the Inceptionv3 architecture and transfer learning algorithm for extracting features from pathological images. Utilizing a neural network with fully connected layers and employing the SoftMax function for image classification. Additionally, the concept of image partitioning is introduced to handle high-resolution images. To achieve the ultimate classification outcome, the classification probabilities of each image block are aggregated using three algorithms: summation, product, and maximum. Experimental validation was conducted on the BreaKHis public dataset, resulting in accuracy rates surpassing 0.92 across all four magnification coefficients (40X, 100X, 200X, and 400X). It demonstrates that the proposed method effectively enhances the accuracy in classifying pathological images of breast cancer.

eess.IV↗

arXiv2024

Survival Prediction Across Diverse Cancer Types Using Neural Networks

Gastric cancer and Colon adenocarcinoma represent widespread and challenging malignancies with high mortality rates and complex treatment landscapes. In response to the critical need for accurate prognosis in cancer patients, the medical community has embraced the 5-year survival rate as a vital metric for estimating patient outcomes. This study introduces a pioneering approach to enhance survival prediction models for gastric and Colon adenocarcinoma patients. Leveraging advanced image analysis techniques, we sliced whole slide images (WSI) of these cancers, extracting comprehensive features to capture nuanced tumor characteristics. Subsequently, we constructed patient-level graphs, encapsulating intricate spatial relationships within tumor tissues. These graphs served as inputs for a sophisticated 4-layer graph convolutional neural network (GCN), designed to exploit the inherent connectivity of the data for comprehensive analysis and prediction. By integrating patients' total survival time and survival status, we computed C-index values for gastric cancer and Colon adenocarcinoma, yielding 0.57 and 0.64, respectively. Significantly surpassing previous convolutional neural network models, these results underscore the efficacy of our approach in accurately predicting patient survival outcomes. This research holds profound implications for both the medical and AI communities, offering insights into cancer biology and progression while advancing personalized treatment strategies. Ultimately, our study represents a significant stride in leveraging AI-driven methodologies to revolutionize cancer prognosis and improve patient outcomes on a global scale.

eess.IV↗

arXiv2024

SEPE-SQED: Symbolic Quick Error Detection by Semantically Equivalent Program Execution

Symbolic quick error detection (SQED) has greatly improved efficiency in formal chip verification. However, it has a limitation in detecting single-instruction bugs due to its reliance on the self-consistency property. To address this, we propose a new variant called symbolic quick error detection by semantically equivalent program execution (SEPE-SQED), which utilizes program synthesis techniques to find sequences with equivalent meanings to original instructions. SEPE-SQED effectively detects single-instruction bugs by differentiating their impact on the original instruction and its semantically equivalent program (instruction sequence). To manage the search space associated with program synthesis, we introduce the CEGIS based on the highest priority first algorithm. The experimental results show that our proposed CEGIS approach improves the speed of generating the desired set of equivalent programs by 50% in time compared to previous methods. Compared to SQED, SEPE-SQED offers a wider variety of instruction combinations and can provide a shorter trace for triggering bugs in certain scenarios.

cs.SE↗

arXiv2024

Model Independent Approach of the JUNO $^8$B Solar Neutrino Program

The physics potential of detecting $^8$B solar neutrinos will be exploited at the Jiangmen Underground Neutrino Observatory (JUNO), in a model independent manner by using three distinct channels of the charged-current (CC), neutral-current (NC) and elastic scattering (ES) interactions. Due to the largest-ever mass of $^{13}$C nuclei in the liquid-scintillator detectors and the {expected} low background level, $^8$B solar neutrinos would be observable in the CC and NC interactions on $^{13}$C for the first time. By virtue of optimized event selections and muon veto strategies, backgrounds from the accidental coincidence, muon-induced isotopes, and external backgrounds can be greatly suppressed. Excellent signal-to-background ratios can be achieved in the CC, NC and ES channels to guarantee the $^8$B solar neutrino observation. From the sensitivity studies performed in this work, we show that JUNO, with ten years of data, can reach the {1$σ$} precision levels of 5%, 8% and 20% for the $^8$B neutrino flux, $\sin^2θ_{12}$, and $Δm^2_{21}$, respectively. It would be unique and helpful to probe the details of both solar physics and neutrino physics. In addition, when combined with SNO, the world-best precision of 3% is expected for the $^8$B neutrino flux measurement.

hep-ex↗

arXiv2024

SISSA: Real-time Monitoring of Hardware Functional Safety and Cybersecurity with In-vehicle SOME/IP Ethernet Traffic

Scalable service-Oriented Middleware over IP (SOME/IP) is an Ethernet communication standard protocol in the Automotive Open System Architecture (AUTOSAR), promoting ECU-to-ECU communication over the IP stack. However, SOME/IP lacks a robust security architecture, making it susceptible to potential attacks. Besides, random hardware failure of ECU will disrupt SOME/IP communication. In this paper, we propose SISSA, a SOME/IP communication traffic-based approach for modeling and analyzing in-vehicle functional safety and cyber security. Specifically, SISSA models hardware failures with the Weibull distribution and addresses five potential attacks on SOME/IP communication, including Distributed Denial-of-Services, Man-in-the-Middle, and abnormal communication processes, assuming a malicious user accesses the in-vehicle network. Subsequently, SISSA designs a series of deep learning models with various backbones to extract features from SOME/IP sessions among ECUs. We adopt residual self-attention to accelerate the model's convergence and enhance detection accuracy, determining whether an ECU is under attack, facing functional failure, or operating normally. Additionally, we have created and annotated a dataset encompassing various classes, including indicators of attack, functionality, and normalcy. This contribution is noteworthy due to the scarcity of publicly accessible datasets with such characteristics.Extensive experimental results show the effectiveness and efficiency of SISSA.

cs.CR↗

arXiv2023

Learning Image Deraining Transformer Network with Dynamic Dual Self-Attention

Recently, Transformer-based architecture has been introduced into single image deraining task due to its advantage in modeling non-local information. However, existing approaches tend to integrate global features based on a dense self-attention strategy since it tend to uses all similarities of the tokens between the queries and keys. In fact, this strategy leads to ignoring the most relevant information and inducing blurry effect by the irrelevant representations during the feature aggregation. To this end, this paper proposes an effective image deraining Transformer with dynamic dual self-attention (DDSA), which combines both dense and sparse attention strategies to better facilitate clear image reconstruction. Specifically, we only select the most useful similarity values based on top-k approximate calculation to achieve sparse attention. In addition, we also develop a novel spatial-enhanced feed-forward network (SEFN) to further obtain a more accurate representation for achieving high-quality derained results. Extensive experiments on benchmark datasets demonstrate the effectiveness of our proposed method.

cs.CV↗

arXiv2023

Science with the Einstein Telescope: a comparison of different designs

The Einstein Telescope (ET), the European project for a third-generation gravitational-wave detector, has a reference configuration based on a triangular shape consisting of three nested detectors with 10 km arms, where in each arm there is a `xylophone' configuration made of an interferometer tuned toward high frequencies, and an interferometer tuned toward low frequencies and working at cryogenic temperature. Here, we examine the scientific perspectives under possible variations of this reference design. We perform a detailed evaluation of the science case for a single triangular geometry observatory, and we compare it with the results obtained for a network of two L-shaped detectors (either parallel or misaligned) located in Europe, considering different choices of arm-length for both the triangle and the 2L geometries. We also study how the science output changes in the absence of the low-frequency instrument, both for the triangle and the 2L configurations. We examine a broad class of simple `metrics' that quantify the science output, related to compact binary coalescences, multi-messenger astronomy and stochastic backgrounds, and we then examine the impact of different detector designs on a more specific set of scientific objectives.

gr-qc↗

arXiv2022

Magneto-elastic coupling in a sinusoidal modulated magnet Cr$_2$GaN

We use neutron powder diffraction to investigate the magnetic and crystalline structure of Cr$_2$GaN. A magnetic phase transition is identified at $T \approx 170$ K, whereas no trace of structural transition is observed down to 6 K. Combining Rietveld refinement with irreducible representations, the spin configuration of Cr ions in Cr$_2$GaN is depicted as an incommensurate sinusoidal modulated structure characterized by a propagating vector ${k}$=(0.365, 0.365, 0). Upon warming up to the paramagnetic state, the magnetic order parameter closely resembles to the temperature dependence of $c$-axis lattice parameter, suggesting strong magneto-elastic coupling in this compound. Therefore, Cr$_2$GaN provides a potential platform for the exploration of magnetically tuned properties such as magnetoelectric, magnetostrictive and magnetocaloric effects, as well as their applications.

cond-mat.str-el↗

arXiv2022

Unpaired Deep Image Dehazing Using Contrastive Disentanglement Learning

We offer a practical unpaired learning based image dehazing network from an unpaired set of clear and hazy images. This paper provides a new perspective to treat image dehazing as a two-class separated factor disentanglement task, i.e, the task-relevant factor of clear image reconstruction and the task-irrelevant factor of haze-relevant distribution. To achieve the disentanglement of these two-class factors in deep feature space, contrastive learning is introduced into a CycleGAN framework to learn disentangled representations by guiding the generated images to be associated with latent factors. With such formulation, the proposed contrastive disentangled dehazing method (CDD-GAN) employs negative generators to cooperate with the encoder network to update alternately, so as to produce a queue of challenging negative adversaries. Then these negative adversaries are trained end-to-end together with the backbone representation network to enhance the discriminative information and promote factor disentanglement performance by maximizing the adversarial contrastive loss. During the training, we further show that hard negative examples can suppress the task-irrelevant factors and unpaired clear exemples can enhance the task-relevant factors, in order to better facilitate haze removal and help image restoration. Extensive experiments on both synthetic and real-world datasets demonstrate that our method performs favorably against existing unpaired dehazing baselines.

eess.IV↗

arXiv2022

The Spin of New Black Hole Candidate: MAXI J1803-298 Observed by NuSTAR and NICER

MAXI J1803-298, a newly-discovered Galactic transient and black hole candidate, was first detected by \emph{MAXI}/GSC on May 1st, 2021. In this paper, we present a detailed spectral analysis of MAXI J1803-298. Utilizing the X-ray reflection fitting method, we perform a joint fit to the spectra of MAXI J1803-298, respectively, observed by \emph{NuSTAR} and \emph{NICER}/XTI on the same day over the energy range between 0.7-79.0 keV, and found its spin (and the inclination angle i) can be constrained to be close to an extreme value, 0.991 ($i\sim$ $70 ^{\circ}$), at 68\% confidence interval. The results suggest that MAXI J1803-298 may be a fast-rotating black hole with a large inclination angle.

astro-ph.HE↗

arXiv2022

Unpaired Deep Image Deraining Using Dual Contrastive Learning

Learning single image deraining (SID) networks from an unpaired set of clean and rainy images is practical and valuable as acquiring paired real-world data is almost infeasible. However, without the paired data as the supervision, learning a SID network is challenging. Moreover, simply using existing unpaired learning methods (e.g., unpaired adversarial learning and cycle-consistency constraints) in the SID task is insufficient to learn the underlying relationship from rainy inputs to clean outputs as there exists significant domain gap between the rainy and clean images. In this paper, we develop an effective unpaired SID adversarial framework which explores mutual properties of the unpaired exemplars by a dual contrastive learning manner in a deep feature space, named as DCD-GAN. The proposed method mainly consists of two cooperative branches: Bidirectional Translation Branch (BTB) and Contrastive Guidance Branch (CGB). Specifically, BTB exploits full advantage of the circulatory architecture of adversarial consistency to generate abundant exemplar pairs and excavates latent feature distributions between two domains by equipping it with bidirectional mapping. Simultaneously, CGB implicitly constrains the embeddings of different exemplars in the deep feature space by encouraging the similar feature distributions closer while pushing the dissimilar further away, in order to better facilitate rain removal and help image restoration. Extensive experiments demonstrate that our method performs favorably against existing unpaired deraining approaches on both synthetic and real-world datasets, and generates comparable results against several fully-supervised or semi-supervised models.

cs.CV↗

arXiv2022

Detailed analysis on the reflection component for the black hole candidate MAXI J1348-630

The black hole candidate MAXI J1348-630 was discovered on January 26th, 2019, with the Gas Slit Camera (GSC) on-board \textit{MAXI}. We report a detailed spectral analysis of this source by using the archived data of \textit{NuSTAR}. A total of 9 observations covered the complete outburst evolution of MAXI J1348-630 from the hard state to the soft state and finally back to the hard state. Additionally, the intermediate state is found in the transition from the hard state to the soft state. We use the state-of-art reflection model \verb'relxill' family to fit all the 9 spectra, and the spectra from two focal plane module detectors of \textit{NuSTAR} are jointly fitted for each observation. In particular, we concentrate on the results of the black hole spin parameter and the inclination of the accretion disk. Based on the analysis of the inner radius of the accretion disk, we obtain the spin parameter $a_* =0.78_{-0.04}^{+0.04}$, and the inclination angle of the inner disk $i = 29.2_{-0.5}^{+0.3}$ degrees. Furthermore, we also find that when the black hole is in the hard state, the accretion disk would show a significant truncation. The high iron abundance and ionization of the accretion disk obtained in the fitting results can be possibly explained by the high density of the accretion disk.

astro-ph.HE↗

arXiv2021

Is Sized Typing for Coq Practical?

Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven't they been adapted to Coq? In this paper, we venture to answer this question with CIC$\widehat{*}$, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq's kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is wildly impractical in terms of performance.

cs.PL↗

arXiv2021

Estimating the spin of the black hole candidate MAXI J1659-152 with the X-ray continuum-fitting method

As a transient X-ray binary, MAXI J1659-152 contains a black hole candidate as its compact star. MAXI J1659-152 was discovered on 2010 September 25 during its only known outburst. Previously-published studies of this outburst indicate that MAXI J1659-152 may have an extreme retrograde spin, which, if confirmed, would provide an important clue as to the origin of black hole spin. In this paper, utilizing updated dynamical binary-system parameters (i.e. the black hole mass, the orbital inclination and the source distance) provided by \cite{Torres2021}, we analyze 65 spectra of MAXI J1659-152 from \emph{RXTE}/PCA, in order to assess the spin parameter. With a final selection of 9 spectra matching our $f_{\mathrm{sc}} \lesssim 25 \%$, soft-state criteria, we apply a relativistic thin disk spectroscopic model \texttt{kerrbb2} over 3.0-45.0 keV. We find that inclination angle correlates inversely with spin, and, considering the possible values for inclination angle, we constrain spin to be $-1 < a_{*} \lesssim 0.44$ at 90\% confidence interval via X-ray continuum-fitting. We can only rule out an extreme prograde (positive) spin. We confirm that an extreme retrograde solution is possible and is not ruled out by considering accretion torques given the young age of the system.

astro-ph.HE↗

arXiv2021

String length constraining from the stochastic gravitational waves background

We study the stochastic gravitational waves from string gas cosmology. With the help of the Lambert W function, we derive the exact energy density spectrum of the stochastic gravitational waves in term of tensor-to-scalar. New feathers with the spectrum are found. First, the non-Hagedorn phase can be ruled out by the current B-mode polarization in the cosmic microwave background. Second, the exact spectrum from the Hagedorn phase with a logarithmic term is shown to be unique in the measurable frequency range. Third, which is the most important, we find the string length can be constrained to be lower than 7 $\sim$ orders of that Planck scale.

gr-qc↗

arXiv2021

Exploring the sky localization and early warning capabilities of third generation gravitational wave detectors in three-detector network configurations

This work characterises the sky localization and early warning performance of networks of third generation gravitational wave detectors, consisting of different combinations of detectors with either the Einstein Telescope or Cosmic Explorer configuration in sites in North America, Europe and Australia. Using a Fisher matrix method which includes the effect of earth rotation, we estimate the sky localization uncertainty for $1.4\text{M}\odot$-$1.4\text{M}\odot$ binary neutron star mergers at distances $40\text{Mpc}$, $200\text{Mpc}$, $400\text{Mpc}$, $800\text{Mpc}$, $1600\text{Mpc}$, and an assumed astrophysical population up to redshift of 2 to characterize its performance for binary neutron star observations. We find that, for binary neutron star mergers at $200\text{Mpc}$ and a network consisting of the Einstein Telescope, Cosmic Explorer and an extra Einstein Telescope-like detector in Australia(2ET1CE), the upper limit of the size of the 90% credible region for the best localized 90% signals is $0.25\text{deg}^2$. For the simulated astrophysical distribution, this upper limit is $91.79\text{deg}^2$. If the Einstein Telescope-like detector in Australia is replaced with a Cosmic Explorer-like detector(1ET2CE), for $200\text{Mpc}$ case, the upper limit is $0.18\text{deg}^2$, while for astrophysical distribution, it is $56.77\text{deg}^2$. We note that the 1ET2CE network can detect 7.2% more of the simulated astrophysical population than the 2ET1CE network. In terms of early warning performance, we find that a network of 2ET1CE and 1ET2CE networks can both provide early warnings of the order of 1 hour prior to merger with sky localization uncertainties of 30 square degrees or less. Our study concludes that the 1ET2CE network is a good compromise between binary neutron stars detection rate, sky localization and early warning capabilities.

astro-ph.IM↗

arXiv2021

Spectral Analysis of New Black Hole Candidate AT2019wey Observed by NuSTAR

AT2019wey is a new galactic X-ray binary that was first discovered as an optical transient by the Australia Telescope Large Area Survey (ATLAS) on December 7, 2019. AT2019wey consists of a black hole candidate as well as a low-mass companion star ($M_{\text {star }} \lesssim 0.8 M_{\odot}$) and is likely to have a short orbital period ($P_{\text {orb }} \lesssim 8$ h). Although AT2019wey began activation in the X-ray band during almost the entire outburst on March 8, 2020, it did not enter the soft state during the entire outburst. In this study, we present a detailed spectral analysis of AT2019wey in the low/hard state during its X-ray outburst on the basis of Nuclear Spectroscopic Telescope Array \emph observations. We obtain tight constraints on several of its important physical parameters by applying the State-of-art \texttt{relxill} relativistic reflection model family. In particular, we determine that the measured inner radius of the accretion disk is most likely to have extended to the innermost stable circular orbit (ISCO) radius, i.e., $R_{\text{in}}=1.38^{+0.23}_{-0.16}~R_{\text{ISCO}}$. Hence, assuming $R_{\text{in}}$=$R_{\text{ISCO}}$, we find the spin of AT2019wey to be $a_{*}\sim$ $0.97$, which is close to the extreme and an inner disk inclination angle of ~$i\sim$ $22 ^{\circ}$. Additionally, according to our adopted models, AT2019wey tends to have a relatively high iron abundance of $A_{\mathrm{Fe}}\sim$ 5 $A_{\mathrm{Fe}, \odot}$ and a high disk ionization state of $\log ξ\sim$ 3.4.

astro-ph.HE↗