論文の概要: Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation

• arxiv url: http://arxiv.org/abs/2508.00017v2
• Date: Fri, 26 Sep 2025 11:33:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-29 18:47:02.667338
• Title: Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation
• Title（参考訳）: 生成論理:決定論的推論と知識生成のための新しいコンピュータアーキテクチャ
• Authors: Nikolai Sergeev,
• Abstract要約: Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。 GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present Generative Logic (GL), a deterministic architecture that starts from user-supplied axiomatic definitions (and, optionally, a list of simple facts for counterexample (CE) construction), written in a minimalist Mathematical Programming Language (MPL), and systematically explores their deductive neighborhood. Definitions are compiled into a distributed grid of simple Logic Blocks (LBs) that exchange messages; whenever the premises of an inference rule unify, a new fact is emitted with full provenance to its sources, yielding replayable, auditable proof graphs. A prototype software implementation instantiates the workflow on first-order Peano arithmetic. Starting only from the Peano axioms, GL enumerates conjectures, applies normalization, type, and CE filter, and automatically reconstructs machine-checkable proofs of foundational arithmetic laws, including associativity and commutativity of addition, associativity and commutativity of multiplication, and distributivity. On commodity hardware, the prover phase requires approximately 7 seconds; a complete run finishes in about 5 minutes. Generated proofs export to navigable HTML so that every inference step can be inspected independently. We outline a hardware-software co-design path toward massively parallel realizations and describe prospective integration with probabilistic models (e.g., large language models) for auto-formalization and conjecture seeding. The Python, C++, and MPL code to reproduce the Peano experiments, along with the full proof graphs in HTML as well as machine-readable text format, are available in the project's GitHub repository at github.com/Generative-Logic/GL commit 56c9233 and are permanently archived at doi:10.5281/zenodo.17206386.
• Abstract（参考訳）: 本稿では,ユーザが提供する公理的定義から始まる決定論的アーキテクチャである生成論理(GL)について述べる。 定義は、メッセージを交換する単純なLogic Blocks(LB)の分散グリッドにコンパイルされる。推論ルールの前提が統一されると、新しい事実がソースに完全に証明され、再生可能で監査可能な証明グラフが生成される。 プロトタイプソフトウェア実装は、一階ペアノ算術に基づいてワークフローをインスタンス化する。 ペアノ公理のみから始めて、GLは予想を列挙し、正規化、型、CEフィルタを適用し、加法の連想性、可換性、積の連想性、可換性、および分布性を含む基礎的算術法のマシンチェック可能な証明を自動的に再構築する。 一般的なハードウェアでは、証明フェーズは約7秒で完了し、完全な実行は約5分で終了する。 生成された証明はナビゲート可能なHTMLにエクスポートされ、すべての推論ステップを独立して検査することができる。 本稿では,大規模並列実現に向けたハードウェア・ソフトウェア共同設計の道程を概説し,自動形式化と予測シードのための確率モデル(例えば,大規模言語モデル)との将来的な統合について述べる。 Peano実験を再現するPython、C++、MPLコードは、HTMLの完全な証明グラフと機械可読テキストフォーマットと共に、github.com/Generative-Logic/GL commit 56c9233のプロジェクトのGitHubリポジトリで利用可能であり、doi:10.5281/zenodo.17206386で永久にアーカイブされている。

関連論文リスト

• TorchLean: Formalizing Neural Networks in Lean [71.68907600404513]
  本稿では,学習モデルを一級数学的対象として扱うフレームワークであるTorchLeanを紹介する。 我々はTorchLeanのエンドツーエンドを、証明された堅牢性、PINNの物理インフォームド残差、Lyapunovスタイルのニューラルコントローラ検証で検証する。
  論文  参考訳（メタデータ） (2026-02-26T05:11:44Z)
• Generalization and Completeness of Stochastic Local Search Algorithms [0.0]
  局所探索(SLS)アルゴリズムを一意な形式モデルに一般化する。 このモデルには、2つの重要な構成要素がある: できるだけ大きいように設計された共通構造と、できるだけ小さいことを意図したパラメトリック構造である。 SLSアルゴリズムのチューリング完全性を証明するために,本モデルを用いた。
  論文  参考訳（メタデータ） (2026-01-20T18:17:45Z)
• Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography [0.0]
  線形性の概念は数学と計算機科学の両方において中心的な役割を果たす。 この論文では線形性に基づいたプログラミングパラダイムのモデル化にLinear Logic (LL) を用いることについて論じている。 ADLLとCryptoBLLの2つの部分から構成される。
  論文  参考訳（メタデータ） (2025-10-20T07:02:48Z)
• APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
  APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。 Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
  論文  参考訳（メタデータ） (2025-04-27T05:04:02Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  ニューラルネットワークを文字列のバイナリ分類器として直接訓練し評価する。 3つのニューラルアーキテクチャに対して、チョムスキー階層の様々な言語について結果を提供する。 我々の貢献は、将来の研究において、言語認識の主張を理論的に健全に検証するのに役立つだろう。
  論文  参考訳（メタデータ） (2024-11-11T16:33:25Z)
• Autoregressive Large Language Models are Computationally Universal [59.34397993748194]
  変換器に基づく言語モデルの自己回帰復号化により,普遍計算が実現可能であることを示す。 まず、2027年の生産規則を持つラグシステムにより、普遍チューリングマシンをシミュレートできることを示す。 我々は、チャーチ・チューリングの論文により、拡張自己回帰(greedy)復号化によるgemini-1.5-pro-001が汎用コンピュータであると結論付けた。
  論文  参考訳（メタデータ） (2024-10-04T06:05:17Z)
• On the Representational Capacity of Neural Language Models with Chain-of-Thought Reasoning [87.73401758641089]
  CoT推論による現代言語モデル(LM)の性能向上 LMは弦上の分布の族を確率的チューリングマシンと同一に表現できることを示す。
  論文  参考訳（メタデータ） (2024-06-20T10:59:02Z)
• Learning to Reason via Program Generation, Emulation, and Search [33.11955431589091]
  言語モデル(LM)によるプログラム合成は、多くの推論能力を解放した。 すべての推論タスクは、コードとして容易に表現できるわけではない。例えば、常識的推論、道徳的意思決定、皮肉な理解を含むタスクである。 我々は,プログラム合成スキルをこのようなタスクに拡張するために,コード生成とエミュレートされた実行(CoGEX)を提案する。
  論文  参考訳（メタデータ） (2024-05-25T19:40:50Z)
• Improving Complex Reasoning over Knowledge Graph with Logic-Aware Curriculum Tuning [89.89857766491475]
  カリキュラムベースの論理認識型チューニングフレームワークであるLACTを提案する。 具体的には、任意の一階論理クエリをバイナリツリー分解によって拡張する。 広く使われているデータセットに対する実験では、LATは高度な手法よりも大幅に改善(平均+5.5% MRRスコア)し、新しい最先端技術を実現している。
  論文  参考訳（メタデータ） (2024-05-02T18:12:08Z)
• Leveraging Large Language Models for Automated Proof Synthesis in Rust [6.202137610101939]
  大規模言語モデル(LLM)は、コード解析と合成に成功している。 我々は、LLMと静的解析を組み合わせることで、Verusと呼ばれるRustベースの形式検証フレームワークの不変性、アサーション、その他の証明構造を合成する。 プロトタイプでは,検証タスクを複数の小さなタスクに分割し,反復的にGPT-4をクエリし,その出力と軽量な静的解析を組み合わせる。
  論文  参考訳（メタデータ） (2023-11-07T05:47:47Z)
• 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)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Advising OpenMP Parallelization via a Graph-Based Approach with Transformers [2.393682571484038]
  我々は,OpenMPのプラグマと共有メモリ属性を並列コードで検出し,予測する,OMPifyと呼ばれる新しい手法を提案する。 OMPifyは、ソースコードのグラフベースの表現を利用するTransformerベースのモデルに基づいている。 以上の結果から,OMPifyは汎用および人気の高いChatGPTやPragFormerモデルなど,既存のアプローチよりも優れていることが示された。
  論文  参考訳（メタデータ） (2023-05-16T16:56:10Z)
• CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives (full version) [12.790826917588575]
  暗号は例外であり、多くのパフォーマンスクリティカルなルーチンがアセンブリで直接書かれてきた。 CryptOptは、GCCやClangが生成するものよりもはるかに高速なアセンブリコードに高レベルの暗号関数プログラムを専門とする、最初のコンパイルパイプラインである。 形式検証の面では、FiatOptフレームワーク(関数型プログラムをCライクなIRコードに変換する)に接続し、新たに公式に認証されたプログラム等価チェッカーで拡張する。
  論文  参考訳（メタデータ） (2022-11-19T11:07:39Z)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  自動定理証明(Automated Theorem Proving)は、いくつかの予想(クエリ)が一連の公理(事実と規則)の論理的な結果であることを示すことができるコンピュータプログラムの開発を扱う。 近年のアプローチでは、自然言語(英語)で表される公理の予想を導出するトランスフォーマーに基づくアーキテクチャが提案されている。 本研究は, 一般化の項における最先端結果を実現するニューラルユニファイザという, 新たなアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2021-09-17T10:48:39Z)
• Statistically Meaningful Approximation: a Case Study on Approximating Turing Machines with Transformers [50.85524803885483]
  本研究は,統計的学習性を示すために近似ネットワークを必要とする統計有意(SM)近似の形式的定義を提案する。 回路とチューリングマシンの2つの機能クラスに対するSM近似について検討する。
  論文  参考訳（メタデータ） (2021-07-28T04:28:55Z)
• StreamBlocks: A compiler for heterogeneous dataflow computing (technical report) [1.5293427903448022]
  この作業では、オープンソースのコンパイラとランタイムであるStreamBlocksを導入し、CALデータフロープログラミング言語を使用して、プラットフォーム間で計算処理を分割する。 StreamBlocksは、最高のハードウェア/ソフトウェアパーティションを特定するためのプロファイル誘導ツールを使用して、デザインスペースの探索をサポートする。
  論文  参考訳（メタデータ） (2021-07-20T08:46:47Z)

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

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