論文の概要: Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing

• arxiv url: http://arxiv.org/abs/2606.27926v1
• Date: Fri, 26 Jun 2026 10:20:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-29 18:24:25.451395
• Title: Verifiable Geometry Problem Solving: Solver-Driven Autoformalization and Theorem Proposing
• Title（参考訳）: 検証可能な幾何学的問題の解法: 解法駆動型オートフォーマライゼーションと定理証明
• Abstract要約: 本稿では,SD-GPSを提案する。SD-GPSは,定式化と導出の両面において,シンボリック・ソルバを実行オラクルとして扱う,ソルバ駆動のフレームワークである。 SD-GPSは, 既存のMLLM, ニューラル, ニューラルシンボリックな手法よりも, 標準完備化, 多重選択, クロスモーダル参照方式よりも優れていた。
• 参考スコア（独自算出の注目度）: 27.961458371130018
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Geometry Problem Solving have increasingly adopt the neuro-symbolic paradigm, combining neural intuition with symbolic rigor. However, current frameworks suffer from severe bottlenecks in two core stages: autoformalization, which treats multimodal translation as a static task decoupled from downstream solver compatibility, and theorem prediction, where solvers frequently hit a deductive impasse due to fixed rule libraries. To address these, we propose SD-GPS, a solver-driven framework that treats the symbolic solver as an execution oracle throughout both formalization and deduction. First, Solver-Driven Autoformalization unifies supervised formal-language adaptation and solvability-guided reinforcement learning into a single module built on QwenVL3-2B, making executability the central training signal. Second, Verified Theorem Proposing introduces an impasse-aware agent that proposes local auxiliary lemmas from current proof states, ensuring soundness by filtering all proposals through symbolic verification. Empirical evaluations on Geometry3K and PGPS9K demonstrate that SD-GPS consistently outperforms existing MLLM, neural, and neuro-symbolic methods across standard completion, multiple-choice, and cross-modal reference regimes, proving that closing the loop between multimodal perception and symbolic execution significantly improves geometric reasoning, offering profound insights into how neural agents can be grounded by formal systems to achieve verifiable problem-solving capabilities.
• Abstract（参考訳）: 幾何学的問題解決は、神経直観と記号的厳密さを組み合わせた、神経-記号的パラダイムをますます取り入れている。 しかし、現在のフレームワークは、下流のソルバ互換性から切り離された静的なタスクとしてマルチモーダル翻訳を扱うオートフォーマル化(autoformalization)と、固定されたルールライブラリによってしばしば減算的障害にぶつかる定理予測の2つの中核段階において深刻なボトルネックに悩まされている。 そこで我々は,SD-GPSを提案する。SD-GPSは,定式化と導出の両面において,シンボリック・ソルバを実行オラクルとして扱う,ソルバ駆動のフレームワークである。 まず、Solver-Driven Autoformalizationは、教師付き形式言語適応と可解性誘導強化学習をQwenVL3-2B上に構築した単一モジュールに統一し、実行可能性を中心的な訓練信号とする。 第二に、検証定理証明法(Verified Theorem Proposing)は、現在の証明状態から局所的な補助補題を提案し、記号的検証を通じて全ての提案をフィルタリングすることで音質を保証する不適切なエージェントを導入している。 Geometry3K と PGPS9K に関する実証的な評価は、SD-GPS が既存のMLLM、ニューラル、ニューラル、ニューラルシンボリックの手法を標準完備化、複数選択、およびクロスモーダルレファレンスで一貫して上回り、マルチモーダルな知覚とシンボリックな実行の間のループを閉じることが幾何学的推論を著しく改善することを証明する。

関連論文リスト

• BiNSGPS: Geometry Problem Solving via Bidirectional Neuro-Symbolic Interaction [45.32907555157728]
  BiNSGPSはMLLMアドバイザとソルバ間の双方向神経・シンボリック相互作用を確立するフレームワークである。 MLLMアドバイザはシンボルソルバからのフィードバックを積極的に取り入れ、一貫性のない形式表現を動的に修正する。
  論文  参考訳（メタデータ） (2026-06-03T09:18:37Z)
• Branched Signature Kernel Solvers for ODEs with rough Single-Trajectory signals [2.94985644773306]
  単軌道で駆動される常微分方程式に対する分岐シグネチャカーネルソルバを開発する。 Emphcount-sampling構造は、単一の観察をN+1$ネストされたトレーニングパスの階層的なファミリーに変換する。 カーネル・コロケーション・フレームワークは、アンザッツを解の最高階微分または解自体に配置する。
  論文  参考訳（メタデータ） (2026-05-25T13:22:07Z)
• Heuristic Classification of Thoughts Prompting (HCoT): Integrating Expert System Heuristics for Structured Reasoning into Large Language Models [9.545957160908115]
  HCoT(Huristic- classification-of-Thoughts prompting schema) HCoT(Huristic- classification-of-Thoughts prompting schema) HCoT(Huristic- classification-of-Thoughts prompting schema)
  論文  参考訳（メタデータ） (2026-04-14T07:24:08Z)
• A Survey of Reasoning in Autonomous Driving Systems: Open Challenges and Emerging Paradigms [49.66022971508878]
  私たちは、推論はモジュラーコンポーネントからシステムの認知コアに高めるべきだと論じています。 応答性推論のトレードオフやソーシャルゲーム推論など,7つの中核的推論課題を導出し,体系化する。 我々は,LLMに基づく推論と,ミリ秒スケールで安全クリティカルな車両制御の要求との間の,高レイテンシ,熟考的特性の根本的かつ未解決な緊張関係を同定する。
  論文  参考訳（メタデータ） (2026-03-11T07:40:53Z)
• VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning [4.3414302048068745]
  本稿では,大規模言語モデルとSMTソルバを組み合わせたニューロシンボリック・フレームワークを提案する。 本稿では,(1)形式的意味的等価性チェックによるマルチモデルコンセンサス,(2)適切な検証戦略に異なるクレーム型を指示するセマンティックルーティング,(3)最小補正サブセットによる正確な論理的エラーローカライゼーション,の3点を紹介する。 GPT-OSS-120Bモデルでは、VERGEはシングルパスアプローチと比較して、一連の推論ベンチマークにおいて平均18.7%の性能向上を示す。
  論文  参考訳（メタデータ） (2026-01-27T20:59:11Z)
• Matrix Factorization Framework for Community Detection under the Degree-Corrected Block Model [48.989531198582704]
  我々は,DCBM推論を制約付き非負行列分解問題として再定義できることを示した。 我々のアプローチは、任意の特定のネットワーク構造に適応し、DCBMで表現可能な任意の構造を持つグラフに適用する。 合成および実ベンチマークネットワークの実験により,本手法はDCBMの推測に匹敵するコミュニティを検出する。
  論文  参考訳（メタデータ） (2026-01-09T19:16:29Z)
• AutoGPS: Automated Geometry Problem Solving via Multimodal Formalization and Deductive Reasoning [14.44742282076576]
  AutoGPSは、簡潔で信頼性があり、人間の解釈可能な推論プロセスで幾何学的問題を解決する、神経象徴的な協調フレームワークである。 MPFは、ニューラルネットワークのクロスモーダル理解を利用して、幾何学的問題を構造化された形式言語表現に変換する。 DSRは形式化を入力とし、ハイパーグラフ拡張タスクとして幾何学的問題解決を定式化する。
  論文  参考訳（メタデータ） (2025-05-29T12:01:20Z)
• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  平面幾何学的問題解法 (PGPS) のニューラルネットワークモデルを提案し, モーダル融合, 推論過程, 知識検証の3つの重要なステップについて述べる。 推論のために、幾何学的推論過程を記述するための説明可能な解プログラムを設計し、自己限定デコーダを用いて解プログラムを自動回帰的に生成する。 また, PGPS9Kと呼ばれる大規模幾何学的問題データセットを構築し, テキスト節, 解法プログラム, 関連知識解決器の詳細なアノテーションを含む。
  論文  参考訳（メタデータ） (2024-07-10T02:45:22Z)
• Task-Oriented Sensing, Computation, and Communication Integration for Multi-Device Edge AI [108.08079323459822]
  本稿では,AIモデルの分割推論と統合センシング通信(ISAC)を併用した,新しいマルチインテリジェントエッジ人工レイテンシ(AI)システムについて検討する。 推定精度は近似的だが抽出可能な計量、すなわち判別利得を用いて測定する。
  論文  参考訳（メタデータ） (2022-07-03T06:57:07Z)
• Message Passing Neural PDE Solvers [60.77761603258397]
  我々は、バックプロップ最適化されたニューラル関数近似器で、グラフのアリーデザインのコンポーネントを置き換えるニューラルメッセージパッシング解決器を構築した。 本稿では, 有限差分, 有限体積, WENOスキームなどの古典的手法を表現的に含んでいることを示す。 本研究では, 異なる領域のトポロジ, 方程式パラメータ, 離散化などにおける高速, 安定, 高精度な性能を, 1次元, 2次元で検証する。
  論文  参考訳（メタデータ） (2022-02-07T17:47:46Z)
• Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning [123.06420835072225]
  3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。 我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。 イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
  論文  参考訳（メタデータ） (2021-05-10T07:46:55Z)

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

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