論文の概要: Towards a Certifying Grounder

• arxiv url: http://arxiv.org/abs/2607.21199v1
• Date: Thu, 23 Jul 2026 11:19:24 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-24 18:26:25.386965
• Title: Towards a Certifying Grounder
• Title（参考訳）: グラウンドの認定に向けて
• Abstract要約: 高次理論を等価量化子のない公式に変換するグラウンディングは、宣言的解法において重要なステップである。 本稿では,(1)導出の証明形式であるCertiFOX,(2)グラウンディング・ノーマル・フォーム(GNF),(3)独立した証明チェッカーであるCheckFOXについて述べる。
• 参考スコア（独自算出の注目度）: 41.775186944241234
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Grounding, the translation of high-level theories into equivalent quantifier-free formulas, is a crucial step in declarative solving, yet it has so far escaped the proof-logging revolution. When this grounding step is not certifying, there is no way of knowing that the obtained solutions actually correspond to the original problem specification, resulting in a trust gap. In this paper, we close the trust gap between the user's high-level specification and the solver's low-level input by introducing a novel certifying grounding framework for first-order logic model expansion (FOX) over finite domains. We present CertiFOX, a framework consisting of: (1) a proof format for grounding derivations, (2) GroundFOX, a certifying grounder operating on theories in Grounding Normal Form (GNF)--a new normal form designed for compact, domain-aware grounding--and (3) CheckFOX, an independent proof checker. Our approach guarantees that the grounder's output is equivalent to the input specification, setting the stage for trustworthy end-to-end certified solving pipelines for declarative languages. Experimental evaluation confirms that CertiFOX is a feasible approach. The GroundFOX grounder is broadly comparable with other grounders, and proof checking with CheckFOX adds overhead within a small constant factor of grounding time.
• Abstract（参考訳）: 高レベルの理論を等価な量化子のない公式に翻訳するグラウンディングは、宣言的解法における重要なステップであるが、これまでのところ証明語学革命から脱却している。 この基底ステップが認証されていない場合、得られた解が元の問題仕様に実際に対応していることを知る方法がないため、信頼ギャップが生じる。 本稿では,ユーザの高レベル仕様と解決者の低レベル入力との信頼ギャップを,有限領域上の一階述語論理モデル拡張(FOX)のための新しい認証基盤フレームワークを導入することにより解消する。 本稿では,(1)導出の証明形式であるCertiFOX,(2)グラウンディング・ノーマル・フォーム(GNF)における理論に基づいて動作する認証グラウンドダー,(3)独立した証明チェッカーであるCheckFOXについて述べる。 提案手法は,入力仕様とグルーダの出力が等価であることを保証し,宣言型言語に対する信頼性の高いエンドツーエンドの問題解決パイプラインのステージを設定する。 実験的評価により、CertiFOXは実現可能なアプローチであることが確認された。 GroundFOXグラウンドは、他のグラウンドと広く同等であり、CheckFOXによる証明チェックは、グラウンドタイムの小さな定数係数でオーバーヘッドを追加する。

関連論文リスト

• GRACE: Graph-Grounded Reflective Agent Copilot Engine for Expert-in-the-Loop Knowledge Expansion [2.729876880765472]
  大規模言語モデルは、しばしばもっともらしいが根拠のないクレームを生成する。 GRACEは、応答をアトミックなクレームに分解し、信頼された知識の先駆者に対してそれらを根拠とするフレームワークである。 複数の言語モデルおよび一般知識とドメイン固有知識の両方にまたがるデータセット上でGRACEを評価する。
  論文  参考訳（メタデータ） (2026-09-03T20:03:20Z)
• Precision Is Not Faithfulness: Coverage-Aware Evaluation of Grounded Generation with a Complete Oracle [0.0]
  基準自由忠実度測定は、モデルが基底真理に対して行う各原子的クレームを検証する。 彼らが盲点を共有していることを示す:彼らは精度だけを計測し、主張されている主張は支持されているか? 戦略的基底真理が決定論的に導出される領域であるF1テレメトリを用いて、この測定を可能にする。
  論文  参考訳（メタデータ） (2026-06-08T11:56:25Z)
• Controlling False Discovery in Arbitrarily Structured Hypothesis Spaces via Reproducing Kernels [47.16593717985932]
  連続的なドメイン、グラフ、階層を1つのアルゴリズムで統一するフレームワークをカーネル選択のみで導入する。 FDR(False Discovery Rate)を制御するための2つの決定ルールを提供します。 本手法は,高次元実世界のデータセットから得られた空間的位置とタンパク質間相互作用グラフを用いた遺伝子発現タスクの2つの情報源で検証する。
  論文  参考訳（メタデータ） (2026-05-17T17:42:56Z)
• Text Corpora as Concept Fields: Black-Box Hallucination and Novelty Measurement [3.035872403903575]
  本稿では,テキストコーパスのtextbfConcept Field について紹介する。 我々は、観測されたデルタとフィールドの局所ガウス推定の間の平均的な絶対的なz-距離である$で、フィールドとの合意を採点する。 提案手法は, 連邦規制法典に基づく接地性検出と, プロジェクト・グーテンベルクにおける新規性検出の2つの大規模設定において評価される。
  論文  参考訳（メタデータ） (2026-05-06T16:38:49Z)
• Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models [94.68358825189738]
  本稿では,予測精度と推論品質を協調的に最適化する検証済み領域の学習後フレームワークを提案する。 我々は,エンジン信号に対して推論ステップを確定的に検証できる制御テストベッドであるチェスのVPSを評価する。 VPSは、推論品質を著しく向上させながら精度を保ち、勝利率エラーを最大30%削減し、一貫性をほぼ飽和状態に回復する。
  論文  参考訳（メタデータ） (2026-04-03T15:19:46Z)
• ODD: Overlap-aware Estimation of Model Performance under Distribution Shift [8.569585481097839]
  以前の作業では、分散シフトの下で実際のエラー境界を導出するために、不一致不一致(DIS2)を使用していた。 オーバーラップ・アウェア・ディスレパンシー(ODD)を考案する ODDベースのバウンダリはドメインオーバラップを推定するためにドメイン分類器を使用し、DIS2よりもターゲット性能を予測します。
  論文  参考訳（メタデータ） (2025-06-17T21:05:42Z)
• Look Ma, No Ground Truth! Ground-Truth-Free Tuning of Structure from Motion and Visual SLAM [64.57742015099531]
  評価は、モーション(SfM)と視覚SLAM(VSLAM)システムから構造を開発・調整する上で重要である。 この土台真実への依存は、様々な環境におけるSfMおよびSLAMアプリケーションを制限する。 幾何学的基底真理の必要をなくすため,GTF評価手法を提案する。
  論文  参考訳（メタデータ） (2024-12-02T04:40:03Z)
• Probing Factually Grounded Content Transfer with Factual Ablation [68.78413677690321]
  グラウンドドジェネレーションは、事実情報の信頼性のある外部文書(グラウンドディング)に描画する。 事実を計測するのも簡単で、すべての事実ではなく、世代が根拠に同意するかどうかをテストする。 本稿では,現実的な根拠からの情報を用いて,世代がプロンプトを拡大するコンテンツ転送問題について検討する。
  論文  参考訳（メタデータ） (2022-03-18T19:18:54Z)
• Tune it the Right Way: Unsupervised Validation of Domain Adaptation via Soft Neighborhood Density [125.64297244986552]
  本稿では,点間の類似度分布のエントロピーを計算し,ソフト近傍の密度を測定する教師なし検証基準を提案する。 私たちの基準は、競合する検証方法よりもシンプルですが、より効果的です。
  論文  参考訳（メタデータ） (2021-08-24T17:41:45Z)

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

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