OpenRaiser/Intern-Atlas huggingface dataset:
Logistic Regression: Tight Bounds for Stochastic and Online Optimization
Venue: arXiv cs.LG 2014
Year: 2014

The logistic loss function is often advocated in machine learning and statistics as a smooth and strictly convex surrogate for the 0-1 loss. In this paper we investigate the question of whether these smoothness and convexity properties make the logistic loss preferable to other widely considered options such as the hinge loss. We show that in contrast to known asymptotic bounds, as long as the number of prediction/optimization iterations is sub exponential, the logistic loss provides no improvement over a generic non-smooth loss function such as the hinge loss. In particular we show that the convergence rate of stochastic logistic optimization is bounded from below by a polynomial in the diameter of the decision set and the number of prediction iterations, and provide a matching tight upper bound. This resolves the COLT open problem of McMahan and Streeter (2012).
Analysis and Transformation Tools for Constrained Horn Clause Verification
Venue: arXiv cs.PL 2014
Year: 2014

Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited to certain subclasses of CHC problems. Our aim in this work is to investigate the use of a combination of off-the-shelf techniques from the literature in analysis and transformation of Constraint Logic Programs (CLPs) to solve challenging CHC verification problems. We find that many problems can be solved using a combination of tools based on well-known techniques from abstract interpretation, semantics-preserving transformations, program specialisation and query-answer transformations. This gives insights into the design of automatic, more general CHC verification tools based on a library of components.
Matching concepts across HOL libraries
Venue: arXiv cs.LO 2014
Year: 2014

Many proof assistant libraries contain formalizations of the same mathematical concepts. The concepts are often introduced (defined) in different ways, but the properties that they have, and are in turn formalized, are the same. For the basic concepts, like natural numbers, matching them between libraries is often straightforward, because of mathematical naming conventions. However, for more advanced concepts, finding similar formalizations in different libraries is a non-trivial task even for an expert. In this paper we investigate automatic discovery of similar concepts across libraries of proof assistants. We propose an approach for normalizing properties of concepts in formal libraries and a number of similarity measures. We evaluate the approach on HOL based proof assistants HOL4, HOL Light and Isabelle/HOL, discovering 398 pairs of isomorphic constants and types.
Aerial-Terrestrial Communications: Terrestrial Cooperation and Energy-Efficient Transmissions to Aerial-Base Stations
Venue: arXiv cs.NI 2014
Year: 2014

Hybrid aerial-terrestrial communication networks based on Low Altitude Platforms (LAPs) are expected to optimally meet the urgent communication needs of emergency relief and recovery operations for tackling large scale natural disasters. The energy-efficient operation of such networks is important given the fact that the entire network infrastructure, including the battery operated ground terminals, exhibits requirements to operate under power-constrained situations. In this paper, we discuss the design and evaluation of an adaptive cooperative scheme intended to extend the survivability of the battery operated aerial-terrestrial communication links. We propose and evaluate a real-time adaptive cooperative transmission strategy for dynamic selection between direct and cooperative links based on the channel conditions for improved energy efficiency. We show that the cooperation between mobile terrestrial terminals on the ground could improve the energy efficiency in the uplink depending on the temporal behavior of the terrestrial and the aerial uplink channels. The corresponding delay in having cooperative (relay-based) communications with relay selection is also addressed. The simulation analysis corroborates that the adaptive transmission technique improves the overall energy efficiency of the network whilst maintaining low latency enabling real time applications.
SMT-based Model Checking for Recursive Programs
Venue: arXiv cs.LO 2014
Year: 2014

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE "lazily". We use existing interpolation techniques to over-approximate QE and introduce "Model Based Projection" to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.
Formalization of Complex Vectors in Higher-Order Logic
Venue: arXiv cs.LO 2014
Year: 2014

Complex vector analysis is widely used to analyze continuous systems in many disciplines, including physics and engineering. In this paper, we present a higher-order-logic formalization of the complex vector space to facilitate conducting this analysis within the sound core of a theorem prover: HOL Light. Our definition of complex vector builds upon the definitions of complex numbers and real vectors. This extension allows us to extensively benefit from the already verified theorems based on complex analysis and real vector analysis. To show the practical usefulness of our library we adopt it to formalize electromagnetic fields and to prove the law of reflection for the planar waves.
A Module System for Domain-Specific Languages
Venue: arXiv cs.PL 2014
Year: 2014

Domain-specific languages (DSLs) are routinely created to simplify difficult or specialized programming tasks. They expose useful abstractions and design patterns in the form of language constructs, provide static semantics to eagerly detect misuse of these constructs, and dynamic semantics to completely define how language constructs interact. However, implementing and composing DSLs is a non-trivial task, and there is a lack of tools and techniques. We address this problem by presenting a complete module system over LP for DSL construction, reuse, and composition. LP is already useful for DSL design, because it supports executable language specifications using notations familiar to language designers. We extend LP with a module system that is simple (with a few concepts), succinct (for key DSL specification scenarios), and composable (on the level of languages, compilers, and programs). These design choices reflect our use of LP for industrial DSL design. Our module system has been implemented in the FORMULA language, and was used to build key Windows 8 device drivers via DSLs. Though we present our module system as it actually appears in our FORMULA language, our emphasis is on concepts adaptable to other LP languages.
Seismic Wave Scattering Through a Compressed Hybrid BEM/FEM Method
Venue: arXiv cs.CE 2014
Year: 2014

Approximated numerical techniques, for the solution of the elastic wave scattering problem over semi-infinite domains are reviewed. The approximations involve the representation of the half-space by a boundary condition described in terms of 2D boundary element discretizations. The classical BEM matrices are initially re-written into the form of a dense dynamic stiffness matrix and later approximated to a banded matrix. The resulting final banded matrix is then used like a standard finite element to solve the wave scattering problem at lower memory requirements. The accuracy of the reviewed methods is benchmarked against the classical problems of a semi-circular and a rectangular canyon. Results are presented in the time and frequency domain, as well as in terms of relative errors in the considered approximations. The main goal of the paper is to give the analyst a method that can be used at the practising level where an approximate solution is enough in order to support engineering decisions.
Exploiting Prior Knowledge in Compressed Sensing Wireless ECG Systems
Venue: arXiv cs.CE 2014
Year: 2014

Recent results in telecardiology show that compressed sensing (CS) is a promising tool to lower energy consumption in wireless body area networks for electrocardiogram (ECG) monitoring. However, the performance of current CS-based algorithms, in terms of compression rate and reconstruction quality of the ECG, still falls short of the performance attained by state-of-the-art wavelet based algorithms. In this paper, we propose to exploit the structure of the wavelet representation of the ECG signal to boost the performance of CS-based methods for compression and reconstruction of ECG signals. More precisely, we incorporate prior information about the wavelet dependencies across scales into the reconstruction algorithms and exploit the high fraction of common support of the wavelet coefficients of consecutive ECG segments. Experimental results utilizing the MIT-BIH Arrhythmia Database show that significant performance gains, in terms of compression rate and reconstruction quality, can be obtained by the proposed algorithms compared to current CS-based methods.
Architectural Design of a RAM Arbiter
Venue: arXiv cs.AR 2014
Year: 2014

Standard memory modules to store (and access) data are designed for use with a single system accessing it. More complicated memory modules would be accessed through a memory controller, which are also designed for one system. For multiple systems to access a single memory module there must be some facilitation that allows them to access the memory without overriding or corrupting the access from the others. This was done with the use of a memory arbiter, which controls the flow of traffic into the memory controller. The arbiter has a set of rules to abide to in order to choose which system gets through to the memory controller. In this project, a regular RAM module is designed for use with one system. Furthermore, a memory arbiter is also designed in Verilog that allows for more than one system to use a single RAM module in a controlled and synchronized manner. The arbiter uses a fixed priority scheme to avoid starvation of the system. In addition one of the major problems associated with such systems i.e. The Address Clash Problem has been nicely tackled and solved. The design is verified in simulation and validated on a Xilinx ML605 evaluation board with a Virtex 6 FPGA.
Coarse-to-Fine Classification via Parametric and Nonparametric Models for Computer-Aided Diagnosis
Venue: arXiv cs.CV 2014
Year: 2014

Classification is one of the core problems in Computer-Aided Diagnosis (CAD), targeting for early cancer detection using 3D medical imaging interpretation. High detection sensitivity with desirably low false positive (FP) rate is critical for a CAD system to be accepted as a valuable or even indispensable tool in radiologists' workflow. Given various spurious imagery noises which cause observation uncertainties, this remains a very challenging task. In this paper, we propose a novel, two-tiered coarse-to-fine (CTF) classification cascade framework to tackle this problem. We first obtain classification-critical data samples (e.g., samples on the decision boundary) extracted from the holistic data distributions using a robust parametric model (e.g., \cite{Raykar08}); then we build a graph-embedding based nonparametric classifier on sampled data, which can more accurately preserve or formulate the complex classification boundary. These two steps can also be considered as effective "sample pruning" and "feature pursuing + $k$NN/template matching", respectively. Our approach is validated comprehensively in colorectal polyp detection and lung nodule detection CAD systems, as the top two deadly cancers, using hospital scale, multi-site clinical datasets. The results show that our method achieves overall better classification/detection performance than existing state-of-the-art algorithms using single-layer classifiers, such as the support vector machine variants \cite{Wang08}, boosting \cite{Slabaugh10}, logistic regression \cite{Ravesteijn10}, relevance vector machine \cite{Raykar08}, $k$-nearest neighbor \cite{Murphy09} or spectral projections on graph \cite{Cai08}.
Compressing the Data Densely by New Geflochtener to Accelerate Web
Venue: arXiv cs.IT 2014
Year: 2014

At the present scenario of the internet, there exist many optimization techniques to improve the Web speed but almost expensive in terms of bandwidth. So after a long investigation on different techniques to compress the data without any loss, a new algorithm is proposed based on L Z 77 family which selectively models the references with backward movement and encodes the longest matches through greedy parsing with the shortest path technique to compresses the data with high density. This idea seems to be useful since the single Web Page contains many repetitive words which create havoc in consuming space, so let it removes such unnecessary redundancies with 70% efficiency and compress the pages with 23.75 - 35% compression ratio.
Algebraic Codes and a New Physical Layer Transmission Protocol for Wireless Distributed Storage Systems
Venue: arXiv cs.IT 2014
Year: 2014

In a wireless storage system, having to communicate over a fading channel makes repair transmissions prone to physical layer errors. The first approach to combat fading is to utilize the existing optimal space-time codes. However, it was recently pointed out that such codes are in general too complex to decode when the number of helper nodes is bigger than the number of antennas at the newcomer or data collector. In this paper, a novel protocol for wireless storage transmissions based on algebraic space-time codes is presented in order to improve the system reliability while enabling feasible decoding. The diversity-multiplexing gain tradeoff (DMT) of the system together with sphere-decodability even with low number of antennas are used as the main design criteria, thus naturally establishing a DMT-complexity tradeoff. It is shown that the proposed protocol outperforms the simple time-division multiple access (TDMA) protocol, while still falling behind the optimal DMT.
Transport Capacity of Distributed Wireless CSMA Networks
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, we study the transport capacity of large multi-hop wireless CSMA networks. Different from previous studies which rely on the use of centralized scheduling algorithm and/or centralized routing algorithm to achieve the optimal capacity scaling law, we show that the optimal capacity scaling law can be achieved using entirely distributed routing and scheduling algorithms. Specifically, we consider a network with nodes Poissonly distributed with unit intensity on a $\sqrt{n}\times\sqrt{n}$ square $B_{n}\subset\Re^{2}$. Furthermore, each node chooses its destination randomly and independently and transmits following a CSMA protocol. By resorting to the percolation theory and by carefully tuning the three controllable parameters in CSMA protocols, i.e. transmission power, carrier-sensing threshold and count-down timer, we show that a throughput of $Θ\left(\frac{1}{\sqrt{n}}\right)$ is achievable in distributed CSMA networks. Furthermore, we derive the pre-constant preceding the order of the transport capacity by giving an upper and a lower bound of the transport capacity. The tightness of the bounds is validated using simulations.
Identification of functionally related enzymes by learning-to-rank methods
Venue: arXiv cs.LG 2014
Year: 2014

Enzyme sequences and structures are routinely used in the biological sciences as queries to search for functionally related enzymes in online databases. To this end, one usually departs from some notion of similarity, comparing two enzymes by looking for correspondences in their sequences, structures or surfaces. For a given query, the search operation results in a ranking of the enzymes in the database, from very similar to dissimilar enzymes, while information about the biological function of annotated database enzymes is ignored. In this work we show that rankings of that kind can be substantially improved by applying kernel-based learning algorithms. This approach enables the detection of statistical dependencies between similarities of the active cleft and the biological function of annotated enzymes. This is in contrast to search-based approaches, which do not take annotated training data into account. Similarity measures based on the active cleft are known to outperform sequence-based or structure-based measures under certain conditions. We consider the Enzyme Commission (EC) classification hierarchy for obtaining annotated enzymes during the training phase. The results of a set of sizeable experiments indicate a consistent and significant improvement for a set of similarity measures that exploit information about small cavities in the surface of enzymes.
An Efficient Binary Technique for Trace Simplifications of Concurrent Programs
Venue: arXiv cs.SE 2014
Year: 2014

Execution of concurrent programs implies frequent switching between different thread contexts. This property perplexes analyzing and reasoning about concurrent programs. Trace simplification is a technique that aims at alleviating this problem via transforming a concurrent program trace (execution) into a semantically equivalent one. The resulted trace typically includes less number of context switches than that in the original trace. This paper presents a new static approach for trace simplification. This approach is based on a connectivity analysis that calculates for each trace-point connectivity and context-switching information. The paper also presents a novel operational semantics for concurrent programs. The semantics is used to prove the correctness and efficiency of the proposed techniques for connectivity analysis and trace simplification. The results of experiments testing the proposed technique on problems treated by previous work for trace simplification are also shown in the paper. The results prove the efficiency and effectiveness of the proposed method.
Preliminary Report on the Structure of Croatian Linguistic Co-occurrence Networks
Venue: arXiv cs.CL 2014
Year: 2014

In this article, we investigate the structure of Croatian linguistic co-occurrence networks. We examine the change of network structure properties by systematically varying the co-occurrence window sizes, the corpus sizes and removing stopwords. In a co-occurrence window of size $n$ we establish a link between the current word and $n-1$ subsequent words. The results point out that the increase of the co-occurrence window size is followed by a decrease in diameter, average path shortening and expectedly condensing the average clustering coefficient. The same can be noticed for the removal of the stopwords. Finally, since the size of texts is reflected in the network properties, our results suggest that the corpus influence can be reduced by increasing the co-occurrence window size.
Optimization of Radio and Computational Resources for Energy Efficiency in Latency-Constrained Application Offloading
Venue: arXiv cs.IT 2014
Year: 2014

Providing femto-access points (FAPs) with computational capabilities will allow (either total or partial) offloading of highly demanding applications from smart-phones to the so called femto-cloud. Such offloading promises to be beneficial in terms of battery saving at the mobile terminal (MT) and/or latency reduction in the execution of applications, whenever the energy and/or time required for the communication process are compensated by the energy and/or time savings that result from the remote computation at the FAPs. For this problem, we provide in this paper a framework for the joint optimization of the radio and computational resource usage exploiting the tradeoff between energy consumption and latency, and assuming that multiple antennas are available at the MT and the serving FAP. As a result of the optimization, the optimal communication strategy (e.g., transmission power, rate, precoder) is obtained, as well as the optimal distribution of the computational load between the handset and the serving FAP. The paper also establishes the conditions under which total or no offloading are optimal, determines which is the minimum affordable latency in the execution of the application, and analyzes as a particular case the minimization of the total consumed energy without latency constraints.
On Disjoint Golomb Rulers
Venue: arXiv cs.IT 2014
Year: 2014

A set $\{a_i\:|\: 1\leq i \leq k\}$ of non-negative integers is a Golomb ruler if differences $a_i-a_j$, for any $i \neq j$, are all distinct. A set of $I$ disjoint Golomb rulers (DGR) each being a $J$-subset of $\{1,2,\cdots, n\}$ is called an $(I,J,n)-DGR$. Let $H(I, J)$ be the least positive $n$ such that there is an $(I,J,n)-DGR$. In this paper, we propose a series of conjectures on the constructions and structures of DGR. The main conjecture states that if $A$ is any set of positive integers such that $|A| = H(I, J)$, then there are $I$ disjoint Golomb rulers, each being a $J$-subset of $A$, which generalizes the conjecture proposed by Koml{ó}s, Sulyok and Szemer{é}di in 1975 on the special case $I = 1$. These conjectures are computationally verified for some values of $I$ and $J$ through modest computation. Eighteen exact values of $H(I,J)$ and ten upper bounds on $H(I,J)$ are obtained by computer search for $7 \leq I \leq 13$ and $10 \leq J \leq 13$. Moveover for $I > 13$ and $10 \leq J \leq 13$, $H(I,J)=IJ$ are determined without difficulty.
Kronecker PCA Based Spatio-Temporal Modeling of Video for Dismount Classification
Venue: arXiv cs.CV 2014
Year: 2014

We consider the application of KronPCA spatio-temporal modeling techniques [Greenewald et al 2013, Tsiligkaridis et al 2013] to the extraction of spatiotemporal features for video dismount classification. KronPCA performs a low-rank type of dimensionality reduction that is adapted to spatio-temporal data and is characterized by the T frame multiframe mean and covariance of p spatial features. For further regularization and improved inverse estimation, we also use the diagonally corrected KronPCA shrinkage methods we presented in [Greenewald et al 2013]. We apply this very general method to the modeling of the multivariate temporal behavior of HOG features extracted from pedestrian bounding boxes in video, with gender classification in a challenging dataset chosen as a specific application. The learned covariances for each class are used to extract spatiotemporal features which are then classified, achieving competitive classification performance.
Geometric projection-based switching policy for multiple energy harvesting transmitters
Venue: arXiv cs.IT 2014
Year: 2014

Transmitter switching can provide resiliency and robustness to a communication system with multiple energy harvesting transmitters. However, excessive transmitter switching will bring heavy control overhead. In this paper, a geometric projection-based transmitter switching policy is proposed for a communication system with multiple energy harvesting transmitters and one receiver, which can reduce the number of switches. The results show that the proposed transmitter switching policy outperforms several heuristic ones.