REVIEW 2 cited by
GFLean: An Autoformalisation Framework for Lean via GF
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 2 Pith papers
-
Integrating Rules and Semantics for LLM-Based C-to-Rust Translation
IRENE combines rule-based retrieval, structured summarization, and compiler feedback to improve LLM-based C-to-Rust translation accuracy and safety.
-
Step-Wise Formal Verification for LLM-Based Mathematical Problem Solving
MATH-VF formalizes LLM math solutions into SimpleMath and uses a tool-augmented critic to verify each reasoning step and offer corrective feedback.
Discussion (0). Continue with ORCID to comment.