Experimental results from applying GPT-4 to an unpublished formal language
Computation and Language
2023-05-23 v1 Logic in Computer Science
Logic
Abstract
Can large language models be used to complete mathematical tasks that are traditionally performed either manually or with the aid of theorem provers? To answer this question, a state-of-the-art system, GPT-4, was provided with a concise natural language specification for a previously unpublished formal system and asked to complete a number of tasks, from stating function and type definitions to proving simple theorems and verifying user-supplied proofs. The system completed all tasks successfully, showed extensive domain knowledge, invented helpful new syntax and semantics, and exhibited generalization and inference abilities. So the answer seems to be: yes.
Keywords
Cite
@article{arxiv.2305.12196,
title = {Experimental results from applying GPT-4 to an unpublished formal language},
author = {Gregor vom Scheidt},
journal= {arXiv preprint arXiv:2305.12196},
year = {2023}
}