arXiv subjects

Kai Jia

Publications and source records attributed to Kai Jia.

33 records · Page 2Linked to original sources

arXiv2023

Sound Explanation for Trustworthy Machine Learning

We take a formal approach to the explainability problem of machine learning systems. We argue against the practice of interpreting black-box models via attributing scores to input components due to inherently conflicting goals of attribution-based interpretation. We prove that no attribution algorithm satisfies specificity, additivity, completeness, and baseline invariance. We then formalize the concept, sound explanation, that has been informally adopted in prior work. A sound explanation entails providing sufficient information to causally explain the predictions made by a system. Finally, we present the application of feature selection as a sound explanation for cancer prediction models to cultivate trust among clinicians.

cs.LG↗

arXiv2023

Effective Neural Network $L_0$ Regularization With BinMask

$L_0$ regularization of neural networks is a fundamental problem. In addition to regularizing models for better generalizability, $L_0$ regularization also applies to selecting input features and training sparse neural networks. There is a large body of research on related topics, some with quite complicated methods. In this paper, we show that a straightforward formulation, BinMask, which multiplies weights with deterministic binary masks and uses the identity straight-through estimator for backpropagation, is an effective $L_0$ regularizer. We evaluate BinMask on three tasks: feature selection, network sparsification, and model regularization. Despite its simplicity, BinMask achieves competitive performance on all the benchmarks without task-specific tuning compared to methods designed for each task. Our results suggest that decoupling weights from mask optimization, which has been widely adopted by previous work, is a key component for effective $L_0$ regularization.

cs.LG↗

arXiv2023

Delving Deep into Pixel Alignment Feature for Accurate Multi-view Human Mesh Recovery

Regression-based methods have shown high efficiency and effectiveness for multi-view human mesh recovery. The key components of a typical regressor lie in the feature extraction of input views and the fusion of multi-view features. In this paper, we present Pixel-aligned Feedback Fusion (PaFF) for accurate yet efficient human mesh recovery from multi-view images. PaFF is an iterative regression framework that performs feature extraction and fusion alternately. At each iteration, PaFF extracts pixel-aligned feedback features from each input view according to the reprojection of the current estimation and fuses them together with respect to each vertex of the downsampled mesh. In this way, our regressor can not only perceive the misalignment status of each view from the feedback features but also correct the mesh parameters more effectively based on the feature fusion on mesh vertices. Additionally, our regressor disentangles the global orientation and translation of the body mesh from the estimation of mesh parameters such that the camera parameters of input views can be better utilized in the regression process. The efficacy of our method is validated in the Human3.6M dataset via comprehensive ablation experiments, where PaFF achieves 33.02 MPJPE and brings significant improvements over the previous best solutions by more than 29%. The project page with code and video results can be found at https://kairobo.github.io/PaFF/.

cs.CV↗

arXiv2022

On the Impact of Player Capability on Congestion Games

We study the impact of player capability on social welfare in congestion games. We introduce a new game, the Distance-bounded Network Congestion game (DNC), as the basis of our study. DNC is a symmetric network congestion game with a bound on the number of edges each player can use. We show that DNC is PLS-complete in contrast to standard symmetric network congestion games which are in P. To model different player capabilities, we propose using programs in a Domain-Specific Language (DSL) to compactly represent player strategies. We define a player's capability as the maximum size of the programs they can use. We introduce two variants of DNC with accompanying DSLs representing the strategy spaces. We propose four capability preference properties to characterize the impact of player capability on social welfare at equilibrium. We then establish necessary and sufficient conditions for the four properties in the context of our DNC variants. Finally, we study a specific game where we derive exact expressions of the social welfare in terms of the capability bound. This provides examples where the social welfare at equilibrium increases, stays the same, or decreases as players become more capable.

cs.GT↗

arXiv2022

Mixed Capability Games

We present a new class of strategic games, mixed capability games, as a foundation for studying how different player capabilities impact the dynamics and outcomes of strategic games. We analyze the impact of different player capabilities via a capability transfer function that characterizes the payoff of each player at equilibrium given capabilities for all players in the game. In this paper, we model a player's capability as the size of the strategy space available to that player. We analyze a mixed capability variant of the Gold and Mines Game recently proposed by Yang et al. and derive its capability transfer function in closed form.

cs.GT↗

arXiv2022

A Less Uncertain Sampling-Based Method of Batch Bayesian Optimization

This paper presents a method called sampling-computation-optimization (SCO) to design batch Bayesian optimization. SCO does not construct new high-dimensional acquisition functions but samples from the existing one-site acquisition function to obtain several candidate samples. To reduce the uncertainty of the sampling, the general discrepancy is computed to compare these samples. Finally, the genetic algorithm and switch algorithm are used to optimize the design. Several strategies are used to reduce the computational burden in the SCO. From the numerical results, the SCO designs were less uncertain than those of other sampling-based methods. As for application in batch Bayesian optimization, SCO can find a better solution when compared with other batch methods in the same dimension and batch size. In addition, it is also flexible and can be adapted to different one-site methods. Finally, a complex experimental case is given to illustrate the application value and scenario of SCO method.

math.OC↗

arXiv2021

Exploiting Verified Neural Networks via Floating Point Numerical Error

Researchers have developed neural network verification algorithms motivated by the need to characterize the robustness of deep neural networks. The verifiers aspire to answer whether a neural network guarantees certain properties with respect to all inputs in a space. However, many verifiers inaccurately model floating point arithmetic but do not thoroughly discuss the consequences. We show that the negligence of floating point error leads to unsound verification that can be systematically exploited in practice. For a pretrained neural network, we present a method that efficiently searches inputs as witnesses for the incorrectness of robustness claims made by a complete verifier. We also present a method to construct neural network architectures and weights that induce wrong results of an incomplete verifier. Our results highlight that, to achieve practically reliable verification of neural networks, any verification system must accurately (or conservatively) model the effects of any floating point computations in the network inference or verification system.

cs.LG↗

arXiv2021

Verifying Low-dimensional Input Neural Networks via Input Quantization

Deep neural networks are an attractive tool for compressing the control policy lookup tables in systems such as the Airborne Collision Avoidance System (ACAS). It is vital to ensure the safety of such neural controllers via verification techniques. The problem of analyzing ACAS Xu networks has motivated many successful neural network verifiers. These verifiers typically analyze the internal computation of neural networks to decide whether a property regarding the input/output holds. The intrinsic complexity of neural network computation renders such verifiers slow to run and vulnerable to floating-point error. This paper revisits the original problem of verifying ACAS Xu networks. The networks take low-dimensional sensory inputs with training data provided by a precomputed lookup table. We propose to prepend an input quantization layer to the network. Quantization allows efficient verification via input state enumeration, whose complexity is bounded by the size of the quantization space. Quantization is equivalent to nearest-neighbor interpolation at run time, which has been shown to provide acceptable accuracy for ACAS in simulation. Moreover, our technique can deliver exact verification results immune to floating-point error if we directly enumerate the network outputs on the target inference implementation or on an accurate simulation of the target implementation.

cs.LG↗

arXiv2021

Deep Retrieval: Learning A Retrievable Structure for Large-Scale Recommendations

One of the core problems in large-scale recommendations is to retrieve top relevant candidates accurately and efficiently, preferably in sub-linear time. Previous approaches are mostly based on a two-step procedure: first learn an inner-product model, and then use some approximate nearest neighbor (ANN) search algorithm to find top candidates. In this paper, we present Deep Retrieval (DR), to learn a retrievable structure directly with user-item interaction data (e.g. clicks) without resorting to the Euclidean space assumption in ANN algorithms. DR's structure encodes all candidate items into a discrete latent space. Those latent codes for the candidates are model parameters and learnt together with other neural network parameters to maximize the same objective function. With the model learnt, a beam search over the structure is performed to retrieve the top candidates for reranking. Empirically, we first demonstrate that DR, with sub-linear computational complexity, can achieve almost the same accuracy as the brute-force baseline on two public datasets. Moreover, we show that, in a live production recommendation system, a deployed DR approach significantly outperforms a well-tuned ANN baseline in terms of engagement metrics. To the best of our knowledge, DR is among the first non-ANN algorithms successfully deployed at the scale of hundreds of millions of items for industrial recommendation systems.

cs.IR↗

arXiv2021

SANM: A Symbolic Asymptotic Numerical Solver with Applications in Mesh Deformation

Solving nonlinear systems is an important problem. Numerical continuation methods efficiently solve certain nonlinear systems. The Asymptotic Numerical Method (ANM) is a powerful continuation method that usually converges faster than Newtonian methods. ANM explores the landscape of the function by following a parameterized solution curve approximated with a high-order power series. Although ANM has successfully solved a few graphics and engineering problems, prior to our work, applying ANM to new problems required significant effort because the standard ANM assumes quadratic functions, while manually deriving the power series expansion for nonquadratic systems is a tedious and challenging task. This paper presents a novel solver, SANM, that applies ANM to solve symbolically represented nonlinear systems. SANM solves such systems in a fully automated manner. SANM also extends ANM to support many nonquadratic operators, including intricate ones such as singular value decomposition. Furthermore, SANM generalizes ANM to support the implicit homotopy form. Moreover, SANM achieves high computing performance via optimized system design and implementation. We deploy SANM to solve forward and inverse elastic force equilibrium problems and controlled mesh deformation problems with a few constitutive models. Our results show that SANM converges faster than Newtonian solvers, requires little programming effort for new problems, and delivers comparable or better performance than a hand-coded, specialized ANM solver. While we demonstrate on mesh deformation problems, SANM is generic and potentially applicable to many tasks.

math.NA↗

arXiv2021

On a Conjecture of Bahri-Xu

In order to study the Yamabe changing-sign problem, Bahri and Xu proposed a conjecture which is a universal inequality for $p$ points in $\mathbb R^m$. They have verified the conjecture for $p\leq3$. In this paper, we first simplify this conjecture by giving two sufficient and necessary conditions inductively. Then we prove the conjecture for the basic case $m=1$ with arbitrary $p$. In addition, for the cases when $p=4,5$ and $m\geq2$, we manage to reduce them to the basic case $m=1$ and thus prove them as well.

math.CA↗

arXiv2020

Efficient Exact Verification of Binarized Neural Networks

Concerned with the reliability of neural networks, researchers have developed verification techniques to prove their robustness. Most verifiers work with real-valued networks. Unfortunately, the exact (complete and sound) verifiers face scalability challenges and provide no correctness guarantees due to floating point errors. We argue that Binarized Neural Networks (BNNs) provide comparable robustness and allow exact and significantly more efficient verification. We present a new system, EEV, for efficient and exact verification of BNNs. EEV consists of two parts: (i) a novel SAT solver that speeds up BNN verification by natively handling the reified cardinality constraints arising in BNN encodings; and (ii) strategies to train solver-friendly robust BNNs by inducing balanced layer-wise sparsity and low cardinality bounds, and adaptively cancelling the gradients. We demonstrate the effectiveness of EEV by presenting the first exact verification results for L-inf-bounded adversarial robustness of nontrivial convolutional BNNs on the MNIST and CIFAR10 datasets. Compared to exact verification of real-valued networks of the same architectures on the same tasks, EEV verifies BNNs hundreds to thousands of times faster, while delivering comparable verifiable accuracy in most cases.

cs.AI↗

arXiv2019

Optimal Sliced Latin Hypercube Designs with Slices of Arbitrary Run Sizes

Sliced Latin hypercube designs (SLHDs) are widely used in computer experiments with both quantitative and qualitative factors and in batches. Optimal SLHDs achieve better space-filling property on the whole experimental region. However, most existing methods for constructing optimal SLHDs have restriction on the run sizes. In this paper, we propose a new method for constructing SLHDs with arbitrary run sizes, and a new combined space-filling measurement describing the space-filling property for both the whole design and its slices. Furthermore, we develop general algorithms to search the optimal SLHD with arbitrary run sizes under the proposed measurement. Examples are presented to illustrate that effectiveness of the proposed methods.

math.ST↗

arXiv2018

MegDet: A Large Mini-Batch Object Detector

The improvements in recent CNN-based object detection works, from R-CNN [11], Fast/Faster R-CNN [10, 31] to recent Mask R-CNN [14] and RetinaNet [24], mainly come from new network, new framework, or novel loss design. But mini-batch size, a key factor in the training, has not been well studied. In this paper, we propose a Large MiniBatch Object Detector (MegDet) to enable the training with much larger mini-batch size than before (e.g. from 16 to 256), so that we can effectively utilize multiple GPUs (up to 128 in our experiments) to significantly shorten the training time. Technically, we suggest a learning rate policy and Cross-GPU Batch Normalization, which together allow us to successfully train a large mini-batch detector in much less time (e.g., from 33 hours to 4 hours), and achieve even better accuracy. The MegDet is the backbone of our submission (mmAP 52.5%) to COCO 2017 Challenge, where we won the 1st place of Detection task.

cs.CV↗

arXiv2016

Theano: A Python framework for fast computation of mathematical expressions

Theano is a Python library that allows to define, optimize, and evaluate mathematical expressions involving multi-dimensional arrays efficiently. Since its introduction, it has been one of the most used CPU and GPU mathematical compilers - especially in the machine learning community - and has shown steady performance improvements. Theano is being actively and continuously developed since 2008, multiple frameworks have been built on top of it and it has been used to produce many state-of-the-art machine learning models. The present article is structured as follows. Section I provides an overview of the Theano software and its community. Section II presents the principal features of Theano and how to use them, and compares them with other similar projects. Section III focuses on recently-introduced functionalities and improvements. Section IV compares the performance of Theano against Torch7 and TensorFlow on several machine learning models. Section V discusses current limitations of Theano and potential ways of improving it.

cs.SC↗