arXiv subjects

Nathan Fenner

Publications and source records attributed to Nathan Fenner.

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↗

arXiv2018

Accurate Uncertainties for Deep Learning Using Calibrated Regression

Methods for reasoning under uncertainty are a key building block of accurate and reliable machine learning systems. Bayesian methods provide a general framework to quantify uncertainty. However, because of model misspecification and the use of approximate inference, Bayesian uncertainty estimates are often inaccurate -- for example, a 90% credible interval may not contain the true outcome 90% of the time. Here, we propose a simple procedure for calibrating any regression algorithm; when applied to Bayesian and probabilistic models, it is guaranteed to produce calibrated uncertainty estimates given enough data. Our procedure is inspired by Platt scaling and extends previous work on classification. We evaluate this approach on Bayesian linear regression, feedforward, and recurrent neural networks, and find that it consistently outputs well-calibrated credible intervals while improving performance on time series forecasting and model-based reinforcement learning tasks.

cs.LG↗