Reproduce “Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases” on OpenResearch
Turn your favorite coding agents into research agents that review literature, develop hypotheses, and run experiments.
Universal app for Apple silicon and Intel. Requires macOS 11 or later.
About this paper
Marcus J. Min, Mike He, Zhaoyu Li, Zixuan Yi, Sharad Malik, Aarti Gupta, Xujie Si, Osbert Bastani
This research introduces and advocates for theory-level autoformalization, aiming to automatically translate entire, interconnected theoretical contexts into formal knowledge bases. The work identifies key limitations of current autoformalization, such as evaluation and abstraction learning, proposing a research agenda focused on new benchmarks, general-purpose models, and a common intermediate representation to address these challenges.
Key insights
- Existing statement-level autoformalization is insufficient for real-world projects and implicitly relies on human-built theoretical contexts, limiting its scalability.
- Practical formalization efforts are inherently theory-level, demanding the construction of interconnected formal definitions, axioms, and proofs.
- Advancements in theoretical discovery are often tied to the creation of new abstractions, a process that could be facilitated by formalizing large bodies of knowledge.
Summary by alphaXiv.
Tip: change arxiv.org to autoarxiv.org in any arXiv abstract link to open the paper here.