LLMは形式化で「ゲーム」するのか？論理推論における忠実性（faithfulness）を評価する

要旨: 正式検証は証明の妥当性は保証しますが、形式化の忠実性までは保証しません。自然言語による論理推論では、モデルがライブラリの制約なしにゼロから公理体系を構築します。このとき、「妥当な証明」と「忠実な翻訳」の間にあるギャップは、とりわけ深刻になります。本研究では、フロンティアモデルがLean 4 の証明生成の際にこのギャップを利用しているかどうかを調査します。この振る舞いを、我々は形式化ゲーム（formalization gaming）と呼びます。
我々は、303件の一階論理問題（FOLIOから203件、Multi-LogiEvalから100件）に対してGPT-5とDeepSeek-R1を評価し、形式化と証明を分離する二段階パイプラインと、統一的生成を比較します。コンパイル率が87-99%であるにもかかわらず、統一的生成において体系的なゲームが行われているという証拠は見つかりません。モデルは、たとえそれを促すように設計されたプロンプトのもとでも、無理に証明を成立させようとするより失敗の報告を選好します。とはいえ、我々の検出をすり抜ける不忠実性が依然として起こり得ます。二段階パイプラインは、不忠実性の異なる2つのモードを明らかにします。GPT-5は証明生成中に公理をでっち上げており、段階間比較によって検出可能なリアクティブなフォールバックです。一方、DeepSeek-R1は形式化の際に前提を誤訳しており、検出を完全に回避する、内部的には整合的な出力を生成します。これらの結果は、高いコンパイル率や精度が忠実な推論と同一視されるべきではないことを示しています。コードとデータは https://github.com/koreankiwi99/formalization-gaming で利用可能です。