Minerva

Minerva: they basically fine-tuned a language model on ArXiv papers and web pages containing LaTeX, so that it can produce latex. This is great because it can do 'literate proofs', interspersing text explanations with written-out math. But there's no mechanism to check the math? You could imagine a few things:

• give the model access to a calculator (or better yet, mathematica) based on its immediate previous outputs. so if it spits out 80 - 20 = then it sees the calculated result as a possible input it can attend to and maybe reproduce.
• train a discriminator model to check if logic is correct.