Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
veganism.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Veganism Social is a welcoming space on the internet for vegans to connect and engage with the broader decentralized social media community.

Administered by:

Server stats:

293
active users

veganism.social: AboutStatusPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.0-alpha.5+vegan

#IsabelleHOL

14 posts7 participants2 posts today
Public
José A. Alonso

Simplified and verified: A second look at a proof-producing union-find algorithm. ~ Lukas Stevens, Rebecca Ghidini. arxiv.org/abs/2504.10246 #ITP #IsabelleHOL

arXiv logo
arXiv.orgSimplified and Verified: A Second Look at a Proof-Producing Union-Find AlgorithmUsing Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then, we prove the original formulation of the explain operation to be equal to our version. Finally, we refine this data structure to Imperative HOL, enabling us to export efficient imperative code. The formalisation provides a stepping stone towards the verification of proof-producing congruence closure algorithms which are a core ingredient of Satisfiability Modulo Theories (SMT) solvers.
Public
José A. Alonso

Lemmanaid: Neuro-symbolic lemma conjecturing. ~ Yousef Alhessi et als. arxiv.org/abs/2504.04942 #LLMs #ITP #IsabelleHOL

arXiv.orgLemmanaid: Neuro-Symbolic Lemma ConjecturingAutomatically conjecturing useful, interesting and novel lemmas would greatly improve automated reasoning tools and lower the bar for formalizing mathematics in proof assistants. It is however a very challenging task for both neural and symbolic approaches. We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid, that combines Large Language Models (LLMs) and symbolic methods, and evaluate it on proof libraries for the Isabelle proof assistant. We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details. We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods. Our results indicate that neural and symbolic techniques are complementary. By leveraging the best of both symbolic and neural methods we can generate useful lemmas for a wide range of input domains, facilitating computer-assisted theory development and formalization.
VegansExploreLive feeds
About