-
Learning temporal formulas from examples is hard
Authors:
Corto Mascle,
Nathanaël Fijalkow,
Guillaume Lagarde
Abstract:
We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. In this paper we initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL learning problem is NP-complete, both…
▽ More
We study the problem of learning linear temporal logic (LTL) formulas from examples, as a first step towards expressing a property separating positive and negative instances in a way that is comprehensible for humans. In this paper we initiate the study of the computational complexity of the problem. Our main results are hardness results: we show that the LTL learning problem is NP-complete, both for the full logic and for almost all of its fragments. This motivates the search for efficient heuristics, and highlights the complexity of expressing separating properties in concise natural language.
△ Less
Submitted 26 December, 2023;
originally announced December 2023.
-
Scaling Neural Program Synthesis with Distribution-based Search
Authors:
Nathanaël Fijalkow,
Guillaume Lagarde,
Théo Matricon,
Kevin Ellis,
Pierre Ohlmann,
Akarsh Potta
Abstract:
We consider the problem of automatically constructing computer programs from input-output examples. We investigate how to augment probabilistic and neural program synthesis methods with new search algorithms, proposing a framework called distribution-based search. Within this framework, we introduce two new search algorithms: Heap Search, an enumerative method, and SQRT Sampling, a probabilistic m…
▽ More
We consider the problem of automatically constructing computer programs from input-output examples. We investigate how to augment probabilistic and neural program synthesis methods with new search algorithms, proposing a framework called distribution-based search. Within this framework, we introduce two new search algorithms: Heap Search, an enumerative method, and SQRT Sampling, a probabilistic method. We prove certain optimality guarantees for both methods, show how they integrate with probabilistic and neural techniques, and demonstrate how they can operate at scale across parallel compute environments. Collectively these findings offer theoretical and applied studies of search algorithms for program synthesis that integrate with recent developments in machine-learned program synthesizers.
△ Less
Submitted 24 October, 2021;
originally announced October 2021.
-
The Complexity of Learning Linear Temporal Formulas from Examples
Authors:
Nathanaël Fijalkow,
Guillaume Lagarde
Abstract:
In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we obtain tight bounds for approximation of the fragment containing only the next operator and conjunctions, and prove NP-completeness results for many fragments.
In this paper we initiate the study of the computational complexity of learning linear temporal logic (LTL) formulas from examples. We construct approximation algorithms for fragments of LTL and prove hardness results; in particular we obtain tight bounds for approximation of the fragment containing only the next operator and conjunctions, and prove NP-completeness results for many fragments.
△ Less
Submitted 1 February, 2021;
originally announced February 2021.
-
On Efficient Low Distortion Ultrametric Embedding
Authors:
Vincent Cohen-Addad,
Karthik C. S.,
Guillaume Lagarde
Abstract:
A classic problem in unsupervised learning and data analysis is to find simpler and easy-to-visualize representations of the data that preserve its essential properties. A widely-used method to preserve the underlying hierarchical structure of the data while reducing its complexity is to find an embedding of the data into a tree or an ultrametric. The most popular algorithms for this task are the…
▽ More
A classic problem in unsupervised learning and data analysis is to find simpler and easy-to-visualize representations of the data that preserve its essential properties. A widely-used method to preserve the underlying hierarchical structure of the data while reducing its complexity is to find an embedding of the data into a tree or an ultrametric. The most popular algorithms for this task are the classic linkage algorithms (single, average, or complete). However, these methods on a data set of $n$ points in $Ω(\log n)$ dimensions exhibit a quite prohibitive running time of $Θ(n^2)$.
In this paper, we provide a new algorithm which takes as input a set of points $P$ in $\mathbb{R}^d$, and for every $c\ge 1$, runs in time $n^{1+\fracρ{c^2}}$ (for some universal constant $ρ>1$) to output an ultrametric $Δ$ such that for any two points $u,v$ in $P$, we have $Δ(u,v)$ is within a multiplicative factor of $5c$ to the distance between $u$ and $v$ in the "best" ultrametric representation of $P$. Here, the best ultrametric is the ultrametric $\tildeΔ$ that minimizes the maximum distance distortion with respect to the $\ell_2$ distance, namely that minimizes $\underset{u,v \in P}{\max}\ \frac{\tildeΔ(u,v)}{\|u-v\|_2}$.
We complement the above result by showing that under popular complexity theoretic assumptions, for every constant $\varepsilon>0$, no algorithm with running time $n^{2-\varepsilon}$ can distinguish between inputs in $\ell_\infty$-metric that admit isometric embedding and those that incur a distortion of $\frac{3}{2}$.
Finally, we present empirical evaluation on classic machine learning datasets and show that the output of our algorithm is comparable to the output of the linkage algorithms while achieving a much faster running time.
△ Less
Submitted 15 August, 2020;
originally announced August 2020.
-
$d$-Galvin families
Authors:
Johan Håstad,
Guillaume Lagarde,
Joseph Swernofsky
Abstract:
The Galvin problem asks for the minimum size of a family $\mathcal{F} \subseteq \binom{[n]}{n/2}$ with the property that, for any set $A$ of size $\frac n 2$, there is a set $S \in \mathcal{F}$ which is balanced on $A$, meaning that $|S \cap A| = |S \cap \overline{A}|$. We consider a generalization of this question that comes from a possible approach in complexity theory. In the generalization the…
▽ More
The Galvin problem asks for the minimum size of a family $\mathcal{F} \subseteq \binom{[n]}{n/2}$ with the property that, for any set $A$ of size $\frac n 2$, there is a set $S \in \mathcal{F}$ which is balanced on $A$, meaning that $|S \cap A| = |S \cap \overline{A}|$. We consider a generalization of this question that comes from a possible approach in complexity theory. In the generalization the required property is, for any $A$, to be able to find $d$ sets from a family $\mathcal{F} \subseteq \binom{[n]}{n/d}$ that form a partition of $[n]$ and such that each part is balanced on $A$. We construct such families of size polynomial in the parameters $n$ and $d$.
△ Less
Submitted 9 January, 2019;
originally announced January 2019.
-
Lempel-Ziv: a "one-bit catastrophe" but not a tragedy
Authors:
Guillaume Lagarde,
Sylvain Perifel
Abstract:
The so-called "one-bit catastrophe" for the compression algorithm LZ'78 asks whether the compression ratio of an infinite word can change when a single bit is added in front of it. We answer positively this open question raised by Lutz and others: we show that there exists an infinite word $w$ such that $ρ_{sup}(w)=0$ but $ρ_{inf}(0w)>0$, where $ρ_{sup}$ and $ρ_{inf}$ are respectively the…
▽ More
The so-called "one-bit catastrophe" for the compression algorithm LZ'78 asks whether the compression ratio of an infinite word can change when a single bit is added in front of it. We answer positively this open question raised by Lutz and others: we show that there exists an infinite word $w$ such that $ρ_{sup}(w)=0$ but $ρ_{inf}(0w)>0$, where $ρ_{sup}$ and $ρ_{inf}$ are respectively the $\limsup$ and the $\liminf$ of the compression ratios $ρ$ of the prefixes. To that purpose we explore the behaviour of LZ'78 on finite words and show the following results:
- There is a constant $C>0$ such that, for any finite word $w$ and any letter $a$, $ρ(aw)\leq C\sqrt{ρ(w)\log|w|}$. Thus, sufficiently compressible words ($ρ(w)=o(1/\log|w|)$) remain compressible with a letter in front;
- The previous result is tight up to a multiplicative constant for any compression ratio $ρ(w)=O(1/\log|w|)$. In particular, there are infinitely many words $w$ satisfying $ρ(w)=O(1/\log|w|)$ but $ρ(0w)=Ω(1)$.
△ Less
Submitted 31 July, 2017; v1 submitted 13 July, 2017;
originally announced July 2017.
-
De Bruijn-Erdős type theorems for graphs and posets
Authors:
Pierre Aboulker,
Guillaume Lagarde,
David Malec,
Abhishek Methuku,
Casey Tompkins
Abstract:
A classical theorem of De Bruijn and Erdős asserts that any noncollinear set of n points in the plane determines at least n distinct lines. We prove that an analogue of this theorem holds for graphs. Restricting our attention to comparability graphs, we obtain a version of the De Bruijn-Erdős theorem for partially ordered sets (posets). Moreover, in this case, we have an improved bound on the numb…
▽ More
A classical theorem of De Bruijn and Erdős asserts that any noncollinear set of n points in the plane determines at least n distinct lines. We prove that an analogue of this theorem holds for graphs. Restricting our attention to comparability graphs, we obtain a version of the De Bruijn-Erdős theorem for partially ordered sets (posets). Moreover, in this case, we have an improved bound on the number of lines depending on the height of the poset. The extremal configurations are also determined.
△ Less
Submitted 28 January, 2015; v1 submitted 27 January, 2015;
originally announced January 2015.
