REVIEW 6 cited by
Autoformalization with Large Language Models
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
abstract
Autoformalization is the process of automatically translating from natural language mathematics to formal specifications and proofs. A successful autoformalization system could advance the fields of formal verification, program synthesis, and artificial intelligence. While the long-term goal of autoformalization seemed elusive for a long time, we show large language models provide new prospects towards this goal. We make the surprising observation that LLMs can correctly translate a significant portion ($25.3\%$) of mathematical competition problems perfectly to formal specifications in Isabelle/HOL. We demonstrate the usefulness of this process by improving a previously introduced neural theorem prover via training on these autoformalized theorems. Our methodology results in a new state-of-the-art result on the MiniF2F theorem proving benchmark, improving the proof rate from $29.6\%$ to $35.2\%$.
Forward citations
Cited by 6 Pith papers
-
ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis
ProofAug extracts progressively coarser valid proof skeletons from failed LLM proof attempts and fills them with automated theorem provers, improving miniF2F pass rates and sample efficiency in Isabelle and Lean.
-
Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph
A graph-of-thought agent with retrieval and a term-grounded semantic checker auto-formalizes research-level math statements in Lean, hitting 68.5% on ProofNet and 6/14 homological conjectures where baselines score 0.
-
FormaRL: Enhancing Autoformalization with no Labeled Data
A reinforcement learning framework improves autoformalization without labeled data by rewarding outputs that pass Lean syntax and LLM consistency checks.
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
Explicit Formulas and Unimodality Phenomena for General Position Polynomials
Explicit formulas for general position polynomials of complete multipartite graphs are given, with log-concavity and unimodality for balanced parts of size r≤4 and counterexamples for larger r and some coronas.
-
Intermediate Languages Matter: Formal Languages and LLMs affect Neurosymbolic Reasoning
Formal languages matter as the intermediate representation in neurosymbolic reasoning: first-order logic outperforms logic programming languages (ASP, Pyke) in average accuracy.
Discussion (0). Continue with ORCID to comment.