Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Johnathan Mercer

TL;DR

This work presents EvoGPT-f, an evolutionary framework to benchmark differential machine learnability across five formal mathematics corpora (Lean 3/4, Coq, HOL 4/ HOL Light) using multiple tokenization schemes. By evolving populations of Transformer models within a formal-language environment and employing two normalization strategies, the study demonstrates differential learnability across languages, with Lean 4 and Coq showing notable adaptability—particularly after Lean 3→4 migration. The framework includes an end-to-end data/experiment handling stack and an interactive dashboard, enabling cross-language comparisons and reproducible, scalable experimentation. It lays a foundation for systematic quantitative and qualitative cross-community research in formal mathematics AI, while outlining practical directions to expand preprocessing, tokenization, ontology mapping, scaling, and proof-checker integration.

Abstract

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.

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

TL;DR

This work presents EvoGPT-f, an evolutionary framework to benchmark differential machine learnability across five formal mathematics corpora (Lean 3/4, Coq, HOL 4/ HOL Light) using multiple tokenization schemes. By evolving populations of Transformer models within a formal-language environment and employing two normalization strategies, the study demonstrates differential learnability across languages, with Lean 4 and Coq showing notable adaptability—particularly after Lean 3→4 migration. The framework includes an end-to-end data/experiment handling stack and an interactive dashboard, enabling cross-language comparisons and reproducible, scalable experimentation. It lays a foundation for systematic quantitative and qualitative cross-community research in formal mathematics AI, while outlining practical directions to expand preprocessing, tokenization, ontology mapping, scaling, and proof-checker integration.

Abstract

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.
Paper Structure (14 sections, 2 equations, 16 figures, 4 tables, 1 algorithm)

This paper contains 14 sections, 2 equations, 16 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Formal Mathematics Corpora
  3. EvoGPT-f Framework
  4. EvoGPT-f Results
  5. Model and Framework Validation
  6. Benchmarking Formal Language Learnability
  7. Discussion
  8. Example to Compare Formal Math Languages
  9. Byte Pair Encoding Vocabulary Size Selection
  10. Additional Distribution Details
  11. Underlying Distributions of the Mean Loss Curves shown in Fig. \ref{['fig:line_plot3_entropy_and_discrepancy_adj_val_loss_by_generation_cf_tkn_main']}
  12. Underlying Distributions of the Mean Loss Curves by Corpus
  13. Modeling Details
  14. EvoEDA - Application for Exploratory Analysis

Figures (16)

  • Figure 1: Validation to Training Loss Ratio across Generations
  • Figure 3: Spearman Correlation between GPT Hyperparameters and Validation Loss
  • Figure 5: Selection for Larger Embedding Dimension
  • Figure 7: a.) Original Validation Loss, b.) Entropy Adjusted Validation Loss, c.) Overfitting Penalty Adjusted Validation Loss, d.) Final Adjusted Validation Loss
  • Figure 8: Mean Calibrated Loss $L_{c}^{n_{1}}$
  • ...and 11 more figures