0.8B 小模型 + 纸张画布,在浏览器里实现可形式化验证的精确算术
Mostafa 'Neo' Mohsenvand · hf · 2026-11-09
Sketchpad 项目用 Qwen3.5-0.8B 加低秩适配器,在浏览器里于一张「渲染的纸」上执行算术:每次前向只读取三格视野、输出一位数字/进借位和下一步操作,固定运行时只移动视野、不写任何结果数字。关键突破:
- 精确性变成可检验的有限性质:用 Lean 形式化证明——只要模型对运行时能呈现的有限视野集合全部正确,就对任意长度输入精确;并证明若步骤还能读取更早步骤则有限测试不再充分
- 在笔记本 GPU 浏览器内,全部 2446 个视野通过验证
- 支持任意长度的带符号加减、长乘除、平方根、最大公约数;预注册 200/200 全对,1000 位加法和 20 位乘法 220/220,而 10 个对比模型中最强的 GPT-6.1 Sol 也只做对 217
- 在此之上构建的符号运行时可对多项式求解/展开/因式分解;适配器上的乘法门可在不用纸时精确恢复基座模型
「研究」频道最新
- 最强 3D 生成模型仍反复犯三类低级错误：Z-fighting、单面几何、坐标系错位 — teortaxesTex · 2026-11-09
- EPFL 研究者将在线讲解掩码扩散语言模型的轨迹感知训练 — AnnaCiaunica · 2026-11-09
- UC伯克利等新论文：Agent 自我进化提分 5.2 却丢掉 10 个原本会做的任务 — rohanpaul_ai · 2026-11-09
- MoE训练终极手册已有中文版：3万字50+交互图表全覆盖 — Nouamanetazi · 2026-11-09
- 斯坦福DSP传奇Julius Smith三小时深度访谈上线YouTube — teropa · 2026-11-09
- 硬件感知 LDM 实现:状态回卷+窗口写入,大幅降低激活内存与访存开销 — SonglinYang4 · 2026-11-09