-
GPT-4 Technical Report
Authors:
OpenAI,
Josh Achiam,
Steven Adler,
Sandhini Agarwal,
Lama Ahmad,
Ilge Akkaya,
Florencia Leoni Aleman,
Diogo Almeida,
Janko Altenschmidt,
Sam Altman,
Shyamal Anadkat,
Red Avila,
Igor Babuschkin,
Suchir Balaji,
Valerie Balcom,
Paul Baltescu,
Haiming Bao,
Mohammad Bavarian,
Jeff Belgum,
Irwan Bello,
Jake Berdine,
Gabriel Bernadett-Shapiro,
Christopher Berner,
Lenny Bogdonoff,
Oleg Boiko
, et al. (256 additional authors not shown)
Abstract:
We report the development of GPT-4, a large-scale, multimodal model which can accept image and text inputs and produce text outputs. While less capable than humans in many real-world scenarios, GPT-4 exhibits human-level performance on various professional and academic benchmarks, including passing a simulated bar exam with a score around the top 10% of test takers. GPT-4 is a Transformer-based mo…
▽ More
We report the development of GPT-4, a large-scale, multimodal model which can accept image and text inputs and produce text outputs. While less capable than humans in many real-world scenarios, GPT-4 exhibits human-level performance on various professional and academic benchmarks, including passing a simulated bar exam with a score around the top 10% of test takers. GPT-4 is a Transformer-based model pre-trained to predict the next token in a document. The post-training alignment process results in improved performance on measures of factuality and adherence to desired behavior. A core component of this project was develo** infrastructure and optimization methods that behave predictably across a wide range of scales. This allowed us to accurately predict some aspects of GPT-4's performance based on models trained with no more than 1/1,000th the compute of GPT-4.
△ Less
Submitted 4 March, 2024; v1 submitted 15 March, 2023;
originally announced March 2023.
-
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
Authors:
Thomas Powell
Abstract:
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizabili…
▽ More
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizability interpretation of our logic that extracts programs into a mixed functional/imperative language. All programs expressible in this language act on the state in a sequential manner, and we make this intuition precise by interpreting them in a semantic metatheory using the state monad. Our basic framework is very general, and our intention is that it can be instantiated and extended in a variety of different ways. We outline in detail one such extension: A monadic version of Heyting arithmetic with a wellfounded while rule, and conclude by outlining several other directions for future work.
△ Less
Submitted 25 January, 2024; v1 submitted 4 January, 2023;
originally announced January 2023.
-
Supervised machine learning techniques for data matching based on similarity metrics
Authors:
Pim Verschuuren,
Serena Palazzo,
Tom Powell,
Steve Sutton,
Alfred Pilgrim,
Michele Faucci Giannelli
Abstract:
Businesses, governmental bodies and NGO's have an ever-increasing amount of data at their disposal from which they try to extract valuable information. Often, this needs to be done not only accurately but also within a short time frame. Clean and consistent data is therefore crucial. Data matching is the field that tries to identify instances in data that refer to the same real-world entity. In th…
▽ More
Businesses, governmental bodies and NGO's have an ever-increasing amount of data at their disposal from which they try to extract valuable information. Often, this needs to be done not only accurately but also within a short time frame. Clean and consistent data is therefore crucial. Data matching is the field that tries to identify instances in data that refer to the same real-world entity. In this study, machine learning techniques are combined with string similarity functions to the field of data matching. A dataset of invoices from a variety of businesses and organizations was preprocessed with a grou** scheme to reduce pair dimensionality and a set of similarity functions was used to quantify similarity between invoice pairs. The resulting invoice pair dataset was then used to train and validate a neural network and a boosted decision tree. The performance was compared with a solution from FISCAL Technologies as a benchmark against currently available deduplication solutions. Both the neural network and boosted decision tree showed equal to better performance.
△ Less
Submitted 15 September, 2021; v1 submitted 8 July, 2020;
originally announced July 2020.
-
On the computational content of Zorn's lemma
Authors:
Thomas Powell
Abstract:
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven us…
▽ More
We give a computational interpretation to an abstract instance of Zorn's lemma formulated as a wellfoundedness principle in the language of arithmetic in all finite types. This is achieved through Gödel's functional interpretation, and requires the introduction of a novel form of recursion over non-wellfounded partial orders whose existence in the model of total continuous functionals is proven using domain theoretic techniques. We show that a realizer for the functional interpretation of open induction over the lexicographic ordering on sequences follows as a simple application of our main results.
△ Less
Submitted 28 April, 2020; v1 submitted 10 January, 2020;
originally announced January 2020.
-
A unifying framework for continuity and complexity in higher types
Authors:
Thomas Powell
Abstract:
We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main…
▽ More
We set up a parametrised monadic translation for a class of call-by-value functional languages, and prove a corresponding soundness theorem. We then present a series of concrete instantiations of our translation, demonstrating that a number of fundamental notions concerning higher-order computation, including termination, continuity and complexity, can all be subsumed into our framework. Our main goal is to provide a unifying scheme which brings together several concepts which are often treated separately in the literature. However, as a by-product, we also obtain (i) a method for extracting moduli of continuity for closed functionals of type $(\mathbb{N}\to\mathbb{N})\to\mathbb{N}$ definable in (extensions of) System T, and (ii) a characterisation of the time complexity of bar recursion.
△ Less
Submitted 8 September, 2020; v1 submitted 25 June, 2019;
originally announced June 2019.
-
An algorithmic approach to the existence of ideal objects in commutative algebra
Authors:
Thomas Powell,
Peter M Schuster,
Franziskus Wiesnet
Abstract:
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, wh…
▽ More
The existence of ideal objects, such as maximal ideals in nonzero rings, plays a crucial role in commutative algebra. These are typically justified using Zorn's lemma, and thus pose a challenge from a computational point of view. Giving a constructive meaning to ideal objects is a problem which dates back to Hilbert's program, and today is still a central theme in the area of dynamical algebra, which focuses on the elimination of ideal objects via syntactic methods. In this paper, we take an alternative approach based on Kreisel's no counterexample interpretation and sequential algorithms. We first give a computational interpretation to an abstract maximality principle in the countable setting via an intuitive, state based algorithm. We then carry out a concrete case study, in which we give an algorithmic account of the result that in any commutative ring, the intersection of all prime ideals is contained in its nilradical.
△ Less
Submitted 7 March, 2019;
originally announced March 2019.
-
Dependent choice as a termination principle
Authors:
Thomas Powell
Abstract:
We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
We introduce a new formulation of the axiom of dependent choice that can be viewed as an abstract termination principle, which generalises the recursive path orderings used to establish termination of rewrite systems. We consider several variants of our termination principle, and relate them to general termination theorems in the literature.
△ Less
Submitted 25 February, 2019;
originally announced February 2019.
-
Sequential algorithms and the computational content of classical proofs
Authors:
Thomas Powell
Abstract:
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes which interact with an oracle, and allows these processes to be modelled at any given level of abstraction. We discuss general constructions on algorithms which rep…
▽ More
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes which interact with an oracle, and allows these processes to be modelled at any given level of abstraction. We discuss general constructions on algorithms which represent specific patterns which often appear in classical reasoning, and in particular, we develop a computational interpretation of the rule of dependent choice which is phrased purely on the level of algorithms, giving us a clearer insight into the computational meaning of proofs in classical analysis.
△ Less
Submitted 28 December, 2018;
originally announced December 2018.
-
Computational interpretations of classical reasoning: From the epsilon calculus to stateful programs
Authors:
Thomas Powell
Abstract:
The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus, modified realizability and the dialectica interpretation - and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.
The problem of giving a computational meaning to classical reasoning lies at the heart of logic. This article surveys three famous solutions to this problem - the epsilon calculus, modified realizability and the dialectica interpretation - and re-examines them from a modern perspective, with a particular emphasis on connections with algorithms and programming.
△ Less
Submitted 14 December, 2018;
originally announced December 2018.
-
A proof theoretic study of abstract termination principles
Authors:
Thomas Powell
Abstract:
We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in Gödel's system T plus bar recursion. We then carry out a complexity analysis of these terms, and demonstrate how this can…
▽ More
We carry out a proof theoretic analysis of the wellfoundedness of recursive path orders in an abstract setting. We outline a very general termination principle and extract from its wellfoundedness proof subrecursive bounds on the size of derivation trees which can be defined in Gödel's system T plus bar recursion. We then carry out a complexity analysis of these terms, and demonstrate how this can be applied to bound the derivational complexity of term rewrite systems.
△ Less
Submitted 22 February, 2019; v1 submitted 12 June, 2017;
originally announced June 2017.
-
Well quasi-orders and the functional interpretation
Authors:
Thomas Powell
Abstract:
The purpose of this article is to study the role of Gödel's functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash-Williams' famous minimal bad sequence construction, and the exploration of a number of much broader problems which are related to this, particularly the question of the constructive meaning of Zor…
▽ More
The purpose of this article is to study the role of Gödel's functional interpretation in the extraction of programs from proofs in well quasi-order theory. The main focus is on the interpretation of Nash-Williams' famous minimal bad sequence construction, and the exploration of a number of much broader problems which are related to this, particularly the question of the constructive meaning of Zorn's lemma and the notion of recursion over the non-wellfounded lexicographic ordering on infinite sequences.
△ Less
Submitted 9 June, 2017;
originally announced June 2017.
-
Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice
Authors:
Thomas Powell
Abstract:
During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work we present the many variants…
▽ More
During the last twenty years or so a wide range of realizability interpretations of classical analysis have been developed. In many cases, these are achieved by extending the base interpreting system of primitive recursive functionals with some form of bar recursion, which realizes the negative translation of either countable or countable dependent choice. In this work we present the many variants of bar recursion used in this context as instantiations of a general, parametrised recursor, and give a uniform proof that under certain conditions this recursor realizes a corresponding family of parametrised dependent choice principles. From this proof, the soundness of most of the existing bar recursive realizability interpretations of choice, including those based on the Berardi-Bezem-Coquand functional, modified realizability and the more recent products of selection functions of Escardó and Oliva, follows as a simple corollary. We achieve not only a uniform framework in which familiar realizability interpretations of choice can be compared, but show that these represent just simple instances of a large family of potential interpretations of dependent choice principles.
△ Less
Submitted 12 March, 2015; v1 submitted 3 November, 2014;
originally announced November 2014.
-
Spector bar recursion over finite partial functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recu…
▽ More
We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recursive updates, terminating the computation whenever $\varphi(\hat{u})\in\mbox{dom}(u)$. We begin by exploring theoretical aspects of this new form of recursion, then in the main part of the paper we show that demand-driven bar recursion can be directly used to give an alternative functional interpretation of classical countable choice. We provide a short case study as an illustration, in which we extract a new bar recursive program from the proof that there is no injection from $\mathbb{N}\to\mathbb{N}$ to $\mathbb{N}$, and compare this to the program that would be obtained using Spector's original variant. We conclude by formally establishing that our new bar recursor is primitive recursively equivalent to the original Spector bar recursion, and thus defines the same class of functionals when added to Gödel's system $\sf T$.
△ Less
Submitted 17 August, 2015; v1 submitted 23 October, 2014;
originally announced October 2014.
-
Applying Gödel's Dialectica Interpretation to Obtain a Constructive Proof of Higman's Lemma
Authors:
Thomas Powell
Abstract:
We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words.
We use Gödel's Dialectica interpretation to analyse Nash-Williams' elegant but non-constructive "minimal bad sequence" proof of Higman's Lemma. The result is a concise constructive proof of the lemma (for arbitrary decidable well-quasi-orders) in which Nash-Williams' combinatorial idea is clearly present, along with an explicit program for finding an embedded pair in sequences of words.
△ Less
Submitted 10 October, 2012;
originally announced October 2012.
-
A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.
△ Less
Submitted 1 June, 2012; v1 submitted 25 April, 2012;
originally announced April 2012.
-
A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis
Authors:
Paulo Oliva,
Thomas Powell
Abstract:
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the prod…
▽ More
It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the product gives these theorems a natural computational interpretation that can be clearly understood in game theoretic terms.
△ Less
Submitted 23 April, 2012;
originally announced April 2012.
