AI系统自主发现用Z3验证六类安全问题，效果精准无误。
Emergent Formal Verification: How an Autonomous AI Ecosystem Independently Discovered SMT-Based Safety Across Six Domains
- AI自主生成代码并用Z3求解器验证安全，无需人工指导。
- 在181个测试中实现零误报零漏报，检出实锤漏洞。
- 适合研究AI自我验证机制与形式化安全的学者。
一个自主人工智能生态（SUBSTRATE S3）在未明确指令使用形式化方法的情况下，独立提出了在六个不同领域的AI安全验证中使用Z3 SMT求解器：大模型生成代码的验证、AI代理工具API安全性、后精炼推理正确性、命令行接口命令验证、硬件组装验证以及智能合约安全。这些发现出现在8个产品中，持续13天，不同版本间杰卡德相似度低于15%，表明形式化验证不仅是有用技术，更是复杂系统自我安全推理的涌现属性。我们提出统一框架substrate-guard，通过通用API在所有六类输出上应用Z3验证，在五个已实现领域共181个测试案例中达到100%分类准确率，零假阳性与零假阴性。该框架检测到经验测试无法发现的真实缺陷，包括分支无关的RISC-V汇编中INT_MIN溢出，并数学证明了工具API中未约束字符串参数在形式上不可验证。
原文摘要 · Abstract (English)
An autonomous AI ecosystem (SUBSTRATE S3), generating product specifications without explicit instructions about formal methods, independently proposed the use of Z3 SMT solver across six distinct domains of AI safety: verification of LLM-generated code, tool API safety for AI agents, post-distillation reasoning correctness, CLI command validation, hardware assembly verification, and smart contract safety. These convergent discoveries, occurring across 8 products over 13 days with Jaccard similarity below 15% between variants, suggest that formal verification is not merely a useful technique for AI safety but an emergent property of any sufficiently complex system reasoning about its own safety. We propose a unified framework (substrate-guard) that applies Z3-based verification across all six output classes through a common API, and evaluate it on 181 test cases across five implemented domains, achieving 100% classification accuracy with zero false positives and zero false negatives. Our framework detected real bugs that empirical testing would miss, including an INT_MIN overflow in branchless RISC-V assembly and mathematically proved that unconstrained string parameters in tool APIs are formally unverifiable.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。