Searcharxiv⌕ Search

arXiv subjects

Guoqiang Li

Publications and source records attributed to Guoqiang Li.

At least 37 records · Page 2Linked to original sources

Stress Softening Damage in Strongly Nonlinear Viscoelastic Soft Materials A Physics Informed Data Driven Constitutive Model with Time Temperature Coupling

This study presents a novel physics informed, data-driven modeling framework for capturing the strongly nonlinear thermo-viscoelastic behavior of soft materials exhibiting stress softening, with emphasis on the Mullins effect. Unlike previous approaches limited to quasi-static or isothermal conditions, our model unifies rate dependence, temperature sensitivity, large strain cyclic loading, and evolving damage mechanisms. Thermodynamic admissibility is ensured via a custom loss function that embeds the Clausius Duhem inequality and explicitly constrains the damage variable for physically realistic softening. A Temporal Convolutional Network is trained on high fidelity experimental data across multiple temperatures, strain rates, and stretch levels, enabling the model to capture rich thermomechanical coupling and history dependence. The framework generalizes to unseen thermo mechanical conditions, higher strain rates, and larger deformations, and remains robust to input noise. Validation against finite element simulations using Abaqus/Explicit demonstrates excellent agreement under cyclic loading and damage evolution, confirming the surrogate models effectiveness for advanced simulation workflows.

cond-mat.soft↗

DCE-LLM: Dead Code Elimination with Large Language Models

Dead code introduces several challenges in software development, such as increased binary size and maintenance difficulties. It can also obscure logical errors and be exploited for obfuscation in malware. For LLM-based code-related tasks, dead code introduces vulnerabilities that can mislead these models, raising security concerns. Although modern compilers and IDEs offer dead code elimination, sophisticated patterns can bypass these tools. A universal approach that includes classification, location, explanation, and correction is needed, yet current tools often require significant manual effort. We present DCE-LLM, a framework for automated dead code elimination using a small CodeBERT model with an attribution-based line selector to efficiently locate suspect code. LLMs then generate judgments and explanations, fine-tuned on a large-scale, annotated dead code dataset to provide detailed explanations and patches. DCE-LLM outperforms existing tools, with advanced unreachability detection, automated correction, and support for multiple programming languages. Experimental results show DCE-LLM achieves over 94% F1 scores for unused and unreachable code, significantly surpassing GPT-4o by 30%.

cs.SE↗

MUC-G4: Minimal Unsat Core-Guided Incremental Verification for Deep Neural Network Compression

The rapid development of deep learning has led to challenges in deploying neural networks on edge devices, mainly due to their high memory and runtime complexity. Network compression techniques, such as quantization and pruning, aim to reduce this complexity while maintaining accuracy. However, existing incremental verification methods often focus only on quantization and struggle with structural changes. This paper presents MUC-G4 (Minimal Unsat Core-Guided Incremental Verification), a novel framework for incremental verification of compressed deep neural networks. It encodes both the original and compressed networks into SMT formulas, classifies changes, and use \emph{Minimal Unsat Cores (MUCs)} from the original network to guide efficient verification for the compressed network. Experimental results show its effectiveness in handling quantization and pruning, with high proof reuse rates and significant speedup in verification time compared to traditional methods. MUC-G4 hence offers a promising solution for ensuring the safety and reliability of compressed neural networks in practical applications.

cs.LG↗

Single-Cell Trajectory Reconstruction Reveals Migration Potential of Cell Populations

Cell migration, which is strictly regulated by intracellular and extracellular cues, is crucial for normal physiological processes and the progression of certain diseases. However, there is a lack of an efficient approach to analyze super-statistical and time-varying characteristics of cell migration based on single trajectories. Here, we propose an approach to reconstruct single-cell trajectories, which incorporates wavelet transform, power spectrum of an OU-process, and fits of the power spectrum to analyze statistical and time-varying properties of customized target-finding and migration metrics. Our results reveal diverse relationships between motility parameters and dynamic metrics, especially the existence of an optimal parameter range. Moreover, the analysis reveals that the loss of Arpin protein enhances the migration potential of D. discoideum, and a previously reported result that the rescued amoeba is distinguishable from the wild-type amoeba. Significantly, time-varying dynamic metrics emerge periodic phenomena under the influence of irregularly changing parameters, which correlates with migration potential. Our analysis suggests that the approach provides a powerful tool for estimating time-dependent migration potential and statistical features of single-cell trajectories, enabling a better understanding of the relationship between intracellular proteins and cellular behaviors. This also provides more insights on the migration dynamics of single cells and cell populations.

physics.bio-ph↗

Large Language Model guided Deep Reinforcement Learning for Decision Making in Autonomous Driving

Deep reinforcement learning (DRL) shows promising potential for autonomous driving decision-making. However, DRL demands extensive computational resources to achieve a qualified policy in complex driving scenarios due to its low learning efficiency. Moreover, leveraging expert guidance from human to enhance DRL performance incurs prohibitively high labor costs, which limits its practical application. In this study, we propose a novel large language model (LLM) guided deep reinforcement learning (LGDRL) framework for addressing the decision-making problem of autonomous vehicles. Within this framework, an LLM-based driving expert is integrated into the DRL to provide intelligent guidance for the learning process of DRL. Subsequently, in order to efficiently utilize the guidance of the LLM expert to enhance the performance of DRL decision-making policies, the learning and interaction process of DRL is enhanced through an innovative expert policy constrained algorithm and a novel LLM-intervened interaction mechanism. Experimental results demonstrate that our method not only achieves superior driving performance with a 90\% task success rate but also significantly improves the learning efficiency and expert guidance utilization efficiency compared to state-of-the-art baseline algorithms. Moreover, the proposed method enables the DRL agent to maintain consistent and reliable performance in the absence of LLM expert guidance. The code and supplementary videos are available at https://bitmobility.github.io/LGDRL/.

cs.RO↗

ARCEAK: An Automated Rule Checking Framework Enhanced with Architectural Knowledge

Automated Rule Checking (ARC) plays a crucial role in advancing the construction industry by addressing the laborious, inconsistent, and error-prone nature of traditional model review conducted by industry professionals. Manual assessment against intricate sets of rules often leads to significant project delays and expenses. In response to these challenges, ARC offers a promising solution to improve efficiency and compliance in design within the construction sector. However, the main challenge of ARC lies in translating regulatory text into a format suitable for computer processing. Current methods for rule interpretation require extensive manual labor, thereby limiting their practicality. To address this issue, our study introduces a novel approach that decomposes ARC into two distinct tasks: rule information extraction and verification code generation. Leveraging generative pre-trained transformers, our method aims to streamline the interpretation of regulatory texts and simplify the process of generating model compliance checking code. Through empirical evaluation and case studies, we showcase the effectiveness and potential of our approach in automating code compliance checking, enhancing the efficiency and reliability of construction projects.

cs.SE↗

Affine Disjunctive Invariant Generation with Farkas' Lemma

In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approach for the automated generation of affine disjunctive invariants for affine while loops via Farkas' Lemma, a fundamental theorem on linear inequalities. Our main contributions are two-fold. First, we combine Farkas' Lemma with a succinct control flow transformation to derive disjunctive invariants from the conditional branches in the loop. Second, we propose an invariant propagation technique that minimizes the invariant computation effort by propagating previously solved invariants to yet unsolved locations as much as possible. Furthermore, we resolve the infeasibility checking in the application of Farkas' Lemma which has not been addressed previously, and extend our approach to nested loops via loop summary. Experimental evaluation over more than 100 affine while loops (mostly from SV-COMP 2023) demonstrates that our approach is promising to generate tight linear invariants over affine programs.

cs.LO↗

Can Language Models Pretend Solvers? Logic Code Simulation with LLMs

Transformer-based large language models (LLMs) have demonstrated significant potential in addressing logic problems. capitalizing on the great capabilities of LLMs for code-related activities, several frameworks leveraging logical solvers for logic reasoning have been proposed recently. While existing research predominantly focuses on viewing LLMs as natural language logic solvers or translators, their roles as logic code interpreters and executors have received limited attention. This study delves into a novel aspect, namely logic code simulation, which forces LLMs to emulate logical solvers in predicting the results of logical programs. To further investigate this novel task, we formulate our three research questions: Can LLMs efficiently simulate the outputs of logic codes? What strength arises along with logic code simulation? And what pitfalls? To address these inquiries, we curate three novel datasets tailored for the logic code simulation task and undertake thorough experiments to establish the baseline performance of LLMs in code simulation. Subsequently, we introduce a pioneering LLM-based code simulation technique, Dual Chains of Logic (DCoL). This technique advocates a dual-path thinking approach for LLMs, which has demonstrated state-of-the-art performance compared to other LLM prompt strategies, achieving a notable improvement in accuracy by 7.06% with GPT-4-Turbo.

cs.AI↗

Reconstruction of Poloidal Magnetic Fluxes on EAST based on Neural Networks with Measured Signals

The accurate construction of tokamak equilibria, which is critical for the effective control and optimization of plasma configurations, depends on the precise distribution of magnetic fields and magnetic fluxes. Equilibrium fitting codes, such as EFIT relying on traditional equilibrium algorithms, require solving the GS equation by iterations based on the least square method constrained with measured magnetic signals. The iterative methods face numerous challenges and complexities in the pursuit of equilibrium optimization. Furthermore, these methodologies heavily depend on the expertise and practical experience, demanding substantial resource allocation in personnel and time. This paper reconstructs magnetic equilibria for the EAST tokamak based on artificial neural networks through a supervised learning method. We use a fully connected neural network to replace the GS equation and reconstruct the poloidal magnetic flux distribution by training the model based on EAST datasets. The training set, validation set, and testing set are partitioned randomly from the dataset of poloidal magnetic flux distributions of the EAST experiments in 2016 and 2017 years. The feasibility of the neural network model is verified by comparing it to the offline EFIT results. It is found that the neural network algorithm based on the supervised machine learning method can accurately predict the location of different closed magnetic flux surfaces at a high efficiency. The similarities of the predicted X-point position and last closed magnetic surface are both 98%. The Pearson coherence of the predicted q profiles is 92%. Compared with the target value, the model results show the potential of the neural network model for practical use in plasma modeling and real-time control of tokamak operations.

physics.plasm-ph↗

On membrane-based approaches for rare earths separation and extraction-recent developments

This article aims to: i) review the current membrane-based methods in REEs separation focusing on non-liquid membranes (imprinted, polymer inclusion, nanocomposite, metal-/covalent organic framework membranes), ii) present the considerations of the essential scientific and technical issues, e.g. extraction performances, separation efficiency, REEs transport features, and iii) discuss their transport models and mechanisms as well as membrane stability.

cond-mat.mtrl-sci↗

GPS Attack Detection and Mitigation for Safe Autonomous Driving using Image and Map based Lateral Direction Localization

The accuracy and robustness of vehicle localization are critical for achieving safe and reliable high-level autonomy. Recent results show that GPS is vulnerable to spoofing attacks, which is one major threat to autonomous driving. In this paper, a novel anomaly detection and mitigation method against GPS attacks that utilizes onboard camera and high-precision maps is proposed to ensure accurate vehicle localization. First, lateral direction localization in driving lanes is calculated by camera-based lane detection and map matching respectively. Then, a real-time detector for GPS spoofing attack is developed to evaluate the localization data. When the attack is detected, a multi-source fusion-based localization method using Unscented Kalman filter is derived to mitigate GPS attack and improve the localization accuracy. The proposed method is validated in various scenarios in Carla simulator and open-source public dataset to demonstrate its effectiveness in timely GPS attack detection and data recovery.

cs.RO↗

Data-Flow-Based Normalization Generation Algorithm of R1CS for Zero-Knowledge Proof

The communities of blockchains and distributed ledgers have been stirred up by the introduction of zero-knowledge proofs (ZKPs). Originally designed to solve privacy issues, ZKPs have now evolved into an effective remedy for scalability concerns and are applied in Zcash (internet money like Bitcoin). To enable ZKPs, Rank-1 Constraint Systems (R1CS) offer a verifier for bi-linear equations. To accurately and efficiently represent R1CS, several language tools like Circom, Noir, and Snarky have been proposed to automate the compilation of advanced programs into R1CS. However, due to the flexible nature of R1CS representation, there can be significant differences in the compiled R1CS forms generated from circuit language programs with the same underlying semantics. To address this issue, this paper uses a data-flow-based R1CS paradigm algorithm, which produces a standardized format for different R1CS instances with identical semantics. By using the normalized R1CS format circuits, the complexity of circuits' verification can be reduced. In addition, this paper presents an R1CS normalization algorithm benchmark, and our experimental evaluation demonstrates the effectiveness and correctness of our methods.

cs.FL↗

Differential Newborn Face Morphing Attack Detection using Wavelet Scatter Network

Face Recognition System (FRS) are shown to be vulnerable to morphed images of newborns. Detecting morphing attacks stemming from face images of newborn is important to avoid unwanted consequences, both for security and society. In this paper, we present a new reference-based/Differential Morphing Attack Detection (MAD) method to detect newborn morphing images using Wavelet Scattering Network (WSN). We propose a two-layer WSN with 250 $\times$ 250 pixels and six rotations of wavelets per layer, resulting in 577 paths. The proposed approach is validated on a dataset of 852 bona fide images and 2460 morphing images constructed using face images of 42 unique newborns. The obtained results indicate a gain of over 10\% in detection accuracy over other existing D-MAD techniques.

cs.CV↗

Vulnerability of Face Morphing Attacks: A Case Study on Lookalike and Identical Twins

Face morphing attacks have emerged as a potential threat, particularly in automatic border control scenarios. Morphing attacks permit more than one individual to use travel documents that can be used to cross borders using automatic border control gates. The potential for morphing attacks depends on the selection of data subjects (accomplice and malicious actors). This work investigates lookalike and identical twins as the source of face morphing generation. We present a systematic study on benchmarking the vulnerability of Face Recognition Systems (FRS) to lookalike and identical twin morphing images. Therefore, we constructed new face morphing datasets using 16 pairs of identical twin and lookalike data subjects. Morphing images from lookalike and identical twins are generated using a landmark-based method. Extensive experiments are carried out to benchmark the attack potential of lookalike and identical twins. Furthermore, experiments are designed to provide insights into the impact of vulnerability with normal face morphing compared with lookalike and identical twin face morphing.

cs.CV↗

Effects of resonant magnetic perturbations on neutral beam heating in a tokamak

Effects of resonant magnetic perturbations (RMPs) on tangential neutral beam heating in the EAST tokamak are studied numerically. RMPs with linear resistive magnetohydrodynamics response are used in the modeling. A variety of representing configurations of RMP coil currents are examined and their effects on the NBI heating efficiency are compared, in order to find a parameter window where deleterious effects of RMPs on NBI heating efficiency are minimized. It is found that the internal redistribution of fast ions by RMPs induces local accumulation of fast ions, resulting in higher local fast ion pressure than the case without RMPs. It is also found that the toroidal phasing of the RMP with respect to the fast ion source has slight effects on the steady-state radial profile of fast ions. The dependence of fast ion loss fraction on the RMP up-down phase difference shows similar behavior as the dependence of the radial width of chaotic magnetic field on the phase difference. A statistical method of identifying resonances between RMPs and lost fast ions is proposed and the results indicate that some resonances between RMPs and lost passing particles may be of non-integer fractional order, rather than the usual integer order.

physics.plasm-ph↗

BPPChecker: An SMT-based Model Checker on Basic Parallel Processes(Full Version)

Program verification on concurrent programs is a big challenge due to general undecidable results. Petri nets and its extensions are used in most works. However, existing verifiers based on Petri nets are difficult to be complete and efficient. Basic Parallel Process (BPP), as a subclass of Petri nets, can be used as a model for describing and verifying concurrent programs with lower complexity. We propose and implement BPPChecker, the first model checker for verifying a subclass of CTL on BPP. We propose constraint-based algorithms for the problem of model checking on BPPs and handle formulas by SMT solver Z3. For EF operator, we reduce the model checking of EF-formulas to the satisfiability problem of existential Presburger formula. For EG operator, we provide a k-step bounded semantics and reduce the model checking of EG-formulas to the satisfiability problem of linear integer arithmetic. Besides, we give Actor Communicating System (ACS) the over-approximation BPP-based semantics and evaluate BPPChecker on ACSs generated from real Erlang programs. Experimental results show that BPPChecker performs more efficiently than the existing tools for a series of branching-time property verification problems of Erlang programs.

cs.LO↗

Essence of Factual Knowledge

Knowledge bases are collections of domain-specific and commonsense facts. Recently, the sizes of KBs are rocketing due to automatic extraction for knowledge and facts. For example, the number of facts in WikiData is up to 974 million! According to our observation, current KBs, especially domain KBs, show strong relevance in relations according to some topics. These patterns can be used to conclude and infer for part of facts in the KBs. Therefore, the original KBs can be minimzed by extracting patterns and essential facts.

cs.DB↗