formal-methods

本文探讨了使用抽象栈机器实现逻辑程序的方法，详细说明了推理规则（如加法）的不同模式分配如何转换为状态机转换以进行计算。

Specula 团队的研究人员创建了 SysMoBench 基准测试，用于评估大语言模型能否准确建模实际计算系统的 TLA+ 规范，还是仅仅照本宣科地背诵教材内容。该基准测试涵盖四个阶段共 11 个系统，揭示了当前大语言模型在准确建模系统实现与参考论文方面的系统性差距。

本文介绍了 RGAO，这是一种用于多智能体代码生成的检索引导自适应编排框架，可根据代码复杂度动态选择拓扑结构。它提供了一种形式化的预算代数，在显著降低相较于基线方法的路由错误率的同时，确保了资源的可证明守恒。

一篇2026年的博客文章回顾了M.H. van Emden 1982年提出的“计算机辅助思维”愿景，并指出当今的对话式大语言模型未能实现他所设想的那种结构化、基于逻辑、能产生思维摩擦的对话者。