論文の概要: Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1

• arxiv url: http://arxiv.org/abs/2604.17229v1
• Date: Sun, 19 Apr 2026 03:27:16 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-21 21:52:52.405143
• Title: Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1
• Title（参考訳）: Yanasse氏:Deep Visionのアナロジーから新たな証明を見つける(パート1)
• Authors: Alexandre Linhares,
• Abstract要約: システムはマドリブの27の上位領域の戦術的利用分布を抽出する。 zスコアを計算して、ソースエリアで多用されるが、ターゲットエリアで稀または欠落している戦術を特定する。 これは、GPUアクセラレーションされたNPハードアナログを用いて、ソースとターゲットの証明状態と一致する。
• 参考スコア（独自算出の注目度）: 51.56484100374058
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Project Yanasse presents a method for discovering new proofs of theorems in one area of mathematics by transferring proof strategy patterns (e.g., Lean 4 tactic invocation patterns) from a structurally distant area. The system extracts tactic usage distributions across 27 top-level areas of Mathlib (217,133 proof states), computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area, matches source and target proof states via GPU-accelerated NP-hard analogy (running on a MacBook Air via Apple's MPS backend), and then asks an AI reasoning agent to semantically adapt--not symbol-substitute--the source tactics invocation pattern to the target theorem. In this first part of the study, the method is applied to the pair Probability -> Representation Theory, producing 4 Lean-verified new proofs out of 10 attempts (40%). The proofs compile with zero sorry declarations. The key finding is that tactic schemas decompose into a head (domain-gated, rarely transfers) and a modifier (domain-general, often transfers): filter upwards's head fails in representation theory (no Filter structure), but its [LIST] with ω modifier transfers cleanly as ext1 + simp [LIST] + rfl. Crucially, the underlying matching engine--deep vision lib.py--is entirely domain independent: the same optimization code for an NP-hard matching that matches chess positions by analogy matches Lean proof states by analogy, without knowing which domain it is processing. Only a relation extractor is domain-specific.
• Abstract（参考訳）: Project Yanasseは、構造的に離れた領域から証明戦略パターン(例:Lean 4 戦術的実行パターン)を転送することで、数学の一分野における新しい定理の証明を発見する方法を提示している。 このシステムは、27のMathlib(217,133の証明状態)のトップレベル領域にわたる戦術的利用分布を抽出し、zスコアを計算して、ソース領域で多用されるが、ターゲット領域で希少または欠落した戦術を特定し、ソースとターゲットの証明状態をGPUアクセラレーションされたNPハードアナログ(AppleのMPSバックエンドを介してMacBook Air上で実行される)でマッチングし、AI推論エージェントに、ターゲット定理に意味的に適応する--not symbol-substitute--ソースの戦術実行パターンを求める。 この研究の第1部では、この手法をペアの確率 ->表現理論に適用し、10の試行(40%)のうち4つのリーン検証された新しい証明を生成します。 証明は、申し訳ない宣言をゼロでコンパイルする。 鍵となる発見は、戦術スキーマがヘッド(ドメインゲート、まれに転送される)と修飾子(ドメイン一般、しばしば転送される)に分解されることである: 上向きの頭部は表現理論(フィルタ構造はない)で失敗するが、ω修飾子の[LIST]はext1 + simp [LIST] + rflとしてクリーンに転送される。 重要なことに、深いビジョン lib.py- は、完全にドメインに依存している: NP-hardマッチングのための同じ最適化コードで、どのドメインが処理しているかを知らずに、アナログによってチェスの位置にマッチする。 関係抽出器のみがドメイン固有である。

関連論文リスト

• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Gödel's Poetry [0.0]
  本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
  論文  参考訳（メタデータ） (2025-12-16T10:00:01Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
  Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。 GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
  論文  参考訳（メタデータ） (2025-07-25T17:29:19Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Enhancing Neural Theorem Proving through Data Augmentation and Dynamic Sampling Method [1.8130068086063336]
  本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。 単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。 ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2023-12-20T09:55:21Z)
• 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)

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

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