論文の概要: Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source

• arxiv url: http://arxiv.org/abs/2603.13514v1
• Date: Fri, 13 Mar 2026 18:47:31 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-17 16:19:35.249048
• Title: Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source
• Title（参考訳）: 実行可能な考古学: IPL-V源からの論理理論の再検討
• Authors: Jeff Shrager,
• Abstract要約: 私はCommon Lispで書かれた新しいIPL-Vインタプリタの構築について説明する。 私は、1963年のStefferudの技術的レポートから直接書き起こされたコードから、論理論者の忠実な再アニメーションを説明します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Logic Theorist (LT), created by Allen Newell, J. C. Shaw, and Herbert Simon in 1955-1956, is widely regarded as the first artificial intelligence program. While the original conceptual model was described in 1956, it underwent several iterations as the underlying Information Processing Language (IPL) evolved. Here I describe the construction of a new IPL-V interpreter, written in Common Lisp, and the faithful reanimation of the Logic Theorist from code transcribed directly from Stefferud's 1963 RAND technical report. Stefferud's version represents a pedagogical re-coding of the original heuristic logic into the standardized IPL-V. The reanimated LT successfully proves 16 of 23 attempted theorems from Chapter 2 of Principia Mathematica, results that are historically consistent with the original system's behavior within its search limits. To the author's knowledge, this is the first successful execution of the original Logic Theorist code in over half a century.
• Abstract（参考訳）: 1955-1956年にアレン・ニューウェル、J・C・ショー、ハーバート・サイモンによって作られた論理理論(LT)は、最初の人工知能プログラムとみなされている。 オリジナルの概念モデルは1956年に記述されたが、基盤となる情報処理言語(IPL)が進化するにつれて、幾度かの繰り返しが行われた。 ここでは、Common Lispで書かれた新しいIPL-Vインタプリタの構築と、1963年のStefferudの技術的レポートから直接書き起こされたコードからの論理理論者の忠実な再アニメーションについて説明する。 Stefferud のバージョンは、元のヒューリスティック論理を標準化された IPL-V に再コーディングしたものである。 再アニメーションされたLTは、Principia Mathematicaの2章の23の定理のうち16の証明に成功した。 著者の知識では、これは最初の論理理論のコードの実行が半世紀以上で成功した最初の例である。

関連論文リスト

• Statistical Learning Theory in Lean 4: Empirical Processes from Scratch [57.00315741159824]
  本稿では,経験的プロセス理論に基づく統計学習理論(SLT)の総合的なLean 4形式化について述べる。 エンドツーエンドの正式なインフラストラクチャは、最新のLean 4 Mathlibライブラリに欠けている内容を実装しています。 この研究は再利用可能な形式基盤を確立し、機械学習理論の今後の発展への扉を開く。
  論文  参考訳（メタデータ） (2026-02-02T16:24:53Z)
• NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models [5.211983629897431]
  我々は一階述語論理翻訳フレームワークNL2LOGICを提案する。 LogicNLIの実験では、抽象ProofWriterベンチマークにより、NL2LOGICは99%の構文的精度を実現し、最先端のベースラインに対して最大30%のセマンティックな正確性向上を実現している。 NL2LOGICをLogic-LMに組み込むことでほぼ完全な実行性が得られ、Logic-LMのオリジナルの数発の制約のない翻訳モジュールと比較して下流の推論精度が31%向上する。
  論文  参考訳（メタデータ） (2026-01-29T14:51:32Z)
• Training LLMs with LogicReward for Faithful and Rigorous Reasoning [75.30425553246177]
  定理証明器を用いてステップレベルの論理的正しさを強制することでモデルトレーニングを指導する報酬システムであるLogicRewardを提案する。 LogicRewardで構築されたデータに基づいてトレーニングされた8Bモデルは、GPT-4oとo4-miniを11.6%、自然言語推論と論理的推論タスクで2%超えた。
  論文  参考訳（メタデータ） (2025-12-20T03:43:02Z)
• Complex Logical Instruction Generation [32.47317492080224]
  大言語モデル(LLM)がロジックに富んだ命令でどれだけうまく機能するかは、まだ解明されていない。 LogicIFGenとLogicIFEvalを提案する。 LogicIFGenは、コード関数から検証可能な命令を生成するためのスケーラブルで自動化されたフレームワークである。 LogicIFEvalは426の検証可能なロジックリッチな命令からなるベンチマークである。
  論文  参考訳（メタデータ） (2025-08-12T17:54:27Z)
• Faithful Logical Reasoning via Symbolic Chain-of-Thought [39.94884827166363]
  シンボリック表現と論理規則をChain-of-Thoughtプロンプトと統合するフレームワークであるSymbCoTを提案する。 我々は、SymbCoTがCoT法よりも大幅に改善されていることを示す。 これは、論理的推論のために記号表現と規則をCoTに結合する最初の方法である。
  論文  参考訳（メタデータ） (2024-05-28T16:55:33Z)
• DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
  制約付き復号法は,事前訓練された大言語(Ms と PLMs)が生成するテキストの意味やスタイルを,推論時に様々なタスクに対して制御することを目的としている。 これらの方法は、しばしば、欲求的かつ明示的にターゲットを選択することによって、もっともらしい連続を導く。 認知二重プロセス理論に着想を得て,新しい復号化フレームワークDECDERを提案する。
  論文  参考訳（メタデータ） (2024-03-04T11:49:08Z)
• What's Left? Concept Grounding with Logic-Enhanced Foundation Models [76.74146485832125]
  本稿では,ドメインに依存しない一階述語論理型プログラムを用いて,ドメイン間の概念を基礎と推論するために学習する統一フレームワークを提案する。 LEFTは,2次元画像,3次元シーン,人間の動き,ロボット操作という4つの領域で,柔軟に概念を学習する。
  論文  参考訳（メタデータ） (2023-10-24T17:50:20Z)
• 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)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  自動定理証明(Automated Theorem Proving)は、いくつかの予想(クエリ)が一連の公理(事実と規則)の論理的な結果であることを示すことができるコンピュータプログラムの開発を扱う。 近年のアプローチでは、自然言語(英語)で表される公理の予想を導出するトランスフォーマーに基づくアーキテクチャが提案されている。 本研究は, 一般化の項における最先端結果を実現するニューラルユニファイザという, 新たなアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2021-09-17T10:48:39Z)

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

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