GFLean: An Autoformalisation Framework for Lean via GF
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.
Code (0)
등록된 구현이 없습니다.
Tasks
TranslationSimilar Papers 제목 키워드 기반
Conjecturing: An Overlooked Step in Formal Mathematical Reasoning
Autoformalisation, the task of expressing informal mathematical statements in formal language, is often viewed as a direct translation process. This, however, disregards a critical preceding step: conjecturing. Many math…
Mathematical ReasoningFormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean
Formalising informal mathematical reasoning into formally verifiable code is a significant challenge for large language models. In scientific fields such as physics, domain-specific machinery (\textit{e.g.} Dirac notatio…
Mathematical ReasoningCode GenerationTheorem Prover as a Judge for Synthetic Data Generation
The demand for synthetic data in mathematical reasoning has increased due to its potential to enhance the mathematical capabilities of large language models (LLMs). However, ensuring the validity of intermediate reasonin…
Mathematical ProofsMathematical Reasoningreinforcement-learningReinforcement Learning+1TopoAlign: A Framework for Aligning Code to Math via Topological Decomposition
Large Language Models (LLMs) excel at both informal and formal (e.g. Lean 4) mathematical reasoning but still struggle with autoformalisation, the task of transforming informal into formal mathematical statements. Autofo…
Mathematical ReasoningTransfer LearningInvestigating the Robustness of Deductive Reasoning with Large Language Models
Large Language Models (LLMs) have been shown to achieve impressive results for many reasoning-based Natural Language Processing (NLP) tasks, suggesting a degree of deductive reasoning capability. However, it remains uncl…
counterfactual