小模型加受限视图与 Lean 证明，实现任意长度可验证精确算术。
资讯摘要
论文提出 Sketchpad，让 Qwen3.5-0.8B 加低秩适配器在渲染的“纸面”上逐步执行算术，每次前向只读取三格视图并输出一位数字、进位或借位及下一步操作，由固定运行时移动视图。作者用 Lean 证明：只要模型在运行时呈现的有限视图集上精确，就在任意长度输入上精确；若步骤还读取先前步骤则有限测试不足。部署设备上 2,446 个视图全部通过，浏览器中 200/200 预注册题、220/220 长算题均解出。
要点速读
- 模型每步只读三格视图，输出数字、进位/借位和下一步操作，运行时负责移动视图而不写结果数字。
- Lean 证明：模型在有限视图集上精确，等价于在任意长度输入上精确；步骤读取先前步骤时有限测试不够。
- 在笔记本 GPU 的浏览器中 2,446 个视图全部通过，200/200 预注册题和 220/220 长算题解出，对比中最强的 GPT-6.1 Sol 解出 217 题。
中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/11/5 08:00:38（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。