-
Quantitative equidistribution of periodic points for rational maps
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
We show that periodic points of period $n$ of a complex rational map of degree $d$ equidistribute towards the equilibrium measure $μ_f$ of the rational map with a rate of convergence of $(nd^{-n})^{1/2}$ for $\mathscr{C}^1$-observables. This is a consequence of a quantitative equidistribution of Galois invariant finite subsets of preperiodic points à la Favre and Rivera-Letelier. Our proof relies…
▽ More
We show that periodic points of period $n$ of a complex rational map of degree $d$ equidistribute towards the equilibrium measure $μ_f$ of the rational map with a rate of convergence of $(nd^{-n})^{1/2}$ for $\mathscr{C}^1$-observables. This is a consequence of a quantitative equidistribution of Galois invariant finite subsets of preperiodic points à la Favre and Rivera-Letelier. Our proof relies on the Hölder regularity of the quasi-psh Green function of a rational map, an estimate of Baker concerning Hsia kernel, as well as on the product formula and its generalization by Moriwaki for finitely generated fields over $\mathbb{Q}$.
△ Less
Submitted 5 May, 2025;
originally announced May 2025.
-
Learning Conjecturing from Scratch
Authors:
Thibault Gauthier,
Josef Urban
Abstract:
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP systems because they require a combination of inductive and arithmetical reasoning.
Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the cor…
▽ More
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP systems because they require a combination of inductive and arithmetical reasoning.
Starting from scratch, our approach consists of a feedback loop that iterates between (i) training a neural translator to learn the correspondence between the problems solved so far and the induction predicates useful for them, (ii) using the trained neural system to generate many new induction predicates for the problems, (iii) fast runs of the z3 prover attempting to prove the problems using the generated predicates, (iv) using heuristics such as predicate size and solution speed on the proved problems to choose the best predicates for the next iteration of training.
The algorithm discovers on its own many interesting induction predicates, ultimately solving 5565 problems, compared to 2265 problems solved by CVC5, Vampire or Z3 in 60 seconds.
△ Less
Submitted 3 March, 2025;
originally announced March 2025.
-
Julia sets and bifurcation loci
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
We prove that several dynamically defined fractals in $\mathbb{C}$ and $\mathbb{C}^2$ which arise from different type of polynomial dynamical systems can not be the same objects. One of our main results is that the closure of Misiurewicz PCF cubic polynomials (the strong bifurcation locus) cannot be the Julia set of a regular polynomial endomorphism of $\mathbb{C}^2$. We also show that the Julia s…
▽ More
We prove that several dynamically defined fractals in $\mathbb{C}$ and $\mathbb{C}^2$ which arise from different type of polynomial dynamical systems can not be the same objects. One of our main results is that the closure of Misiurewicz PCF cubic polynomials (the strong bifurcation locus) cannot be the Julia set of a regular polynomial endomorphism of $\mathbb{C}^2$. We also show that the Julia set of a Hénon map and a polynomial endomorphism cannot coincide.
△ Less
Submitted 25 November, 2024;
originally announced November 2024.
-
Hölder estimates and uniformity in arithmetic dynamics
Authors:
Thomas Gauthier
Abstract:
In this note we study common preperiodic points of rational maps of the Riemann Sphere. We show that given any degrees $d_1,d_2\geq2$, outside a Zariski closed subset of the space of pairs of rational maps $(f,g)$ of degree $d_1$ and $d_2$ respectively, the maps $f$ and $g$ share at most a uniformly bounded number of common preperiodic points. This generalizes a result of DeMarco and Mavraki to ma…
▽ More
In this note we study common preperiodic points of rational maps of the Riemann Sphere. We show that given any degrees $d_1,d_2\geq2$, outside a Zariski closed subset of the space of pairs of rational maps $(f,g)$ of degree $d_1$ and $d_2$ respectively, the maps $f$ and $g$ share at most a uniformly bounded number of common preperiodic points. This generalizes a result of DeMarco and Mavraki to maps of possibly different degrees. Our main contribution is the use of Hölder properties of the Green function of a rational map to obtain height estimates.
△ Less
Submitted 25 November, 2024; v1 submitted 18 July, 2024;
originally announced July 2024.
-
Domain Adaptation of Llama3-70B-Instruct through Continual Pre-Training and Model Merging: A Comprehensive Evaluation
Authors:
Shamane Siriwardhana,
Mark McQuade,
Thomas Gauthier,
Lucas Atkins,
Fernando Fernandes Neto,
Luke Meyers,
Anneketh Vij,
Tyler Odenthal,
Charles Goddard,
Mary MacCarthy,
Jacob Solawetz
Abstract:
We conducted extensive experiments on domain adaptation of the Meta-Llama-3-70B-Instruct model on SEC data, exploring its performance on both general and domain-specific benchmarks. Our focus included continual pre-training (CPT) and model merging, aiming to enhance the model's domain-specific capabilities while mitigating catastrophic forgetting. Through this study, we evaluated the impact of int…
▽ More
We conducted extensive experiments on domain adaptation of the Meta-Llama-3-70B-Instruct model on SEC data, exploring its performance on both general and domain-specific benchmarks. Our focus included continual pre-training (CPT) and model merging, aiming to enhance the model's domain-specific capabilities while mitigating catastrophic forgetting. Through this study, we evaluated the impact of integrating financial regulatory data into a robust language model and examined the effectiveness of our model merging techniques in preserving and improving the model's instructive abilities. The model is accessible at hugging face: https://huggingface.co/arcee-ai/Llama-3-SEC-Base, arcee-ai/Llama-3-SEC-Base. This is an intermediate checkpoint of our final model, which has seen 20B tokens so far. The full model is still in the process of training. This is a preprint technical report with thorough evaluations to understand the entire process.
△ Less
Submitted 21 June, 2024;
originally announced June 2024.
-
Broadband Multi-wavelength Properties of M87 during the 2018 EHT Campaign including a Very High Energy Flaring Episode
Authors:
J. C. Algaba,
M. Balokovic,
S. Chandra,
W. Y. Cheong,
Y. Z. Cui,
F. D'Ammando,
A. D. Falcone,
N. M. Ford,
M. Giroletti,
C. Goddi,
M. A. Gurwell,
K. Hada,
D. Haggard,
S. Jorstad,
A. Kaur,
T. Kawashima,
S. Kerby,
J. Y. Kim,
M. Kino,
E. V. Kravchenko,
S. S. Lee,
R. S. Lu,
S. Markoff,
J. Michail,
J. Neilsen
, et al. (721 additional authors not shown)
Abstract:
The nearby elliptical galaxy M87 contains one of the only two supermassive black holes whose emission surrounding the event horizon has been imaged by the Event Horizon Telescope (EHT). In 2018, more than two dozen multi-wavelength (MWL) facilities (from radio to gamma-ray energies) took part in the second M87 EHT campaign. The goal of this extensive MWL campaign was to better understand the physi…
▽ More
The nearby elliptical galaxy M87 contains one of the only two supermassive black holes whose emission surrounding the event horizon has been imaged by the Event Horizon Telescope (EHT). In 2018, more than two dozen multi-wavelength (MWL) facilities (from radio to gamma-ray energies) took part in the second M87 EHT campaign. The goal of this extensive MWL campaign was to better understand the physics of the accreting black hole M87*, the relationship between the inflow and inner jets, and the high-energy particle acceleration. Understanding the complex astrophysics is also a necessary first step towards performing further tests of general relativity. The MWL campaign took place in April 2018, overlapping with the EHT M87* observations. We present a new, contemporaneous spectral energy distribution (SED) ranging from radio to very high energy (VHE) gamma-rays, as well as details of the individual observations and light curves. We also conduct phenomenological modelling to investigate the basic source properties. We present the first VHE gamma-ray flare from M87 detected since 2010. The flux above 350 GeV has more than doubled within a period of about 36 hours. We find that the X-ray flux is enhanced by about a factor of two compared to 2017, while the radio and millimetre core fluxes are consistent between 2017 and 2018. We detect evidence for a monotonically increasing jet position angle that corresponds to variations in the bright spot of the EHT image. Our results show the value of continued MWL monitoring together with precision imaging for addressing the origins of high-energy particle acceleration. While we cannot currently pinpoint the precise location where such acceleration takes place, the new VHE gamma-ray flare already presents a challenge to simple one-zone leptonic emission model approaches, and emphasises the need for combined image and spectral modelling.
△ Less
Submitted 5 December, 2024; v1 submitted 24 April, 2024;
originally announced April 2024.
-
A Formal Proof of R(4,5)=25
Authors:
Thibault Gauthier,
Chad E. Brown
Abstract:
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover…
▽ More
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The authors have performed the computational parts of the proof with different implementations in order to reduce the possibility of an error in their programs. In this work, we prove this theorem in the interactive theorem prover HOL4 limiting the uncertainty to the small HOL4 kernel. Instead of verifying their algorithms directly, we rely on the HOL4 interface to MiniSat SAT to prove gluing lemmas. To reduce the number of such lemmas and thus make the computational part of the proof feasible, we implement a generalization algorithm. We verify that its output covers all the possible cases by implementing a custom SAT-solver extended with a graph isomorphism checker.
△ Less
Submitted 12 June, 2024; v1 submitted 2 April, 2024;
originally announced April 2024.
-
Learning Guided Automated Reasoning: A Brief Survey
Authors:
Lasse Blaauwbroek,
David Cerna,
Thibault Gauthier,
Jan Jakubův,
Cezary Kaliszyk,
Martin Suda,
Josef Urban
Abstract:
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance…
▽ More
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In practice, such systems however face large combinatorial explosion, and therefore include many heuristics and choice points that considerably influence their performance. This is an opportunity for trained machine learning predictors, which can guide the work of such reasoning systems. Conversely, deductive search supported by the notion of logically valid proof allows one to train machine learning systems on large reasoning corpora. Such bodies of proof are usually correct by construction and when combined with more and more precise trained guidance they can be boostrapped into very large corpora, with increasingly long reasoning chains and possibly novel proof ideas. In this paper we provide an overview of several automated reasoning and theorem proving domains and the learning and AI methods that have been so far developed for them. These include premise selection, proof guidance in several settings, AI systems and feedback loops iterating between reasoning and learning, and symbolic classification problems.
△ Less
Submitted 6 March, 2024;
originally announced March 2024.
-
The Geometric Dynamical Northcott Property in the quadratic family
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
The aim of this note is to give a proof of Theorem A from our work on the geometric Northcott property in the simpler case of the quadratic family; being in dimension $1$ in both the dynamical space and the parameter space, and having a simple and explicit parametrization of the family allow to simplify the proof and, we hope, make the ideas more apparent.
The aim of this note is to give a proof of Theorem A from our work on the geometric Northcott property in the simpler case of the quadratic family; being in dimension $1$ in both the dynamical space and the parameter space, and having a simple and explicit parametrization of the family allow to simplify the proof and, we hope, make the ideas more apparent.
△ Less
Submitted 20 July, 2023;
originally announced July 2023.
-
Variation of canonical heights of subvarieties for polarized endomorphisms
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
When an endomorphism $f:X\to X$ of a projective variety which is polarized by an ample line bundle $L$, i.e. such that $f^*L\simeq L^{\otimes d}$ with $d\geq2$, is defined over a number field, Call and Silverman defined a canonical height $\widehat{h}_f$ for $f$. In a family $(\mathcal{X},\mathcal{f},\mathcal{L})$ parametrized by a curve $S$ together with a section $P:S\to \mathcal{X}$, they show…
▽ More
When an endomorphism $f:X\to X$ of a projective variety which is polarized by an ample line bundle $L$, i.e. such that $f^*L\simeq L^{\otimes d}$ with $d\geq2$, is defined over a number field, Call and Silverman defined a canonical height $\widehat{h}_f$ for $f$. In a family $(\mathcal{X},\mathcal{f},\mathcal{L})$ parametrized by a curve $S$ together with a section $P:S\to \mathcal{X}$, they show that $\widehat{h}_{f_t}(P(t))/h(t)$ converges to the height $\widehat{h}_{f_η}(P_η)$ on the generic fiber.
In the present paper, we prove the equivalent statement when studying the variation of canonical heights of subvarieties $Y_t$ varying in a family $\mathcal{Y}$ of any relative dimension.
△ Less
Submitted 20 July, 2023;
originally announced July 2023.
-
Sparsity of postcritically finite maps of $\mathbb{P}^k$ and beyond: A complex analytic approach
Authors:
Thomas Gauthier,
Johan Taflin,
Gabriel Vigny
Abstract:
An endomorphism $f:\mathbb{P}^k\to\mathbb{P}^k$ of degree $d\geq2$ is said to be postcritically finite (or PCF) if its critical set $\mathrm{Crit}(f)$ is preperiodic, i.e. if there are integers $m>n\geq0$ such that $f^m(\mathrm{Crit}(f))\subseteq f^n(\mathrm{Crit}(f))$. When $k\geq2$, it was conjectured by Ingram, Ramadas and Silverman that, in the space $\mathrm{End}_d^k$ of all endomorphisms of…
▽ More
An endomorphism $f:\mathbb{P}^k\to\mathbb{P}^k$ of degree $d\geq2$ is said to be postcritically finite (or PCF) if its critical set $\mathrm{Crit}(f)$ is preperiodic, i.e. if there are integers $m>n\geq0$ such that $f^m(\mathrm{Crit}(f))\subseteq f^n(\mathrm{Crit}(f))$. When $k\geq2$, it was conjectured by Ingram, Ramadas and Silverman that, in the space $\mathrm{End}_d^k$ of all endomorphisms of degree $d$ of $\mathbb{P}^k$, such endomorphisms are not Zariski dense. We prove this conjecture. Further, in the space $\mathrm{Poly}_d^2$ of all regular polynomial endomorphisms of degree $d\geq2$ of the affine plane $\mathbb{A}^2$, we construct a dense and Zariski open subset where we have a uniform bound on the number of preperiodic points lying in the critical set.
The proofs are a combination of the theory of heights in arithmetic dynamics and methods from real dynamics to produce open subsets with maximal bifurcation.
△ Less
Submitted 3 May, 2023;
originally announced May 2023.
-
The James Webb Space Telescope Mission
Authors:
Jonathan P. Gardner,
John C. Mather,
Randy Abbott,
James S. Abell,
Mark Abernathy,
Faith E. Abney,
John G. Abraham,
Roberto Abraham,
Yasin M. Abul-Huda,
Scott Acton,
Cynthia K. Adams,
Evan Adams,
David S. Adler,
Maarten Adriaensen,
Jonathan Albert Aguilar,
Mansoor Ahmed,
Nasif S. Ahmed,
Tanjira Ahmed,
Rüdeger Albat,
Loïc Albert,
Stacey Alberts,
David Aldridge,
Mary Marsha Allen,
Shaune S. Allen,
Martin Altenburg
, et al. (983 additional authors not shown)
Abstract:
Twenty-six years ago a small committee report, building on earlier studies, expounded a compelling and poetic vision for the future of astronomy, calling for an infrared-optimized space telescope with an aperture of at least $4m$. With the support of their governments in the US, Europe, and Canada, 20,000 people realized that vision as the $6.5m$ James Webb Space Telescope. A generation of astrono…
▽ More
Twenty-six years ago a small committee report, building on earlier studies, expounded a compelling and poetic vision for the future of astronomy, calling for an infrared-optimized space telescope with an aperture of at least $4m$. With the support of their governments in the US, Europe, and Canada, 20,000 people realized that vision as the $6.5m$ James Webb Space Telescope. A generation of astronomers will celebrate their accomplishments for the life of the mission, potentially as long as 20 years, and beyond. This report and the scientific discoveries that follow are extended thank-you notes to the 20,000 team members. The telescope is working perfectly, with much better image quality than expected. In this and accompanying papers, we give a brief history, describe the observatory, outline its objectives and current observing program, and discuss the inventions and people who made it possible. We cite detailed reports on the design and the measured performance on orbit.
△ Less
Submitted 10 April, 2023;
originally announced April 2023.
-
A Mathematical Benchmark for Inductive Theorem Provers
Authors:
Thibault Gauthier,
Chad E. Brown,
Mikolas Janota,
Josef Urban
Abstract:
We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs requi…
▽ More
We present a benchmark of 29687 problems derived from the On-Line Encyclopedia of Integer Sequences (OEIS). Each problem expresses the equivalence of two syntactically different programs generating the same OEIS sequence. Such programs were conjectured by a learning-guided synthesis system using a language with looping operators. The operators implement recursion, and thus many of the proofs require induction on natural numbers. The benchmark contains problems of varying difficulty from a wide area of mathematical domains. We believe that these characteristics will make it an effective judge for the progress of inductive theorem provers in this domain for years to come.
△ Less
Submitted 6 April, 2023;
originally announced April 2023.
-
Complex Dynamics of birational maps of $\mathbb{P}^k$ defined over a number field
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
Jonsson and Reschke showed that birational selfmaps on projective surface defined over a number field satisfy the energy condition of Bedford and Diller so their ergodic properties are very well understood. Under suitable hypotheses on the indeterminacy loci, we extend that result to birational maps $\mathbb{P}^k\dashrightarrow\mathbb{P}^k$, $k\geq2$, defined over a number field, showing that they…
▽ More
Jonsson and Reschke showed that birational selfmaps on projective surface defined over a number field satisfy the energy condition of Bedford and Diller so their ergodic properties are very well understood. Under suitable hypotheses on the indeterminacy loci, we extend that result to birational maps $\mathbb{P}^k\dashrightarrow\mathbb{P}^k$, $k\geq2$, defined over a number field, showing that they satisfy a similar energy condition introduced by De Thélin and the second author. As a consequence, we can construct for such maps their Green measure and deduce several important ergodic consequences.
Under a mild additional hypothesis, we show that generic sequences of Galois invariant subset of periodic points equidistribute toward the Green measure.
△ Less
Submitted 22 March, 2023;
originally announced March 2023.
-
Alien Coding
Authors:
Thibault Gauthier,
Miroslav Olšák,
Josef Urban
Abstract:
We introduce a self-learning algorithm for synthesizing programs for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many iterations of a self-learning loop that interleaves (i) training neural machine translation to learn the correspondence between sequences and the programs discovered so far, and (ii) proposing many new programs for each OE…
▽ More
We introduce a self-learning algorithm for synthesizing programs for OEIS sequences. The algorithm starts from scratch initially generating programs at random. Then it runs many iterations of a self-learning loop that interleaves (i) training neural machine translation to learn the correspondence between sequences and the programs discovered so far, and (ii) proposing many new programs for each OEIS sequence by the trained neural machine translator. The algorithm discovers on its own programs for more than 78000 OEIS sequences, sometimes developing unusual programming methods. We analyze its behavior and the invented programs in several experiments.
△ Less
Submitted 30 August, 2023; v1 submitted 26 January, 2023;
originally announced January 2023.
-
Entire or rational maps with integer multipliers
Authors:
Xavier Buff,
Thomas Gauthier,
Valentin Huguin,
Jasmin Raissy
Abstract:
Let $\mathcal{O}_{K}$ be the ring of integers of an imaginary quadratic field $K$. Recently, Ji and Xie proved that every rational map $f \colon \widehat{\mathbb{C}} \rightarrow \widehat{\mathbb{C}}$ of degree $d \geq 2$ whose multipliers all lie in $\mathcal{O}_{K}$ is a power map, a Chebyshev map or a Lattès map. Their proof relies on a result from non-Archimedean dynamics obtained by Rivera-Let…
▽ More
Let $\mathcal{O}_{K}$ be the ring of integers of an imaginary quadratic field $K$. Recently, Ji and Xie proved that every rational map $f \colon \widehat{\mathbb{C}} \rightarrow \widehat{\mathbb{C}}$ of degree $d \geq 2$ whose multipliers all lie in $\mathcal{O}_{K}$ is a power map, a Chebyshev map or a Lattès map. Their proof relies on a result from non-Archimedean dynamics obtained by Rivera-Letelier. In the present note, we show that one can avoid using this result by considering a differential equation instead. Our proof of Ji and Xie's result also applies to the case of entire maps. Thus, we also show that every nonaffine entire map $f \colon \mathbb{C} \rightarrow \mathbb{C}$ whose multipliers all lie in $\mathcal{O}_{K}$ is a power map or a Chebyshev map.
△ Less
Submitted 15 September, 2023; v1 submitted 7 December, 2022;
originally announced December 2022.
-
Self-Supervised 3D Monocular Object Detection by Recycling Bounding Boxes
Authors:
Sugirtha T,
Sridevi M,
Khailash Santhakumar,
Hao Liu,
B Ravi Kiran,
Thomas Gauthier,
Senthil Yogamani
Abstract:
Modern object detection architectures are moving towards employing self-supervised learning (SSL) to improve performance detection with related pretext tasks. Pretext tasks for monocular 3D object detection have not yet been explored yet in literature. The paper studies the application of established self-supervised bounding box recycling by labeling random windows as the pretext task. The classif…
▽ More
Modern object detection architectures are moving towards employing self-supervised learning (SSL) to improve performance detection with related pretext tasks. Pretext tasks for monocular 3D object detection have not yet been explored yet in literature. The paper studies the application of established self-supervised bounding box recycling by labeling random windows as the pretext task. The classifier head of the 3D detector is trained to classify random windows containing different proportions of the ground truth objects, thus handling the foreground-background imbalance. We evaluate the pretext task using the RTM3D detection model as baseline, with and without the application of data augmentation. We demonstrate improvements of between 2-3 % in mAP 3D and 0.9-1.5 % BEV scores using SSL over the baseline scores. We propose the inverse class frequency re-weighted (ICFW) mAP score that highlights improvements in detection for low frequency classes in a class imbalanced dataset with long tails. We demonstrate improvements in ICFW both mAP 3D and BEV scores to take into account the class imbalance in the KITTI validation dataset. We see 4-5 % increase in ICFW metric with the pretext task.
△ Less
Submitted 25 June, 2022;
originally announced June 2022.
-
Topos: A Secure, Trustless, and Decentralized Interoperability Protocol
Authors:
Théo Gauthier,
Sébastien Dan,
Monir Hadji,
Antonella Del Pozzo,
Yackolley Amoussou-Guenou
Abstract:
Topos is an open interoperability protocol designed to reduce as much as possible trust assumptions by replacing them with cryptographic constructions and decentralization while exhibiting massive scalability. The protocol does not make use of a central blockchain, nor uses consensus to ensure consistent delivery of messages across a heterogeneous ecosystem of public and private blockchains, named…
▽ More
Topos is an open interoperability protocol designed to reduce as much as possible trust assumptions by replacing them with cryptographic constructions and decentralization while exhibiting massive scalability. The protocol does not make use of a central blockchain, nor uses consensus to ensure consistent delivery of messages across a heterogeneous ecosystem of public and private blockchains, named subnets, but instead relies on a weak causal reliable broadcast implemented by a distributed network which we call $\textit{Transmission Control Engine}$ (TCE). The validity of cross-subnet messages is ensured by the $\textit{Universal Certificate Interface}$ (UCI) and stems from zkSTARK proofs asserting the validity of subnets' state transitions executed by the Topos zkVM. Such proofs of computational integrity are publicly verifiable by any other participants in and out the protocol such as other subnets or audit companies. The interface between the TCE and subnets leverages the ICE-FROST protocol, an innovative threshold signature scheme, whose static public key allows for uniquely identifying subnets after they register in the protocol. The Topos protocol is designed to provide $\textit{uniform security}$ to the ecosystem and to handle any type of subnets (e.g., permissioned, permissionless) in order to fit any business use cases and pave the way for global adoption and a new standard for the Internet base layer.
△ Less
Submitted 8 February, 2023; v1 submitted 7 June, 2022;
originally announced June 2022.
-
Learning Program Synthesis for Integer Sequences from Scratch
Authors:
Thibault Gauthier,
Josef Urban
Abstract:
We present a self-learning approach for synthesizing programs from integer sequences. Our method relies on a tree search guided by a learned policy. Our system is tested on the On-Line Encyclopedia of Integer Sequences. There, it discovers, on its own, solutions for 27987 sequences starting from basic operators and without human-written training examples.
We present a self-learning approach for synthesizing programs from integer sequences. Our method relies on a tree search guided by a learned policy. Our system is tested on the On-Line Encyclopedia of Integer Sequences. There, it discovers, on its own, solutions for 27987 sequences starting from basic operators and without human-written training examples.
△ Less
Submitted 29 November, 2022; v1 submitted 24 February, 2022;
originally announced February 2022.
-
Simulation-to-Reality domain adaptation for offline 3D object annotation on pointclouds with correlation alignment
Authors:
Weishuang Zhang,
B Ravi Kiran,
Thomas Gauthier,
Yanis Mazouz,
Theo Steger
Abstract:
Annotating objects with 3D bounding boxes in LiDAR pointclouds is a costly human driven process in an autonomous driving perception system. In this paper, we present a method to semi-automatically annotate real-world pointclouds collected by deployment vehicles using simulated data. We train a 3D object detector model on labeled simulated data from CARLA jointly with real world pointclouds from ou…
▽ More
Annotating objects with 3D bounding boxes in LiDAR pointclouds is a costly human driven process in an autonomous driving perception system. In this paper, we present a method to semi-automatically annotate real-world pointclouds collected by deployment vehicles using simulated data. We train a 3D object detector model on labeled simulated data from CARLA jointly with real world pointclouds from our target vehicle. The supervised object detection loss is augmented with a CORAL loss term to reduce the distance between labeled simulated and unlabeled real pointcloud feature representations. The goal here is to learn representations that are invariant to simulated (labeled) and real-world (unlabeled) target domains. We also provide an updated survey on domain adaptation methods for pointclouds.
△ Less
Submitted 26 February, 2022; v1 submitted 5 February, 2022;
originally announced February 2022.
-
When do two rational functions have locally biholomorphic Julia sets?
Authors:
Romain Dujardin,
Charles Favre,
Thomas Gauthier
Abstract:
In this article we address the following question, whose interest was recently renewed by problems arising in arithmetic dynamics: under which conditions does there exist a local biholomorphism between the Julia sets of two given one-dimensional rational maps? In particular we find criteria ensuring that such a local isomorphism is induced by an algebraic correspondence. This extends and unifies c…
▽ More
In this article we address the following question, whose interest was recently renewed by problems arising in arithmetic dynamics: under which conditions does there exist a local biholomorphism between the Julia sets of two given one-dimensional rational maps? In particular we find criteria ensuring that such a local isomorphism is induced by an algebraic correspondence. This extends and unifies classical results due to Baker, Beardon, Eremenko, Levin, Przytycki and others. The proof involves entire curves and positive currents.
△ Less
Submitted 11 January, 2022;
originally announced January 2022.
-
Learned Provability Likelihood for Tactical Search
Authors:
Thibault Gauthier
Abstract:
We present a method to estimate the provability of a mathematical formula. We adapt the tactical theorem prover TacticToe to factor in these estimations. Experiments over the HOL4 library show an increase in the number of theorems re-proven by TacticToe thanks to this additional guidance. This amelioration in performance together with concurrent updates to the TacticToe framework lead to an improv…
▽ More
We present a method to estimate the provability of a mathematical formula. We adapt the tactical theorem prover TacticToe to factor in these estimations. Experiments over the HOL4 library show an increase in the number of theorems re-proven by TacticToe thanks to this additional guidance. This amelioration in performance together with concurrent updates to the TacticToe framework lead to an improved user experience.
△ Less
Submitted 6 September, 2021;
originally announced September 2021.
-
Good height functions on quasi-projective varieties: equidistribution and applications in dynamics
Authors:
Thomas Gauthier
Abstract:
In the present article, we define a notion of good height functions on quasi-projective varieties $V$ defined over number fields and prove an equidistribution theorem of small points for such height functions. Those good height functions are defined as limits of height functions associated with semi-positive adelic metrization on big and nef $\mathbb{Q}$-line bundles on projective models of $V$ sa…
▽ More
In the present article, we define a notion of good height functions on quasi-projective varieties $V$ defined over number fields and prove an equidistribution theorem of small points for such height functions. Those good height functions are defined as limits of height functions associated with semi-positive adelic metrization on big and nef $\mathbb{Q}$-line bundles on projective models of $V$ satisfying mild assumptions.
Building on a recent work of the author and Vigny as well as on a classical estimate of Call and Silverman, and inspiring from recent works of Kühne and Yuan and Zhang, we deduce the equidistribution of generic sequence of preperiodic parameters for families of polarized endomorphisms with marked points.
△ Less
Submitted 22 March, 2023; v1 submitted 6 May, 2021;
originally announced May 2021.
-
Exploring 2D Data Augmentation for 3D Monocular Object Detection
Authors:
Sugirtha T,
Sridevi M,
Khailash Santhakumar,
B Ravi Kiran,
Thomas Gauthier,
Senthil Yogamani
Abstract:
Data augmentation is a key component of CNN based image recognition tasks like object detection. However, it is relatively less explored for 3D object detection. Many standard 2D object detection data augmentation techniques do not extend to 3D box. Extension of these data augmentations for 3D object detection requires adaptation of the 3D geometry of the input scene and synthesis of new viewpoint…
▽ More
Data augmentation is a key component of CNN based image recognition tasks like object detection. However, it is relatively less explored for 3D object detection. Many standard 2D object detection data augmentation techniques do not extend to 3D box. Extension of these data augmentations for 3D object detection requires adaptation of the 3D geometry of the input scene and synthesis of new viewpoints. This requires accurate depth information of the scene which may not be always available. In this paper, we evaluate existing 2D data augmentations and propose two novel augmentations for monocular 3D detection without a requirement for novel view synthesis. We evaluate these augmentations on the RTM3D detection model firstly due to the shorter training times . We obtain a consistent improvement by 4% in the 3D AP (@IoU=0.7) for cars, ~1.8% scores 3D AP (@IoU=0.25) for pedestrians & cyclists, over the baseline on KITTI car detection dataset. We also demonstrate a rigorous evaluation of the mAP scores by re-weighting them to take into account the class imbalance in the KITTI validation dataset.
△ Less
Submitted 21 April, 2021;
originally announced April 2021.
-
The Geometric Dynamical Northcott Property For Regular Polynomial Automorphisms of the Affine Plane
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
We establish the finiteness of periodic points, that we called Geometric Dynamical Northcott Property, for regular polynomials automorphisms of the affine plane over a function field $\mathbf{K}$ of characteristic zero, improving results of Ingram.
For that, we show that when $\mathbf{K}$ is the field of rational functions of a smooth complex projective curve, the canonical height of a subvariet…
▽ More
We establish the finiteness of periodic points, that we called Geometric Dynamical Northcott Property, for regular polynomials automorphisms of the affine plane over a function field $\mathbf{K}$ of characteristic zero, improving results of Ingram.
For that, we show that when $\mathbf{K}$ is the field of rational functions of a smooth complex projective curve, the canonical height of a subvariety is the mass of an appropriate bifurcation current and that a marked point is stable if and only if its canonical height is zero. We then establish the Geometric Dynamical Northcott Property using a similarity argument.
△ Less
Submitted 30 October, 2020;
originally announced October 2020.
-
Tree Neural Networks in HOL4
Authors:
Thibault Gauthier
Abstract:
We present an implementation of tree neural networks within the proof assistant HOL4. Their architecture makes them naturally suited for approximating functions whose domain is a set of formulas. We measure the performance of our implementation and compare it with other machine learning predictors on the tasks of evaluating arithmetical expressions and estimating the truth of propositional formula…
▽ More
We present an implementation of tree neural networks within the proof assistant HOL4. Their architecture makes them naturally suited for approximating functions whose domain is a set of formulas. We measure the performance of our implementation and compare it with other machine learning predictors on the tasks of evaluating arithmetical expressions and estimating the truth of propositional formulas.
△ Less
Submitted 3 September, 2020;
originally announced September 2020.
-
The arithmetic of polynomial dynamical pairs
Authors:
Charles Favre,
Thomas Gauthier
Abstract:
We study one-dimensional algebraic families of pairs given by a polynomial with a marked point. We prove an "unlikely intersection" statement for such pairs thereby exhibiting strong rigidity features for these pairs. We infer from this result the dynamical André-Oort conjecture for curves in the moduli space of polynomials, by describing one-dimensional families in this parameter space containing…
▽ More
We study one-dimensional algebraic families of pairs given by a polynomial with a marked point. We prove an "unlikely intersection" statement for such pairs thereby exhibiting strong rigidity features for these pairs. We infer from this result the dynamical André-Oort conjecture for curves in the moduli space of polynomials, by describing one-dimensional families in this parameter space containing infinitely many post-critically finite parameters.
△ Less
Submitted 28 April, 2020;
originally announced April 2020.
-
Parametric Lyapunov exponents
Authors:
Henry De Thélin,
Thomas Gauthier,
Gabriel Vigny
Abstract:
In an algebraic family of rational maps of $\mathbb{P}^1$, we show that, for almost every parameter for the trace of the bifurcation current of a marked critical value, the critical value is Collet-Eckmann. This extends previous results of Graczyk and Świcatek in the unicritical family, using Makarov theorem. Our methods are based instead on ideas of laminar currents theory.
In an algebraic family of rational maps of $\mathbb{P}^1$, we show that, for almost every parameter for the trace of the bifurcation current of a marked critical value, the critical value is Collet-Eckmann. This extends previous results of Graczyk and Świcatek in the unicritical family, using Makarov theorem. Our methods are based instead on ideas of laminar currents theory.
△ Less
Submitted 30 March, 2020;
originally announced March 2020.
-
The Geometric Dynamical Northcott and Bogomolov Properties
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
We establish the dynamical Northcott property for polarized endomorphisms of a projective variety over a function field $\mathbf{K}$ of characteristic zero, and we relate this property to the notion of stability in complex dynamics. This extends previous results of Benedetto, Baker and DeMarco in dimension $1$, and of Chatzidakis-Hrushovski in higher dimension. Our proof uses complex dynamics argu…
▽ More
We establish the dynamical Northcott property for polarized endomorphisms of a projective variety over a function field $\mathbf{K}$ of characteristic zero, and we relate this property to the notion of stability in complex dynamics. This extends previous results of Benedetto, Baker and DeMarco in dimension $1$, and of Chatzidakis-Hrushovski in higher dimension. Our proof uses complex dynamics arguments and does not rely on the previous ones.
We first show that, when $\mathbf{K}$ is the field of rational functions of a normal complex projective variety, the canonical height of a subvariety is the mass of an appropriate bifurcation current and that a marked point is stable if and only if its canonical height is zero. We then establish the geometric dynamical Northcott property characterizing points of height zero in this setting, using a similarity argument. Moving from points to subvarieties, we propose, for polarized endomorphisms, a dynamical version of the geometric Bogomolov conjecture, recently proved by Cantat, Gao, Habegger, and Xie in the original setting of abelian varieties.
△ Less
Submitted 17 September, 2024; v1 submitted 17 December, 2019;
originally announced December 2019.
-
Self-Learned Formula Synthesis in Set Theory
Authors:
Chad E. Brown,
Thibault Gauthier
Abstract:
A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments.
A reinforcement learning algorithm accomplishes the task of synthesizing a set-theoretical formula that evaluates to given truth values for given assignments.
△ Less
Submitted 3 December, 2019;
originally announced December 2019.
-
Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic
Authors:
Thibault Gauthier
Abstract:
The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modules and the HOL4 library is achieved by the choice of tree neural networks (TNNs) as machine learning models and the internal use of HOL4 terms to represent tree structures of TNNs. Recursive improvement is possible when…
▽ More
The paper describes a deep reinforcement learning framework based on self-supervised learning within the proof assistant HOL4. A close interaction between the machine learning modules and the HOL4 library is achieved by the choice of tree neural networks (TNNs) as machine learning models and the internal use of HOL4 terms to represent tree structures of TNNs. Recursive improvement is possible when a task is expressed as a search problem. In this case, a Monte Carlo Tree Search (MCTS) algorithm guided by a TNN can be used to explore the search space and produce better examples for training the next TNN. As an illustration, term synthesis tasks on combinators and Diophantine equations are specified and learned. We achieve a success rate of 65% on combinator synthesis problems outperforming state-of-the-art ATPs run with their best general set of strategies. We set a precedent for statistically guided synthesis of Diophantine equations by solving 78.5% of the generated test problems.
△ Less
Submitted 24 April, 2020; v1 submitted 25 October, 2019;
originally announced October 2019.
-
GRUNGE: A Grand Unified ATP Challenge
Authors:
Chad E. Brown,
Thibault Gauthier,
Cezary Kaliszyk,
Geoff Sutcliffe,
Josef Urban
Abstract:
This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers t…
▽ More
This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formats on corresponding problems, and compare their performances. This also results in a new "grand unified" large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple ATP formalisms in complementary ways, and jointly learn from the accumulated knowledge.
△ Less
Submitted 19 November, 2019; v1 submitted 6 March, 2019;
originally announced March 2019.
-
Dynamical pairs with an absolutely continuous bifurcation measure
Authors:
Thomas Gauthier
Abstract:
In this article, we study algebraic dynamical pairs $(f,a)$ parametrized by an irreducible quasi-projective curve $Λ$ having an absolutely continuous bifurcation measure. We prove that, if $f$ is non-isotrivial and $(f,a)$ is unstable, this is equivalent to the fact that $f$ is a family of Lattès maps. To do so, we prove the density of transversely prerepelling parameters in the bifucation locus o…
▽ More
In this article, we study algebraic dynamical pairs $(f,a)$ parametrized by an irreducible quasi-projective curve $Λ$ having an absolutely continuous bifurcation measure. We prove that, if $f$ is non-isotrivial and $(f,a)$ is unstable, this is equivalent to the fact that $f$ is a family of Lattès maps. To do so, we prove the density of transversely prerepelling parameters in the bifucation locus of $(f,a)$ and a similarity property, at any transversely prerepelling parameter $λ_0$, between the measure $μ_{f,a}$ and the maximal entropy measure of $f_{λ_0}$. We also establish an equivalent result for dynamical pairs of $\mathbb{P}^k$, under an additional assumption.
△ Less
Submitted 15 April, 2021; v1 submitted 4 October, 2018;
originally announced October 2018.
-
The bifurcation measure has maximal entropy
Authors:
Henry De Thélin,
Thomas Gauthier,
Gabriel Vigny
Abstract:
Let $Λ$ be a complex manifold and let $(f_λ)_{λ\in Λ}$ be a holomorphic family of rational maps of degree $d\geq 2$ of $\mathbb{P}^1$. We define a natural notion of entropy of bifurcation, mimicking the classical definition of entropy, by the parametric growth rate of critical orbits. We also define a notion a measure-theoretic bifurcation entropy for which we prove a variational principle: the me…
▽ More
Let $Λ$ be a complex manifold and let $(f_λ)_{λ\in Λ}$ be a holomorphic family of rational maps of degree $d\geq 2$ of $\mathbb{P}^1$. We define a natural notion of entropy of bifurcation, mimicking the classical definition of entropy, by the parametric growth rate of critical orbits. We also define a notion a measure-theoretic bifurcation entropy for which we prove a variational principle: the measure of bifurcation is a measure of maximal entropy. We rely crucially on a generalization of Yomdin's bound of the volume of the image of a dynamical ball.
Applying our technics to complex dynamics in several variables, we notably define and compute the entropy of the trace measure of the Green currents of a holomorphic endomorphism of $\mathbb{P}^k$.
△ Less
Submitted 29 May, 2018;
originally announced May 2018.
-
TacticToe: Learning to Prove with Tactics
Authors:
Thibault Gauthier,
Cezary Kaliszyk,
Josef Urban,
Ramana Kumar,
Michael Norrish
Abstract:
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the…
▽ More
We implement a automated tactical prover TacticToe on top of the HOL4 interactive theorem prover. TacticToe learns from human proofs which mathematical technique is suitable in each proof situation. This knowledge is then used in a Monte Carlo tree search algorithm to explore promising tactic-level proof paths. On a single CPU, with a time limit of 60 seconds, TacticToe proves 66.4 percent of the 7164 theorems in HOL4's standard library, whereas E prover with auto-schedule solves 34.5 percent. The success rate rises to 69.0 percent by combining the results of TacticToe and E prover.
△ Less
Submitted 1 December, 2021; v1 submitted 2 April, 2018;
originally announced April 2018.
-
Learning to Reason with HOL4 tactics
Authors:
Thibault Gauthier,
Cezary Kaliszyk,
Josef Urban
Abstract:
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropr…
▽ More
Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such "hammer" tech- niques complement traditional proof assistant automation as implemented by tactics and decision procedures. In this paper we present a unified proof assistant automation approach which attempts to automate the selection of appropriate tactics and tactic-sequences com- bined with an optimized small-scale hammering approach. We implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified A*-algorithm directly in HOL4 that explores different tactic-level proof paths, guiding their selection by learning from a large number of previous tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids translation to FOL, working directly on the HOL level. By combining tactic prediction and premise selection, TacticToe is able to re-prove 39 percent of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves 32 percent in the same amount of time.
△ Less
Submitted 2 April, 2018;
originally announced April 2018.
-
Approximation of non-archimedean Lyapunov exponents and applications over global fields
Authors:
Thomas Gauthier,
Yusuke Okuyama,
Gabriel Vigny
Abstract:
Let $K$ be an algebraically closed field of characteristic 0 that is complete with respect to a non-archimedean absolute value. We establish a locally uniform approximation formula of the Lyapunov exponent of a rational map $f$ of $\mathbb{P}^1$ of degree $d>1$ over $K$, in terms of the multipliers of $n$-periodic points of $f$, with an explicit control in terms of $n$, $f$ and $K$. As an immediat…
▽ More
Let $K$ be an algebraically closed field of characteristic 0 that is complete with respect to a non-archimedean absolute value. We establish a locally uniform approximation formula of the Lyapunov exponent of a rational map $f$ of $\mathbb{P}^1$ of degree $d>1$ over $K$, in terms of the multipliers of $n$-periodic points of $f$, with an explicit control in terms of $n$, $f$ and $K$. As an immediate consequence, we obtain an estimate for the blow-up of the Lyapunov exponent near a pole in one-dimensional families of rational maps over $K$. Combined with our former archimedean version, this non-archimedean quantitative approximation allows us to show:
- a quantified version of Silverman's and Ingram's recent comparison between the critical height and any ample height on the moduli space $\mathcal{M}_d(\bar{\mathbb{Q}})$,
- two improvements of McMullen's finiteness of the multiplier maps: reduction to multipliers of cycles of exact given period and an effective bound from below on the period,
- a characterization of non-affine isotrivial rational maps defined over the function field $\mathbb{C}(X)$ of a normal projective variety $X$ in terms of the growth of the degree of the multipliers.
△ Less
Submitted 27 March, 2018; v1 submitted 19 March, 2018;
originally announced March 2018.
-
Continuity of the Green function in meromorphic families of polynomials
Authors:
Charles Favre,
Thomas Gauthier
Abstract:
We prove that along any marked point the Green function of a meromorphic family of polynomials parameterized by the punctured unit disk explodes exponentially fast near the origin with a continuous error term.
We prove that along any marked point the Green function of a meromorphic family of polynomials parameterized by the punctured unit disk explodes exponentially fast near the origin with a continuous error term.
△ Less
Submitted 29 June, 2017; v1 submitted 14 June, 2017;
originally announced June 2017.
-
Collet, Eckmann and the bifurcation measure
Authors:
Matthieu Astorg,
Thomas Gauthier,
Nicolae Mihalache,
Gabriel Vigny
Abstract:
The moduli space $\mathcal{M}_d$ of degree $d\geq2$ rational maps can naturally be endowed with a measure $μ_\mathrm{bif}$ detecting maximal bifurcations, called the bifurcation measure. We prove that the support of the bifurcation measure $μ_\mathrm{bif}$ has positive Lebesgue measure. To do so, we establish a general sufficient condition for the conjugacy class of a rational map to belong to the…
▽ More
The moduli space $\mathcal{M}_d$ of degree $d\geq2$ rational maps can naturally be endowed with a measure $μ_\mathrm{bif}$ detecting maximal bifurcations, called the bifurcation measure. We prove that the support of the bifurcation measure $μ_\mathrm{bif}$ has positive Lebesgue measure. To do so, we establish a general sufficient condition for the conjugacy class of a rational map to belong to the support of $μ_\mathrm{bif}$ and we exhibit a large set of Collet-Eckmann rational maps which satisfy this condition. As a consequence, we get a set of Collet-Eckmann rational maps of positive Lebesgue measure which are approximated by hyperbolic rational maps.
△ Less
Submitted 17 May, 2017;
originally announced May 2017.
-
Hyperbolic components of rational maps: Quantitative equidistribution and counting
Authors:
Thomas Gauthier,
Yûsuke Okuyama,
Gabriel Vigny
Abstract:
Let $Λ$ be a quasi-projective variety and assume that, either $Λ$ is a subvariety of the moduli space $\mathcal{M}_d$ of degree $d$ rational maps, or $Λ$ parametrizes an algebraic family $(f_λ)_{λ\inΛ}$ of degree $d$ rational maps on $\mathbb{P}^1$. We prove the equidistribution of parameters having $p$ distinct neutral cycles towards the $p$-th bifurcation current letting the periods of the cycle…
▽ More
Let $Λ$ be a quasi-projective variety and assume that, either $Λ$ is a subvariety of the moduli space $\mathcal{M}_d$ of degree $d$ rational maps, or $Λ$ parametrizes an algebraic family $(f_λ)_{λ\inΛ}$ of degree $d$ rational maps on $\mathbb{P}^1$. We prove the equidistribution of parameters having $p$ distinct neutral cycles towards the $p$-th bifurcation current letting the periods of the cycles go to $\infty$, with an exponential speed of convergence. We deduce several fundamental consequences of this result on equidistribution and counting of hyperbolic components. A key step of the proof is a locally uniform version of the quantitative approximation of the Lyapunov exponent of a rational map by the $\log^+$ of the modulus of the multipliers of periodic points.
△ Less
Submitted 16 May, 2017; v1 submitted 15 May, 2017;
originally announced May 2017.
-
Distribution of points with prescribed derivative in polynomial dynamics
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
In analogy to the equidistribution of preimages of a prescribed point by the iterates of a polynomial map in the complex plane towards the equilibrium measure, we show here the equidistribution of points for which the derivative of the n-th iterate of the polynomial takes a suitable prescribed value towards the equilibrium measure. We then give a similar statement in the space of degree d polynomi…
▽ More
In analogy to the equidistribution of preimages of a prescribed point by the iterates of a polynomial map in the complex plane towards the equilibrium measure, we show here the equidistribution of points for which the derivative of the n-th iterate of the polynomial takes a suitable prescribed value towards the equilibrium measure. We then give a similar statement in the space of degree d polynomials for the equidistribution of parameters for which the n-derivative at a given critical value has a prescribed derivative towards the activity current of the corresponding critical point.
△ Less
Submitted 17 June, 2016;
originally announced June 2016.
-
Classification of special curves in the space of cubic polynomials
Authors:
Charles Favre,
Thomas Gauthier
Abstract:
We describe all special curves in the parameter space of complex cubic polynomials, that is all algebraic irreducible curves containing infinitely many post-critically finite polynomials. This solves in a strong form a conjecture by Baker and DeMarco for cubic polynomials.
We also prove that an irreducible component of the algebraic curve consisting of those cubic polynomials that admit an orbit…
▽ More
We describe all special curves in the parameter space of complex cubic polynomials, that is all algebraic irreducible curves containing infinitely many post-critically finite polynomials. This solves in a strong form a conjecture by Baker and DeMarco for cubic polynomials.
We also prove that an irreducible component of the algebraic curve consisting of those cubic polynomials that admit an orbit of any given period and given multiplier is special if and only if the multiplier is 0.
△ Less
Submitted 20 June, 2016; v1 submitted 16 March, 2016;
originally announced March 2016.
-
Symmetrization of Rational Maps: Arithmetic Properties and Families of Lattès Maps of $\mathbb P^k$
Authors:
Thomas Gauthier,
Benjamin Hutz,
Scott Kaschner
Abstract:
In this paper we study properties of endomorphisms of $\p^k$ using a symmetric product construction $(\p^1)^k/\mathfrak{S}_k \cong \p^k$. Symmetric products have been used to produce examples of endomorphisms of $\p^k$ with certain characteristics, $k\geq2$. In the present note, we discuss the use of these maps to enlighten stability phenomena in parameter spaces. In particular, we study $k$-deep…
▽ More
In this paper we study properties of endomorphisms of $\p^k$ using a symmetric product construction $(\p^1)^k/\mathfrak{S}_k \cong \p^k$. Symmetric products have been used to produce examples of endomorphisms of $\p^k$ with certain characteristics, $k\geq2$. In the present note, we discuss the use of these maps to enlighten stability phenomena in parameter spaces. In particular, we study $k$-deep post-critically finite maps and characterize families of Lattès maps.
△ Less
Submitted 5 December, 2022; v1 submitted 15 March, 2016;
originally announced March 2016.
-
Distribution of postcritically finite polynomials iii: Combinatorial continuity
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
In the first part of the present paper, we continue our study of distribution of postcritically finite parameters in the moduli space of polynomials: we show the equidistribution of Misiurewicz parameters with prescribed combinatorics toward the bifurcation measure. Our results essentially rely on a combinatorial description of the escape locus and of the bifurcation measure developped by Kiwi an…
▽ More
In the first part of the present paper, we continue our study of distribution of postcritically finite parameters in the moduli space of polynomials: we show the equidistribution of Misiurewicz parameters with prescribed combinatorics toward the bifurcation measure. Our results essentially rely on a combinatorial description of the escape locus and of the bifurcation measure developped by Kiwi and Dujardin-Favre. In the second part of the paper, we construct a bifurcation measure for the connectedness locus of the quadratic anti-holomorphic family which is supported by a strict subset of the boundary of the Tricorn. We also establish an approximation property by Misiurewicz parameters in the spirit of the previous one. Finally, we answer a question of Kiwi, exhibiting in the moduli space of degree 4 polynomials, non-trivial Impression of specific combinatorics.
△ Less
Submitted 2 February, 2016;
originally announced February 2016.
-
Premise Selection and External Provers for HOL4
Authors:
Thibault Gauthier,
Cezary Kaliszyk
Abstract:
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the t…
▽ More
Learning-assisted automated reasoning has recently gained popularity among the users of Isabelle/HOL, HOL Light, and Mizar. In this paper, we present an add-on to the HOL4 proof assistant and an adaptation of the HOLyHammer system that provides machine learning-based premise selection and automated reasoning also for HOL4. We efficiently record the HOL4 dependencies and extract features from the theorem statements, which form a basis for premise selection. HOLyHammer transforms the HOL4 statements in the various TPTP-ATP proof formats, which are then processed by the ATPs. We discuss the different evaluation settings: ATPs, accessible lemmas, and premise numbers. We measure the performance of HOLyHammer on the HOL4 standard library. The results are combined accordingly and compared with the HOL Light experiments, showing a comparably high quality of predictions. The system directly benefits HOL4 users by automatically finding proofs dependencies that can be reconstructed by Metis.
△ Less
Submitted 11 September, 2015;
originally announced September 2015.
-
Sharing HOL4 and HOL Light proof knowledge
Authors:
Thibault Gauthier,
Cezary Kaliszyk
Abstract:
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectur…
▽ More
New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOL(y)Hammer, whose single best strategy could automatically find proofs for 30% of the HOL Light problems, can prove 40% with the knowledge from HOL4.
△ Less
Submitted 11 September, 2015;
originally announced September 2015.
-
Distribution of postcritically finite polynomials II: Speed of convergence
Authors:
Thomas Gauthier,
Gabriel Vigny
Abstract:
In the moduli space of degree d polynomials, we prove the equidistribution of postcritically finite polynomials toward the bifurcation measure. More precisely, using complex analytic arguments and pluripotential theory, we prove the exponential speed of convergence for C 2-observables. This improves results obtained with arithmetic methods by Favre and Rivera-Letellier in the unicritical family an…
▽ More
In the moduli space of degree d polynomials, we prove the equidistribution of postcritically finite polynomials toward the bifurcation measure. More precisely, using complex analytic arguments and pluripotential theory, we prove the exponential speed of convergence for C 2-observables. This improves results obtained with arithmetic methods by Favre and Rivera-Letellier in the unicritical family and Favre and the first author in the space of degree d polynomials. We deduce from that the equidistribution of hyperbolic parameters with (d -- 1) distinct attracting cycles of given multipliers toward the bifurcation measure with exponential speed for C 1-observables. As an application, we prove the equidistribution (up to an explicit extraction) of parameters with (d -- 1) distinct cycles with prescribed multiplier toward the bifurcation measure for any (d -- 1) multipliers outside a pluripolar set.
△ Less
Submitted 2 December, 2016; v1 submitted 27 May, 2015;
originally announced May 2015.
-
Matching concepts across HOL libraries
Authors:
Thibault Gauthier,
Cezary Kaliszyk
Abstract:
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 advan…
▽ More
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.
△ Less
Submitted 15 May, 2014;
originally announced May 2014.
-
Equidistribution towards the bifurcation current I : Multipliers and degree d polynomials
Authors:
Thomas Gauthier
Abstract:
In the moduli space of degree d polynomials, the set Per\_n(w) of classes [f] for which f admits a cycle of exact period n and multiplier w is known to be an algebraic hypersurface. We prove that, given a complex number w, these hypersurfaces equidistribute towards the bifurcation current as n tends to infinity.
In the moduli space of degree d polynomials, the set Per\_n(w) of classes [f] for which f admits a cycle of exact period n and multiplier w is known to be an algebraic hypersurface. We prove that, given a complex number w, these hypersurfaces equidistribute towards the bifurcation current as n tends to infinity.
△ Less
Submitted 24 April, 2015; v1 submitted 29 December, 2013;
originally announced December 2013.
-
Quadratic polynomials, multipliers and equidistribution
Authors:
Xavier Buff,
Thomas Gauthier
Abstract:
Given a sequence of complex numbers ρ_n, we study the asymptotic distribution of the sets of parameters c ε C such that the quadratic maps z^2 +c has a cycle of period n and multiplier ρ_n. Assume 1/n.log|ρ_n| tends to L. If L {\leq} log 2, they equidistribute on the boundary of the Mandelbrot set. If L > log 2 they equidistribute on the equipotential of the Mandelbrot set of level 2L - 2 log 2.
Given a sequence of complex numbers ρ_n, we study the asymptotic distribution of the sets of parameters c ε C such that the quadratic maps z^2 +c has a cycle of period n and multiplier ρ_n. Assume 1/n.log|ρ_n| tends to L. If L {\leq} log 2, they equidistribute on the boundary of the Mandelbrot set. If L > log 2 they equidistribute on the equipotential of the Mandelbrot set of level 2L - 2 log 2.
△ Less
Submitted 12 June, 2013;
originally announced June 2013.
