論文の概要: FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
- arxiv url: http://arxiv.org/abs/2608.10916v1
- Date: Tue, 11 Aug 2026 13:36:52 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-12 19:14:46.053574
- Title: FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation
- Title（参考訳）: FaithformBench: 数学的連鎖の忠実性のベンチマーク
- Abstract要約: 自動形式化システムは、自然言語推論のステップをリーンのような証明アシスタントの形式的なステートメントにマッピングします。
既存のアプローチでは、人間に注釈を付けた高価な真実を必要とするか、LLMの審査員や埋め込みモデルに依存している。
本稿では,AF忠実度に関する新しいベンチマークを提案する。これは適用が安価で,仮定が弱く,肯定的,否定的な両例を評価できる。
- 参考スコア（独自算出の注目度）: 26.089963426404164
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalisation (AF) systems map natural language reasoning steps into formal statements in a proof assistant such as Lean. We consider how to assess the faithfulness of these systems. Existing approaches require expensive human-annotated ground truth, or rely on LLM judges or embedding models, which come with limited guarantees of accuracy. In addition, these methods typically only consider inputs that are known to be correct, and therefore do not assess whether the AF translates incorrect inputs faithfully. To address these limitations, we propose a new benchmark for AF faithfulness that is cheap to apply, sound under weak assumptions, and assesses both positive and negative examples. Our method is based on automatically generating perturbed reasoning steps that are designed to be invalid, and then measuring validity preservation on unperturbed steps and invalidity preservation on perturbed steps. We apply our method to eight AF systems across four mathematical datasets, and observe pervasive sycophancy: many AFs "silently correct" invalid inputs into provable statements. The most validity-preserving fine-tuned AFs are also the most sycophantic, suggesting a tension between validity and invalidity preservation in current AF systems.
- Abstract（参考訳）: 自動形式化(AF)システムは、自然言語推論のステップをリーンのような証明アシスタントの形式的なステートメントにマッピングします。
これらのシステムの忠実さを評価する方法について検討する。
既存のアプローチでは、高価な人間による注釈付けの真理や、LLMの審査員や埋め込みモデルに依存しており、精度の保証は限られている。
加えて、これらの手法は一般的に正しいことが知られている入力のみを考慮し、したがってAFが誤った入力を忠実に翻訳するかどうかを判断しない。
これらの制約に対処するため、安易に適用可能なAF忠実度に関する新しいベンチマークを提案し、弱い仮定の下で音を鳴らし、正と負の両方の例を評価する。
提案手法は, 無効となるように設計された摂動推論ステップを自動生成し, 摂動ステップの妥当性, 摂動ステップの妥当性を計測する。
提案手法を4つの数学的データセットにまたがる8つのAFシステムに適用し、多くのAFが証明可能なステートメントに「正当に正当」な入力を行った。
最も有効に調整されたAFは最もシコファンであり、現在のAFシステムにおける妥当性と無効性保存の緊張を示唆している。
関連論文リスト
- Non-Parametric Rehearsal Learning via Conditional Mean Embeddings [88.89267783967263]
本研究では,不必要な未来(AUF)問題をテキスト化するための非パラメトリックリハーサル学習手法を提案する。
具体的には、カーネル機械を用いてAUFの目的を、動作誘起分布変化から所望性モデリングを遠ざける統一表現に再構成する。
論文 参考訳（メタデータ） (2026-05-09T15:30:52Z) - Confidence-Aware Alignment Makes Reasoning LLMs More Reliable [65.44962502963378]
CASPOは、トークンレベルの信頼度とステップワイドな論理的正しさを、個別の報酬モデルをトレーニングせずに整合させるフレームワークである。
推論中、信頼を意識した思考(CaT)を提案し、不確実な推論枝を無視可能なO(V)レイテンシで動的に生成する。
10のベンチマークと複数のモデルファミリでの実験では、CASPOは推論の信頼性と推論効率を一貫して改善している。
論文 参考訳（メタデータ） (2026-05-08T07:08:25Z) - Draft-and-Prune: Improving the Reliability of Auto-formalization for Logical Reasoning [5.119925615308174]
自動形式化(AF)は自然言語推論問題を解法実行プログラムに翻訳する。
D&P(Draft-and-Prune, Draft-and-Prune, Draft-and-Prune, D&P)は、AFに基づく論理的推論を多様性と検証によって改善する推論時フレームワークである。
D&Pは追加の監督なしにAFベースの推論を大幅に強化する。
論文 参考訳（メタデータ） (2026-03-18T00:35:14Z) - Certainty-Validity: A Diagnostic Framework for Discrete Commitment Systems [0.0]
「マシーン学習評価尺度」は、全てのエラーが等価な離散的なコミットメントシステムであると仮定する。
信頼不正確」な振る舞いは、モデルが曖昧なデータの中で構造を幻覚させる場所である。
推論システムのための「Good Training」は、精度ではなく、Certainty-Validity Scoreの最大化によって定義されなければならない。
論文 参考訳（メタデータ） (2026-02-10T21:53:02Z) - Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
大きな言語モデル(LLM)は目覚ましい能力を示すが、その次は論理的不整合と報奨ハックを生み出す。
本稿では,自然言語生成プロセスと形式的記号的検証を動的にインターリーブする形式論理検証誘導フレームワークを提案する。
我々はこのフレームワークを,形式論理検証誘導制御による微調整とポリシー最適化の相乗効果を生かした,新しい2段階のトレーニングパイプラインを通じて運用する。
論文 参考訳（メタデータ） (2026-01-30T07:01:25Z) - 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) - Improving AEBS Validation Through Objective Intervention Classification Leveraging the Prediction Divergence Principle [0.0]
本研究は,予測分散原理(PDP)を利用した規則に基づく分類手法を提案する。
この手法を人間のラベル付けと組み合わせることで、分類の透明性と一貫性が向上し、全体的な検証プロセスが改善されることが示唆された。
論文 参考訳（メタデータ） (2025-07-10T15:55:05Z) - STL: Surprisingly Tricky Logic (for System Validation) [0.04301276597844757]
検証正当性を決定する上では,仕様書の真正性,形式的手法に精通した被験者の親密性,教育水準が重要な要因であることが判明した。
参加者は肯定バイアスを示し、有効仕様の精度は大幅に向上したが、無効仕様の精度は著しく低下した。
論文 参考訳（メタデータ） (2023-05-26T21:01:26Z) - Logical Satisfiability of Counterfactuals for Faithful Explanations in
NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。
これは、説明に表される論理述語に基づいて、反実仮説を生成する。
そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文 参考訳（メタデータ） (2022-05-25T03:40:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。