thesis-v18-formal-verification
收藏资源简介：
该数据集名为SZL Ouroboros Thesis v18 — Formal Verification of Agentic AI，是一个关于可验证智能体AI治理的学术论文及相关资源集合。核心内容是一篇206页的论文，标题为The Ouroboros Substrate: a Governance-Mathematical Foundation for Verifiable Agentic AI。该论文提出了一种基于Lean 4形式化验证的智能体AI运行时框架，其中每个治理不变量都由Lean内核针对Mathlib v4.13.0进行机器检查。数据集包含论文PDF、10张可重新生成的图表（基于包含10,000个样本的基准数据）以及一个形式化定理库的索引。该定理库包含总共375个定理，分布在25个章节中，其中134个定理为lake-verified（已通过Lean验证），241个为skeleton状态（证明待完成，但类型签名正确）。论文的主要技术贡献包括：Lutar演算与A1-A15公理系统、具有SCITT兼容性的双见证收据链、针对Lambda轴的PAC-Bayes泛化边界、包含16个定理存根的Lean Czar目录，以及OpenTelemetry SEMCONV扩展。数据集适用于学术研究（引用或扩展Lutar演算、PAC-Bayes治理边界或收据链范畴论）、在智能体AI系统中实施DSSE/SLSA治理收据的实践者、在AI安全课程中使用形式化验证示例的教育工作者，以及通过运行`lake build`验证定理-证明对应关系的审计人员。数据集明确说明其不是LLM模型或模型检查点，不包含完整的正式证明（大部分定理为存根），不是生产级运行时，且未经外部同行评审。
数据集概述：SZL Ouroboros Thesis v18 — Formal Verification of Agentic AI Governance
基本信息
- 数据集名称: SZL Ouroboros Thesis v18 — Formal Verification of Agentic AI Governance
- 数据集ID:
SZLHOLDINGS/thesis-v18-formal-verification - 语言: 英语 (en)
- 许可证: Creative Commons Attribution 4.0 International (CC-BY-4.0)
- DOI: 10.5281/zenodo.20434276
- 作者: Stephen P. Lutar，所属机构: SZL Holdings，ORCID: 0009-0001-0110-4173
- 大小: 少于1K (n<1K)
- 任务类别: 其他
数据集描述
本数据集是SZL基底的规范说明，共206页，包含76个命名的定理与推论，以及134个经Lake验证的Lean 4条目。数据集版本链从v14演进至v18.0，涉及7个Zenodo DOI。
数据集内容
thesis_v18.tex: 主要LaTeX源文件thesis.pdf: 编译后的PDF文档 (206页)theorems_index.json: 机器可读的定理索引PROVENANCE.md: DOI链及验证说明figures/: 包含10张基于N=10,000基准数据生成的图表
版本链与DOI
| 版本 | DOI |
|---|---|
| 概念锚点 | 10.5281/zenodo.19944926 |
| v14 | 10.5281/zenodo.20424992 |
| v15 | 10.5281/zenodo.20424995 |
| v16 | 10.5281/zenodo.20424996 |
| v17 | 10.5281/zenodo.20431181 |
| v18.0 thesis | 10.5281/zenodo.20434276 |
| v18.0.0 software | 10.5281/zenodo.20434308 |
验证数据统计
- 页面数: 206
- 定理与推论数: 76
- Lake验证的Lean文件数: 134
- Lean骨架文件数: 241
- 剩余未完成证明 (
sorry): 7个 (均已标记Mathlib消解路径) - 版本链DOI数: 7 (均HTTP 200)
- 论文版本追踪数: 18
相关资源
- 交互式浏览器: SZLHOLDINGS/lean-proof-playground
- 证明库: SZLHOLDINGS/a11oy-v19-substrate
- LaTeX源码: github.com/szl-holdings/ouroboros-thesis
- Lean证明: github.com/szl-holdings/lutar-lean
引用格式
bibtex @misc{lutar2026ouroboros, title = {Ouroboros: Formal Verification of Agentic AI Governance — v18.0}, author = {Lutar, Stephen P.}, year = {2026}, doi = {10.5281/zenodo.20434276}, url = {https://doi.org/10.5281/zenodo.20434276} }
