Abstract Automated theorem provers often perform better when told what shapes of terms are interesting. In this paper we discover interesting term shapes automatically, in the form of abstractions , term patterns that occur over and over again in proofs. Our tool Twitch produces abstractions automatically and can do so in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. Twitch is built on top of Stitch , a tool designed for discovering reusable library functions in program synthesis tasks. We have also extended Twee, an equational theorem prover, to use the generated abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it proves problems previously unsolved by Twee, as well as yielding speed-ups on many other problems.

Large language models (LLMs) offer an inexpensive yet powerful way to annotate text, but are often inconsistent when compared with experts.These errors can bias downstream estimates of population parameters such as regression coefficients and causal effects.To mitigate this bias, researchers have developed debiasing methods such as Design-based Supervised Learning (DSL) and Prediction-Powered Inference (PPI), which promise valid estimation by combining LLM annotations with a limited number of expensive expert annotations.Although these methods produce consistent estimates under theoretical assumptions, it is unknown how they compare in finite samples of sizes encountered in applied research.We make two contributions: First, we study how each method's performance scales with the number of expert annotations, highlighting regimes where LLM bias or limited expert labels significantly affect results.Second, we compare DSL and PPI across a range of tasks, finding that although both achieve low bias with large datasets, DSL often outperforms PPI on bias reduction and empirical efficiency, but its performance is less consistent across datasets.Our findings indicate that there is a bias-variance tradeoff at the level of debiasing methods, calling for more research on developing metrics for quantifying their efficiency in finite samples.

Abstract We investigate how the automated inductive proof capabilities of the first-order prover Vampire can be improved by adding lemmas conjectured by the QuickSpec theory exploration system and by training strategy schedules specialized for inductive proofs. We find that adding lemmas improves performance (measured in number of proofs found for benchmark problems) by $$40\%$$ 40 % compared to Vampire’s plain structural induction as baseline. Strategy training alone increases the number of proofs found by $$130\%$$ 130 % , and the two methods in combination provide an increase of $$183\%$$ 183 % . By combining strategy training and lemma discovery we can prove more inductive benchmarks than previous state-of-the-art inductive proof systems (HipSpec and CVC4).

Large Language Models (LLMs) make natural interfaces to factual knowledge, but their usefulness is limited by their tendency to deliver inconsistent answers to semantically equivalent questions.For example, a model might predict both "Anne Redpath passed away in Edinburgh."and "Anne Redpath's life ended in London."In this work, we identify potential causes of inconsistency and evaluate the effectiveness of two mitigation strategies: up-scaling and augmenting the LM with a retrieval corpus.Our results on the LLaMA and Atlas models show that both strategies reduce inconsistency while retrieval augmentation is considerably more efficient.We further consider and disentangle the consistency contributions of different components of Atlas.For all LMs evaluated we find that syntactical form and other evaluation task artifacts impact consistency.Taken together, our results provide a better understanding of the factors affecting the factual consistency of language models.

This document gives the outline of a system demonstration for the QuickSpec theory exploration tool.

Abstract QuickSpec is a theory exploration system which tests a Haskell program to find equational properties of it, automatically. The equations can be used to help understand the program, or as lemmas to help prove the program correct. QuickSpec is largely automatic: the user just supplies the functions to be tested and QuickCheck data generators. Previous theory exploration systems, including earlier versions of QuickSpec itself, scaled poorly. This paper describes a new architecture for theory exploration with which we can find vastly more complex laws than before, and much faster. We demonstrate theory exploration in QuickSpec on problems both from functional programming and mathematics.