Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification

📄 arXiv: 2603.03175v1 📥 PDF

作者: Aman Kumar, Deepak Narayan Gadde, Luu Danh Minh, Vaisakh Naduvodi Viswambharan, Keerthan Kopparam Radhakrishna, Sivaram Pothireddypalli

分类: cs.AI

发布日期: 2026-03-03

备注: Published at the DVCon U.S. 2026

💡 一句话要点

Saarthi框架通过规则和RAG增强，提升形式验证领域特定通用智能。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式验证 通用人工智能 检索增强生成 知识图谱 SystemVerilog断言

📋 核心要点

  1. 现有基于LLM的智能体在形式验证等复杂任务中易出错，缺乏领域特定知识。
  2. Saarthi通过结构化规则和GraphRAG增强，提升SVA生成准确性和迭代效率。
  3. 实验表明，Saarthi在断言准确性上提升70%，迭代次数减少50%。

📝 摘要（中文）

Saarthi是一个基于多智能体协作的AI框架，用于执行端到端的形式验证。尽管该框架提供了一个从规范到覆盖闭包的完整流程，并具有约40%的有效性，但仍存在一些挑战需要解决，以使其更加稳健和可靠。通用人工智能（AGI）仍然是一个遥远的目标，当前基于大型语言模型（LLM）的智能体容易产生幻觉和犯错，尤其是在处理形式验证等复杂任务时。然而，通过适当的增强和改进，我们相信Saarthi可以成为实现形式验证领域特定通用智能的重要一步。特别是对于需要短期、短上下文（STSC）能力的问题，如形式验证，Saarthi可以成为辅助验证工程师工作的强大工具。在本文中，我们提出了对Saarthi框架的两项关键增强：（1）一种结构化的规则手册和规范语法，以提高SystemVerilog断言（SVA）生成的准确性和可控性；（2）集成先进的检索增强生成（RAG）技术，例如GraphRAG，为智能体提供访问技术知识和最佳实践的途径，以进行迭代改进和输出优化。我们还使用NVIDIA的CVDP基准测试中具有挑战性的测试用例对这些增强功能进行了基准测试，目标是形式验证。我们的基准测试结果非常突出，生成的断言的准确性提高了70%，实现覆盖闭包所需的迭代次数减少了50%。

🔬 方法详解

问题定义：论文旨在解决形式验证中，现有基于LLM的智能体（如Saarthi）在生成SystemVerilog断言（SVA）时准确性不足，以及达到覆盖闭包所需迭代次数过多的问题。现有方法依赖于通用LLM，缺乏对形式验证领域知识的有效利用，导致断言生成容易出错，需要人工干预进行多次迭代。

核心思路：论文的核心思路是通过引入结构化的规则手册和规范语法，以及集成先进的检索增强生成（RAG）技术，特别是GraphRAG，来增强Saarthi框架的领域知识和推理能力。结构化规则和语法用于约束SVA的生成过程，减少语法错误和语义歧义。GraphRAG则用于检索相关的技术知识和最佳实践，指导智能体进行迭代改进。

技术框架：Saarthi框架的整体流程包括：规范输入、SVA生成、验证和覆盖分析、迭代改进。论文主要改进了SVA生成和迭代改进两个阶段。在SVA生成阶段，引入了结构化的规则手册和规范语法。在迭代改进阶段，集成了GraphRAG，用于检索相关知识并指导智能体进行优化。

关键创新：论文的关键创新在于将结构化规则和GraphRAG相结合，用于增强形式验证智能体的领域知识和推理能力。与传统的基于LLM的方法相比，该方法能够更有效地利用领域知识，提高SVA生成的准确性和迭代效率。GraphRAG的使用使得智能体能够访问更丰富的知识图谱，从而更好地理解规范并生成更有效的断言。

关键设计：结构化规则手册和规范语法的设计需要领域专家参与，定义SVA生成的语法规则和语义约束。GraphRAG的关键在于构建高质量的知识图谱，包含形式验证相关的技术知识、最佳实践和常见错误。知识图谱的构建和维护需要持续的投入和领域专家的参与。此外，RAG的检索策略和生成策略也需要仔细设计，以确保检索到的知识能够有效地指导SVA的生成和改进。

📊 实验亮点

实验结果表明，通过引入结构化规则和GraphRAG，Saarthi框架在SVA生成准确性上提升了70%，实现覆盖闭包所需的迭代次数减少了50%。这些显著的提升表明该方法能够有效地提高形式验证的效率和质量。

🎯 应用场景

该研究成果可应用于芯片设计验证、软件形式验证等领域，通过自动化生成高质量的断言，减少人工验证工作量，缩短验证周期，提高产品质量。未来可扩展到其他需要领域知识的AI应用场景，例如法律咨询、医疗诊断等。

📄 摘要（原文）

Saarthi is an agentic AI framework that uses multi-agent collaboration to perform end-to-end formal verification. Even though the framework provides a complete flow from specification to coverage closure, with around 40% efficacy, there are several challenges that need to be addressed to make it more robust and reliable. Artificial General Intelligence (AGI) is still a distant goal, and current Large Language Model (LLM)-based agents are prone to hallucinations and making mistakes, especially when dealing with complex tasks such as formal verification. However, with the right enhancements and improvements, we believe that Saarthi can be a significant step towards achieving domain-specific general intelligence for formal verification. Especially for problems that require Short Term, Short Context (STSC) capabilities, such as formal verification, Saarthi can be a powerful tool to assist verification engineers in their work. In this paper, we present two key enhancements to the Saarthi framework: (1) a structured rulebook and specification grammar to improve the accuracy and controllability of SystemVerilog Assertion (SVA) generation, and (2) integration of advanced Retrieval Augmented Generation (RAG) techniques, such as GraphRAG, to provide agents with access to technical knowledge and best practices for iterative refinement and improvement of outputs. We also benchmark these enhancements for the overall Saarthi framework using challenging test cases from NVIDIA's CVDP benchmark targeting formal verification. Our benchmark results stand out with a 70% improvement in the accuracy of generated assertions, and a 50% reduction in the number of iterations required to achieve coverage closure.