Table of Contents
This repository reproduces the in-context Autoformalism experiments from the paper Autoformalism with Large Language Models. There are minor difference in the approach, for example, the strongest results in the paper were obtained with the Codex model which is now retired, so we use GPT-4 and Llama3 in its place. Our models are also chat variants so the exact format of the few-shot prompt is slightly different. Given these small difference, we create the exact same prompts on the exact same dataset to attempt to recreate the results of the paper.
The results are in the experiments folder, viewable as notebooks.
pip install autoformalism-with-llmsautoformalism-with-llms is distributed under the terms of the MIT license.