From the 1 of 5 linked papers with an AI index.
5 papers
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
Marcus J. Min, Mike He, Zhaoyu Li +5
The paper proposes shifting autoformalization from isolated statements to theory-level, aiming to automatically translate whole bodies of mathematical knowledge—including axioms, d…
Theory-Scale Auto-Formalization of Logics for Computer Science
Yuming Feng, Frederick Pu, One An +5
Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherent…
A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants
BarıŠBayazıt, Yao Li, Xujie Si
Large language models (LLMs) can potentially help with verification using proof assistants by automating proofs. However, it is unclear how effective LLMs are in this task. In this…
LLM Library Learning Fails: A LEGO-Prover Case Study
Ian Berlot-Attwell, Frank Rudzicz, Xujie Si
Recent advancements in the coding, reasoning, and tool-using abilities of LLMs have spurred interest in library learning (i.e., online learning through the creation, storage, and r…
Library Learning Doesn't: The Curious Case of the Single-Use "Library"
Ian Berlot-Attwell, Frank Rudzicz, Xujie Si
Advances in Large Language Models (LLMs) have spurred a wave of LLM library learning systems for mathematical reasoning. These systems aim to learn a reusable library of tools, suc…