自动形式化相关 AI 资讯 · AI 热点

8月11日

14:25

14:25

官方一手marktechpost@Michal Sutter

webAI发布了TwIL-LM模型家族，包含1.7B和3B参数版本，能将英文翻译成一阶逻辑并检查结论是否从前提推出。3B模型可在CPU或4GB显存上运行，1.7B模型下载大小为1.06GB。两个版本均采用非商业许可。模型卡显示，头条基准分数属于未发布的检查点，而非Hub上的权重。

AI模型 TwIL-LM webAI 形式逻辑

推荐理由：想本地跑形式逻辑？TwIL-LM 1.7B和3B能翻译英文到一阶逻辑，3B只要4GB显存，但注意基准分数是未发布版本的。

6月29日

10:06

10:06

官方一手arXiv: DeepSeek@Chengxiao Dai, Zhaokun Yan, Zhanhui Lin

该论文提出信号覆盖矩阵，将自动形式化输出按Lean elaborate检验（通过/失败）和语义等价判断（等价/不等价）分为四类。在ProofNet#和MiniF2F-test上使用DeepSeek V4-Pro进行实验，发现三种精化反馈方法（Lean-Retry、Sample-Filter、SAF）相比Vanilla的TS增益+34到+36，其中约64%来自类型层恢复，语义层净变化为0。TO到TS的转换率为23/61（Wilson 95% CI [26.6%, 50.3%]），该层恢复率可预测保留方法上的ΔTS误差在2/186以内。两个判断者在精化反馈输出上的分歧达26至37个百分点（Vanilla仅7个百分点），30%至56%的符号判断假阴性源于elaborator强制重写。

论文 ProofNet MiniF2F DeepSeek V4-Pro

推荐理由：这篇论文用信号覆盖矩阵把自动形式化的错误拆成类型和语义两类，告诉你每个方法的增益到底来自哪，而不是只看总分。

6月9日

11:52

11:52

官方账号arXiv cs.AI@Wesley Pegden

精选

Trellis 是一个自动形式化系统，利用 LLM 智能体在确定性约束的工作流中，通过迭代优化自然语言证明，逐步推进 Lean 自动形式化任务。该系统受数学家对“严谨证明”的直觉启发——即证明的任何部分都可以被进一步详细阐述。Trellis 在有限预算下使用通用智能体实现了可靠的自动形式化，其专业化来自“严谨性”含义驱动的工作流，而非特定任务训练。论文还展示了该系统生成的 Ramsey 理论最新突破的端到端 Lean 形式化证明。

论文自动形式化 Lean LLM智能体

推荐理由：Trellis 解决了自动形式化中可靠性与成本之间的平衡问题，做定理证明或形式化验证的开发者可以直接用这个工作流来生成 Lean 证明，值得关注其开源实现。