論文の概要: Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
- arxiv url: http://arxiv.org/abs/2606.28572v1
- Date: Fri, 26 Jun 2026 19:57:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-30 18:07:15.611488
- Title: Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings
- Title（参考訳）: ニューラル・プローフ・エンベディングにおける選択公理の幾何学的計測
- Abstract要約: 我々はLean 4のカーネルレベルの公理依存性の追跡を用いて、選択の公理が証明空間に測定可能な幾何学的相関を持つことを示す。
このシグネチャは長さ,ファイル,著者,トピックコントロールに留まり,正規化証明源で訓練されたフルソースエンコーダの下で複製されることを示す。
- 参考スコア（独自算出の注目度）: 0.2538209532048866
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space that obeys a one-parameter mixture law and has operational consequences for neural theorem provers. To do this, we partition $471{,}260$ declarations of Mathlib by transitive dependence on the axiom of choice and represent a filtered population of $42{,}355$ traced theorems by their sequences of tactic invocations. We use the constructive proofs in this dataset to train a self-supervised proof encoder and show that when using it to measure classical proofs, three complementary measurements (anomaly score, reconstruction loss, and density-superlevel containment) exhibit a common decline with the proof's distance from the axiom in the dependency graph, from sharp separation at the shallow boundary (AUC $0.847$ at distance $2$) to indistinguishability at distance~$9{+}$. Robustness controls show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source. Operationally, we show that on an evaluation sample of $251$ Mathlib theorems, Lean's \texttt{aesop} tactic solves constructive theorems at $13\times$ the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to $5\times$. The geometric anomaly score predicts \texttt{aesop} failure beyond proof length, providing an operational link between the geometric signature and prover performance.
- Abstract（参考訳）: 選択の公理は数学の基礎を1世紀以上にわたって分けてきたが、古典的証明と建設的証明の区別は哲学的かつ方法論的なもののままである。
我々はLean 4の公理依存性のカーネルレベル追跡を用いて、選択公理が1パラメータ混合法則に従う証明空間に測定可能な幾何学的相関を持つことを示す。
これを行うために、選択公理への推移的依存により、マドリブの471{,}260$宣言を分割し、その戦術的実行の列によって、42{,}355$トレースされた定理のフィルタされた集団を表す。
このデータセットにおける構成的証明を用いて、自己教師付き証明エンコーダを訓練し、古典的な証明を測定する際に、3つの相補的測定(異常スコア、再構成損失、密度-超レベル包摂)が、依存グラフの公理からの距離から、浅い境界での鋭い分離 (AUC $0.847$ at distance $2$) から、距離~9{+}$ の区別不可能まで、共通の減少を示すことを示す。
ロバストネスコントロールは、シグネチャが長さ、ファイル、著者、トピックコントロールに残り、正規化された証明ソースでトレーニングされたフルソースエンコーダの下で複製されることを示している。
操作的には、251$Mathlib定理の評価サンプルにおいて、Lean's \texttt{aesop} 戦術が構成定理を13\times$で解き、ReProver 戦術発生器を用いたニューラル誘導ハイブリッドがギャップを5\times$に圧縮することを示した。
幾何学的異常スコアは、証明長を超えて \texttt{aesop} の故障を予測し、幾何学的シグネチャと証明器のパフォーマンスの操作的リンクを提供する。
関連論文リスト
- Autonomous disproofs of the sum-product conjecture over $\mathbb R$ with GPT-5.5 Pro [5.634825161148485]
GPT-5.5 Pro 上に構築した問題に依存しない3段プロンプトパイプラインを提案する。
エージェントが自律的に生成した正しい証明は、和積予想が8つの独立トライアルのうち7つのアーケードの$mathbb R$に対して偽であることを示している。
論文 参考訳（メタデータ） (2026-07-09T23:28:37Z) - An Information-Geometric Justification for Composite Coherence in Event-Based Narrative Extraction [0.27074235008521247]
ここで$A$は文書埋め込みと$T=1-d_mathrmJS$の角的類似性である。
4つのコーパス、3つの埋め込みファミリー、3つのトピックモデルはフレームワークと一致している。
論文 参考訳（メタデータ） (2026-06-28T00:05:15Z) - ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。
ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。
実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文 参考訳（メタデータ） (2026-06-09T06:50:15Z) - LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
信頼性の高い研究レベルのLean AutoformalizationのためのマルチエージェントハーネスであるLeanMarathonを紹介します。
4つのコントラクトスコープエージェントがこの青写真を構築し、監査し、証明し、修復する。
我々は4つのErds問題にまたがる最近の2つの研究論文でLeanMarathonを評価した。
論文 参考訳（メタデータ） (2026-06-03T20:09:39Z) - Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
システムはマドリブの27の上位領域の戦術的利用分布を抽出する。
zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。
これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
論文 参考訳（メタデータ） (2026-04-19T03:27:16Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving [36.20164235042574]
本研究では,レムマ型全耐久推論モデルである textbfSeed-Prover を提案する。
IMOレベルの競合問題を解決するために、深い推論と広い推論の両方を可能にする3つのテストタイム推論戦略を設計する。
シード・プロバーは、過去のIMO問題の78.1%ドルを証明し、ミニF2Fを飽和させ、パットナムベンチで50%以上を達成し、それまでの最先端よりも大きな差を付けた。
論文 参考訳（メタデータ） (2025-07-31T17:00:30Z) - Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification [56.218970738892764]
Chain-of-Thoughtプロンプトは、大規模言語モデル(LLM)から推論能力を引き出すデファクトメソッドとなっている。
検出が極めて難しいCoTの幻覚を緩和するために、現在の方法は不透明なボックスとして機能し、彼らの判断に対する確認可能な証拠を提供しておらず、おそらくその効果を制限する。
任意のスコアを割り当てるのではなく、各推論ステップで形式数学言語Lean 4で数学的主張を明確にし、幻覚を識別するための公式な証明を提供しようとしている。
論文 参考訳（メタデータ） (2025-06-05T03:16:08Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。