7 papers
Aligning Faithfulness for Theory-Scale Autoformalization
Yuming Feng, Tadd Mao, Dhruva Arekar +4
Autoformalization (AF) requires more than compilation: formal statements must preserve the meaning of their informal sources, a property known as faithfulness. An emerging frontier…
Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs
Tadd Mao, Tianjun Zhong, Dhruva Arekar +5
In formal verification, both the autoformalization of statements and automated proof search have been studied extensively. While automated proof search can produce a formal proof t…
Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
Marcus J. Min, Mike He, Zhaoyu Li +5
Autoformalization translates informal natural language into formal, machine-verifiable languages. While most work focuses on individual statements, real formalization efforts are i…
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…