AI助手能自动将人类提示转化为Isabelle形式化证明。
Just Type It in Isabelle! AI Agents Drafting, Mechanizing, and Generalizing from Human Hints
- 用AI代理从人类提示中自动推导并形式化证明。
- 在Isabelle中实现完整且最小的类型注解，支持多态λ演算。
- 适合形式化验证与自动化推理研究者参考。
类型注解对于以保留其语义的方式打印项至关重要，尤其是在重新解析和类型推断时。我们研究了在Isabelle中使用的秩一多态λ演算项的完全且最小类型注解问题。基于Smolka、Blanchette等人的前期工作，本文给出了该问题的元理论描述，包含完整的形式化规范与证明，并在Isabelle/HOL中进行了形式化。我们的开发是一系列实验，包括人工与大模型驱动的形式化工作流：一人一模型分别撰写手稿证明，随后由AI代理将两者自动形式化至Isabelle，再通过人类提示进一步干预，完成优化与泛化。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。