論文の概要: Computer-Orchestrated Design of Algorithms: From Join Specification to Implementation
- arxiv url: http://arxiv.org/abs/2603.19434v1
- Date: Thu, 19 Mar 2026 19:52:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-23 19:48:38.857529
- Title: Computer-Orchestrated Design of Algorithms: From Join Specification to Implementation
- Title（参考訳）: アルゴリズムのコンピュータ構成設計: 仕様の整合化から実装へ
- Authors: Zeyuan Hu,
- Abstract要約: 本稿では,TreeTracker Join(mathsfTTJ$)の物理的共同設計に使用されるコンピュータオーケストレーションテストフレームワークを提案する。
$mathsfCODA$は、状態の管理ミスやジョインツリーとブッシープラン間のコンフリクトのマッピングなど、微妙な翻訳欠陥をうまく分離する。
これらの翻訳課題に直面することが、$mathsfCODA$のアーキテクチャ上の進化を、堅牢で構造を意識したテスト生成パイプラインへと引き起こした経緯を詳述する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Equipping query processing systems with provable theoretical guarantees has been a central focus at the intersection of database theory and systems in recent years. However, the divergence between theoretical abstractions and system assumptions creates a gap between an algorithm's high-level logical specification and its low-level physical implementation. Ensuring the correctness of this logical-to-physical translation is crucial for realizing theoretical optimality as practical performance gains. Existing database testing frameworks struggle to address this need because necessary algorithm-specific inputs such as join trees are absent from standard test case generation, and integrating complex algorithms into these frameworks imposes prohibitive engineering overhead. Fallback solutions, such as using macro-benchmark queries, are inherently too noisy for isolating intricate defects during this translation. In this experience paper, we present a retrospective analysis of $\mathsf{CODA}$, a computer-orchestrated testing framework utilized during the physical co-design of TreeTracker Join ($\mathsf{TTJ}$), a theoretically optimal yet practical join algorithm recently published in ACM TODS. By synthesizing minimal reproducible examples, $\mathsf{CODA}$ successfully isolates subtle translation defects, such as state mismanagement and mapping conflicts between join trees and bushy plans. We demonstrate that this logical-to-physical translation process is a bidirectional feedback loop: early structural testing not only hardened $\mathsf{TTJ}$'s physical implementation but also exposed a boundary condition that directly refined the formal precondition of $\mathsf{TTJ}$ itself. Finally, we detail how confronting these translation challenges drove the architectural evolution of $\mathsf{CODA}$ into a robust, structure-aware test generation pipeline for join-tree-dependent algorithms.
- Abstract（参考訳）: 近年,データベース理論とシステムとの交差に注目が集まっている。
しかし、理論的抽象化とシステム仮定の相違により、アルゴリズムの高レベル論理仕様と低レベル物理実装との間にギャップが生じる。
この論理-物理変換の正確性を保証することは、理論的最適性を実用的な性能向上として実現するために不可欠である。
既存のデータベーステスティングフレームワークは、ジョインツリーのようなアルゴリズム固有の入力が標準的なテストケース生成に欠如しているため、このニーズに対処するのに苦労している。
マクロベンチマーククエリのようなフォールバックソリューションは、本質的には、この翻訳中に複雑な欠陥を分離するにはノイズが多すぎる。
本稿では、最近ACM TODSで発表された理論上最適だが実用的な結合アルゴリズムであるTreeTracker Join(\mathsf{TTJ}$)の物理的共設計時に使用されるコンピュータオーケストレーションテストフレームワークである$\mathsf{CODA}$の振り返り分析について述べる。
最小限の再現可能な例を合成することにより、$\mathsf{CODA}$は、状態管理ミスやジョインツリーとブッシープラン間の衝突のマッピングなど、微妙な翻訳欠陥をうまく分離する。
初期構造検査は、$\mathsf{TTJ}$の物理的実装だけでなく、$\mathsf{TTJ}$の形式的前提条件を直接洗練する境界条件も明らかにした。
最後に、これらの翻訳課題に直面することが、$\mathsf{CODA}$のアーキテクチャ進化を、ジョインツリー依存アルゴリズムのための堅牢で構造対応なテスト生成パイプラインにどのように引き起こしたかを詳述する。
関連論文リスト
- Can LLMs Prove Robotic Path Planning Optimality? A Benchmark for Research-Level Algorithm Verification [5.637461397736495]
本稿では,ロボット経路計画アルゴリズムの近似比証明について,LLM(Large Language Models)を評価するための最初のベンチマークを紹介する。
我々の評価では、最強のモデルでさえ、外部のドメイン知識なしで完全に有効な証明を作成するのに苦労していることが明らかになっている。
論文 参考訳（メタデータ） (2026-03-19T20:55:46Z) - TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib? [104.38098884163541]
新たな定義枠組みに適用した場合の現在のATPシステムの堅牢性を評価する。
本稿では,terence Tao氏のAnalytic Iから派生した,学部レベルのベンチマークであるTaoBenchを紹介する。
公平な評価のために,各問題に対してコンパイル可能な自己完結型ローカル環境を自動的に抽出するエージェントパイプラインを構築した。
論文 参考訳（メタデータ） (2026-03-13T07:39:47Z) - Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
本研究では,大規模状態空間を持つ決定過程(MDP)における非マルコフ報酬の論理的仕様に関する新しい枠組みを提案する。
我々のアプローチは有限トレース(LTLfMT)上での線形時間論理モデュロ理論を利用する
本稿では,報酬マシンとHER(Hindsight Experience Replay)をベースとした一階述語論理仕様の翻訳手法を提案する。
論文 参考訳（メタデータ） (2026-02-05T22:11:28Z) - Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。
提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
論文 参考訳（メタデータ） (2025-10-02T15:15:50Z) - Bootstrapping as a Morphism: An Arithmetic Geometry Approach to Asymptotically Faster Homomorphic Encryption [0.9179857807576733]
本稿では,従来の回路評価モデルを完全にバイパスするブートストラップ手法を提案する。
直射射影としてブートストラップ操作を再構成するために,現代の算術幾何学のツールを適用した。
我々の研究は、$O(d cdot textpoly(log q))$、$d$が環次元、$q$が暗号文である完全かつ確実に正しいブートストラップアルゴリズムである。
論文 参考訳（メタデータ） (2025-09-29T03:39:01Z) - READER: Retrieval-Assisted Drafter for Efficient LLM Inference [0.0386965802948046]
自己回帰言語モデルはトークンシーケンスよりも分解された確率をインスタンス化するが、その厳密なシーケンシャルなデコーディングプロセスは、遅延推論に固有の低いバウンドを課す。
このボトルネックは、大規模生成モデルのスケーラブルなデプロイにおける中心的な障害として現れています。
本稿では,補助的ドラフトモデルのトレーニングを回避した投機的復号化フレームワークREADERを提案する。
論文 参考訳（メタデータ） (2025-08-12T16:47:48Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Fractal Structure and Generalization Properties of Stochastic
Optimization Algorithms [71.62575565990502]
最適化アルゴリズムの一般化誤差は、その一般化尺度の根底にあるフラクタル構造の複雑性'にバウンドできることを示す。
さらに、特定の問題(リニア/ロジスティックレグレッション、隠れ/層ニューラルネットワークなど)とアルゴリズムに対して、結果をさらに専門化します。
論文 参考訳（メタデータ） (2021-06-09T08:05:36Z) - String Theories involving Regular Membership Predicates: From Practice
to Theory and Back [12.98284167710378]
文字列制約系に対する満足度問題に対するアルゴリズムは、対象ケースに存在する制約の構造を徹底的に理解する必要がある。
本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,決定不能性を証明する。
特に、現実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直結する。
論文 参考訳（メタデータ） (2021-05-15T13:13:50Z) - On Effective Parallelization of Monte Carlo Tree Search [51.15940034629022]
モンテカルロ木探索(MCTS)は、探索木を構築するためにかなりの数のロールアウトを必要とするため、計算コストがかかる。
効果的な並列MCTSアルゴリズムを設計する方法は、体系的に研究されておらず、まだよく分かっていない。
我々は,より効率的な並列MCTSアルゴリズムの設計に,提案する必要条件をどのように適用できるかを実証する。
論文 参考訳（メタデータ） (2020-06-15T21:36:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。