OpenRaiser/Intern-Atlas huggingface dataset:
On the Convergence Properties of Optimal AdaBoost
Venue: arXiv cs.LG 2023
Year: 2023

AdaBoost is one of the most popular ML algorithms. It is simple to implement and often found very effective by practitioners, while still being mathematically elegant and theoretically sound. AdaBoost's interesting behavior in practice still puzzles the ML community. We address the algorithm's stability and establish multiple convergence properties of "Optimal AdaBoost," a term coined by Rudin, Daubechies, and Schapire in 2004. We prove, in a reasonably strong computational sense, the almost universal existence of time averages, and with that, the convergence of the classifier itself, its generalization error, and its resulting margins, among many other objects, for fixed data sets under arguably reasonable conditions. Specifically, we frame Optimal AdaBoost as a dynamical system and, employing tools from ergodic theory, prove that, under a condition that Optimal AdaBoost does not have ties for best weak classifier eventually, a condition for which we provide empirical evidence from high dimensional real-world datasets, the algorithm's update behaves like a continuous map. We provide constructive proofs of several arbitrarily accurate approximations of Optimal AdaBoost; prove that they exhibit certain cycling behavior in finite time, and that the resulting dynamical system is ergodic; and establish sufficient conditions for the same to hold for the actual Optimal-AdaBoost update. We believe that our results provide reasonably strong evidence for the affirmative answer to two open conjectures, at least from a broad computational-theory perspective: AdaBoost always cycles and is an ergodic dynamical system. We present empirical evidence that cycles are hard to detect while time averages stabilize quickly. Our results ground future convergence-rate analysis and may help optimize generalization ability and alleviate a practitioner's burden of deciding how long to run the algorithm.
GNU epsilon -- an extensible programming language
Venue: arXiv cs.PL 2023
Year: 2023

Reductionism is a viable strategy for designing and implementing practical programming languages, leading to solutions which are easier to extend, experiment with and formally analyze. We formally specify and implement an extensible programming language, based on a minimalistic first-order imperative core language plus strong abstraction mechanisms, reflection and self-modification features. The language can be extended to very high levels: by using Lisp-style macros and code-to-code transforms which automatically rewrite high-level expressions into core forms, we define closures and first-class continuations on top of the core. Non-self-modifying programs can be analyzed and formally reasoned upon, thanks to the language simple semantics. We formally develop a static analysis and prove a soundness property with respect to the dynamic semantics. We develop a parallel garbage collector suitable to multi-core machines to permit efficient execution of parallel programs.
Operational Concurrency Control in the Face of Arbitrary Scale and Latency
Venue: arXiv cs.DS 2023
Year: 2023

We present for the first time a complete solution to the problem of proving the correctness of a concurrency control algorithm for collaborative text editors against the standard consistency model. The success of our approach stems from the use of comprehensive stringwise operational transformations, which appear to have escaped a formal treatment until now. Because these transformations sometimes lead to an increase in the number of operations as they are transformed, we cannot use inductive methods and adopt the novel idea of decreasing diagrams instead. We also base our algorithm on a client-server model rather than a peer-to-peer one, which leads to the correct application of operational transformations to both newly generated and pending operations. And lastly we solve the problem of latency, so that our algorithm works perfectly in practice. The result of these innovations is the first ever formally correct concurrency control algorithm for collaborative text editors together with a fast, fault tolerant and highly scalable implementation.
On cascade products of answer set programs
Venue: arXiv cs.LO 2023
Year: 2023

Describing complex objects by elementary ones is a common strategy in mathematics and science in general. In their seminal 1965 paper, Kenneth Krohn and John Rhodes showed that every finite deterministic automaton can be represented (or "emulated") by a cascade product of very simple automata. This led to an elegant algebraic theory of automata based on finite semigroups (Krohn-Rhodes Theory). Surprisingly, by relating logic programs and automata, we can show in this paper that the Krohn-Rhodes Theory is applicable in Answer Set Programming (ASP). More precisely, we recast the concept of a cascade product to ASP, and prove that every program can be represented by a product of very simple programs, the reset and standard programs. Roughly, this implies that the reset and standard programs are the basic building blocks of ASP with respect to the cascade product. In a broader sense, this paper is a first step towards an algebraic theory of products and networks of nonmonotonic reasoning systems based on Krohn-Rhodes Theory, aiming at important open issues in ASP and AI in general.
On the Complexity of Dynamic Mechanism Design
Venue: arXiv cs.GT 2023
Year: 2023

We introduce a dynamic mechanism design problem in which the designer wants to offer for sale an item to an agent, and another item to the same agent at some point in the future. The agent's joint distribution of valuations for the two items is known, and the agent knows the valuation for the current item (but not for the one in the future). The designer seeks to maximize expected revenue, and the auction must be deterministic, truthful, and ex post individually rational. The optimum mechanism involves a protocol whereby the seller elicits the buyer's current valuation, and based on the bid makes two take-it-or-leave-it offers, one for now and one for the future. We show that finding the optimum deterministic mechanism in this situation - arguably the simplest meaningful dynamic mechanism design problem imaginable - is NP-hard. We also prove several positive results, among them a polynomial linear programming-based algorithm for the optimum randomized auction (even for many bidders and periods), and we show strong separations in revenue between non-adaptive, adaptive, and randomized auctions, even when the valuations in the two periods are uncorrelated. Finally, for the same problem in an environment in which contracts cannot be enforced, and thus perfection of equilibrium is necessary, we show that the optimum randomized mechanism requires multiple rounds of cheap talk-like interactions.
FAQ: Questions Asked Frequently
Venue: arXiv cs.DB 2023
Year: 2023

We define and study the Functional Aggregate Query (FAQ) problem, which encompasses many frequently asked questions in constraint satisfaction, databases, matrix operations, probabilistic graphical models and logic. This is our main conceptual contribution. We then present a simple algorithm called "InsideOut" to solve this general problem. InsideOut is a variation of the traditional dynamic programming approach for constraint programming based on variable elimination. Our variation adds a couple of simple twists to basic variable elimination in order to deal with the generality of FAQ, to take full advantage of Grohe and Marx's fractional edge cover framework, and of the analysis of recent worst-case optimal relational join algorithms. As is the case with constraint programming and graphical model inference, to make InsideOut run efficiently we need to solve an optimization problem to compute an appropriate 'variable ordering'. The main technical contribution of this work is a precise characterization of when a variable ordering is 'semantically equivalent' to the variable ordering given by the input FAQ expression. Then, we design an approximation algorithm to find an equivalent variable ordering that has the best 'fractional FAQ-width'. Our results imply a host of known and a few new results in graphical model inference, matrix operations, relational joins, and logic. We also briefly explain how recent algorithms on beyond worst-case analysis for joins and those for solving SAT and #SAT can be viewed as variable elimination to solve FAQ over compactly represented input functions.
Calculation of the confidence bounds for the fraction nonconforming of normal populations of measurements in clinical laboratory medicine
Venue: arXiv cs.CE 2023
Year: 2023

The fraction nonconforming is a key quality measure used in statistical quality control design in clinical laboratory medicine. The confidence bounds of normal populations of measurements for the fraction nonconforming each of the lower and upper quality specification limits when both the random and the systematic error are unknown can be calculated using the noncentral t-distribution, as it is described in detail and illustrated with examples.
Adopting Robustness and Optimality in Fitting and Learning
Venue: arXiv cs.LG 2023
Year: 2023

We generalized a modified exponentialized estimator by pushing the robust-optimal (RO) index $λ$ to $-\infty$ for achieving robustness to outliers by optimizing a quasi-Minimin function. The robustness is realized and controlled adaptively by the RO index without any predefined threshold. Optimality is guaranteed by expansion of the convexity region in the Hessian matrix to largely avoid local optima. Detailed quantitative analysis on both robustness and optimality are provided. The results of proposed experiments on fitting tasks for three noisy non-convex functions and the digits recognition task on the MNIST dataset consolidate the conclusions.
On the uniform one-dimensional fragment
Venue: arXiv cs.LO 2023
Year: 2023

The uniform one-dimensional fragment of first-order logic, U1, is a formalism that extends two-variable logic in a natural way to contexts with relations of all arities. We survey properties of U1 and investigate its relationship to description logics designed to accommodate higher arity relations, with particular attention given to DLR_reg. We also define a description logic version of a variant of U1 and prove a range of new results concerning the expressivity of U1 and related logics.
Markov Chains and Unambiguous Automata
Venue: arXiv cs.LO 2023
Year: 2023

Unambiguous automata are nondeterministic automata in which every word has at most one accepting run. In this paper we give a polynomial-time algorithm for model checking discrete-time Markov chains against ω-regular specifications represented as unambiguous automata. We furthermore show that the complexity of this model checking problem lies in NC: the subclass of P comprising those problems solvable in poly-logarithmic parallel time. These complexity bounds match the known bounds for model checking Markov chains against specifications given as deterministic automata, notwithstanding the fact that unambiguous automata can be exponentially more succinct than deterministic automata. We report on an implementation of our procedure, including an experiment in which the implementation is used to model check LTL formulas on Markov chains.
Lets keep it simple, Using simple architectures to outperform deeper and more complex architectures
Venue: arXiv cs.CV 2023
Year: 2023

Major winning Convolutional Neural Networks (CNNs), such as AlexNet, VGGNet, ResNet, GoogleNet, include tens to hundreds of millions of parameters, which impose considerable computation and memory overhead. This limits their practical use for training, optimization and memory efficiency. On the contrary, light-weight architectures, being proposed to address this issue, mainly suffer from low accuracy. These inefficiencies mostly stem from following an ad hoc procedure. We propose a simple architecture, called SimpleNet, based on a set of designing principles, with which we empirically show, a well-crafted yet simple and reasonably deep architecture can perform on par with deeper and more complex architectures. SimpleNet provides a good tradeoff between the computation/memory efficiency and the accuracy. Our simple 13-layer architecture outperforms most of the deeper and complex architectures to date such as VGGNet, ResNet, and GoogleNet on several well-known benchmarks while having 2 to 25 times fewer number of parameters and operations. This makes it very handy for embedded systems or systems with computational and memory limitations. We achieved state-of-the-art result on CIFAR10 outperforming several heavier architectures, near state of the art on MNIST and competitive results on CIFAR100 and SVHN. We also outperformed the much larger and deeper architectures such as VGGNet and popular variants of ResNets among others on the ImageNet dataset. Models are made available at: https://github.com/Coderx7/SimpleNet
Ebert's asymmetric three person three color Hat Game
Venue: arXiv cs.IT 2023
Year: 2023

We generalize Ebert's Hat Problem for three persons and three colors. All players guess simultaneously the color of their own hat observing only the hat colors of the other players. It is also allowed for each player to pass: no color is guessed. The team wins if at least one player guesses his or her hat color correct and none of the players has an incorrect guess. This paper studies Ebert's hat problem, where the probabilities of the colors may be different (asymmetric case). Our goal is to maximize the probability of winning the game and to describe winning strategies. In this paper we use the notion of an adequate set. The construction of adequate sets is independent of underlying probabilities and we can use this fact in the analysis of the asymmetric case. Another point of interest is the fact that computational complexity using adequate sets is much less than using standard methods.
Is Parallel Programming Hard, And, If So, What Can You Do About It? (Release v2023.06.11a)
Venue: arXiv cs.DC 2023
Year: 2023

The purpose of this book is to help you program shared-memory parallel systems without risking your sanity. Nevertheless, you should think of the information in this book as a foundation on which to build, rather than as a completed cathedral. Your mission, if you choose to accept, is to help make further progress in the exciting field of parallel programming-progress that will in time render this book obsolete. Parallel programming in the 21st century is no longer focused solely on science, research, and grand-challenge projects. And this is all to the good, because it means that parallel programming is becoming an engineering discipline. Therefore, as befits an engineering discipline, this book examines specific parallel-programming tasks and describes how to approach them. In some surprisingly common cases, these tasks can be automated. This book is written in the hope that presenting the engineering discipline underlying successful parallel-programming projects will free a new generation of parallel hackers from the need to slowly and painstakingly reinvent old wheels, enabling them to instead focus their energy and creativity on new frontiers. However, what you get from this book will be determined by what you put into it. It is hoped that simply reading this book will be helpful, and that working the Quick Quizzes will be even more helpful. However, the best results come from applying the techniques taught in this book to real-life problems. As always, practice makes perfect. But no matter how you approach it, we sincerely hope that parallel programming brings you at least as much fun, excitement, and challenge that it has brought to us!
A categorical characterization of relative entropy on standard Borel spaces
Venue: arXiv cs.IT 2023
Year: 2023

We give a categorical treatment, in the spirit of Baez and Fritz, of relative entropy for probability distributions defined on standard Borel spaces. We define a category suitable for reasoning about statistical inference on standard Borel spaces. We define relative entropy as a functor into Lawvere's category and we show convexity, lower semicontinuity and uniqueness.
Attention Is All You Need
Venue: arXiv cs.CL 2023
Year: 2023

The dominant sequence transduction models are based on complex recurrent or convolutional neural networks in an encoder-decoder configuration. The best performing models also connect the encoder and decoder through an attention mechanism. We propose a new simple network architecture, the Transformer, based solely on attention mechanisms, dispensing with recurrence and convolutions entirely. Experiments on two machine translation tasks show these models to be superior in quality while being more parallelizable and requiring significantly less time to train. Our model achieves 28.4 BLEU on the WMT 2014 English-to-German translation task, improving over the existing best results, including ensembles by over 2 BLEU. On the WMT 2014 English-to-French translation task, our model establishes a new single-model state-of-the-art BLEU score of 41.8 after training for 3.5 days on eight GPUs, a small fraction of the training costs of the best models from the literature. We show that the Transformer generalizes well to other tasks by applying it successfully to English constituency parsing both with large and limited training data.
Stabbing Planes
Venue: arXiv cs.CC 2023
Year: 2023

We develop a new semi-algebraic proof system called Stabbing Planes which formalizes modern branch-and-cut algorithms for integer programming and is in the style of DPLL-based modern SAT solvers. As with DPLL there is only a single rule: the current polytope can be subdivided by branching on an inequality and its "integer negation." That is, we can (nondeterministically choose) a hyperplane $ax \geq b$ with integer coefficients, which partitions the polytope into three pieces: the points in the polytope satisfying $ax \geq b$, the points satisfying $ax \leq b-1$, and the middle slab $b - 1 < ax < b$. Since the middle slab contains no integer points it can be safely discarded, and the algorithm proceeds recursively on the other two branches. Each path terminates when the current polytope is empty, which is polynomial-time checkable. Among our results, we show that Stabbing Planes can efficiently simulate the Cutting Planes proof system, and is equivalent to a tree-like variant of the RCP system of [Krajicek98]. As well, we show that it possesses short proofs of the canonical family of systems of $\mathbb{F}_2$-linear equations known as the Tseitin formulas. Finally, we prove linear lower bounds on the rank of Stabbing Planes refutations by adapting lower bounds in communication complexity and use these bounds in order to show that Stabbing Planes proofs cannot be balanced. In doing so, we show that real communication protocols cannot be balanced and establish the first lower bound on the real communication complexity of the set disjointness function.
Qualitative software engineering research -- reflections and guidelines
Venue: arXiv cs.SE 2023
Year: 2023

Researchers are increasingly recognizing the importance of human aspects in software development. Since qualitative methods are used to explore human behavior in-depth, we believe that studies using such methods will become more common. Existing qualitative software engineering guidelines do not cover the full breadth of qualitative methods and the knowledge on how to use them like in social sciences. The purpose of this study was to extend the software engineering community's current body of knowledge regarding available qualitative methods and their quality assurance frameworks, and to provide recommendations and guidelines for their use. With the support of an epistemological argument and a survey of the literature, we suggest that future research would benefit from (1) utilizing a broader set of research methods, (2) more strongly emphasizing reflexivity, and (3) employing qualitative guidelines and quality criteria. We present an overview of three qualitative methods commonly used in social sciences but rarely seen in software engineering research, namely interpretative phenomenological analysis, narrative analysis, and discourse analysis. Furthermore, we discuss the meaning of reflexivity in relation to the software engineering context and suggest means of fostering it. Our paper will help software engineering researchers better select and then guide the application of a broader set of qualitative research methods.
Contextual Modal Type Theory with Polymorphic Contexts
Venue: arXiv cs.LO 2023
Year: 2023

Modal types -- types that are derived from proof systems of modal logic -- have been studied as theoretical foundations of metaprogramming, where program code is manipulated as first-class values. In modal type systems, modality corresponds to a type constructor for code types and controls free variables and their types in code values. Nanevski et al. have proposed contextual modal type theory, which has modal types with fine-grained information on free variables: modal types are explicitly indexed by contexts -- the types of all free variables in code values. This paper presents $λ_{\forall[]}$, a novel extension of contextual modal type theory with parametric polymorphism over contexts. Such an extension has been studied in the literature but unlike earlier proposals, $λ_{\forall[]}$ is more general in that multiple parts of a single context can be abstracted. We formalize \lamfb with its type system and operational semantics given by $β$-reduction and prove its basic properties including subject reduction, strong normalization, and confluence. Moreover, to demonstrate the expressive power of polymorphic contexts, we show a type-preserving embedding from a two-level fragment of Davies' $λ_{\bigcirc}$, which is based on linear-time temporal logic, to $λ_{\forall[]}$.
VAMS: Verifiable Auditing of Access to Confidential Data
Venue: arXiv cs.CR 2023
Year: 2023

We propose VAMS, a system that enables transparency for audits of access to data requests without compromising the privacy of parties in the system. VAMS supports audits on an aggregate level and an individual level, by relying on three mechanisms. A tamper-evident log provides integrity for the log entries that are audited. A tagging scheme allows users to query log entries that relate to them, without allowing others to do so. MultiBallot, a novel extension of the ThreeBallot voting scheme, is used to generate a synthetic dataset that can be used to publicly verify published statistics with a low expected privacy loss. We evaluate two implementations of VAMS, and show that both the log and the ability to verify published statistics are practical for realistic use cases such as access to healthcare records and law enforcement access to communications records.
Algorithmic Pirogov-Sinai theory
Venue: arXiv cs.DS 2023
Year: 2023

We develop an efficient algorithmic approach for approximate counting and sampling in the low-temperature regime of a broad class of statistical physics models on finite subsets of the lattice $\mathbb Z^d$ and on the torus $(\mathbb Z/n \mathbb Z)^d$. Our approach is based on combining contour representations from Pirogov-Sinai theory with Barvinok's approach to approximate counting using truncated Taylor series. Some consequences of our main results include an FPTAS for approximating the partition function of the hard-core model at sufficiently high fugacity on subsets of $\mathbb Z^d$ with appropriate boundary conditions and an efficient sampling algorithm for the ferromagnetic Potts model on the discrete torus $(\mathbb Z/n \mathbb Z)^d$ at sufficiently low temperature.