論文の概要: Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
- arxiv url: http://arxiv.org/abs/2604.19459v1
- Date: Tue, 21 Apr 2026 13:37:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-22 22:41:49.788863
- Title: Do LLMs Game Formalization? Evaluating Faithfulness in Logical Reasoning
- Title（参考訳）: LLMのゲーム形式化は可能か? : 論理推論における忠実度の評価
- Authors: Kyuhee Kim, Auguste Poiroux, Antoine Bosselut,
- Abstract要約: 形式検証は証明の正当性を保証するが、形式化の忠実性は保証しない。
私たちは、Lean 4の証明を生成する際に、フロンティアモデルがこのギャップを利用するかどうかを調査します。
統一世代における体系的なゲーミングの証拠は見つからない。
- 参考スコア（独自算出の注目度）: 20.336209492846752
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification guarantees proof validity but not formalization faithfulness. For natural-language logical reasoning, where models construct axiom systems from scratch without library constraints, this gap between valid proofs and faithful translations is especially acute. We investigate whether frontier models exploit this gap when generating Lean 4 proofs, a behavior we term formalization gaming. We evaluate GPT-5 and DeepSeek-R1 on 303 first-order logic problems (203 from FOLIO, 100 from Multi-LogiEval), comparing unified generation against a two-stage pipeline that separates formalization from proving. Despite compilation rates of 87-99%, we find no evidence of systematic gaming in unified generation: models prefer reporting failure over forcing proofs, even under prompting designed to encourage it. However, unfaithfulness that evades our detection signals may still occur. The two-stage pipeline reveals two distinct modes of unfaithfulness: GPT-5 fabricates axioms during proof generation, a reactive fallback detectable via cross-stage comparison, while DeepSeek-R1 mistranslates premises during formalization, producing internally consistent outputs that evade detection entirely. These findings show that high compilation rates or accuracies should not be equated with faithful reasoning. Code and data are available at https://github.com/koreankiwi99/formalization-gaming.
- Abstract（参考訳）: 形式検証は証明の正当性を保証するが、形式化の忠実性は保証しない。
モデルがライブラリの制約なしにゼロから公理系を構築する自然言語論理的推論では、有効な証明と忠実な翻訳の間のギャップは特に深刻である。
フォーマライゼーションゲームという振る舞いであるLean 4の証明を生成する際に、フロンティアモデルがこのギャップを利用するかどうかを調査する。
GPT-5とDeepSeek-R1を303の1次論理問題(FOLIOから203、Multi-LogiEvalから100)で評価し、形式化と証明を分離した2段階のパイプラインと比較した。
87～99%のコンパイル率にもかかわらず、統一世代における体系的なゲーミングの証拠は見つからない。
しかし、検出信号から逃れる不誠実さはまだ発生しているかもしれない。
GPT-5は証明生成時に公理を生成、反応性のフォールバックはクロスステージ比較により検出され、DeepSeek-R1は形式化時に前提を誤訳し、内部的に一貫した出力を生成し、検出を完全に回避する。
以上の結果から,高いコンパイル率や精度を忠実な推論と同一視するべきではないことが示唆された。
コードとデータはhttps://github.com/koreankiwi99/formalization-gaming.comで公開されている。
関連論文リスト
- Structured Abductive-Deductive-Inductive Reasoning for LLMs via Algebraic Invariants [0.0]
大規模言語モデルは、構造化論理的推論において体系的な制限を示す。
LLM支援推論のための明示的なプロトコルとして、パースの三部構造推論を運用するシンボリックな足場を提案する。
論文 参考訳（メタデータ） (2026-04-17T05:59:16Z) - CausalT5K: Diagnosing and Informing Refusal for Trustworthy Causal Reasoning of Skepticism, Sycophancy, Detection-Correction, and Rung Collapse [1.4608214000864057]
CausalT5Kは10ドメインにわたる5000以上のケースの診断ベンチマークである。
合成ベンチマークとは異なり、CausalT5Kはリアルな物語に因果トラップを埋め込んでいる。
予備的な実験では、静的監査ポリシーが普遍的に失敗する4段階のコントロールランドスケープが示される。
論文 参考訳（メタデータ） (2026-02-09T17:36:56Z) - Translating Informal Proofs into Formal Proofs Using a Chain of States [20.0011959667642]
本稿では,自然言語で表現された非公式な数学的証明を,制約付き計算予算の下でLean4の形式的証明に変換する問題に対処する。
まず、中間形式的証明状態の列である状態の連鎖(CoS)を、非公式引数の論理構造に沿って抽出する。
次に、CoS内の隣接状態間の遷移戦略を生成し、完全な形式的証明を構築する。
論文 参考訳（メタデータ） (2025-12-11T06:08:34Z) - ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings [9.764411884491052]
ProofBridgeは、NLの定理と証明を自動的にリーン4に翻訳するフレームワークです。
中心となるのは、NL と FL (NL-FL) の定理対を共有意味空間で整列する合同埋め込みモデルである。
我々の訓練は、NL-FL 対が意味論的に同値である場合に限り、この空間において NL-FL の定理が密接にマッピングされることを保証する。
論文 参考訳（メタデータ） (2025-10-17T14:20:50Z) - Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。
まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。
次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。
最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
論文 参考訳（メタデータ） (2025-02-11T15:27:35Z) - Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
LLMの複雑な推論には2行のアプローチが採用されている。
1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。
他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。
具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
論文 参考訳（メタデータ） (2023-11-16T11:26:21Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - ProoFVer: Natural Logic Theorem Proving for Fact Verification [24.61301908217728]
本稿では,自然論理を用いた事実検証システムProoFVerを提案する。
証明の生成により、ProoFVerは説明可能なシステムになる。
証明により,人間がProoFVerの判断を正しくシミュレートできることが判明した。
論文 参考訳（メタデータ） (2021-08-25T17:23:04Z) - AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
実世界の情報ニーズから10kクレームを抽出したファクトチェックデータセットであるAmbiFCを提示する。
アンビFCの証拠に対する主張を比較する際に,曖昧さから生じる不一致を分析した。
我々は,このあいまいさをソフトラベルで予測するモデルを開発した。
論文 参考訳（メタデータ） (2021-04-01T17:40:08Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。