論文の概要: Autoformalizing Argumentative Material Inferences

• arxiv url: http://arxiv.org/abs/2609.16991v1
• Date: Tue, 15 Sep 2026 11:05:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-16 14:56:08.46532
• Title: Autoformalizing Argumentative Material Inferences
• Title（参考訳）: 自動定式化材料推論
• Abstract要約: 我々は、ガード補完として議論材料推論のための自己形式化を開発する。 GUARDは、証明された信条を大幅に改善する。 シンボル的ソフトな批判と明示的な仮定層がこれらの利益の大部分を担っていることを示す。
• 参考スコア（独自算出の注目度）: 26.35292656634472
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Natural language arguments are compelling before they are formally explicit. A premise supports a claim through defeasible warrants, background commitments, and exception conditions that the text leaves implicit. However, formal verification requires the opposite. Making such arguments machine-checkable requires constructing the missing commitments, not only translating given sentences into logic. Construction, however, carries a risk that translation does not: a system free to add premises can make any claim provable, and a formally valid proof may assert the claim outright, prove it without the original premise, or establish more than the claim itself. We address this problem by formulating autoformalization for argumentative material inference as guard completion, in which non-monotonic material support is turned into monotonic formal inference relative to an explicitly constructed guard set. A completion is accepted only when its proof both passes the theorem prover and survives contrastive tests of premise dependence and claim selectivity. We implement this formulation in GUARD, a neuro-symbolic framework in which LLMs construct and formalize candidate guards, Isabelle/HOL verifies the resulting theories and returns step-level feedback for iterative refinement, and the system abstains when no faithful completion can be reached. Our empirical results on Debatepedia and ARCT using different LLMs demonstrate that GUARD yields significant improvements in verified-faithful (+35.3, +32.9 points) and substantial reductions in leakage (-25.9, -21.9 points) over the state-of-the-art LLM-driven theorem proving approach. Moreover, we show that the symbolic soft critique and the explicit assumption layer account for most of these gains, with the soft critique also improving the initial validity of the elicited context and reducing the number of iterations required for successful verification.
• Abstract（参考訳）: 自然言語の議論は、正式に明示される前に説得力がある。 前提は、テキストが暗黙に残す、デファシブルな保証、バックグラウンドのコミットメント、例外条件を通じてクレームをサポートする。 しかし、正式な検証にはその逆が必要である。 そのような引数を機械チェック可能にするには、与えられた文を論理に翻訳するだけでなく、欠落したコミットメントを構築する必要がある。 しかし、建設は、翻訳ができないリスクを負う: 前提を付けないシステムは、いかなる主張も証明可能であり、公式の証明は、請求を正しく主張し、元の前提なしで証明し、請求そのもの以上のものを確立することができる。 議論材料推論の自己形式化をガード完備化として定式化し,非単調材料サポートを明示的に構成されたガード集合に対して単調な形式推論に変換することでこの問題に対処する。 完備化は、その証明がともに定理証明器を通過し、前提依存とクレーム選択性の対照的な試験を生き残る場合にのみ受け入れられる。 この定式化は、LLMが候補ガードを構築し、形式化するニューロシンボリックなフレームワークであるGUARDで実施され、Isabelle/HOLは結果の理論を検証し、反復的な改善のためのステップレベルのフィードバックを返す。 異なる LLM を用いたDebatepedia と ARCT の実証実験の結果,GUARD は証明された信頼度 (+35.3,+32.9 点) と,最先端の LLM 駆動定理証明法に比べてリーク率 (-25.9,-21.9 点) が著しく低下していることが示されている。 さらに,これらの利得のほとんどについて,記号的ソフト批判と明示的仮定層が考慮されていることを示し,ソフト批判は,提案したコンテキストの初期妥当性を改善し,検証に要するイテレーション数を削減している。

関連論文リスト

• Faithful Autoformalization of Natural Language Assertions [2.8921494813790094]
  Monty: アサーションのための自動形式化フレームワークを紹介します。 本手法は,新しい適合度測定値を用いたフィルタリング形式化に基づく。 提案手法は,LLMを用いてアサーションの翻訳を行う場合よりも,基礎的真理を確実に生成することを示す。
  論文  参考訳（メタデータ） (2026-07-14T22:12:14Z)
• Neurosymbolic Learning for Inference-Time Argumentation [18.461907013598424]
  クレーム検証は、健康やファイナンスなど、ハイテイクな環境において重要な問題である。 第三次クレーム検証のためのトレーニング可能なニューロシンボリックフレームワークである推論時間議論(ITA)を導入する。
  論文  参考訳（メタデータ） (2026-05-19T16:49:29Z)
• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。 LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
  論文  参考訳（メタデータ） (2026-04-07T19:33:54Z)
• Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism [2.215655942741476]
  本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
  論文  参考訳（メタデータ） (2026-04-07T01:19:41Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  我々は,系統的かつ包括的な推論プロセスを実行するためのモデルを導くことで,モデルがよりきめ細やかで正確な絞り込み決定を実行できることを提案する。 我々は,(i)クレームの分解,(ii)サブクレームの属性と包含分類,および(iii)集約分類から成る3段階の推論プロセスを定義し,そのような導出推論が実際に幻覚検出の改善をもたらすことを示す。
  論文  参考訳（メタデータ） (2025-06-05T17:02:52Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  本稿では、精度割当てに対する離散探索アルゴリズムであるVeracity Search(VS)を紹介する。 その他の方法では、後続の精度値よりも後続の分布において難解な推論を行う。 VSを一般化し、新しいコンテキストで正確なゼロショットの精度推論を可能にする。
  論文  参考訳（メタデータ） (2025-05-17T04:16:36Z)
• CRAVE: A Conflicting Reasoning Approach for Explainable Claim Verification Using LLMs [15.170312674645535]
  CRAVE は、説明可能なクレーム VErification に対する Conflicting Reasoning Approach である。 大規模な言語モデルによって推論される矛盾する理性に基づいて、複雑なクレームを検証することができる。 CRAVEは最先端の手法よりもはるかに優れた性能を実現している。
  論文  参考訳（メタデータ） (2025-04-21T07:20:31Z)
• Aligning Large Language Models for Faithful Integrity Against Opposing Argument [71.33552795870544]
  大規模言語モデル(LLM)は複雑な推論タスクにおいて印象的な機能を示している。 原文が正しい場合でも、会話中に不誠実な議論によって容易に誤解される。 本稿では,信頼度と信頼度を両立させる新しい枠組みを提案する。
  論文  参考訳（メタデータ） (2025-01-02T16:38:21Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)

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

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