-
Coding information into all infinite subsets of a dense set
Authors:
Matthew Harrison-Trainor,
Lu Liu,
Patrick Lutz
Abstract:
Suppose you have an uncomputable set $X$ and you want to find a set $A$, all of whose infinite subsets compute $X$. There are several ways to do this, but all of them seem to produce a set $A$ which is fairly sparse. We show that this is necessary in the following technical sense: if $X$ is uncomputable and $A$ is a set of positive lower density then $A$ has an infinite subset which does not compu…
▽ More
Suppose you have an uncomputable set $X$ and you want to find a set $A$, all of whose infinite subsets compute $X$. There are several ways to do this, but all of them seem to produce a set $A$ which is fairly sparse. We show that this is necessary in the following technical sense: if $X$ is uncomputable and $A$ is a set of positive lower density then $A$ has an infinite subset which does not compute $X$. We also prove an analogous result for PA degree: if $X$ is uncomputable and $A$ is a set of positive lower density then $A$ has an infinite subset which is not of PA degree. We will show that these theorems are sharp in certain senses and also prove a quantitative version formulated in terms of Kolmogorov complexity. Our results use a modified version of Mathias forcing and build on work by Seetapun, Liu, and others on the reverse math of Ramsey's theorem for pairs.
△ Less
Submitted 11 August, 2023; v1 submitted 1 June, 2023;
originally announced June 2023.
-
Sparse tree-based initialization for neural networks
Authors:
Patrick Lutz,
Ludovic Arnould,
Claire Boyer,
Erwan Scornet
Abstract:
Dedicated neural network (NN) architectures have been designed to handle specific data types (such as CNN for images or RNN for text), which ranks them among state-of-the-art methods for dealing with these data. Unfortunately, no architecture has been found for dealing with tabular data yet, for which tree ensemble methods (tree boosting, random forests) usually show the best predictive performanc…
▽ More
Dedicated neural network (NN) architectures have been designed to handle specific data types (such as CNN for images or RNN for text), which ranks them among state-of-the-art methods for dealing with these data. Unfortunately, no architecture has been found for dealing with tabular data yet, for which tree ensemble methods (tree boosting, random forests) usually show the best predictive performances. In this work, we propose a new sparse initialization technique for (potentially deep) multilayer perceptrons (MLP): we first train a tree-based procedure to detect feature interactions and use the resulting information to initialize the network, which is subsequently trained via standard stochastic gradient strategies. Numerical experiments on several tabular data sets show that this new, simple and easy-to-use method is a solid concurrent, both in terms of generalization capacity and computation time, to default MLP initialization and even to existing complex deep learning solutions. In fact, this wise MLP initialization raises the resulting NN methods to the level of a valid competitor to gradient boosting when dealing with tabular data. Besides, such initializations are able to preserve the sparsity of weights introduced in the first layers of the network through training. This fact suggests that this new initializer operates an implicit regularization during the NN training, and emphasizes that the first layers act as a sparse feature extractor (as for convolutional layers in CNN).
△ Less
Submitted 30 September, 2022;
originally announced September 2022.
-
Formalizing Galois Theory
Authors:
Thomas Browning,
Patrick Lutz
Abstract:
We describe a project to formalize Galois theory using the Lean theorem prover, which is part of a larger effort to formalize all of the standard undergraduate mathematics curriculum in Lean. We discuss some of the challenges we faced and the decisions we made in the course of this project. The main theorems we formalized are the primitive element theorem, the fundamental theorem of Galois theory,…
▽ More
We describe a project to formalize Galois theory using the Lean theorem prover, which is part of a larger effort to formalize all of the standard undergraduate mathematics curriculum in Lean. We discuss some of the challenges we faced and the decisions we made in the course of this project. The main theorems we formalized are the primitive element theorem, the fundamental theorem of Galois theory, and the equivalence of several characterizations of finite degree Galois extensions.
△ Less
Submitted 22 July, 2021;
originally announced July 2021.
-
Simultaneous Contact and Aerodynamic Force Estimation (s-CAFE) for Aerial Robots
Authors:
Teodor Tomić,
Philipp Lutz,
Korbinian Schmid,
Andrew Mathers,
Sami Haddadin
Abstract:
In this paper, we consider the problem of multirotor flying robots physically interacting with the environment under wind influence. The result are the first algorithms for simultaneous online estimation of contact and aerodynamic wrenches acting on the robot based on real-world data, without the need for dedicated sensors. For this purpose, we investigate two model-based techniques for discrimina…
▽ More
In this paper, we consider the problem of multirotor flying robots physically interacting with the environment under wind influence. The result are the first algorithms for simultaneous online estimation of contact and aerodynamic wrenches acting on the robot based on real-world data, without the need for dedicated sensors. For this purpose, we investigate two model-based techniques for discriminating between aerodynamic and interaction forces. The first technique is based on aerodynamic and contact torque models, and uses the external force to estimate wind speed. Contacts are then detected based on the residual between estimated external torque and expected (modeled) aerodynamic torque. Upon detecting contact, wind speed is assumed to change very slowly. From the estimated interaction wrench, we are also able to determine the contact location. This is embedded into a particle filter framework to further improve contact location estimation. The second algorithm uses the propeller aerodynamic power and angular speed as measured by the speed controllers to obtain an estimate of the airspeed. An aerodynamics model is then used to determine the aerodynamic wrench. Both methods rely on accurate aerodynamics models. Therefore, we evaluate data-driven and physics based models as well as offline system identification for flying robots. For obtaining ground truth data we performed autonomous flights in a 3D wind tunnel. Using this data, aerodynamic model selection, parameter identification, and discrimination between aerodynamic and contact forces could be done. Finally, the developed methods could serve as useful estimators for interaction control schemes with simultaneous compensation of wind disturbances.
△ Less
Submitted 30 October, 2018;
originally announced October 2018.
