arXiv subjects

John Harrison

Publications and source records attributed to John Harrison.

10 recordsLinked to original sources

arXiv2026

s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs

Neurosymbolic approaches leveraging Large Language Models (LLMs) with formal methods have recently achieved strong results on mathematics-oriented theorem-proving benchmarks. However, success on competition-style mathematics does not by itself demonstrate the ability to construct proofs about real-world implementations. We address this gap with a benchmark derived from an industrial cryptographic library whose assembly routines are already verified in HOL Light. s2n-bignum is a library used at AWS for providing fast assembly routines for cryptography, and its correctness is established by formal verification. The task of formally verifying this library has been a significant achievement for the Automated Reasoning Group. It involved two tasks: (1) precisely specifying the correct behavior of a program as a mathematical proposition, and (2) proving that the proposition is correct. In the case of s2n-bignum, both tasks were carried out by human experts. In \textit{s2n-bignum-bench}, we provide the formal specification and ask the LLM to generate a proof script that is accepted by HOL Light within a fixed proof-check timeout. To our knowledge, \textit{s2n-bignum-bench} is the first public benchmark focused on machine-checkable proof synthesis for industrial low-level cryptographic assembly routines in HOL Light. This benchmark provides a challenging and practically relevant testbed for evaluating LLM-based theorem proving beyond competition mathematics. The code to set up and use the benchmark is available here: \href{https://github.com/kings-crown/s2n-bignum-bench}{s2n-bignum-bench}.

cs.PL↗

arXiv2026

Grandes Modelos de Linguagem Multimodais (MLLMs): Da Teoria \`a Pr\'atica

Multimodal Large Language Models (MLLMs) combine the natural language understanding and generation capabilities of LLMs with perception skills in modalities such as image and audio, representing a key advancement in contemporary AI. This chapter presents the main fundamentals of MLLMs and emblematic models. Practical techniques for preprocessing, prompt engineering, and building multimodal pipelines with LangChain and LangGraph are also explored. For further practical study, supplementary material is publicly available online: https://github.com/neemiasbsilva/MLLMs-Teoria-e-Pratica. Finally, the chapter discusses the challenges and highlights promising trends.

cs.CL↗

arXiv2025

Multimodal LLMs See Sentiment

Understanding how visual content conveys sentiment is increasingly important in a digital landscape dominated by imagery. However, sentiment perception depends on complex scene-level semantics, making this a challenging task for computational models. This paper examines how Multimodal Large Language Models (MLLMs) perform sentiment analysis in images through a systematic, evaluation-driven study encompassing three perspectives: (i) direct sentiment classification from images using MLLMs; (ii) sentiment analysis on MLLM-generated descriptions using pre-trained LLMs; and (iii) fine-tuning these LLMs on sentiment-labeled descriptions to assess performance and generalization. Experiments on a recent benchmark show that a two-stage MLLM description-mediated pipeline can substantially improve prediction accuracy under several evaluation settings, particularly when the LLM component is fine-tuned. Across different agreement thresholds and sentiment granularities, the strongest configurations of this pipeline outperform lexicon-, CNN-, and Transformer-based baselines in our benchmark by up to 30.9%, 64.8%, and 42.4%, respectively. In cross-dataset evaluation, the proposed pipeline - without training or fine-tuning on the target dataset - still surpasses the best in-domain baseline by over 8%. Overall, the study provides a comprehensive assessment of MLLM description-mediated sentiment analysis, clarifying the conditions under which it is effective, the scenarios in which it fails, and its comparison with traditional vision-based approaches, while also providing a reproducible benchmark resource for future research.

cs.CV↗

arXiv2025

Relational Hoare Logic for Realistically Modelled Machine Code

Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a realistic machine model is a challenging task. Furthermore, certain security properties -- such as constant-time behavior -- require relational reasoning that goes beyond traditional correctness by linking multiple execution traces within a single specification. Yet, relational verification has been extensively explored at a higher level of abstraction. In this work, we introduce a Hoare-style logic that provides low-level, expressive relational verification. We demonstrate our approach on the s2n-bignum library, proving both constant-time discipline and equivalence between optimized and verification-friendly routines. Formalized in HOL Light, our results confirm the real-world applicability of relational verification in large assembly codebases.

cs.LO↗

arXiv2024

High-Energy Neutrino Flavor State Transition Probabilities

We analytically determine neutrino transitional probabilities and abundance ratios at various distances from the source of creation in several astrophysical contexts, including the Sun, supernovae and cosmic rays. In doing so, we determine the probability of a higher-order transition state from $\nu_\tau\rightarrow\nu_\lambda$, where $\nu_\lambda$ represents a more massive generation than Standard Model neutrinos. We first calculate an approximate cross section for high-energy neutrinos which allows us to formulate comparisons for the oscillation distances of solar, supernova and higher-energy cosmic ray neutrinos. The flavor distributions of the resulting neutrino populations from each source detected at Earth are then compared via fractional density charts.

hep-ph↗

arXiv2021

Planets or asteroids? A geochemical method to constrain the masses of White Dwarf pollutants

Polluted white dwarfs that have accreted planetary material provide a unique opportunity to probe the geology of exoplanetary systems. However, the nature of the bodies which pollute white dwarfs is not well understood: are they small asteroids, minor planets, or even terrestrial planets? We present a novel method to infer pollutant masses from detections of Ni, Cr and Si. During core--mantle differentiation, these elements exhibit variable preference for metal and silicate at different pressures (i.e., object masses), affecting their abundances in the core and mantle. We model core--mantle differentiation self-consistently using data from metal--silicate partitioning experiments. We place statistical constraints on the differentiation pressures, and hence masses, of bodies which pollute white dwarfs by incorporating this calculation into a Bayesian framework. We show that Ni observations are best suited to constraining pressure when pollution is mantle-like, while Cr and Si are better for core-like pollution. We find 3 systems (WD0449-259, WD1350-162 and WD2105-820) whose abundances are best explained by the accretion of fragments of small parent bodies ($<0.2M_\oplus$). For 2 systems (GD61 and WD0446-255), the best model suggests the accretion of fragments of Earth-sized bodies, although the observed abundances remain consistent ($<3\sigma$) with the accretion of undifferentiated material. This suggests that polluted white dwarfs potentially accrete planetary bodies of a range of masses. However, our results are subject to inevitable degeneracies and limitations given current data. To constrain pressure more confidently, we require serendipitous observation of (nearly) pure core and/or mantle material.

astro-ph.EP↗

arXiv2015

A formal proof of the Kepler conjecture

This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

math.MG↗

arXiv2012

Some new results on decidability for elementary algebra and geometry

We carry out a systematic study of decidability for theories of (a) real vector spaces, inner product spaces, and Hilbert spaces and (b) normed spaces, Banach spaces and metric spaces, all formalised using a 2-sorted first-order language. The theories for list (a) turn out to be decidable while the theories for list (b) are not even arithmetical: the theory of 2-dimensional Banach spaces, for example, has the same many-one degree as the set of truths of second-order arithmetic. We find that the purely universal and purely existential fragments of the theory of normed spaces are decidable, as is the AE fragment of the theory of metric spaces. These results are sharp of their type: reductions of Hilbert's 10th problem show that the EA fragments for metric and normed spaces and the AE fragment for normed spaces are all undecidable.

math.LO↗

arXiv2009

A revision of the proof of the Kepler conjecture

The Kepler conjecture asserts that no packing of congruent balls in three-dimensional Euclidean space has density greater than that of the face-centered cubic packing. The original proof, announced in 1998 and published in 2006, is long and complex. The process of revision and review did not end with the publication of the proof. This article summarizes the current status of a long-term initiative to reorganize the original proof into a more transparent form and to provide a greater level of certification of the correctness of the computer code and other details of the proof. A final part of this article lists errata in the original proof of the Kepler conjecture.

math.MG↗

arXiv2006

LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL)

This workshop brings together practioners and researchers who are involved in the everyday aspects of logical systems based on higher-order logic. We hope to create a friendly and highly interactive setting for discussions around the following four topics. Implementation and development of proof assistants based on any notion of impredicativity, automated theorem proving tools for higher-order logic reasoning systems, logical framework technology for the representation of proofs in higher-order logic, formal digital libraries for storing, maintaining and querying databases of proofs. We envision attendees that are interested in fostering the development and visibility of reasoning systems for higher-order logics. We are particularly interested in a discusssion on the development of a higher-order version of the TPTP and in comparisons of the practical strengths of automated higher-order reasoning systems. Additionally, the workshop includes system demonstrations. ESHOL is the successor of the ESCAR and ESFOR workshops held at CADE 2005 and IJCAR 2004.

cs.AI↗