OpenRaiser/Intern-Atlas huggingface dataset:
Robust principal graphs for data approximation
Venue: arXiv cs.DS 2016
Year: 2016

Revealing hidden geometry and topology in noisy data sets is a challenging task. Elastic principal graph is a computationally efficient and flexible data approximator based on embedding a graph into the data space and minimizing the energy functional penalizing the deviation of graph nodes both from data points and from pluri-harmonic configuration (generalization of linearity). The structure of principal graph is learned from data by application of a topological grammar which in the simplest case leads to the construction of principal curves or trees. In order to more efficiently cope with noise and outliers, here we suggest using a trimmed data approximation term to increase the robustness of the method. The modification of the method that we suggest does not affect either computational efficiency or general convergence properties of the original elastic graph method. The trimmed elastic energy functional remains a Lyapunov function for the optimization algorithm. On several examples of complex data distributions we demonstrate how the robust principal graphs learn the global data structure and show the advantage of using the trimmed data approximation term for the construction of principal graphs and other popular data approximators.
A Decision Procedure for Separation Logic in SMT
Venue: arXiv cs.LO 2016
Year: 2016

This paper presents a complete decision procedure for the entire quantifier-free fragment of Separation Logic ($\seplog$) interpreted over heaplets with data elements ranging over a parametric multi-sorted (possibly infinite) domain. The algorithm uses a combination of theories and is used as a specialized solver inside a DPLL($T$) architecture. A prototype was implemented within the CVC4 SMT solver. Preliminary evaluation suggests the possibility of using this procedure as a building block of a more elaborate theorem prover for SL with inductive predicates, or as back-end of a bounded model checker for programs with low-level pointer and data manipulations.
Array Folds Logic
Venue: arXiv cs.FL 2016
Year: 2016

We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as "the first array cell contains the array length," and "the array contains equally many minimal and maximal elements." These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability. AFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.
The Value of Privacy: Strategic Data Subjects, Incentive Mechanisms and Fundamental Limits
Venue: arXiv cs.GT 2016
Year: 2016

We study the value of data privacy in a game-theoretic model of trading private data, where a data collector purchases private data from strategic data subjects (individuals) through an incentive mechanism. The private data of each individual represents her knowledge about an underlying state, which is the information that the data collector desires to learn. Different from most of the existing work on privacy-aware surveys, our model does not assume the data collector to be trustworthy. Then, an individual takes full control of its own data privacy and reports only a privacy-preserving version of her data. In this paper, the value of $ε$ units of privacy is measured by the minimum payment of all nonnegative payment mechanisms, under which an individual's best response at a Nash equilibrium is to report the data with a privacy level of $ε$. The higher $ε$ is, the less private the reported data is. We derive lower and upper bounds on the value of privacy which are asymptotically tight as the number of data subjects becomes large. Specifically, the lower bound assures that it is impossible to use less amount of payment to buy $ε$ units of privacy, and the upper bound is given by an achievable payment mechanism that we designed. Based on these fundamental limits, we further derive lower and upper bounds on the minimum total payment for the data collector to achieve a given learning accuracy target, and show that the total payment of the designed mechanism is at most one individual's payment away from the minimum.
On the Secrecy Capacity of the Broadcast Wiretap Channel with Limited CSI Feedback
Venue: arXiv cs.IT 2016
Year: 2016

In this paper, we investigate the problem of secure broadcasting over block-fading channels with limited channel knowledge at the transmitter. More particularly, we analyze the effect of having imperfect channel state information (CSI) via a finite rate feedback on the throughput of a broadcast channel where the transmission is intended for multiple legitimate receivers in the presence of an eavesdropper. First, we partially characterize the ergodic secrecy capacity of the system when the source broadcasts the same information to all the receivers, i.e., common message transmission. Then, we look at the independent messages case, where the transmitter broadcasts multiple independent messages to the legitimate receivers. For this case, we present lower and upper bounds on the ergodic secrecy sum-capacity. In both scenarios, we show that the proposed lower and upper bounds coincide asymptotically as the capacity of the feedback links becomes large, hence, fully characterizing the secrecy capacity in this case.
A note on the convergence of nonconvex line search
Venue: arXiv cs.NA 2016
Year: 2016

In this note, we consider the line search for a class of abstract nonconvex algorithm which have been deeply studied in the Kurdyka-Lojasiewicz theory. We provide a weak convergence result of the line search in general. When the objective function satisfies the Kurdyka-Lojasiewicz property and some certain assumption, a global convergence result can be derived. An application is presented for the L0-regularized least square minimization in the end of the paper.
A mixed precision semi-Lagrangian algorithm and its performance on accelerators
Venue: arXiv cs.MS 2016
Year: 2016

In this paper we propose a mixed precision algorithm in the context of the semi-Lagrangian discontinuous Galerkin method. The performance of this approach is evaluated on a traditional dual socket workstation as well as on a Xeon Phi and an NVIDIA K80. We find that the mixed precision algorithm can be implemented efficiently on these architectures. This implies that, in addition to the considerable reduction in memory, a substantial increase in performance can be observed as well. Moreover, we discuss the relative performance of our implementations.
Robust cDNA microarray image segmentation and analysis technique based on Hough circle transform
Venue: arXiv cs.CV 2016
Year: 2016

One of the most challenging tasks in microarray image analysis is spot segmentation. A solution to this problem is to provide an algorithm than can be used to find any spot within the microarray image. Circular Hough Transformation (CHT) is a powerful feature extraction technique used in image analysis, computer vision, and digital image processing. CHT algorithm is applied on the cDNA microarray images to develop the accuracy and the efficiency of the spots localization, addressing and segmentation process. The purpose of the applied technique is to find imperfect instances of spots within a certain class of circles by applying a voting procedure on the cDNA microarray images for spots localization, addressing and characterizing the pixels of each spot into foreground pixels and background simultaneously. Intensive experiments on the University of North Carolina (UNC) microarray database indicate that the proposed method is superior to the K-means method and the Support vector machine (SVM). Keywords: Hough circle transformation, cDNA microarray image analysis, cDNA microarray image segmentation, spots localization and addressing, spots segmentation
The Anatomy of a Search and Mining System for Digital Archives
Venue: arXiv cs.DL 2016
Year: 2016

Samtla (Search And Mining Tools with Linguistic Analysis) is a digital humanities system designed in collaboration with historians and linguists to assist them with their research work in quantifying the content of any textual corpora through approximate phrase search and document comparison. The retrieval engine uses a character-based n-gram language model rather than the conventional word-based one so as to achieve great flexibility in language agnostic query processing. The index is implemented as a space-optimised character-based suffix tree with an accompanying database of document content and metadata. A number of text mining tools are integrated into the system to allow researchers to discover textual patterns, perform comparative analysis, and find out what is currently popular in the research community. Herein we describe the system architecture, user interface, models and algorithms, and data storage of the Samtla system. We also present several case studies of its usage in practice together with an evaluation of the systems' ranking performance through crowdsourcing.
Computing Equilibria in Markets with Budget-Additive Utilities
Venue: arXiv cs.GT 2016
Year: 2016

We present the first analysis of Fisher markets with buyers that have budget-additive utility functions. Budget-additive utilities are elementary concave functions with numerous applications in online adword markets and revenue optimization problems. They extend the standard case of linear utilities and have been studied in a variety of other market models. In contrast to the frequently studied CES utilities, they have a global satiation point which can imply multiple market equilibria with quite different characteristics. Our main result is an efficient combinatorial algorithm to compute a market equilibrium with a Pareto-optimal allocation of goods. It relies on a new descending-price approach and, as a special case, also implies a novel combinatorial algorithm for computing a market equilibrium in linear Fisher markets. We complement these positive results with a number of hardness results for related computational questions. We prove that it is NP-hard to compute a market equilibrium that maximizes social welfare, and it is PPAD-hard to find any market equilibrium with utility functions with separate satiation points for each buyer and each good.
Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms
Venue: arXiv cs.LO 2016
Year: 2016

In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination. We make this intuition formal in the context of the non-deterministic λ-calculus by introducing a finiteness structure on resource terms, which is such that a λ-term is strongly normalizing iff the support of its Taylor expansion is finitary. An application of our result is the existence of a normal form for the Taylor expansion of any strongly normalizable non-deterministic λ-term.
Global-Local Face Upsampling Network
Venue: arXiv cs.CV 2016
Year: 2016

Face hallucination, which is the task of generating a high-resolution face image from a low-resolution input image, is a well-studied problem that is useful in widespread application areas. Face hallucination is particularly challenging when the input face resolution is very low (e.g., 10 x 12 pixels) and/or the image is captured in an uncontrolled setting with large pose and illumination variations. In this paper, we revisit the algorithm introduced in [1] and present a deep interpretation of this framework that achieves state-of-the-art under such challenging scenarios. In our deep network architecture the global and local constraints that define a face can be efficiently modeled and learned end-to-end using training data. Conceptually our network design can be partitioned into two sub-networks: the first one implements the holistic face reconstruction according to global constraints, and the second one enhances face-specific details and enforces local patch statistics. We optimize the deep network using a new loss function for super-resolution that combines reconstruction error with a learned face quality measure in adversarial setting, producing improved visual results. We conduct extensive experiments in both controlled and uncontrolled setups and show that our algorithm improves the state of the art both numerically and visually.
Congruence Testing of Point Sets in 4 Dimensions
Venue: arXiv cs.CG 2016
Year: 2016

Congruence between two n-point sets in 4 dimension can be checked in O(n log n) time. On the way to establishing this result, we revisit several parts of 4-dimensional geometry, such as angles and distances between planes, Hopf fibrations, and Coxeter groups.
Peeling and Nibbling the Cactus: Subexponential-Time Algorithms for Counting Triangulations and Related Problems
Venue: arXiv cs.CG 2016
Year: 2016

Given a set of $n$ points $S$ in the plane, a triangulation $T$ of $S$ is a maximal set of non-crossing segments with endpoints in $S$. We present an algorithm that computes the number of triangulations on a given set of $n$ points in time $n^{(11+ o(1))\sqrt{n} }$, significantly improving the previous best running time of $O(2^n n^2)$ by Alvarez and Seidel [SoCG 2013]. Our main tool is identifying separators of size $O(\sqrt{n})$ of a triangulation in a canonical way. The definition of the separators are based on the decomposition of the triangulation into nested layers ("cactus graphs"). Based on the above algorithm, we develop a simple and formal framework to count other non-crossing straight-line graphs in $n^{O(\sqrt{n})}$ time. We demonstrate the usefulness of the framework by applying it to counting non-crossing Hamilton cycles, spanning trees, perfect matchings, $3$-colorable triangulations, connected graphs, cycle decompositions, quadrangulations, $3$-regular graphs, and more.
Digital IP Protection Using Threshold Voltage Control
Venue: arXiv cs.CR 2016
Year: 2016

This paper proposes a method to completely hide the functionality of a digital standard cell. This is accomplished by a differential threshold logic gate (TLG). A TLG with $n$ inputs implements a subset of Boolean functions of $n$ variables that are linear threshold functions. The output of such a gate is one if and only if an integer weighted linear arithmetic sum of the inputs equals or exceeds a given integer threshold. We present a novel architecture of a TLG that not only allows a single TLG to implement a large number of complex logic functions, which would require multiple levels of logic when implemented using conventional logic primitives, but also allows the selection of that subset of functions by assignment of the transistor threshold voltages to the input transistors. To obfuscate the functionality of the TLG, weights of some inputs are set to zero by setting their device threshold to be a high $V_t$. The threshold voltage of the remaining transistors is set to low $V_t$ to increase their transconductance. The function of a TLG is not determined by the cell itself but rather the signals that are connected to its inputs. This makes it possible to hide the support set of the function by essentially removing some variable from the support set of the function by selective assignment of high and low $V_t$ to the input transistors. We describe how a standard cell library of TLGs can be mixed with conventional standard cells to realize complex logic circuits, whose function can never be discovered by reverse engineering. A 32-bit Wallace tree multiplier and a 28-bit 4-tap filter were synthesized on an ST 65nm process, placed and routed, then simulated including extracted parastics with and without obfuscation. Both obfuscated designs had much lower area (25%) and much lower dynamic power (30%) than their nonobfuscated CMOS counterparts, operating at the same frequency.
Efficient Enumeration of Unidirectional Cuts for Technology Mapping of Boolean Networks
Venue: arXiv cs.DS 2016
Year: 2016

In technology mapping, enumeration of subcircuits or cuts to be replaced by a standard cell is an important step that decides both the quality of the solution and execution speed. In this work, we view cuts as set of edges instead of as set of nodes and based on it, provide a classification of cuts. It is shown that if enumeration is restricted to a subclass of cuts called unidirectional cuts, the quality of solution does not degrade. We also show that such cuts are equivalent to a known class of cuts called strong line cuts first proposed in [14]. We propose an efficient enumeration method based on a novel graph pruning algorithm that utilizes network flow to approximate minimum strong line cut. The runtimes for the proposed enumeration method are shown to be quite practical for enumeration of a large number of cuts.
A note on "achieving security, robust cheating resistance, and high-efficiency for outsourcing large matrix multiplication computation to a malicious cloud"
Venue: arXiv cs.CR 2016
Year: 2016

We show that the Lei et al.'s scheme [Information Sciences, 280 (2014), 205-217] fails, because the verifying equation does not hold over the infinite field R. For the field R, the computational errors should be considered seriously. We also remark that the incurred communication cost in the scheme could be overtake the computational gain, which makes it somewhat artificial.
Nonlinear Analysis of an Improved Swing Equation
Venue: arXiv cs.SY 2016
Year: 2016

In this paper, we investigate the properties of an improved swing equation model for synchronous generators. This model is derived by omitting the main simplifying assumption of the conventional swing equation, and requires a novel analysis for the stability and frequency regulation. We consider two scenarios. First we study the case that a synchronous generator is connected to a constant load. Second, we inspect the case of the single machine connected to an infinite bus. Simulations verify the results.
A Trust Model for Data Sharing in Smart Cities
Venue: arXiv cs.CY 2016
Year: 2016

The data generated by the devices and existing infrastructure in the Internet of Things (IoT) should be shared among applications. However, data sharing in the IoT can only reach its full potential when multiple participants contribute their data, for example when people are able to use their smartphone sensors for this purpose. We believe that each step, from sensing the data to the actionable knowledge, requires trust-enabled mechanisms to facilitate data exchange, such as data perception trust, trustworthy data mining, and reasoning with trust related policies. The absence of trust could affect the acceptance of sharing data in smart cities. In this study, we focus on data usage transparency and accountability and propose a trust model for data sharing in smart cities, including system architecture for trust-based data sharing, data semantic and abstraction models, and a mechanism to enhance transparency and accountability for data usage. We apply semantic technology and defeasible reasoning with trust data usage policies. We built a prototype based on an air pollution monitoring use case and utilized it to evaluate the performance of our solution.
Power and Channel Allocation for Non-orthogonal Multiple Access in 5G Systems: Tractability and Computation
Venue: arXiv cs.IT 2016
Year: 2016

Network capacity calls for significant increase for 5G cellular systems. A promising multi-user access scheme, non-orthogonal multiple access (NOMA) with successive interference cancellation (SIC), is currently under consideration. In NOMA, spectrum efficiency is improved by allowing more than one user to simultaneously access the same frequency-time resource and separating multi-user signals by SIC at the receiver. These render resource allocation and optimization in NOMA different from orthogonal multiple access in 4G. In this paper, we provide theoretical insights and algorithmic solutions to jointly optimize power and channel allocation in NOMA. For utility maximization, we mathematically formulate NOMA resource allocation problems. We characterize and analyze the problems' tractability under a range of constraints and utility functions. For tractable cases, we provide polynomial-time solutions for global optimality. For intractable cases, we prove the NP-hardness and propose an algorithmic framework combining Lagrangian duality and dynamic programming (LDDP) to deliver near-optimal solutions. To gauge the performance of the obtained solutions, we also provide optimality bounds on the global optimum. Numerical results demonstrate that the proposed algorithmic solution can significantly improve the system performance in both throughput and fairness over orthogonal multiple access as well as over a previous NOMA resource allocation scheme.
Contrastive Analysis with Predictive Power: Typology Driven Estimation of Grammatical Error Distributions in ESL
Venue: arXiv cs.CL 2016
Year: 2016

This work examines the impact of cross-linguistic transfer on grammatical errors in English as Second Language (ESL) texts. Using a computational framework that formalizes the theory of Contrastive Analysis (CA), we demonstrate that language specific error distributions in ESL writing can be predicted from the typological properties of the native language and their relation to the typology of English. Our typology driven model enables to obtain accurate estimates of such distributions without access to any ESL data for the target languages. Furthermore, we present a strategy for adjusting our method to low-resource languages that lack typological documentation using a bootstrapping approach which approximates native language typology from ESL texts. Finally, we show that our framework is instrumental for linguistic inquiry seeking to identify first language factors that contribute to a wide range of difficulties in second language acquisition.
Position and Vector Detection of Blind Spot motion with the Horn-Schunck Optical Flow
Venue: arXiv cs.CV 2016
Year: 2016

The proposed method uses live image footage which, based on calculations of pixel motion, decides whether or not an object is in the blind-spot. If found, the driver is notified by a sensory light or noise built into the vehicle's CPU. The new technology incorporates optical vectors and flow fields rather than expensive radar-waves, creating cheaper detection systems that retain the needed accuracy while adapting to the current processor speeds.
Recursive Neural Language Architecture for Tag Prediction
Venue: arXiv cs.IR 2016
Year: 2016

We consider the problem of learning distributed representations for tags from their associated content for the task of tag recommendation. Considering tagging information is usually very sparse, effective learning from content and tag association is very crucial and challenging task. Recently, various neural representation learning models such as WSABIE and its variants show promising performance, mainly due to compact feature representations learned in a semantic space. However, their capacity is limited by a linear compositional approach for representing tags as sum of equal parts and hurt their performance. In this work, we propose a neural feedback relevance model for learning tag representations with weighted feature representations. Our experiments on two widely used datasets show significant improvement for quality of recommendations over various baselines.