論文の概要: Verifying Human-Written Reasoning References

• arxiv url: http://arxiv.org/abs/2610.24690v1
• Date: Sat, 17 Oct 2026 13:43:05 GMT
• ステータス: 情報取得中
• システム内更新日: 2026-10-20 11:52:03.593848
• Title: Verifying Human-Written Reasoning References
• Title（参考訳）: 人文推論基準の検証
• Abstract要約: 本稿では,人文導出のための参照中心評価手法を提案する。 我々は、ステップの結論を1次論理(FOL)に変換するために、大きな言語モデル(LLM)と、詳細を確認するためにZ3 SMTソルバを使用する。 サポートが明記されていない230のステップのうち、191は、完全な元の前提に対してチェックする場合に必要となる。
• 参考スコア（独自算出の注目度）: 1.7588080994377207
• License:
• Abstract: Evaluating the reasoning of AI systems often relies on human-written reasoning chains as references, yet the logical support for their individual steps is rarely verified. Although prior neuro-symbolic approaches have formalized and checked reasoning, their reported evaluations do not systematically assess whether step conclusions in human-written reference derivations are entailed by their cited premise sets or investigate the sources of failures in those references. To address these limitations, we present a novel reference-centred assessment method for human-written derivations that combines entailment checking against cited premise sets, full-premise rechecking, and failure attribution to examine the reliability of these derivations and their formal representations. We evaluate it on P-FOLIO, using a large language model (LLM) to translate step conclusions into first-order logic (FOL) and the Z3 SMT solver to check entailment. Of 386 derivations examined, 202 (52.3%) meet all our checking criteria, meaning that every translated step is entailed by its stated support and the required target is established under the available FOL representations. Among 230 steps not entailed by their stated support, 191 become entailed when checked against the complete original premises, indicating that most initial failures reflect incomplete or mismatched support rather than unsupported claims. Manual analysis of the remaining 39 cases identifies 21 human reasoning errors, 11 FOL translation errors, and 7 dataset annotation errors. A separate manual audit of 50 randomly sampled steps that passed the entailment checks found 46 faithful FOL translations (92%). These findings suggest that disagreement with a human-written reasoning reference may originate in the reference or its formal representation rather than in the AI system being evaluated.
• Abstract（参考訳）: AIシステムの推論を評価するには、人間による推論チェーンを参照として利用することが多いが、個々のステップに対する論理的サポートは、ほとんど検証されていない。 従来のニューロシンボリックアプローチは、形式化され、チェックされた推論を行うが、報告された評価は、人間の記述された参照導出におけるステップの結論が、引用された前提セットによって関連付けられているか、またはそれらの参照における失敗の原因が調査されているかどうかを体系的に評価するものではない。 これらの制約に対処するため,提案手法では,引用された前提セットに対する係り受けチェック,実地再確認,障害帰属を組み合わせ,これらの導出の信頼性と形式的表現の検証を行う。 我々は,P-FOLIO上で,大規模言語モデル(LLM)を用いてステップの結論を1次論理(FOL)とZ3 SMTソルバに変換し,詳細を確認する。 調査された386の導出のうち、202(52.3%)は全てのチェック基準を満たしている。 提案されたサポートに関係のない230のステップのうち、191は、完全な元の前提に対してチェックする場合に必要となり、ほとんどの初期失敗は、保証されたクレームよりも不完全または不一致の支持を反映していることを示している。 残りの39件のマニュアル分析では、21の人間の推論エラー、11のFOL翻訳エラー、7のデータセットのアノテーションエラーが特定されている。 追加チェックに合格した50の無作為サンプリングステップの別のマニュアル監査では、46の忠実なFOL翻訳(92%)が見つかった。 これらの結果から,人間による推論基準との相違は,AIシステムの評価よりも,参照や形式的表現に起因している可能性が示唆された。

関連論文リスト

• Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization [10.295359122542969]
  FYANは仕様、検証計画、論理的レビュー、リーン実証の構築、知識のキュレーション、検証にまたがるエンドツーエンドのワークフローをコーディネートする。 中心的なコンポーネントはエビデンスに基づくセマンティック監査(semantic auditing)であり、形式的なステートメントが彼らの非公式な仕様を忠実に保持するかどうかを評価する。 FYANはまた、通常の微分方程式の数値解析のための9,355行のリーンライブラリODENumLibも開発した。
  論文  参考訳（メタデータ） (2026-09-30T08:02:51Z)
• Diagnosing Sampled LLM Reasoning in Formal Geometry: Coverage, Realization, and Validity Evidence [0.5721241882795979]
  CRV(Coverage, Realization, and Validity Evidence)について紹介する。 CRVは,形式的幾何状態を考慮したサンプル付き大言語モデル(LLM)の評価プロトコルである。 正しい答えがプール内で1回か2回しか発生しない場合、読み出し精度は特に低い。
  論文  参考訳（メタデータ） (2026-09-26T20:30:56Z)
• NovGauge: A Fine-Grained Benchmark for Diagnosing LLMs' Capability in Paper Novelty Assessment [54.4265627247104]
  大規模言語モデル(LLM)は、主要なAIカンファレンスでピアレビューでますます使用されている。 既存のベンチマークでは、ノベルティを1つの総合的なスコアとして評価している。 本報告では,詳細なノベルティアセスメント診断のための人手によるベンチマークであるNovGaugeについて述べる。
  論文  参考訳（メタデータ） (2026-09-10T08:34:56Z)
• FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence [9.041607777624504]
  FaithSieveは、自然言語の数学的証明を詳細に評価するためのリーン支援フレームワークである。 証明段階を局所的推論単位に分解し、型付き証明義務を抽出し、検証する。 350-problemのOlympiadデータセットでは、GPT-5.4バックボーンを使用したFaithSieveは81.43%の正確なファーストエラー精度を実現している。
  論文  参考訳（メタデータ） (2026-08-26T18:43:30Z)
• Do large language models scrutinise what they review? A multimodal audit of scoring calibration, error detection, and author-identity effects [0.0]
  大きな言語モデル(LLM)は、ピアレビューを生成するためにますます使われています。 本研究は,2026年国際学習表現会議への165件の応募に対して,2つのマルチモーダルLCMをレビュアーとして評価した。
  論文  参考訳（メタデータ） (2026-07-31T12:12:33Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  本稿では,意味的整合性評価を自己形式化プロセスに統合する反射的自己形式化手法を提案する。 これにより、モデルが形式的なステートメントを反復的に生成し、セマンティックな忠実さを評価し、自己修正された特定エラーを発生させることができる。 実験の結果、ReFormは最強のベースラインに対して平均22.6ポイントの改善を達成した。
  論文  参考訳（メタデータ） (2025-10-28T16:22:54Z)
• SocREval: Large Language Models with the Socratic Method for Reference-Free Reasoning Evaluation [78.23119125463964]
  我々は,参照フリー推論評価における新規な設計手法であるSocREvalを開発した。 SocREvalはGPT-4の性能を大幅に改善し、既存の参照フリーおよび参照ベース推論評価指標を上回っている。
  論文  参考訳（メタデータ） (2023-09-29T18:25:46Z)

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

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