• We consider the problem of how decision making can be fair when the underlying probabilistic model of the world is not known with certainty. We argue that recent notions of fairness in machine learning need to explicitly incorporate parameter uncertainty, hence we introduce the notion of {\em Bayesian fairness} as a suitable candidate for fair decision rules. Using balance, a definition of fairness introduced by Kleinberg et al (2016), we show how a Bayesian perspective can lead to well-performing, fair decision rules even under high uncertainty.
  • We consider partially-specified optimization problems where the goal is to actively, but efficiently, acquire missing information about the problem in order to solve it. An algorithm designer wishes to solve a linear program (LP), $\max \mathbf{c}^T \mathbf{x}$ s.t. $\mathbf{A}\mathbf{x} \leq \mathbf{b}, \mathbf{x} \ge \mathbf{0}$, but does not initially know some of the parameters. The algorithm can iteratively choose an unknown parameter and gather information in the form of a noisy sample centered at the parameter's (unknown) value. The goal is to find an approximately feasible and optimal solution to the underlying LP with high probability while drawing a small number of samples. We focus on two cases. (1) When the parameters $\mathbf{c}$ of the objective are initially unknown, we take an information-theoretic approach and give roughly matching upper and lower sample complexity bounds, with an (inefficient) successive-elimination algorithm. (2) When the parameters $\mathbf{b}$ of the constraints are initially unknown, we propose an efficient algorithm combining techniques from the ellipsoid method for LP and confidence-bound approaches from bandit algorithms. The algorithm adaptively gathers information about constraints only as needed in order to make progress. We give sample complexity bounds for the algorithm and demonstrate its improvement over a naive approach via simulation.
  • The performance of penalized likelihood approaches depends profoundly on the selection of the tuning parameter; however, there is no commonly agreed-upon criterion for choosing the tuning parameter. Moreover, penalized likelihood estimation based on a single value of the tuning parameter suffers from several drawbacks. This article introduces a novel approach for feature selection based on the entire solution paths rather than the choice of a single tuning parameter, which significantly improves the accuracy of the selection. Moreover, the approach allows for feature selection using ridge or other strictly convex penalties. The key idea is to classify variables as relevant or irrelevant at each tuning parameter and then to select all of the variables which have been classified as relevant at least once. We establish the theoretical properties of the method, which requires significantly weaker conditions than existing methods in the literature. We also illustrate the advantages of the proposed approach with simulation studies and a data example.
  • It is an exciting task to recover the scene's 3d-structure and camera pose from the video sequence. Most of the current solutions divide it into two parts, monocular depth recovery and camera pose estimation. The monocular depth recovery is often studied as an independent part, and a better depth estimation is used to solve the pose. While camera pose is still estimated by traditional SLAM (Simultaneous Localization And Mapping) methods in most cases. The use of unsupervised method for monocular depth recovery and pose estimation has benefited from the study of [1] and achieved good results. In this paper, we improve the method of [1]. Our emphasis is laid on the improvement of the idea and related theory, introducing a more reasonable inter frame constraints and finally synthesize the camera trajectory with inter frame pose estimation in the unified world coordinate system. And our results get better performance.
  • We study information elicitation without verification (IEWV) and ask the following question: Can we achieve truthfulness in dominant strategy in IEWV? This paper considers two elicitation settings. The first setting is when the mechanism designer has access to a random variable that is a noisy or proxy version of the ground truth, with known biases. The second setting is the standard peer prediction setting where agents' reports are the only source of information that the mechanism designer has. We introduce surrogate scoring rules (SSR) for the first setting, which use the noisy ground truth to evaluate quality of elicited information, and show that SSR achieve truthful elicitation in dominant strategy. Built upon SSR, we develop a multi-task mechanism, dominant truth serum (DTS), to achieve truthful elicitation in dominant strategy when the mechanism designer only has access to agents' reports (the second setting). The method relies on an estimation procedure to accurately estimate the average bias in the reports of other agents. With the accurate estimation, a random peer agent's report serves as a noisy ground truth and SSR can then be applied to achieve truthfulness in dominant strategy. A salient feature of SSR and DTS is that they both quantify the quality or value of information despite lack of ground truth, just as proper scoring rules do for the with verification setting. Our work complements both the strictly proper scoring rule literature by solving the case where the mechanism designer only has access to a noisy or proxy version of the ground truth, and the peer prediction literature by achieving truthful elicitation in dominant strategy.
  • To address modeling problems of brain-inspired intelligence, this thesis is focused on researching in the semantic-oriented framework design for image, audio, language and video. The Multimedia Neural Cognitive Computing (MNCC) model was designed based on the nervous mechanism and cognitive architecture. Furthermore, the semantic-oriented hierarchical Cross-media Neural Cognitive Computing (CNCC) framework was proposed based on MNCC, and formal description and analysis for CNCC was given. It would effectively improve the performance of semantic processing for multimedia information, and has far-reaching significance for exploration and realization brain-inspired computing.
  • Considering the use of Fully Connected (FC) layer limits the performance of Convolutional Neural Networks (CNNs), this paper develops a method to improve the coupling between the convolution layer and the FC layer by reducing the noise in Feature Maps (FMs). Our approach is divided into three steps. Firstly, we separate all the FMs into n blocks equally. Then, the weighted summation of FMs at the same position in all blocks constitutes a new block of FMs. Finally, we replicate this new block into n copies and concatenate them as the input to the FC layer. This sharing of FMs could reduce the noise in them apparently and avert the impact by a particular FM on the specific part weight of hidden layers, hence preventing the network from overfitting to some extent. Using the Fermat Lemma, we prove that this method could make the global minima value range of the loss function wider, by which makes it easier for neural networks to converge and accelerates the convergence process. This method does not significantly increase the amounts of network parameters (only a few more coefficients added), and the experiments demonstrate that this method could increase the convergence speed and improve the classification performance of neural networks.
  • In this paper, we proposed a class of extremely efficient CNN models, MobileFaceNets, which use less than 1 million parameters and are specifically tailored for high-accuracy real-time face verification on mobile and embedded devices. We first make a simple analysis on the weakness of common mobile networks for face verification. The weakness has been well overcome by our specifically designed MobileFaceNets. Under the same experimental conditions, our MobileFaceNets achieve significantly superior accuracy as well as more than 2 times actual speedup over MobileNetV2. After trained by ArcFace loss on the refined MS-Celeb-1M from scratch, our single MobileFaceNet model of 4.0MB size achieves 99.55% face verification accuracy on LFW and 92.59% TAR@FAR1e-6 on MegaFace Challenge 1, which is even comparable to some state-of-the-art big CNN models of hundreds MB size. The fastest one of our MobileFaceNets has an actual inference time of 18 milliseconds on a mobile phone. Our experiments on LFW, AgeDB, and MegaFace show that our MobileFaceNets achieve significantly improved efficiency compared with state-of-the-art lightweight and mobile CNNs for face verification.
  • An experiment for $p(^{14}\rm{C}$,$^{14}\rm{C}^{*}\rightarrow^{10}\rm{Be}+\alpha)\mathit{p}$ inelastic excitation and decay was performed in inverse kinematics at a beam energy of 25.3 MeV/u. A series of $^{14}\rm{C}$ excited states, including a new one at 18.3(1) MeV, were observed which decay to various states of the final nucleus of $^{10}\rm{Be}$. A specially designed telescope-system, installed around the zero degree, played an essential role in detecting the resonant states near the $\alpha$-separation threshold. A state at 14.1(1) MeV is clearly identified, being consistent with the predicted band-head of the molecular rotational band characterized by the $\pi$-bond linear-chain-configuration. Further clarification of the properties of this exotic state is suggested by using appropriate reaction tools.
  • Transition metal perovskite chalcogenides (TMPC) are a new class of semiconductor materials with broad tunability of physical properties due to their chemical and structural flexibility. Theoretical calculations show that band gaps of TMPCs are tunable from Far IR to UV spectrum. Amongst these materials, more than a handful of materials have energy gap and very high absorption coefficients, which are appropriate for optoelectronic applications, especially solar energy conversion. Despite several promising theoretical predictions, very little experimental studies on their physical properties are currently available, especially optical properties. We report a new synthetic route towards high quality bulk ceramic TMPCs and systematic study of three phases, SrZrS3 in two different room temperature stabilized phases and one of BaZrS3. All three materials were synthesized with a catalyzed solid-state reaction process in sealed ampoules. Structural and chemical characterizations establish high quality of the samples, which is confirmed by the intense room temperature photoluminescence (PL) spectra showing direct band gaps around 1.53eV, 2.13eV and 1.81eV respectively. The potential of these materials for solar energy conversion was evaluated by measurement of PL quantum efficiency and estimate of quasi Fermi level splitting.
  • The Alternating Direction Method of Multipliers (ADMM) decoding of Low Density Parity Check (LDPC) codes has received many attentions due to its excellent performance at the error floor region. In this paper, we develop a parameter-free decoder based on Linear Program (LP) decoding by replacing the binary constraint with the intersection of a box and an $\ell_p$ sphere. An efficient $\ell_2$-box ADMM is designed to handle this model in a distributed fashion. Numerical experiments demonstrate that our decoder attains better adaptability to different Signal-to-Noise Ratio and channels.
  • Rust is a system programming language designed for providing better memory safety whilst maintaining performance. Formalizing Rust is a necessary way to prove its memory safety and construct formal analysis tools for Rust. In this paper, we introduce an executable formal semantics of Rust using K-Framework (K), called K-Rust. K-Rust includes two parts: (1) the formal model of the ownership system, which is one of Rust's most compelling features for realizing its memory safety and zero-coast abstraction; (2) the formal operational semantics of Rust based on a core-language. The formal models are tested against various programs and compared with Rust's compiler to ensure the semantics consistency between K-Rust and the compiler. Through the construction of K-Rust we detected inconsistencies of the ownership mechanism between the Rust compiler and the specification in The Rust Programming Language.
  • Understanding intertrochanteric fracture distribution is an important topic in orthopaedics due to its high morbidity and mortality. The intertrochanteric fracture can contain high dimensional information including complicated 3D fracture lines, which often make it difficult to visualize or to obtain valuable statistics for clinical diagnosis and prognosis applications. This paper proposed a map projection technique to map the high dimensional information into a 2D parametric space. This method can preserve the 3D proximal femur surface and structure while visualizing the entire fracture line with a single plot/view. Using this method and a standardization technique, a total of 100 patients with different ages and genders are studied based on the original radiographs acquired by CT scan. The comparison shows that the proposed map projection representation is more efficient and rich in information visualization than the conventional heat map technique. Using the proposed method, a fracture probability can be obtained at any location in the 2D parametric space, from which the most probable fracture region can be accurately identified. The study shows that age and gender have significant influences on intertrochanteric fracture frequency and fracture line distribution.
  • In recent years, both online retail and video hosting service are exponentially growing. In this paper, we explore a new cross-domain task, Video2Shop, targeting for matching clothes appeared in videos to the exact same items in online shops. A novel deep neural network, called AsymNet, is proposed to explore this problem. For the image side, well- established methods are used to detect and extract features for clothing patches with arbitrary sizes. For the video side, deep visual features are extracted from detected object re- gions in each frame, and further fed into a Long Short-Term Memory (LSTM) framework for sequence modeling, which captures the temporal dynamics in videos. To conduct exact matching between videos and online shopping images, LSTM hidden states, representing the video, and image features, which represent static object images, are jointly mod- eled under the similarity network with reconfigurable deep tree structure. Moreover, an approximate training method is proposed to achieve the efficiency when training. Extensive experiments conducted on a large cross-domain dataset have demonstrated the effectiveness and efficiency of the proposed AsymNet, which outperforms the state-of-the-art methods.
  • In this paper, we present a surface remeshing method with high approximation quality based on Principal Component Analysis. Given a triangular mesh and a user assigned polygon/vertex budget, traditional methods usually require the extra curvature metric field for the desired anisotropy to best approximate the surface, even though the estimated curvature metric is known to be imperfect and already self-contained in the surface. In our approach, this anisotropic control is achieved through the optimal geometry partition without this explicit metric field. The minimization of our proposed partition energy has the following properties: Firstly, on a C2 surface, it is theoretically guaranteed to have the optimal aspect ratio and cluster size as specified in approximation theory for L1 piecewise linear approximation. Secondly, it captures sharp features on practical models without any pre-tagging. We develop an effective merging-swapping framework to seek the optimal partition and construct polygonal/triangular mesh afterwards. The effectiveness and efficiency of our method are demonstrated through the comparison with other state-of-the-art remeshing methods.
  • Cloud-assisted Cognitive Internet of Things has powerful data analytics abilities based on the computing and data storage capabilities of cloud virtual machines, which makes protecting virtual machine filesystem very important for the whole system security. Agentless periodic filesystem monitors are optimal solutions to protect cloud virtual machines because of the secure and low-overhead features. However, most of the periodic monitors usually scan all of the virtual machine filesystem or protected files in every scanning poll, so lots of secure files are scanned again and again even though they are not corrupted. In this paper, we propose a novel agentless periodic filesystem monitor framework for virtual machines with different image formats to improve the performance of agentless periodic monitors. Our core idea is to minimize the scope of the scanning files in both file integrity checking and virus detection. In our monitor, if a file is considered secure, it will not be scanned when it has not been modified. Since our monitor only scans the newly created and modified files, it can check fewer files than other filesystem monitors. To that end, we propose two monitor methods for different types of virtual machine disks to reduce the number of scanning files. For virtual machine with single disk image, we hook the backend driver to capture the disk modification information. For virtual machine with multiple copy-onwrite images, we leverage the copy-on-write feature of QCOW2 images to achieve the disk modification analysis. In addition, our system can restore and remove the corrupted files. The experimental results show that our system is effective for both Windows and Linux virtual machines with different image formats and can reduce the number of scanning files and scanning time.
  • Bitcoin has attracted everyone's attention and interest recently. Ethereum (ETH), a second generation cryptocurrency, extends Bitcoin's design by offering a Turing-complete programming language called Solidity to develop smart contracts. Smart contracts allow creditable execution of contracts on EVM (Ethereum Virtual Machine) without third parties. Developing correct smart contracts is challenging due to its decentralized computation nature. Buggy smart contracts may lead to huge financial loss. Furthermore, smart contracts are very hard, if not impossible, to patch once they are deployed. Thus, there is a recent surge of interest on analyzing/verifying smart contracts. While existing work focuses on EVM opcode, we argue that it is equally important to understand and define the semantics of Solidity since programmers program and reason about smart contracts at the level of source code. In this work, we develop the structural operational semantics for Solidity, which allows us to identify multiple design issues which underlines many problematic smart contracts. Furthermore, our semantics is executable in the K framework, which allows us to verify/falsify contracts automatically.
  • Most existing Zero-Shot Learning (ZSL) methods have the strong bias problem, in which instances of unseen (target) classes tend to be categorized as one of the seen (source) classes. So they yield poor performance after being deployed in the generalized ZSL settings. In this paper, we propose a straightforward yet effective method named Quasi-Fully Supervised Learning (QFSL) to alleviate the bias problem. Our method follows the way of transductive learning, which assumes that both the labeled source images and unlabeled target images are available for training. In the semantic embedding space, the labeled source images are mapped to several fixed points specified by the source categories, and the unlabeled target images are forced to be mapped to other points specified by the target categories. Experiments conducted on AwA2, CUB and SUN datasets demonstrate that our method outperforms existing state-of-the-art approaches by a huge margin of 9.3~24.5% following generalized ZSL settings, and by a large margin of 0.2~16.2% following conventional ZSL settings.
  • Data-flow testing (DFT) checks the correctness of variable definitions by observing their corresponding uses. It has been empirically proved to be more effective than control-flow testing in fault detection, however, its complexities still overwhelm the testers in practice. To tackle this problem, we introduce a hybrid testing framework: (1) The core of our framework is symbolic execution, enhanced by a novel guided path search to improve testing performance; and (2) we systematically cast DFT as reachability checking in software model checking to complement SE, yielding practical DFT that combines the two techniques' strengths. We implemented our framework on the state-of-the-art symbolic execution tool KLEE and model checking tools BLAST, CPAchecker and CBMC, and extensively evaluate it on 30 real-world subjects with collectively 22,793 def-use pairs. The enhanced SE approach not only covers more pairs, but also reduces testing time by 10$\sim$43%. The model checking approach can effectively weed out infeasible pairs that KLEE cannot infer by 70.1$\sim$95.8%. Finally, for all subjects, our hybrid approach can improve data-flow coverage by 28.7$\sim$46.3%, and reduce testing time by up to 64.6% than the symbolic execution approach alone. This hybrid approach also enables the cross-checking of each component for reliable and robust testing results.
  • We present memory-efficient and scalable algorithms for kernel methods used in machine learning. Using hierarchical matrix approximations for the kernel matrix the memory requirements, the number of floating point operations, and the execution time are drastically reduced compared to standard dense linear algebra routines. We consider both the general $\mathcal{H}$ matrix hierarchical format as well as Hierarchically Semi-Separable (HSS) matrices. Furthermore, we investigate the impact of several preprocessing and clustering techniques on the hierarchical matrix compression. Effective clustering of the input leads to a ten-fold increase in efficiency of the compression. The algorithms are implemented using the STRUMPACK solver library. These results confirm that --- with correct tuning of the hyperparameters --- classification using kernel ridge regression with the compressed matrix does not lose prediction accuracy compared to the exact --- not compressed --- kernel matrix and that our approach can be extended to $\mathcal{O}(1M)$ datasets, for which computation with the full kernel matrix becomes prohibitively expensive. We present numerical experiments in a distributed memory environment up to 1,024 processors of the NERSC's Cori supercomputer using well-known datasets to the machine learning community that range from dimension 8 up to 784.
  • Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.
  • The Fast Style Transfer methods have been recently proposed to transfer a photograph to an artistic style in real-time. This task involves controlling the stroke size in the stylized results, which remains an open challenge. In this paper, we present a stroke controllable style transfer network that can achieve continuous and spatial stroke size control. By analyzing the factors that influence the stroke size, we propose to explicitly account for the receptive field and the style image scales. We propose a StrokePyramid module to endow the network with adaptive receptive fields, and two training strategies to achieve faster convergence and augment new stroke sizes upon a trained model respectively. By combining the proposed runtime control strategies, our network can achieve continuous changes in stroke sizes and produce distinct stroke sizes in different spatial regions within the same output image.
  • In this article, a two-grid mixed finite element (TGMFE) method with some second-order time discrete schemes is developed for numerically solving nonlinear fourth-order reaction diffusion equation. The two-grid MFE method is used to approximate spatial direction, and some second-order $\theta$ schemes formulated at time $t_{k-\theta}$ are considered to discretize the time direction. TGMFE method covers two main steps: a nonlinear MFE system based on the space coarse grid is solved by the iterative algorithm and a coarse solution is arrived at, then a linearized MFE system with fine grid is considered and a TGMFE solution is obtained. Here, the stability and a priori error estimates in $L^2$-norm for both nonlinear Galerkin MFE system and TGMFE scheme are derived. Finally, some convergence results are computed for both nonlinear Galerkin MFE system and TGMFE scheme to verify our theoretical analysis, which show that the convergence rate of the time second-order $\theta$ scheme including Crank-Nicolson scheme and second-order backward difference scheme is close to $2$, and that with the comparison to the computing time of nonlinear Galerkin MFE method, the CPU-time by using TGMFE method can be saved.
  • Deep learning defines a new data-driven programming paradigm that constructs the internal system logic of a crafted neuron network through a set of training data. Deep learning (DL) has been widely adopted in many safety-critical scenarios. However, a plethora of studies have shown that the state-of-the-art DL systems suffer from various vulnerabilities which can lead to severe consequences when applied to real-world applications. Currently, the robustness of a DL system against adversarial attacks is usually measured by the accuracy of test data. Considering the limitation of accessible test data, good performance on test data can hardly guarantee the robustness and generality of DL systems. Different from traditional software systems which have clear and controllable logic and functionality, a DL system is trained with data and lacks thorough understanding. This makes it difficult for system analysis and defect detection, which could potentially hinder its real-world deployment without safety guarantees. In this paper, we propose DeepGauge, a comprehensive and multi-granularity testing criteria for DL systems, which renders a complete and multi-faceted portrayal of the testbed. The in-depth evaluation of our proposed testing criteria is demonstrated on two well-known datasets, five DL systems, with four state-of-the-art adversarial data generation techniques. The effectiveness of DeepGauge sheds light on the construction of robust DL systems.
  • The entanglement-assisted (EA) formalism allows arbitrary classical linear codes to transform into entanglement-assisted quantum error correcting codes (EAQECCs) by using pre-shared entanglement between the sender and the receiver. In this work, we propose a decomposition of the defining set of constacyclic codes. Using this method, we construct four classes of $q$-ary entanglement-assisted quantum MDS (EAQMDS) codes based on classical constacyclic MDS codes by exploiting less pre-shared maximally entangled states. We show that a class of $q$-ary EAQMDS have minimum distance upper limit greater than $3q-1$. Some of them have much larger minimum distance than the known quantum MDS (QMDS) codes of the same length. Most of these $q$-ary EAQMDS codes are new in the sense that their parameters are not covered by the codes available in the literature.