GFLean: An Autoformalisation Framework for Lean via GF
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910393950011392 |
|---|---|
| author | Pathak, Shashank |
| author_facet | Pathak, Shashank |
| contents | We present an autoformalisation framework for the Lean theorem prover, called GFLean. GFLean uses a high-level grammar writing tool called Grammatical Framework (GF) for parsing and linearisation. GFLean is implemented in Haskell. We explain the functionalities of GFLean, its inner working and discuss its limitations. We also discuss how we can use neural network based translation programs and rule based translation programs together complimenting each other to build robust autoformalisation frameworks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_01234 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | GFLean: An Autoformalisation Framework for Lean via GF Pathak, Shashank Computation and Language Logic I.2.7 We present an autoformalisation framework for the Lean theorem prover, called GFLean. GFLean uses a high-level grammar writing tool called Grammatical Framework (GF) for parsing and linearisation. GFLean is implemented in Haskell. We explain the functionalities of GFLean, its inner working and discuss its limitations. We also discuss how we can use neural network based translation programs and rule based translation programs together complimenting each other to build robust autoformalisation frameworks. |
| title | GFLean: An Autoformalisation Framework for Lean via GF |
| topic | Computation and Language Logic I.2.7 |
| url | https://arxiv.org/abs/2404.01234 |