arXiv subjects

Shawn Ligocki

Publications and source records attributed to Shawn Ligocki.

3 recordsLinked to original sources

arXiv2025

Determination of the fifth Busy Beaver value

The Busy Beaver value $S(n)$ is the maximum number of steps that an $n$-state 2-symbol Turing machine can perform from the all-zero tape before halting. $S$ was historically introduced by Tibor Rad\'o in 1962 as one of the simplest examples of an uncomputable function. We prove that $S(5) = 47,176,870$ using the Coq proof assistant. The proof enumerates $181,385,789$ Turing machines with 5 states and, for each machine, decides whether it halts or not. Our result marks the first determination of a new Busy Beaver value in over 40 years and the first Busy Beaver value ever to be formally verified, attesting to the effectiveness of massively collaborative online research (bbchallenge$.$org).

cs.LO↗

arXiv2025

Turing machines deciders, part I

The Busy Beaver Challenge (or bbchallenge) aims at collaboratively solving the following conjecture: "$S(5) = 47{,}176{,}870$" [Rad\'o, 1962], [Marxen and Buntrock, 1990], [Aaronson, 2020]. This conjecture says that if a 5-state Turing machine runs for more than 47,176,870 steps without halting, then it will never halt -- starting from the all-0 tape. Proving this conjecture amounts to deciding whether 181,385,789 Turing machines with 5 states halt or not -- starting from the all-0 tape [bbchallenge, 2025]. To do so, we write $\textit{deciders}$: programs that take as input a Turing machine and output either HALT, NONHALT, or UNKNOWN. Each decider is specialised in recognising a particular type of non-halting behavior. After two years of work, the Busy Beaver Challenge achieved its goal in July 2024 by delivering a proof of "$S(5) = 47{,}176{,}870$" formalised in Coq [bbchallenge, 2025]. In this document, we present deciders that were developed before the Coq proof and which were mainly not used in the proof; nonetheless, they are relevant techniques for analysing Turing machines. Part II of this work is the decider section of our paper showing "$S(5) = 47{,}176{,}870$" [bbchallenge, 2025], presenting the deciders that were used in the Coq proof.

cs.LO↗

arXiv2023

A Double Machine Learning Trend Model for Citizen Science Data

1. Citizen and community-science (CS) datasets have great potential for estimating interannual patterns of population change given the large volumes of data collected globally every year. Yet, the flexible protocols that enable many CS projects to collect large volumes of data typically lack the structure necessary to keep consistent sampling across years. This leads to interannual confounding, as changes to the observation process over time are confounded with changes in species population sizes. 2. Here we describe a novel modeling approach designed to estimate species population trends while controlling for the interannual confounding common in citizen science data. The approach is based on Double Machine Learning, a statistical framework that uses machine learning methods to estimate population change and the propensity scores used to adjust for confounding discovered in the data. Additionally, we develop a simulation method to identify and adjust for residual confounding missed by the propensity scores. Using this new method, we can produce spatially detailed trend estimates from citizen science data. 3. To illustrate the approach, we estimated species trends using data from the CS project eBird. We used a simulation study to assess the ability of the method to estimate spatially varying trends in the face of real-world confounding. Results showed that the trend estimates distinguished between spatially constant and spatially varying trends at a 27km resolution. There were low error rates on the estimated direction of population change (increasing/decreasing) and high correlations on the estimated magnitude. 4. The ability to estimate spatially explicit trends while accounting for confounding in citizen science data has the potential to fill important information gaps, helping to estimate population trends for species, regions, or seasons without rigorous monitoring data.

q-bio.QM↗