Aug 2026· ACM Transactions on Software Engineering and Methodology· 0 citations· 101 references
TL;DR
VeRe is proposed, a verification-guided repair framework that leverages linear relaxation to precisely and efficiently estimate the repair significance of neurons and synthesizes ideal intervals that provide sound guarantees for correct behaviors, thereby facilitating surgical and targeted adjustments of neuron parameters to rectify faulty behaviors.
Abstract
Neural network repair aims to fix the ‘bugs’ of neural networks by modifying the model's architecture or parameters. However, due to the data-driven nature of neural networks, it is difficult to explain the relationship between internal neurons and erroneous behaviors, making further repair challenging. While several work exists to identify responsible neurons based on gradient or causality analysis, their effectiveness heavily rely on the quality of available ‘bugged’ data and multiple heuristics. Consequently, achieving precise localization and targeted repair remains a significant challenge, particularly in data-scarce scenarios. In this work, we address the issue utilizing the power of formal verification. Specifically, we propose VeRe, a verification-guided repair framework that leverages linear relaxation to precisely and efficiently estimate the repair significance of neurons. Based on the linear bounds, VeRe synthesizes ideal intervals that provide sound guarantees for correct behaviors, thereby facilitating surgical and targeted adjustments of neuron parameters to rectify faulty behaviors. We evaluated VeRe on various repair tasks, and results show that VeRe consistently achieves superior repair success rates and high generalization with negligible impact on original performance. Notably, VeRe exhibits a significantly lower dependency on repair data than existing baselines, effectively removing faulty behaviors even in data-restricted scenarios.
Hardware verification of the register transfer level (RTL) designs is a critical step in the development of complex digital circuits, ensuring their functional correctness, performance, and reliability. Within this crucial process, bug localization is an essential component for precisely identifying the root causes of design errors. Dynamic bug localization (DBL) stands out as an efficient and automatic approach to locate bug source code by calculating statement suspiciousness based on execution traces. However, DBL methods rely solely on coverage information and simplistic statistical formulas to compute suspiciousness, which has been criticized for their limited precision and inadequate reduction of debugging effort. In this paper, we propose MulFetFL: a multi-features deep learning based bug localization for RTL designs. MulFetFL begins by extracting three multimodal features: abstract syntax tree (AST) features, signal features, and timing features from designs. It then employs Graph Attention Networks (GAT) to enhance node representations. A cross-modal attention mechanism is subsequently applied to fuse these complementary features from different modalities. Finally, the fused features are passed through a multi-layer perceptron (MLP) to compute the suspiciousness score for each statement. Experimental results show that MulFetFL effectively locates 293, 295 and 298 bugs within Top-1/Top-3/Top-5 ranks, significantly outperforming state-of-the-art bug localization methods across a range of benchmark designs.
A novel general neural network repair paradigm termed NCCDA (Neuron-wise Class-Conditional Distribution Alignment), which theoretically prove a generalization error bound under small-sample settings based on Rademacher complexity, providing formal guarantees.
Liming Bao, Yan Wang, Tao Sun· Proceedings of the 32nd ACM...· 0 citations
A branch-and-bound framework to mitigate the issue of verifying relational specifications against relational specifications, which iteratively splits the problem until all sub-problems are verified, and devise a relational neuron selection strategy based on the dual formulation of the verification problem.
Kota Fukuda, Zhenya Zhang, Guanqin Zhang et al.· 0 citations
To ensure the overall quality of AI-enabled software, not only traditional software components but also AI components need to be tested and repaired. Among AI components, Transformer models are increasingly integrated into software systems, which makes their misbehaviors critical. Although prior work in the software engineering community has proposed deep neural network (DNN) repair methods, most overlook Transformer-specific structures. We propose RepTran, a search-based repair method for Transformer models. It targets their feed-forward networks (FFNs), which play a central role in the architecture. RepTran identifies suspicious weights by combining two types of scores: a variance-based neuron score and an existing bidirectional score. It then iteratively optimizes these weights using differential evolution. Our evaluation includes 18 fault benchmarks constructed from CIFAR-100 and Tiny-ImageNet. We compare RepTran against three baselines: random weight selection, Arachne (a state-of-the-art DNN repair method), and ArachneW, which enables Arachne to control the number of selected weights. RepTran achieved an average repair rate of 74.7%, statistically outperforming random selection and Arachne across all benchmarks. Effect size analysis revealed that RepTran achieved higher repair rates than ArachneW regardless of the number of selected weights. These results suggest that RepTran is effective for enhancing the reliability of AI-enabled software.
Yuta Ishimoto, Paolo Arcaini, Fuyuki Ishikawa et al.· arXiv.org· 0 citations
Modern software development increasingly integrates neural models such as code completion engines, automated refactoring systems, and learned optimization modules into traditional codebases, creating hybrid environments commonly referred to as neural-augmented codebases. While these systems achieve significant productivity gains, debugging them presents unique challenges due to the opaque reasoning processes of neural components. Conventional fault localization techniques are insufficient, as they cannot effectively attribute errors originating from model-generated code, neural decision boundaries, or interactions between learned and symbolic components. This paper proposes an explainable fault localization framework that combines program analysis, runtime tracing, and interpretable machine learning techniques to identify, rank, and justify the root causes of failures in neural-augmented codebases. By integrating explainability mechanisms such as attention heatmaps, causal dependency graphs, and interpretable embeddings, the framework enhances developer trust, reduces debugging cost, and provides actionable diagnostic insights. Experimental evaluation on real-world hybrid systems demonstrates improved fault detection accuracy, reduced false positives, and higher interpretability scores compared to state-of-the-art approaches. The results show that explainability is not merely an auxiliary feature, but a critical enabler of scalable, safe adoption of neural components in modern software engineering workflows.
Lei Weing· International Journal of App...· 0 citations
This study shows that template subsumption rates can vary widely across scenarios, and presents FastCert, a novel technique for automatically distributing templates across neural network layers to increase performance impact, eschewing templates entirely if they are unlikely to produce a speedup.
Kanak Das, Shubham Ugare, B. E. Chang et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
