An Evaluation Benchmark for Autoformalization in Lean4
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929380975968256 |
|---|---|
| author | Gulati, Aryan Ladsaria, Devanshu Mishra, Shubhra Sidhu, Jasdeep Miranda, Brando |
| author_facet | Gulati, Aryan Ladsaria, Devanshu Mishra, Shubhra Sidhu, Jasdeep Miranda, Brando |
| contents | Large Language Models (LLMs) hold the potential to revolutionize autoformalization. The introduction of Lean4, a mathematical programming language, presents an unprecedented opportunity to rigorously assess the autoformalization capabilities of LLMs. This paper introduces a novel evaluation benchmark designed for Lean4, applying it to test the abilities of state-of-the-art LLMs, including GPT-3.5, GPT-4, and Gemini Pro. Our comprehensive analysis reveals that, despite recent advancements, these LLMs still exhibit limitations in autoformalization, particularly in more complex areas of mathematics. These findings underscore the need for further development in LLMs to fully harness their potential in scientific research and development. This study not only benchmarks current LLM capabilities but also sets the stage for future enhancements in autoformalization. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_06555 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | An Evaluation Benchmark for Autoformalization in Lean4 Gulati, Aryan Ladsaria, Devanshu Mishra, Shubhra Sidhu, Jasdeep Miranda, Brando Machine Learning Artificial Intelligence Computation and Language Programming Languages Large Language Models (LLMs) hold the potential to revolutionize autoformalization. The introduction of Lean4, a mathematical programming language, presents an unprecedented opportunity to rigorously assess the autoformalization capabilities of LLMs. This paper introduces a novel evaluation benchmark designed for Lean4, applying it to test the abilities of state-of-the-art LLMs, including GPT-3.5, GPT-4, and Gemini Pro. Our comprehensive analysis reveals that, despite recent advancements, these LLMs still exhibit limitations in autoformalization, particularly in more complex areas of mathematics. These findings underscore the need for further development in LLMs to fully harness their potential in scientific research and development. This study not only benchmarks current LLM capabilities but also sets the stage for future enhancements in autoformalization. |
| title | An Evaluation Benchmark for Autoformalization in Lean4 |
| topic | Machine Learning Artificial Intelligence Computation and Language Programming Languages |
| url | https://arxiv.org/abs/2406.06555 |