arXiv cs.AI· Jesse Comer, Fangzhu Shen, Shuo Zhang, Mayur Naik, Sudeepa Roy, Val Tannen·· 3 小时前AI 评分33
Whiel：一个用于认证关系式程序验证的神经符号平台
Whiel: A Neurosymbolic Platform for Certified Relational Program Verification
AI 导读
研究者推出 Whiel 系统，基于 Lean 对命令式关系程序进行认证推理，可编码 Datalog 及其带否定扩展、图查询语言核心片段的包含与等价问题。该系统采用 Hoare 风格组合推理，支持神经符号方式发现循环不变量，验证条件可用 Vampire 一阶定理证明器检查，解法被翻译为 Lean 证明证书。团队在自建 benchmark 套件上评估了其性能。
正文 · 原文
Abstract:We present the Whiel (a contraction of Whi(le-R)el) system for Lean-certified reasoning about imperative relational programs. The system can encode containment and equivalence problems for Datalog, its extensions with negation, and the core fragment of graph query languages. It can also represent optimized or incremental evaluation algorithms that are not expressible in the original query language, as well as first-order specifications of integrity constraints, schema mappings, and views arising in data integration, exchange, and sharing. Whiel's program states are database instances, and its imperative structure enables compositional Hoare-style reasoning with first-order relational specifications, using prophecy variables and leveled invariants to support inductive arguments. Whiel supports neurosymbolic discovery of loop invariants whose verification conditions can be checked using the Vampire first-order theorem prover. Counterexamples are fed back into the neurosymbolic pipeline, while proposed solutions are translated into Lean proof certificates. To validate the Whiel system, we evaluate its performance on a curated benchmark suite. In summary, we envision the Whiel system as a tool for tackling mathematically demanding, typically undecidable problems involving complex query and constraint languages, with a high degree of trust in its output.
| Subjects: | Databases (cs.DB); Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO) |
| Cite as: | arXiv:2611.05612 [cs.DB] |
| (or arXiv:2611.05612v1 [cs.DB] for this version) | |
| https://doi.org/10.48550/arXiv.2611.05612 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Jesse Comer [view email]
[v1]
Tue, 3 Nov 2026 20:56:53 UTC (172 KB)
来源：arXiv cs.AI · arxiv.org