Heterogeneous software systems, which often combine closed-source libraries with exported interfaces, embedded assembly, and components in multiple languages, present significant challenges for formal verification. Our prior work, Hetrify, addressed this by converting RISC-V binaries into semantically equivalent C code, making such programs amenable to verification. However, its unified memory model required frequent dynamic computation of stack addresses, which significantly increased the size of the generated logical formulas, along with high memory usage and longer verification times. To address this, we propose memory access specialization, a static analysis and transformation technique that recovers fixed stack offsets during binary conversion to reduce verification overhead. By replacing symbolic stack accesses with fixed-offset memory references, it eliminates dynamic pointer arithmetic and reduces symbolic encoding complexity. This technique is integrated into Hetrify+, an enhanced verification tool for heterogeneous programs. To validate the effectiveness of our approach, we conduct both formal analysis and extensive empirical evaluation. Formal analysis guarantees the correctness of our method. In our evaluation, Hetrify+ demonstrates the same verification accuracy as the original Hetrify on 100 low-level RISC-V assembly programs, achieving up to 2.5× speedup and 4.9× reduction in memory usage. For 30 large-scale heterogeneous programs that include binary-only components, Hetrify+ maintains a 100% success rate, reducing verification time by 1.9× and memory consumption by 1.2×. These results demonstrate that memory access specialization is key to scaling the verification of heterogeneous programs.

Recurrent Neural Networks (RNNs) are widely used in control system due to their dynamic capabilities. However, the control accuracy of RNN-based systems can be compromised by noise interference, and there has been little research on RNN-based control in disturbed multi-agent systems. To address this, we developed an enhanced Distributed RNN (DRNN) structure and proposed a Novel DRNN-based Control Protocol (NDRNN-CP). This enhancement involves introducing a time-delay component, allowing the protocol to adaptively learn noise variation patterns. As a result, the NDRNN-CP effectively resists various periodic noise interferences and achieves more precise control of each agent. Additionally, our optimized activation function ensures that all agents reach consensus within a predefined time. To demonstrate the advantages of NDRNN-CP, we conducted extensive experiments that confirmed its significant improvements in noise signal resistance and convergence performance.

The heterogeneous nature of contemporary software, comprising components like closed-source libraries, embedded assembly snippets, and modules written in multiple programming languages, leads to significant verification challenges. Currently, there are no mature and available methods to effectively address such problems. To bridge this gap, we propose a verification approach capable of effectively verifying heterogeneous programs. This approach is universally applicable. It theoretically supports the verification of any heterogeneous program that can be compiled into binary code, without being constrained by any specific programming language. The approach begins by compiling the entire program or its unverifiable segments into binary format. Under guarantees of semantic equivalence, these binaries are converted into verifiable C code, which can then be verified using existing C verification tools. Based on the RISC-V architecture, we developed the Hetrify tool to implement this verification approach. The tool is supported by rigorous mathematical proofs to ensure operational semantic equivalence between the converted C programs and their original counterparts. To validate our approach, we conducted verification experiments on 130 programs, including 100 assembly programs and 30 large heterogeneous programs with missing critical function source code, demonstrating the effectiveness of our approach.

Large language models (LLMs) have made significant strides in code generation but often struggle with API hallucination issues, especially for the third-party library. Existing approaches attempt to enhance LLMs by incorporating documentation. However, they face three main challenges: the introduction of irrelevant information that distracts the model; reliance solely on documentation that results in discrepancies between API descriptions and practical usage; and the absence of comprehensive error post-processing mechanisms. To address these challenges, we propose THINK11THINK's benchmark and code is available at https://github.com/Leah-Ljx/think., a knowledge injection method that leverages a custom API knowledge database with two phases: pre-execution enhancement and post-execution optimization. The former reduces irrelevant information and integrates multiple knowledge sources, while the latter identifies seven API error types and suggests three heuristic correction strategies. We manually construct a benchmark by collecting and filtering complex API-related tasks from GitHub to evaluate the effectiveness of our method. The experimental results demonstrate that our method can significantly improve the correctness of API usage in the context of LLMs. We reduce the error rate of programs from 61.18% to 16.64% for GPT-3.5 and from 41.49% to 5.58% for GPT-4o across tasks involving different libraries.

Automated evaluation of programming code on online platforms often relies on predefined test cases.However, due to limited test coverage, many programs receive full marks despite violating intended specifications.We present Maveric, a framework that combines large language models (LLMs) with formal verification to more rigorously assess code correctness.Maveric consists of four agents: a template generator that derives formal specifications from problem descriptions, a consistency checker that validates semantic alignment, a code analyzer that detects potential defects and synthesizes counterexamples, and a counterexample validator that formally verifies their validity.We evaluated Maveric on 100 full-score code submissions from 10 real-world programming tasks sourced from a widely used online education platform.Manual review identified 32 with functional defects.Maveric accurately detected 31 of these with no false positives, completing the evaluation of each program in under one minute.In contrast, LLM-only methods detected 25 defects but yielded 6 false positives, while formal verification alone found 23 and suffered frequent timeouts.Importantly, all defects reported by Maveric were supported by verifiable counterexamples, confirming their semantic violations.These results demonstrate Maveric's effectiveness and practicality for automated program evaluation in educational settings.

Code generation has advanced with large language models (LLMs), but LLMs still struggle with complex tasks, especially in competitive programming. These tasks require understanding complex problems, generating correct code that passes numerous test cases, and meeting tight time and memory limits. We observed that there are some critical hints provided by competition platforms, which often point to the most critical information needed to solve the problem, thus guiding participants to accurate solutions. Inspired by these observations, we propose TEACH1, an approach that tutors LLMs in solving competitive programming by combining critical hints with a structured Chain of Thought (CoT). The key insight of TEACH is to employ a domain-specialized hint generator that is fine-tuned on curated data from competitive programming platforms, enabling it to produce concise and targeted algorithmic hints. By integrating these hints into the reasoning process of LLMs, TEACH helps LLMs bridge the gap between complex tasks and solutions. Furthermore, TEACH simulates human problem-solving through a structured CoT that covers problem understanding, analysis, algorithm selection, and coding. We extensively evaluate TEACH on both proprietary (GPT-3.5, GPT-4o, Claude-3.5-Sonnet, Gemini-2.5-Flash) and open-source (DeepSeek-V3) LLMs. TEACH achieves up to 6.56 absolute (17.4% relative) gain in pass@1 on LeetCode, and demonstrates strong generalization to APPS and ASAC, with maximum pass@1 relative improvements of 17.6% and 26.9%, respectively. Furthermore, existing CoT methods with the hints generated from TEACH yield additional gains, demonstrating its compatibility and extensibility across models and prompting strategies.

Dynamic equations provide mathematical frameworks to capture the evolving behavior of systems, which is essential in various fields. While the zeroing neural network (ZNN) is one of the most effective real-time solvers for dynamic equations, it is highly susceptible to noise interference, which reduces the precision and reliability of solutions. Current research struggles to address more complex noise disturbances, particularly complex-valued and random noise. To overcome this limitation, this article introduces a set of self-learning operators with real-time correction ability to counteract noise interference and obtain a new self-learning noise-resistant ZNN (SLNR-ZNN). The operators within the SLNR-ZNN model adaptively learn the physical forms of noise, utilizing the noise’s derivative properties, through continuous system oscillations to enhance noise tolerance and improve the accuracy of dynamic equation resolution. Theoretical analysis and experimental validation show that SLNR-ZNN effectively resolves linear and nonlinear dynamic equations under various types of noise, including constant, harmonic, complex spectral, and Gaussian white noise. Compared to existing ZNN models, SLNR-ZNN achieves comparable convergence rates and simultaneously maintains significantly lower steady-state errors, which are often reduced by nearly an order of magnitude under noise. Furthermore, simulation experiments demonstrate that the SLNR-ZNN-based control protocol achieves state consensus in leader-following multiagent systems and enables trajectory tracking in the UR5 robotic arm with millimeter-level accuracy, even under composite disturbances. These results highlight its practical value and robustness in robotic control applications.

In this article, a novel distributed gradient neural network (DGNN) with predefined-time convergence (PTC) is proposed to solve consensus problems widely existing in multiagent systems (MASs). Compared with previous gradient neural networks (GNNs) for optimization and computation, the proposed DGNN model works in a nonfully connected way, in which each neuron only needs the information of neighbor neurons to converge to the equilibrium point. The convergence and asymptotic stability of the DGNN model are proved according to the Lyapunov theory. In addition, based on a relatively loose condition, three novel nonlinear activation functions are designed to speedup the DGNN model to PTC, which is proved by rigorous theory. Computer numerical results further verify the effectiveness, especially the PTC, of the proposed nonlinearly activated DGNN model to solve various consensus problems of MASs. Finally, a practical case of the directional consensus is presented to show the feasibility of the DGNN model and a corresponding connectivity-testing example is given to verify the influence on the convergence speed.

In this article, a low-order zeroing neural network (LZNN), a high-order ZNN (HZNN), and a variable-parameter ZNN (VZNN) are designed and applied to the time-changing Cholesky decomposition of any positive-definite matrix, where the LZNN and HZNN models are generated based on the traditional and high-order evolutionary formulas, respectively. In addition, a new activation function (N-Acf) is applied to the LZNN, HZNN, and VZNN models to improve the convergence and robustness. Importantly, the LZNN and HZNN models activated by the N-Acf have faster predefined-time convergence velocity when solving the time-changing Cholesky decomposition problem of any positive-definite matrix, which is demonstrated via theoretical analysis and numerical experiments. Finally, in light of empirical and theoretical evidence, it can be established that the solution model of the VZNN model is able to undergo convergence to the theoretical solution of Cholesky decomposition despite the presence of interposing noise.

Two nonlinear zeroing neural network (ZNN) models with prescribed-time convergence for time-dependent matrix LR and QR factorization are proposed in this article. To do so, two algorithms and two error functions are constructed to transform the time-dependent matrix LR and QR factorization problems into time-dependent linear equation systems, respectively. Simultaneously, a new activation function is introduced based on the initial ZNN models for the prescribed-time convergence of models. The excellent performance (robustness and convergence) of the two proposed ZNN models are analyzed theoretically. Furthermore, the prescribed-time convergence and antinoise abilities of the proposed ZNN models are well demonstrated in numerical experiments. Finally, the proposed ZNN model is applied to the moving target location problem, and the results show that the location error is at the millimeter level.

In this article, considering the effectiveness and efficiency in solving time-varying problems, a new zeroing neural network (ZNN) is proposed to solve time-varying linear equations with column full rank coefficient matrix. In addition, two novel nonlinear activation functions are developed to enhance the comprehensive performance of the ZNN model. It is demonstrated through theoretical analysis and numerical experiments that the nonlinear activated ZNN model has better noise immunity, and faster prescribed-time convergence speed. Finally, the ZNN method is successfully applied to 2-D and 3-D dynamic positioning, with lower positioning error than the traditional pseudoinverse method.

In order to improve the effect of the Exp-Sign activation function (ESAF) and the Sinh-Sign activation function (SSAF) on the convergence and robustness of the zeroing neural network (ZNN) model, two fuzzy adaptive activation functions, named FAESAF and FASSAF, are constructed by using a Mamdani fuzzy logic controller (MFLC) in this article. Thus, a novel ZNN with the FAESAF and the FASSAF is proposed to solve the time-varying linear matrix equation. Different from the ESAF and the SSAF, whose parameters are fixed, the newly constructed FAESAF and FASSAF have an adaptive property, which comes from the fact that their parameters are intelligently generated by the MFLC according to the error norm of the ZNN model. In order to highlight the superior predefined time convergence and robustness of the corresponding ZNN model with the FAESAF and the FASSAF, several theorems are provided, and the corresponding proof is given in detail. Furthermore, the ESAF and the SSAF with different values of parameters are used as a comparison in numerical experiments to verify the superior performance of the FAESAF and the FASSAF. From theoretical analysis and numerical results, we can conclude that the ZNN model with the FAESAF and the FASSAF has better predefined time convergence and robustness compared to the ZNN model with the ESAF and the SSAF under the same conditions.