mlsanityData to 14 Oct 2026

EvoGPT-f: An Evolutionary GPT Framework for Benchmarking Formal Math Languages

arXiv 2402.16878 ↗First posted 12 Feb 2024cs.AI cs.CL cs.LGcited by 0

Not on the map. Why?

Abstract (arXiv)

Formal mathematics is the discipline of translating mathematics into a programming language in which any statement can be unequivocally checked by a computer. Mathematicians and computer scientists have spent decades of painstaking formalization efforts developing languages such as Coq, HOL, and Lean. Machine learning research has converged on these formal math corpora and given rise to an assortment of methodologies to aid in interactive and automated theorem proving. However, these papers have primarily focused on one method, for one proof task, in one language. This paper introduces EvoGPT-f: a novel evolutionary framework for the first systematic quantitative analysis of the differential machine learnability of five formal math corpora (Lean 3, Lean 4, Coq, HOL 4, HOL Light) using four tokenization methods (character, word-level, Byte Pair Encoding and StarCoder tokenizer). This paper does not put to rest the question of the "best" or "easiest" language to learn. Rather, this framework and preliminary findings begin to illuminate the differential machine learnability of these languages, offering a foundation to forge more systematic quantitative and qualitative comparative research across communities.

Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 21 of its 39 references that are in the map. First posted on arXiv 12 Feb 2024.

Builds on

21 of 39 references.

References · 21

  1. 2017Attention Is All You Needcited by 60,361
  2. 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,305
  3. 2015Neural Machine Translation of Rare Words with Subword Unitscited by 2,918
  4. 2017Decoupled Weight Decay Regularizationcited by 1,831
  5. 2023StarCoder: may the source be with you!cited by 799
  6. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  7. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  8. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  9. 2019The Lean mathematical librarycited by 134
  10. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  11. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 81
  12. 2018Reinforcement Learning of Theorem Provingcited by 69
9 more
  1. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  2. 2017Deep Network Guided Proof Searchcited by 47
  3. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  4. 2017Premise Selection for Theorem Proving by Deep Graph Embeddingcited by 44
  5. 2020Learning to Prove Theorems by Learning to Generate Theoremscited by 43
  6. 2016Holophrasm: a neural Automated Theorem Prover for higher-order logiccited by 29
  7. 2019HOList: An Environment for Machine Learning of Higher-Order Theorem Provingcited by 19
  8. 2019Towards Evolutionary Theorem Proving for Isabelle/HOLcited by 4
  9. 2016Automatically Proving Mathematical Theorems with Evolutionary Algorithms and Proof Assistantscited by 1

Built on by

Not cited yet.