arXiv subjects

Haoze Wu

Publications and source records attributed to Haoze Wu.

At least 37 records · Page 2Linked to original sources

arXiv2025

Efficiently Computing Compact Formal Explanations

Building on VeriX (Verified eXplainability, arXiv:2212.01051), a system for producing optimal verified explanations for machine learning models, we present VeriX+, which significantly improves both the size and the generation time of formal explanations. We introduce a bound propagation-based sensitivity technique to improve the size, and a binary search-based traversal with confidence ranking for improving time -- the two techniques are orthogonal and can be used independently or together. We also show how to adapt the QuickXplain algorithm to our setting to provide a trade-off between size and time. Experimental evaluations on standard benchmarks demonstrate significant improvements on both metrics, e.g., a size reduction of $38\%$ on the GTSRB dataset and a time reduction of $90\%$ on MNIST. We demonstrate that our approach is scalable to transformers and real-world scenarios such as autonomous aircraft taxiing and sentiment analysis. We conclude by showcasing several novel applications of formal explanations.

cs.LG↗

arXiv2025

Proof Minimization in Neural Network Verification

The widespread adoption of deep neural networks (DNNs) requires efficient techniques for verifying their safety. DNN verifiers are complex tools, which might contain bugs that could compromise their soundness and undermine the reliability of the verification process. This concern can be mitigated using proofs: artifacts that are checkable by an external and reliable proof checker, and which attest to the correctness of the verification process. However, such proofs tend to be extremely large, limiting their use in many scenarios. In this work, we address this problem by minimizing proofs of unsatisfiability produced by DNN verifiers. We present algorithms that remove facts which were learned during the verification process, but which are unnecessary for the proof itself. Conceptually, our method analyzes the dependencies among facts used to deduce UNSAT, and removes facts that did not contribute. We then further minimize the proof by eliminating remaining unnecessary dependencies, using two alternative procedures. We implemented our algorithms on top of a proof producing DNN verifier, and evaluated them across several benchmarks. Our results show that our best-performing algorithm reduces proof size by 37%-82% and proof checking time by 30%-88%, while introducing a runtime overhead of 7%-20% to the verification process itself.

cs.LO↗

arXiv2025

Satisfiability Modulo Theories for Verifying MILP Certificates

Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a ground formula that completely characterizes the validity of the algorithmic check, removing any ambiguities and imprecisions present in the specification. We formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified ground formula with the Satisfiability Modulo Theory Library (SMT-LIB) and check its validity. Our approach is solver-agnostic, and we test its viability using benchmark instances found in the literature.

cs.LO↗

arXiv2025

Scalable Synthesis and Verification of String Stable Neural Certificates for Interconnected Systems

Ensuring string stability is critical for the safety and efficiency of large-scale interconnected systems. Although learning-based controllers (e.g., those based on reinforcement learning) have demonstrated strong performance in complex control scenarios, their black-box nature hinders formal guarantees of string stability. To address this gap, we propose a novel verification and synthesis framework that integrates discrete-time scalable input-to-state stability (sISS) with neural network verification to formally guarantee string stability in interconnected systems. Our contributions are four-fold. First, we establish a formal framework for synthesizing and robustly verifying discrete-time scalable input-to-state stability (sISS) certificates for neural network-based interconnected systems. Specifically, our approach extends the notion of sISS to discrete-time settings, constructs neural sISS certificates, and introduces a verification procedure that ensures string stability while explicitly accounting for discrepancies between the true dynamics and their neural approximations. Second, we establish theoretical foundations and algorithms to scale the training and verification pipeline to large-scale interconnected systems. Third, we extend the framework to handle systems with external control inputs, thereby allowing the joint synthesis and verification of neural certificates and controllers. Fourth, we validate our approach in scenarios of mixed-autonomy platoons, drone formations, and microgrids. Numerical simulations show that the proposed framework not only guarantees sISS with minimal degradation in control performance but also efficiently trains and verifies controllers for large-scale interconnected systems under specific practical conditions.

eess.SY↗

arXiv2025

Mirage or Method? How Model-Task Alignment Induces Divergent RL Conclusions

Recent advances in applying reinforcement learning (RL) to large language models (LLMs) have led to substantial progress. In particular, a series of remarkable yet often counterintuitive phenomena have been reported in LLMs, exhibiting patterns not typically observed in traditional RL settings. For example, notable claims include that a single training example can match the performance achieved with an entire dataset, that the reward signal does not need to be very accurate, and that training solely with negative samples can match or even surpass sophisticated reward-based methods. However, the precise conditions under which these observations hold - and, critically, when they fail - remain unclear. In this work, we identify a key factor that differentiates RL observations: whether the pretrained model already exhibits strong Model-Task Alignment, as measured by pass@k accuracy on the evaluated task. Through a systematic and comprehensive examination of a series of counterintuitive claims, supported by rigorous experimental validation across different model architectures and task domains, our findings show that while standard RL training remains consistently robust across settings, many of these counterintuitive results arise only when the model and task already exhibit strong model-task alignment. In contrast, these techniques fail to drive substantial learning in more challenging regimes, where standard RL methods remain effective.

cs.LG↗

arXiv2025

Abstraction-Based Proof Production in Formal Verification of Neural Networks

Modern verification tools for deep neural networks (DNNs) increasingly rely on abstraction to scale to realistic architectures. In parallel, proof production is becoming a critical requirement for increasing the reliability of DNN verification results. However, current proofproducing verifiers do not support abstraction-based reasoning, creating a gap between scalability and provable guarantees. We address this gap by introducing a novel framework for proof-producing abstraction-based DNN verification. Our approach modularly separates the verification task into two components: (i) proving the correctness of an abstract network, and (ii) proving the soundness of the abstraction with respect to the original DNN. The former can be handled by existing proof-producing verifiers, whereas we propose the first method for generating formal proofs for the latter. This preliminary work aims to enable scalable and trustworthy verification by supporting common abstraction techniques within a formal proof framework.

cs.LO↗

arXiv2025

Cubing for Tuning

We are exploring the problem of building an automated reasoning procedure that adaptively tunes the high-level solving strategy for a given problem. There are two main distinctive characteristics of our approach: tuning is performed solely online, unlike the common use of tuning as an offline process; and tuning data comes exclusively from the given instance, so we do not rely on the availability of similar benchmarks and can work with unique challenging instances. Our approach builds on top of the divide-and-conquer paradigm that naturally serves partitioned sub-problems for an automated tuning algorithm to obtain a good solving strategy. We demonstrate performance improvement on two classes of important problems--SAT-solving and neural network verification--and show that our method can learn unconventional solving strategies in some cases.

cs.LO↗

arXiv2025

USM: Unbiased Survey Modeling for Limiting Negative User Experiences in Recommendation Systems

Reducing negative user experiences is essential for the success of recommendation platforms. Exposing users to inappropriate content could not only adversely affect users' psychological well-beings, but also potentially drive users away from the platform, sabotaging the platform's long-term success. However, recommendation algorithms tend to weigh more heavily on positive feedback signals due to the scarcity of negative ones, which may result in the neglect of valuable negative user feedback. In this paper, we propose an approach aimed at limiting negative user experiences. Our method primarily relies on distributing in-feed surveys to the users, modeling the users' feedback collected from the survey, and integrating the model predictions into the recommendation system. We further enhance the baseline survey model by integrating the Learning Hidden Unit Contributions module and the Squeeze-and-Excitation module. In addition, we strive to resolve the problem of response Bias by applying a survey-submit model; The A/B testing results indicate a reduction in survey sexual rate and survey inappropriate rate, ranging from -1.44\% to -3.9\%. Additionally, we compared our methods against an online baseline that does not incorporate our approach. The results indicate that our approach significantly reduces the report rate and dislike rate by 1\% to 2.27\% compared to the baseline, confirming the effectiveness of our methods in enhancing user experience. After we launched the survey model based our approach on our platform, the model is able to bring reductions of 1.75\%, 2.57\%, 2.06\% on reports, dislikes, survey inappropriate rate, respectively.

cs.IR↗

arXiv2025

Neural Network Verification is a Programming Language Challenge

Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

cs.PL↗

arXiv2024

The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results

This report summarizes the 5th International Verification of Neural Networks Competition (VNN-COMP 2024), held as a part of the 7th International Symposium on AI Verification (SAIV), that was collocated with the 36th International Conference on Computer-Aided Verification (CAV). VNN-COMP is held annually to facilitate the fair and objective comparison of state-of-the-art neural network verification tools, encourage the standardization of tool interfaces, and bring together the neural network verification community. To this end, standardized formats for networks (ONNX) and specification (VNN-LIB) were defined, tools were evaluated on equal-cost hardware (using an automatic evaluation pipeline based on AWS instances), and tool parameters were chosen by the participants before the final test sets were made public. In the 2024 iteration, 8 teams participated on a diverse set of 12 regular and 8 extended benchmarks. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this iteration of this competition.

cs.LG↗

arXiv2024

Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the ``black box'' nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.

cs.AI↗

arXiv2024

Safe and Reliable Training of Learning-Based Aerospace Controllers

In recent years, deep reinforcement learning (DRL) approaches have generated highly successful controllers for a myriad of complex domains. However, the opaque nature of these models limits their applicability in aerospace systems and safety-critical domains, in which a single mistake can have dire consequences. In this paper, we present novel advancements in both the training and verification of DRL controllers, which can help ensure their safe behavior. We showcase a design-for-verification approach utilizing k-induction and demonstrate its use in verifying liveness properties. In addition, we also give a brief overview of neural Lyapunov Barrier certificates and summarize their capabilities on a case study. Finally, we describe several other novel reachability-based approaches which, despite failing to provide guarantees of interest, could be effective for verification of other DRL systems, and could be of further interest to the community.

cs.AI↗

arXiv2024

GW-MoE: Resolving Uncertainty in MoE Router with Global Workspace Theory

Mixture-of-Experts (MoE) has been demonstrated as an efficient method to scale up models. By dynamically and sparsely selecting activated experts, MoE can effectively reduce computational costs. Despite the success, we observe that many tokens in the MoE models have uncertain routing results. These tokens have nearly equal scores for choosing each expert, and we demonstrate that this uncertainty can lead to incorrect selections. Inspired by the Global Workspace Theory (GWT), we propose a new fine-tuning method, GW-MoE, to address this issue. The core idea is to broadcast the uncertain tokens across experts during fine-tuning. Therefore, these tokens can acquire the necessary knowledge from any expert during inference and become less sensitive to the choice. GW-MoE does not introduce additional inference overhead. We validate that GW can mitigate the uncertain problem and consistently improve in different tasks (text classification, question answering, summarization, code generation, and mathematical problem solving) and model sizes (650M and 8B parameters).

cs.LG↗

arXiv2024

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its initial release.

cs.AI↗

arXiv2024

Lemur: Integrating Large Language Models in Automated Program Verification

The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.

cs.FL↗

arXiv2023

Towards Efficient Verification of Quantized Neural Networks

Quantization replaces floating point arithmetic with integer arithmetic in deep neural network models, providing more efficient on-device inference with less power and memory. In this work, we propose a framework for formally verifying properties of quantized neural networks. Our baseline technique is based on integer linear programming which guarantees both soundness and completeness. We then show how efficiency can be improved by utilizing gradient-based heuristic search methods and also bound-propagation techniques. We evaluate our approach on perception networks quantized with PyTorch. Our results show that we can verify quantized networks with better scalability and efficiency than the previous state of the art.

cs.LG↗

arXiv2023

VeriX: Towards Verified Explainability of Deep Neural Networks

We present VeriX (Verified eXplainability), a system for producing optimal robust explanations and generating counterfactuals along decision boundaries of machine learning models. We build such explanations and counterfactuals iteratively using constraint solving techniques and a heuristic based on feature-level sensitivity ranking. We evaluate our method on image recognition benchmarks and a real-world scenario of autonomous aircraft taxiing.

cs.LG↗

arXiv2023

Soy: An Efficient MILP Solver for Piecewise-Affine Systems

Piecewise-affine (PWA) systems are widely used for modeling and control of robotics problems including modeling contact dynamics. A common approach is to encode the control problem of the PWA system as a Mixed-Integer Convex Program (MICP), which can be solved by general-purpose off-the-shelf MICP solvers. To mitigate the scalability challenge of solving these MICP problems, existing work focuses on devising efficient and strong formulations of the problems, while less effort has been spent on exploiting their specific structure to develop specialized solvers. The latter is the theme of our work. We focus on efficiently handling one-hot constraints, which are particularly relevant when encoding PWA dynamics. We have implemented our techniques in a tool, Soy, which organically integrates logical reasoning, arithmetic reasoning, and stochastic local search. For a set of PWA control benchmarks, Soy solves more problems, faster, than two state-of-the-art MICP solvers.

cs.RO↗