論文の概要: Lemmanaid: Neuro-Symbolic Lemma Conjecturing

• arxiv url: http://arxiv.org/abs/2504.04942v1
• Date: Mon, 07 Apr 2025 11:30:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-08 14:10:01.042072
• Title: Lemmanaid: Neuro-Symbolic Lemma Conjecturing
• Title（参考訳）: Lemmanaid:ニューロシンボリック・レムマ・コンジェクション
• Authors: Yousef Alhessi, Sólrún Halla Einarsdóttir, George Granberry, Emily First, Moa Johansson, Sorin Lerner, Nicholas Smallbone,
• Abstract要約: 本稿では, 実用的神経シンボル型レムマ注入ツールLemmanaidについて紹介する。 レムマの形状を記述したレムマテンプレートを生成するためにLLMをトレーニングし、詳細を記入するためにシンボリックメソッドを使用します。 我々は,レマノイドを完全補題文を生成するために訓練されたLLMと,それ以前の完全記号推論法と比較した。
• 参考スコア（独自算出の注目度）: 4.583367875081881
• License:
• Abstract: Automatically conjecturing useful, interesting and novel lemmas would greatly improve automated reasoning tools and lower the bar for formalizing mathematics in proof assistants. It is however a very challenging task for both neural and symbolic approaches. We present the first steps towards a practical neuro-symbolic lemma conjecturing tool, Lemmanaid, that combines Large Language Models (LLMs) and symbolic methods, and evaluate it on proof libraries for the Isabelle proof assistant. We train an LLM to generate lemma templates that describe the shape of a lemma, and use symbolic methods to fill in the details. We compare Lemmanaid against an LLM trained to generate complete lemma statements as well as previous fully symbolic conjecturing methods. Our results indicate that neural and symbolic techniques are complementary. By leveraging the best of both symbolic and neural methods we can generate useful lemmas for a wide range of input domains, facilitating computer-assisted theory development and formalization.
• Abstract（参考訳）: 有用で興味深い新しい補題を自動推論することで、自動推論ツールを大幅に改善し、証明アシスタントにおける数学の形式化の限界を低くすることができる。 しかし、これはニューラルアプローチとシンボリックアプローチの両方にとって非常に難しいタスクである。 本稿では,Large Language Models (LLMs) とシンボリックメソッドを組み合わせた実用的ニューロシンボリック・レムマ・コンジェクションツールであるLemmanaidについて,Isabelle証明アシスタントの証明ライブラリ上で評価する。 レムマの形状を記述したレムマテンプレートを生成するためにLLMをトレーニングし、詳細を記入するためにシンボリックメソッドを使用します。 我々は,レマノイドを完全補題文を生成するために訓練されたLLMと,それ以前の完全記号推論法と比較した。 以上の結果から,ニューラルネットワークとシンボル技術は相補的であることが示唆された。 記号的手法と神経的手法の両方の長所を活用することで、幅広い入力領域に対して有用な補題を生成することができ、コンピュータ支援理論の開発と形式化が容易になる。

関連論文リスト

• Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning [27.562284768743694]
  大規模言語モデル(LLM)は、証明システム内で証明ステップを生成することによって、数学的定理を正式に証明することができる。 本稿では,LLMが学習した数学的直観と,記号的手法によって符号化された領域固有の洞察を相乗化する,ニューロシンボリック・戦術生成器を提案する。 複数の数学コンペティションから161の挑戦的不等式を評価する。
  論文  参考訳（メタデータ） (2025-02-19T15:54:21Z)
• Advanced Weakly-Supervised Formula Exploration for Neuro-Symbolic Mathematical Reasoning [18.937801725778538]
  本稿では,ニューロシンボリック推論システムにおいて,問題入力や最終出力から弱い監督下で中間ラベルを探索する手法を提案する。 数学データセットに関する実験では,複数の側面から提案した提案の有効性を実証した。
  論文  参考訳（メタデータ） (2025-02-02T02:34:36Z)
• Neuro-Symbolic Data Generation for Math Reasoning [47.00099724151703]
  高品質な教師付き数学的データセットを自動生成する手法を開発した。 本手法は,既存の数学問題を慎重に変更し,新たに生成した問題の多様性と妥当性を両立させる。 実験により,提案手法により生成したデータの品質を実証し,LLaMA-2 と Mistral が最先端のデータを上回ることを示した。
  論文  参考訳（メタデータ） (2024-12-06T08:49:49Z)
• Converging Paradigms: The Synergy of Symbolic and Connectionist AI in LLM-Empowered Autonomous Agents [55.63497537202751]
  コネクショニストと象徴的人工知能(AI)の収束を探求する記事 従来、コネクショナリストAIはニューラルネットワークにフォーカスし、シンボリックAIはシンボリック表現とロジックを強調していた。 大型言語モデル(LLM)の最近の進歩は、人間の言語をシンボルとして扱う際のコネクショナリストアーキテクチャの可能性を強調している。
  論文  参考訳（メタデータ） (2024-07-11T14:00:53Z)
• A Recursive Bateson-Inspired Model for the Generation of Semantic Formal Concepts from Spatial Sensory Data [77.34726150561087]
  本稿では,複雑な感覚データから階層構造を生成するための記号のみの手法を提案する。 このアプローチは、概念や概念の創始の鍵としてのバテソンの差異の概念に基づいている。 このモデルは、トレーニングなしでかなりリッチだが人間に読まれる概念表現を生成することができる。
  論文  参考訳（メタデータ） (2023-07-16T15:59:13Z)
• Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition [0.0]
  本稿では、このような機械学習モデルに説明可能なAI(XAI)技術を用いることで、記号計算に新たな洞察を与えることができるかどうかを考察する。 本稿では、円筒代数分解の変数順序付けをMLを用いて選択するケーススタディを提案する。
  論文  参考訳（メタデータ） (2023-04-24T15:05:04Z)
• Neuro-Symbolic Learning of Answer Set Programs from Raw Data [54.56905063752427]
  Neuro-Symbolic AIは、シンボリックテクニックの解釈可能性と、生データから学ぶ深層学習の能力を組み合わせることを目的としている。 本稿では,ニューラルネットワークを用いて生データから潜在概念を抽出するNSIL(Neuro-Symbolic Inductive Learner)を提案する。 NSILは表現力のある知識を学習し、計算的に複雑な問題を解き、精度とデータ効率の観点から最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2022-05-25T12:41:59Z)
• Closed Loop Neural-Symbolic Learning via Integrating Neural Perception, Grammar Parsing, and Symbolic Reasoning [134.77207192945053]
  従来の手法は強化学習アプローチを用いてニューラルシンボリックモデルを学ぶ。 我々は,脳神経知覚と記号的推論を橋渡しする前に,textbfgrammarモデルをテキストシンボリックとして導入する。 本稿では,トップダウンのヒューマンライクな学習手順を模倣して誤りを伝播する新しいtextbfback-searchアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-06-11T17:42:49Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  本稿では,リアプノフ関数の自動合成法を提案する。 我々は,数値学習者と記号検証器が相互作用して,確実に正しいリアプノフニューラルネットワークを構築する,反例誘導方式を採用する。 提案手法は,Lyapunov関数を他の手法よりも高速かつ広い空間領域で合成する。
  論文  参考訳（メタデータ） (2020-03-19T17:21:02Z)

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

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