arXiv cs.AI· Jesse Comer, Fangzhu Shen, Shuo Zhang, Mayur Naik, Sudeepa Roy, Val Tannen·· 10 小时前AI 评分25
Whiel：面向关系程序验证的神经符号平台，输出经 Lean 认证
Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
AI 导读
Whiel 是一个面向命令式关系程序的神经符号验证系统，可编码 Datalog 及其否定扩展、图查询语言核心片段的包含与等价问题，并将验证方案翻译为 Lean 证明证书。
正文 · AI 翻译
摘要：我们提出 Whiel（Whi(le-R)el 的缩写）系统，用于对命令式关系程序进行 Lean 认证推理。该系统可以编码 Datalog、其带否定的扩展以及图查询语言核心片段的包含与等价问题。它还可以表示无法在原始查询语言中表达的优化或增量求值算法，以及数据集成、交换和共享中出现的一阶完整性约束、模式映射和视图规范。Whiel 的程序状态是数据库实例，其命令式结构支持使用一阶关系规范进行组合式 Hoare 风格推理，并使用预言变量和分层不变式来支持归纳论证。Whiel 支持循环不变式的神经符号发现，其验证条件可以使用 Vampire 一阶定理证明器检查。反例被反馈到神经符号流水线中，而提出的解决方案被转换为 Lean 证明证书。为了验证 Whiel 系统，我们在一个精选的基准测试套件上评估其性能。总之，我们将 Whiel 系统设想为一种工具，用于处理涉及复杂查询和约束语言的、数学上要求高且通常不可判定的问题，并对其输出具有高度信任。
| 主题： | 数据库（cs.DB）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2611.05612 [cs.DB] |
| （或本版本的 arXiv:2611.05612v1 [cs.DB]） | |
| https://doi.org/10.48550/arXiv.2611.05612 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Jesse Comer [查看电子邮件]
[v1]
2026年11月3日星期二 20:56:53 UTC（172 KB）
来源：arXiv cs.AI · arxiv.org