論文の概要: Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

• arxiv url: http://arxiv.org/abs/2605.00677v1
• Date: Fri, 01 May 2026 14:03:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-04 17:43:28.979465
• Title: Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game
• Title（参考訳）: 難解自然数ゲームによるLLMプロデューサのアーキテクチャ推論能力の評価
• Authors: Lixing Li,
• Abstract要約: 本稿では,将来の自動定理発見AIに必要な機能としてアーキテクチャ推論を取り上げる。 リーン4のNatural Number Gameで識別子をリネームすることで、ゼロ知識でクローズドな環境を作りました。 我々は最先端のモデルを評価し、難読化が推論時間を増加させる普遍的な遅延税を求める。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• Abstract: While Large Language Models have achieved notable success on formal mathematics benchmarks such as MiniF2F, it remains unclear whether these results stem from genuine logical reasoning or semantic pattern matching against pre-training data. This paper identifies Architectural Reasoning: the ability to synthesize formal proofs using exclusively local axioms and definitions within an alien math domain, as the necessary ability for future automated theorem discovery AI. We use the Obfuscated Natural Number Game, a benchmark to evaluate Architectural Reasoning. By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment. We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time. The results also reveal a divergence in robustness: while general models (Claude-Sonnet-4.5, GPT-4o) suffer performance degradation, reasoning models (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) maintain the same accuracy despite the absence of semantic cues. These findings provide a quantitative metric for assessing the true capacity for mathematical reasoning.
• Abstract（参考訳）: 大規模言語モデルはMiniF2Fのような形式的な数学のベンチマークで顕著に成功しているが、これらの結果は真の論理的推論や事前学習データとのセマンティックパターンマッチングに由来するかどうかは不明だ。 本稿では,局所的な公理と定義を異種数学領域内でのみ用いる形式的証明を,将来の自動定理発見AIに必要な能力として,アーキテクチャ的推論(Architectural Reasoning)として定義する。 我々は、アーキテクチャ推論を評価するベンチマークであるObfuscated Natural Number Gameを使用している。 リーン4のNatural Number Gameで識別子をリネームすることで、ゼロ知識でクローズドな環境を作りました。 我々は最先端のモデルを評価し、難読化が推論時間を増加させる普遍的な遅延税を求める。 一般的なモデル(Claude-Sonnet-4.5, GPT-4o)は性能劣化に悩まされているが、推論モデル(DeepSeek-R1, GPT-5, DeepSeek-Prover-V2)は意味的手がかりがないにもかかわらず同じ精度を維持している。 これらの結果は、数学的推論の真の能力を評価するための定量的な指標となる。

関連論文リスト

• Benchmarking Testing in Automated Theorem Proving [39.65133452374143]
  T は形式定理の意味的正しさを評価する枠組みである。 5つの実世界のLean 4リポジトリからベンチマークを構築します。 実験により、最先端のモデルでは高いコンパイル成功を達成できるが、セマンティック・メトリックでは著しく性能が低下することが示された。
  論文  参考訳（メタデータ） (2026-04-26T13:24:20Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Pramana: Fine-Tuning Large Language Models for Epistemic Reasoning through Navya-Nyaya [0.0]
  大規模な言語モデルは、流動的なテキストを生成するが、体系的な推論に苦労する。 Appleの研究者が無関係なコンテキストを追加すると、LLMのパフォーマンスは65%低下した。 トレーサブルエビデンスにおけるこの主張を根拠にできないことは、正当化を必要とする領域におけるAIの信頼性を制限します。 2500年前のインドの推論フレームワークであるPramanaの微調整について紹介する。
  論文  参考訳（メタデータ） (2026-02-14T23:45:29Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Do LLMs Overthink Basic Math Reasoning? Benchmarking the Accuracy-Efficiency Tradeoff in Language Models [6.312798900093575]
  大規模言語モデル (LLM) は複雑な数学的ベンチマークでは優れた性能を得るが、基本的な数学的推論では失敗することがある。 本稿では,正確さと過度に考えることの基本的なトレードオフに焦点を当てる。 本研究は,総合モデル評価のための高精度とトークン効率を組み合わせた調和平均計量であるOverthinking Scoreを紹介する。
  論文  参考訳（メタデータ） (2025-07-05T12:31:17Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)

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

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