Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
Rattachement africain : gb, dk. Niveau de preuve : code pays fourni par la source.
Le résumé fourni par la source
Type annotations are essential when printing terms in a way that preserves their meaning under reparsing and type inference. We study the problem of complete and minimal type annotations for rank-one polymorphic $λ$-calculus terms, as used in Isabelle. Building on prior work by Smolka, Blanchette et al., we give a metatheoretical account of the problem, with a full formal specification and proofs, and formalize it in Isabelle/HOL. Our development is a series of experiments featuring human-driven and AI-driven formalization workflows: a human and an LLM-powered AI agent independently produce pen-and-paper proofs, and the AI agent autoformalizes both in Isabelle, with further human-hinted AI interventions refining and generalizing the development.
Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.
Le contrôle bibliographique ouvert
Où se fait cette recherche
-
University of Sheffield Department of Computer Science pays non établi dans la noticeUniversité ou école supérieure
-
King's College London Department of Informatics pays non établi dans la noticeUniversité ou école supérieure
-
King's College School pays non établi dans la noticeUniversité ou école supérieure
-
University of Copenhagen Department of Computer Science pays non établi dans la noticeUniversité ou école supérieure
-
University College Copenhagen pays non établi dans la noticeUniversité ou école supérieure
-
IT University of Copenhagen pays non établi dans la noticeUniversité ou école supérieure
Department of Computer Science — University of Sheffield, Department of Informatics — King's College London et King's College School, avec 3 autres affiliations.
Une affiliation ne permet pas de déduire la nationalité d’un auteur.