面向形式化验证的通用人工智能：Saarthi
人工智能
2026-03-04 v1
摘要
Saarthi 是一个基于多智能体协作的代理人工智能框架，用于执行端到端形式化验证。尽管该框架提供了从规范到覆盖闭合的完整流程，但仅实现约40%的有效性，仍面临若干挑战以提升其稳健性和可靠性。人工通用智能(AGI)仍处于遥远的目标，当前基于大型语言模型(LLM)的代理人易产生幻觉并出错，尤其是在处理形式化验证等复杂任务时。然而，经过适当的增强和改进，Saarthi可是实现形式化验证领域特定通用智能的重要一步。特别是对于需要短期、短上下文(Short Term, Short Context, STSC)能力的任务，如形式化验证，Saarthi可作为强大的工具辅助验证工程师开展工作。本文提出了Saarthi框架的两个关键增强：(1) 结构化规则手册和规范语法以提高SystemVerilog断言(SVA)生成的准确性和可控性；(2) 集成先进的检索增强生成(RAG)技术，如GraphRAG，使代理人能够获取技术知识和最佳实践，以实现输出的迭代式精炼与改进。我们还针对Saarthi框架进行基准测试，使用来自NVIDIA CVDP基准中针对形式化验证的具有挑战性的测试案例。我们的基准结果显示，在生成断言的准确性提升了70%，实现覆盖闭合所需的迭代次数减少了50%。
引用
@article{arxiv.2603.03175,
title = {Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification},
author = {Aman Kumar and Deepak Narayan Gadde and Luu Danh Minh and Vaisakh Naduvodi Viswambharan and Keerthan Kopparam Radhakrishna and Sivaram Pothireddypalli},
journal= {arXiv preprint arXiv:2603.03175},
year = {2026}
}
备注
Published at the DVCon U.S. 2026