論文の概要: Stop Handcrafting Your Engine! GenDB-V: Towards AI-Generated and Formally Verified Database Systems

• arxiv url: http://arxiv.org/abs/2611.02779v1
• Date: Mon, 02 Nov 2026 08:56:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-04 23:36:30.582286
• Title: Stop Handcrafting Your Engine! GenDB-V: Towards AI-Generated and Formally Verified Database Systems
• Title（参考訳）: GenDB-V: AIが生成し、形式的に検証されたデータベースシステムを目指す
• Abstract要約: 我々は、AIエージェントがハードウェアやワークロードに特化したデータベースエンジンを合成してパフォーマンスを向上するシステムGenDB-Vを提案する。 GenDB-Vは、sqlテンプレートと汎用エンジンの特殊実装をサポートする。 検証済みのテンプレート実装では、GenDB-VはDuckDBとUmbraで22.0-61.3xの幾何平均高速化を実現している。 検証された汎用エンジンでは、GenDB-VはTPC-H上での1.27-3.4xの高速化も達成している。
• 参考スコア（独自算出の注目度）: 25.352713493505792
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: For over 50 years, the database community has developed a wide range of successful engines to answer two fundamental questions: how can database systems run faster, and how can we ensure their correctness? Experience with these engines shows that performance depends on hardware and workloads. As both change over time, we repeatedly redesign and rebuild database systems, a time-consuming and expensive process. Correctness remains another long-standing challenge: recent studies continue to uncover wrong-answer bugs even in mature database engines, despite years of development and testing. To address these, we present GenDB-V, a system that enables AI agents to synthesize database engines specialized to hardware and workloads for performance, and formally verified for correctness. GenDB-V supports specialized implementations of SQL templates and general-purpose engines that accept any query within a supported SQL subset. First, we develop SQLSpec to formalize SQL semantics and deterministically construct fixed, implementation-agnostic synthesis targets. Second, we enable joint synthesis of fast code and formal proofs through storage--execution co-optimization, performance-first exploration, and three-layer modular proofs that bridge low-level execution to SQLSpec semantics. Third, we verify the synthesized code and proofs against the fixed synthesis targets in an isolated pipeline, proving SQL correctness and program safety. We evaluate GenDB-V on TPC-H and SEC-EDGAR. For verified template implementations, GenDB-V achieves geometric-mean speedups of 22.0-61.3x over DuckDB and Umbra. For a verified general-purpose engine, GenDB-V also achieves speedups of 1.27-3.4x on TPC-H. GenDB-V also achieves better performance than a testing-based LLM synthesis method, while our audit and tests expose incorrect answers in that method's implementations for 16 of 28 templates.
• Abstract（参考訳）: 50年以上にわたって、データベースコミュニティは、2つの基本的な疑問に答えるために、幅広いエンジンを開発してきた。 これらのエンジンの経験から、パフォーマンスはハードウェアとワークロードに依存していることがわかる。 時間が経つにつれて、私たちはデータベースシステムを再設計し、再構築します。 最近の研究は、長年の開発とテストにもかかわらず、成熟したデータベースエンジンでさえも、誤った答えのバグを発見し続けている。 これらの問題に対処するために、AIエージェントがハードウェアやワークロードに特化したデータベースエンジンを合成し、正確性を正式に検証するシステムGenDB-Vを提案する。 GenDB-VはSQLテンプレートの特別な実装と、サポート対象のSQLサブセット内のクエリを受け入れる汎用エンジンをサポートする。 まずSQLSpecを開発し、SQLセマンティクスを形式化し、固定された実装に依存しない合成ターゲットを決定的に構築する。 次に,SQLSpecセマンティクスに低レベルの実行をブリッジする,ストレージ-実行協調最適化,パフォーマンス優先探索,および3層モジュール証明を通じて,高速コードと形式証明の併用を可能にする。 第三に、分離されたパイプラインにおいて、合成されたコードと固定された合成目標に対する証明を検証し、SQLの正しさとプログラムの安全性を証明します。 我々はTPC-HとSEC-EDGARのGenDB-Vを評価する。 検証済みのテンプレート実装では、GenDB-VはDuckDBとUmbraで22.0-61.3xの幾何平均高速化を実現している。 検証された汎用エンジンでは、GenDB-VはTPC-H上での1.27-3.4xの高速化も達成している。 GenDB-V はテストベースの LLM 合成法よりも優れた性能を実現していますが、監査とテストは、28のテンプレートのうち16のメソッドの実装において、誤った回答を公開しています。

関連論文リスト

• Demonstrating GenDB: Instance-Optimized and Customized Query Processing Code Generation via LLM Agents [25.352713493505792]
  GenDBは、クエリ処理を手動で設計したシステムから、Large Language Models (LLM) によって駆動されるクエリ処理コード生成に移行する、ジェネレーティブなクエリエンジンである。 プロトタイプは、反復的なテンプレートクエリのためのオフラインコード生成に適合する。事前生成コストが多くの実行を償却し、手動検査によって正確性を確保することができるからだ。 我々のデモでは、(1)GenDBがワークロードを視覚的に、インタラクティブに分析し、ハードウェアリソースと基盤となるデータをプロファイルし、クエリプランを作成し、それらに基づいてコードを生成し、最後にファズを使用して、正しく効率的な実装を反復的に実現します。
  論文  参考訳（メタデータ） (2026-07-22T18:01:29Z)
• EvoSQL: Memory-Augmented Critic-Generator Co-Evolution for Text-to-SQL [12.094895321584152]
  エヴォウェン(Evowen)は、ジェネレータと批評家の間の相互作用の共進化である。 発電機・臨界対を強化するために, 自己蒸留政策(SDPO)を導入する。 実験によると、EvowenはMag@16ベースラインよりもオープンソースモデルを一貫して改善している。
  論文  参考訳（メタデータ） (2026-06-04T14:21:19Z)
• GenDB: The Next Generation of Query Processing -- Synthesized, Not Engineered [25.352713493505792]
  大規模言語モデル(LLM)は、次世代のクエリ処理システムを形成し始めている。 我々は、インスタンス最適化およびカスタマイズされたクエリ実行コードを生成するLLMベースのエージェントシステムであるGenDBを提案する。 我々はGenDBとDuckDB、Umbra、MonetDB、ClickHouse、TPCといった最先端のクエリエンジンを比較します。
  論文  参考訳（メタデータ） (2026-03-02T17:03:43Z)
• Text-to-SQL as Dual-State Reasoning: Integrating Adaptive Context and Progressive Generation [54.53145282349042]
  DSR-sourced, textbfDual-textbfS textbfReasoning frameworkを導入する。 ポストトレーニングやインコンテキストの例がなければ、DSR-sourcedは競合性能を達成し、スパイダー2.0-Snowで35.28%、BIRD開発で68.32%に達する。
  論文  参考訳（メタデータ） (2025-11-26T13:52:50Z)
• HES-SQL: Hybrid Reasoning for Efficient Text-to-SQL with Structural Skeleton Guidance [6.653834890554154]
  HES-は、思考モード融合型教師あり微調整の統合により、テキストからレイテンシ生成を進化させる新しいハイブリッドトレーニングフレームワークである。 このフレームワークは、クエリの精度と実行効率を改善しながら、推論モードと非推論モードの切り替えを可能にする。
  論文  参考訳（メタデータ） (2025-10-10T01:15:57Z)
• RAISE: Reasoning Agent for Interactive SQL Exploration [47.77323087050061]
  本稿では,スキーマリンク,クエリ生成,反復的改善を1つのエンドツーエンドコンポーネントに統一する新しいフレームワークを提案する。 本手法は、不慣れなデータベースを扱う際に、人間がどう答えるかをエミュレートする。
  論文  参考訳（メタデータ） (2025-06-02T03:07:08Z)
• TrustGeoGen: Formal-Verified Data Engine for Trustworthy Multi-modal Geometric Problem Solving [106.04001249574786]
  TrustGeoGenは、標準的で信頼性の高いベンチマークを確立するために、正式に検証された幾何問題を生成するデータエンジンである。 1)ダイアグラム,テキスト,ステップバイステップのソリューションの生成を同期するマルチモーダルアライメント,2)すべての推論パスがルール準拠であることを保証する形式検証,3)接続思考,ブリッジング,ヒューマンライクな論理ステップとの論理的推論,4)複数のソリューションと自己回帰バックトラックを備えた多種多様な問題を生成できるTextitGeoExploreシリーズアルゴリズム。
  論文  参考訳（メタデータ） (2025-04-22T10:45:23Z)
• Scaling Automated Database System Testing [3.3302293148249125]
  我々は、Commonsqlの機能のサブセットをサポートするデータベースにテストオラクルを適用するビジョンとプラットフォームを提示する。 本研究では,Commonsqlの機能サブセットをサポートするデータベースに対して,テストオーラクルを適用するためのビジョンとプラットフォームであるSQLancer++を提示する。
  論文  参考訳（メタデータ） (2025-03-27T12:10:36Z)
• DBCopilot: Natural Language Querying over Massive Databases via Schema Routing [47.009638761948466]
  本稿では,DBCopilotについて述べる。DBCopilotは,大規模データベースをルーティングするためのコンパクトで柔軟なコピロットモデルを用いて,課題に対処するフレームワークである。 このフレームワークは、単一の軽量な微分可能な検索インデックスを使用して、大規模データベーススキーマのセマンティックマッピングを構築し、自然言語質問を目的のデータベースやテーブルに関連付け検索方法でナビゲートする。
  論文  参考訳（メタデータ） (2023-12-06T12:37:28Z)
• Injecting Domain Adaptation with Learning-to-hash for Effective and Efficient Zero-shot Dense Retrieval [49.98615945702959]
  我々は,TAS-B高密度検索器の下流ゼロショット検索精度を向上させるためのLTHおよびベクトル圧縮技術を評価する。 以上の結果から, 従来の研究とは異なり, LTH法はゼロショットTAS-B高密度レトリバーを平均14%のnDCG@10で過小評価できることがわかった。
  論文  参考訳（メタデータ） (2022-05-23T17:53:44Z)
• Bridging Textual and Tabular Data for Cross-Domain Text-to-SQL Semantic Parsing [110.97778888305506]
  BRIDGEは、フィールドのサブセットが質問に言及されたセル値で拡張されるタグ付きシーケンスの質問とDBスキーマを表します。 BRIDGEは、人気のクロスDBテキスト-リレーショナルベンチマークで最先端のパフォーマンスを達成しました。 本分析は,BRIDGEが望まれる相互依存を効果的に捕捉し,さらにテキストDB関連タスクに一般化する可能性を示唆している。
  論文  参考訳（メタデータ） (2020-12-23T12:33:52Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。