論文の概要: Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification
- arxiv url: http://arxiv.org/abs/2603.03175v1
- Date: Tue, 03 Mar 2026 17:30:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-04 21:38:10.889916
- Title: Saarthi for AGI: Towards Domain-Specific General Intelligence for Formal Verification
- Title（参考訳）: AGIのためのSaarthi:形式検証のためのドメイン特化汎用インテリジェンスを目指して
- Authors: Aman Kumar, Deepak Narayan Gadde, Luu Danh Minh, Vaisakh Naduvodi Viswambharan, Keerthan Kopparam Radhakrishna, Sivaram Pothireddypalli,
- Abstract要約: SaarthiはエージェントAIフレームワークで、マルチエージェントコラボレーションを使用してエンドツーエンドの形式検証を実行する。
Saarthiフレームワークには2つの重要な拡張点がある。
- 参考スコア（独自算出の注目度）: 1.6788852474910314
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: SaarthiはエージェントAIフレームワークで、マルチエージェントコラボレーションを使用してエンドツーエンドの形式検証を実行する。
フレームワークは仕様からカバレッジクロージャまでの完全なフローを提供するが、約40%の有効性を持つため、より堅牢で信頼性の高いものにするために対処する必要があるいくつかの課題がある。
人工知能(AGI)はまだ遠い目標であり、特に正式な検証のような複雑なタスクを扱う場合、現在のLarge Language Model(LLM)ベースのエージェントは幻覚や間違いを犯しがちである。
しかし、適切な拡張と改善によって、Saarthiは正式な検証のためにドメイン固有の汎用インテリジェンスを達成するための重要なステップになり得ると信じている。
特に、フォーマルな検証のような短期的、短いコンテキスト(STSC)機能を必要とする問題では、Saarthiは、検証エンジニアの作業を支援する強力なツールになります。
本稿では,(1) SystemVerilog Assertion (SVA) 生成の精度と制御性を改善するための構造化ルールブックと仕様文法,(2) GraphRAG などの高度な検索拡張生成(RAG)技術の統合により,エージェントに技術的知識へのアクセスと出力の反復的改善と改善のためのベストプラクティスを提供する。
また、NVIDIAのCVDPベンチマークから正式な検証をターゲットとした挑戦的なテストケースを使用して、Saarthiフレームワーク全体のこれらの拡張をベンチマークします。
ベンチマークの結果,生成したアサーションの精度が70%向上し,カバレッジクロージャの達成に必要なイテレーション回数が50%削減された。
関連論文リスト
- Agentic AI-based Coverage Closure for Formal Verification [1.9085643829335266]
本研究では,Large Language Model (LLM) 対応のGenerative AI (GenAI) を用いたエージェントAI駆動型ワークフローを提案する。
オープンソースおよび内部設計のベンチマークでは、カバレッジメトリクスが測定可能な増加を示し、その改善は設計の複雑さと相関している。
論文 参考訳（メタデータ） (2026-03-03T16:35:03Z) - From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
本稿では,エージェントによる検証・編集機構を統一された単一パス推論プロセスに内部化するフレームワークを提案する。
最小限のデータで、SRI-Coderは、ChatモデルがBaseモデルの完了性能を上回ることができる。
FIMスタイルのチューニングとは異なり、SRIは一般的なコーディング能力を保持し、標準のFIMに匹敵する推論遅延を維持する。
論文 参考訳（メタデータ） (2026-01-19T20:33:53Z) - BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。
提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
論文 参考訳（メタデータ） (2025-11-26T06:39:19Z) - ARC-GEN: A Mimetic Procedural Benchmark Generator for the Abstraction and Reasoning Corpus [3.553493344868413]
本稿では,ARC-AGIトレーニングデータセットの拡張を目的としたオープンソースプロシージャジェネレータであるARC-GENを紹介する。
これまでの取り組みとは異なり、我々のジェネレータは(全4つのタスクをカバーしている)徹底的かつ緩和的です。
また、このジェネレータを用いて、2025年のGoogle Code Golf Championshipに応募したプログラムの正当性を検証するための静的ベンチマークスイートの確立についても論じる。
論文 参考訳（メタデータ） (2025-10-31T18:10:05Z) - Alita-G: Self-Evolving Generative Agent for Agent Generation [54.49365835457433]
汎用エージェントをドメインエキスパートに変換するフレームワークであるALITA-Gを提案する。
このフレームワークでは、ジェネラリストエージェントが対象ドメインタスクのキュレートされたスイートを実行する。
計算コストを削減しながら、大きな利益を得ることができます。
論文 参考訳（メタデータ） (2025-10-27T17:59:14Z) - Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math [80.46254366870447]
私たちは500時間以上の人的労力で生成された段階レベルの検証ベンチマークであるHard2Verifyを紹介します。
我々は29人の生成的批評家とプロセス報酬モデルを評価し、いくつかの点を超えて、オープンソースの検証者がクローズドソースモデルを評価することを実証した。
論文 参考訳（メタデータ） (2025-10-15T16:50:54Z) - Towards Repository-Level Program Verification with Large Language Models [8.05666536952624]
実世界のプロジェクトに自動的な形式検証をスケールするには、モジュール間の依存関係とグローバルなコンテキストを解決する必要がある。
RVBenchは,4つの多種多様な複雑なオープンソースのVerusプロジェクトから構築された,リポジトリレベルの評価のために明示的に設計された最初の検証ベンチマークである。
RagedVerusは、マルチモジュールリポジトリの証明を自動化するために、コンテキスト認識で検索拡張を同期するフレームワークである。
論文 参考訳（メタデータ） (2025-08-31T02:44:04Z) - MES-RAG: Bringing Multi-modal, Entity-Storage, and Secure Enhancements to RAG [65.0423152595537]
本稿では,エンティティ固有のクエリ処理を強化し,正確でセキュアで一貫した応答を提供するMES-RAGを提案する。
MES-RAGは、データアクセスの前に保護を適用してシステムの整合性を確保するための積極的なセキュリティ対策を導入している。
実験の結果,MES-RAGは精度とリコールの両方を著しく改善し,質問応答の安全性と有用性を向上する効果が示された。
論文 参考訳（メタデータ） (2025-03-17T08:09:42Z) - VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。
本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
論文 参考訳（メタデータ） (2024-12-11T19:17:28Z) - DARA: Decomposition-Alignment-Reasoning Autonomous Language Agent for Question Answering over Knowledge Graphs [70.54226917774933]
本稿では,DARA(Decomposition Alignment-Reasoning Agent)フレームワークを提案する。
DARAは2つのメカニズムを通じて、質問を形式的なクエリに効果的に解析する。
我々は,DARAがKGQAの最先端列挙およびランク付けに基づく手法に匹敵する性能が得られることを示す。
論文 参考訳（メタデータ） (2024-06-11T09:09:37Z) - UniOQA: A Unified Framework for Knowledge Graph Question Answering with Large Language Models [4.627548680442906]
OwnThinkは、近年導入された中国の最も広範なオープンドメイン知識グラフである。
質問応答のための2つの並列アプローチを統合する統合フレームワークであるUniOQAを紹介する。
UniOQAは特にSpCQL Logical Accuracyを21.2%に、Execution Accuracyを54.9%に向上させ、このベンチマークで新たな最先端結果を達成した。
論文 参考訳（メタデータ） (2024-06-04T08:36:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。