让大模型用自然语言写数学证明，并自动生成可验证的Lean代码。
Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics
- 模仿人类写数学的自然语言风格，支持直观表达。
- 无需额外训练数据，在miniF2F上已能有效生成可验证证明。
- 适合数学推理研究者与自动化证明工具开发者使用。
我们提出一种基于依赖类型的设计方案，旨在匹配大模型（和人类）撰写数学的方式，补充现有系统如Lean和Rocq。其核心设计包括模仿数学自然语言的界面，以及基于规则的自动化层，自动补全教材中省略的常规步骤，使得通过验证的证明可重新输出为可检查的Lean文件。初步实验表明，即使未使用专门的训练数据，大模型在miniF2F基准测试中也能有效使用该系统。相关Lean输出示例见：https://github.com/xiyuzhai-husky-lang/visored/
原文摘要 · Abstract (English)
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。