論文の概要: Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism

• arxiv url: http://arxiv.org/abs/2605.12524v1
• Date: Tue, 07 Apr 2026 01:19:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-25 12:34:33.786303
• Title: Stress-Testing the Reasoning Competence of LLMs With Proofs Under Minimal Formalism
• Title（参考訳）: 最小形式主義下での証明によるLLMの推論能力のストレス試験
• Authors: Konstantine Arkoudas, Serafim Batzoglou,
• Abstract要約: 本稿では,機械チェック可能な証明を通じて推論を評価するベンチマークスイートProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小の形式表記、特に短いプロンプトに適合するコンパクトな自然言語推論言語であるNDLで表現される。
• 参考スコア（独自算出の注目度）: 2.215655942741476
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce ProofGrid, a benchmark suite for evaluating LLM reasoning through machine-checkable proofs rather than final answers alone. ProofGrid contains 15 tasks spanning proof writing, proof checking, proof masking, and proof gap-filling. Tasks are expressed in minimal formal notation, especially NDL, a compact natural-deduction language that fits in short prompts and supports precise, auditable verification. This yields mechanical, reproducible, and fine-grained evaluation rather than judgments by humans or LLMs. ProofGrid covers a calibrated difficulty spectrum, from foundational reasoning tests to structurally rich challenge tasks that no current model solves, while minimizing reliance on domain knowledge, solver delegation, and long-context artifacts. We also develop a comparative framework for reasoning benchmarks and use it to situate ProofGrid relative to existing work in terms of representation, verification guarantees, and reasoning depth. Methodologically, we introduce an instrumented proof-checking pipeline that tolerates minor surface deviations while locating the first substantive reasoning failure, improving measurement resolution and separating proof planning from low-level execution noise. Using this pipeline, we evaluate a broad range of open and proprietary models. Results show rapid progress but substantial remaining limits: frontier models perform well on several foundational tasks, yet difficult tasks, especially those requiring global combinatorial reasoning or low-level proof synthesis, remain far from solved. We also identify epistemic instability, where models generate flawed proofs yet correctly reject those local inferences in isolation, and formalize this with an Epistemic Stability Index. Finally, we complement accuracy with 2PL IRT analyses, Wright maps, and a normalized task-discrimination measure based on Fisher information.
• Abstract（参考訳）: 本稿では,最終回答のみでなく,機械チェック可能な証明を通じてLLM推論を評価するベンチマークスイートであるProofGridを紹介する。 ProofGridには、証明記述、証明チェック、証明マスキング、証明ギャップ埋めを含む15のタスクが含まれている。 タスクは最小限の形式表記で表現され、特にNDLは、短いプロンプトに適合し、正確で監査可能な検証をサポートするコンパクトな自然言語推論言語である。 これにより、人間やLLMによる判断よりも、機械的、再現性があり、きめ細かい評価が得られる。 ProofGridは、基本的な推論テストから、現在のモデルが解決しない構造的にリッチな課題タスクまで、ドメイン知識やソルバデリゲート、長いコンテキストアーティファクトへの依存を最小限に抑えながら、キャリブレーションされた難易度の範囲をカバーしている。 また、ベンチマークを推論するための比較フレームワークを開発し、既存の作業に対して、表現、検証保証、推論深度の観点からProofGridを定めています。 提案手法では,測定精度を向上し,低レベルの実行ノイズから検証計画を切り離すとともに,第1の実体的推論障害の特定を図りながら,表面の偏差を許容する計器的検定パイプラインを導入する。 このパイプラインを使用して、幅広いオープンモデルとプロプライエタリモデルを評価します。 いくつかの基礎的なタスクにおいてフロンティアモデルはうまく機能するが、特に大域的な組合せ的推論や低レベルな証明合成を必要とするタスクは、解決には程遠いままである。 また、モデルが欠陥のある証明を生成するが、それらの局所的推論を分離して正しく拒絶し、それをエピステミック安定指数で定式化するという、疫学不安定性も確認する。 最後に、2PL IRT解析、ライトマップ、およびフィッシャー情報に基づく正規化タスク識別尺度を用いて精度を補完する。

関連論文リスト

• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  大規模言語モデル(LLM)とエージェントは有望な進歩を示しているが、その真の能力と失敗モードは未だ不明である。 CプログラムのためのLCMおよびエージェントベースの形式仕様生成に関する、最初の体系的および汚染に配慮した研究を提案する。
  論文  参考訳（メタデータ） (2026-05-02T11:31:33Z)
• ProofSketcher: Hybrid LLM + Lightweight Proof Checker for Reliable Math/Logic Reasoning [0.0]
  大規模言語モデル(LLMs)は、数学的および論理的分野における説得的議論を生み出す可能性がある。 LeanとCoqは、構文的および意味的ステートメントがプログラム内のすべての構文的および意味的ステップをパスできるステートメントのみを受け入れることを保証することで、厳格な信頼性を持つ。 本稿では,LLMがコンパクトDSLの型付き証明スケッチを生成し,軽量な信頼できるカーネルがスケッチを明示的な証明義務に拡張するハイブリッドパイプラインを提案する。
  論文  参考訳（メタデータ） (2026-04-07T19:33:54Z)
• PROMISE: Proof Automation as Structural Imitation of Human Reasoning [15.113069562646302]
  ProMISEは,証明状態遷移に対するステートフルな探索として,証明生成を再構成する構造認識フレームワークである。 複数のLLMバックエンドにまたがるSEL4ベンチマークのPROMISEを評価し,SeleneやRangoといった先行システムと比較した。
  論文  参考訳（メタデータ） (2026-04-07T03:49:12Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• A Fano-Style Accuracy Upper Bound for LLM Single-Pass Reasoning in Multi-Hop QA [65.38186593873313]
  MHQA(Multi-Hop Question Answering)は、ノイズ下でのシーケンシャルな推論を通じて、分散した相互依存的な証拠を統合する必要がある。 我々はMHQAのための概念実証マルチコールフレームワークをInfoQAで紹介する。 我々は、理論とフレームワークを検証するために、厳密で騒音に富んだベンチマークを構築した。
  論文  参考訳（メタデータ） (2025-09-25T14:11:57Z)
• What's in a Proof? Analyzing Expert Proof-Writing Processes in F* and Verus [2.8003002159083237]
  我々は,2つの言語で作業する8人の専門家から,詳細なソースコードテレメトリの収集と解析を行うユーザスタディを実施している。 その結果、専門家が証明開発プロセスで遭遇した重要な課題や証明についてどのように考えるかについて興味深い傾向とパターンが明らかになった。 我々はこれらの知見を,AI証明アシスタントのための具体的な設計指針に翻訳する。
  論文  参考訳（メタデータ） (2025-08-01T22:16:30Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)

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

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