論文の概要: Case study: proving sqrt(2) irrational with LPTP and an LLM

• arxiv url: http://arxiv.org/abs/2607.21187v1
• Date: Thu, 23 Jul 2026 11:15:38 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-24 18:26:25.381974
• Title: Case study: proving sqrt(2) irrational with LPTP and an LLM
• Title（参考訳）: 事例研究 : LPTPとLPLMによる不合理性証明(2)
• Abstract要約: 2の平方根が論理プログラミングの文脈における有理数ではないことを示すことを目的としたLLM(Large Language Model)との相互作用を示す。 我々は、論理プログラムに関する特性を記述し証明するために、LPTP(Logic Program Theorem Prover)システムに依存している。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We present the interactions with an LLM (Large Language Model) aiming at proving that the square root of 2 is not a rational number in an LP (Logic Programming) context. We start from a few basic pure logic programming predicate definitions. We rely on the LPTP (Logic Program Theorem Prover) system for stating and proving properties about logic programs. As the proof language of LPTP is based on natural deduction, the proofs are human readable. In our case study, we sketch in LPTP the usual proof showing the irrationality of the square root of 2. Then we describe the interactions we had with the LLM. We end up with a complete formal proof, partially generated by an LLM and fully proof-checked by LPTP.
• Abstract（参考訳）: 2の平方根が論理プログラミングの文脈における有理数ではないことを示すことを目的としたLLM(Large Language Model)との相互作用を示す。 私たちは、いくつかの基本的な純粋論理プログラミング述語定義から始めます。 我々は、論理プログラムに関する特性を記述し証明するために、LPTP(Logic Program Theorem Prover)システムに依存している。 LPTPの証明言語は自然な推論に基づいているため、証明は人間の読みやすい。 今回のケーススタディでは, 2の平方根の不合理性を示す通常の証明をLPTPでスケッチする。 次に、LLMとの相互作用について述べる。 最終的に LLM によって部分的に生成され,LPTP によって完全に検証された完全形式的証明が得られた。

関連論文リスト

• Explorable Theorems: Making Written Theorems Explorable by Grounding Them in Formal Representations [26.38291147763785]
  形式化された表現の基盤となる説明は、静的テキストがサポートしているもの以上のインタラクティブなアベイランスを可能にすると論じる。 このアイデアを、LLMを用いて定理とその記述された証明をリーンに変換するシステムである探索可能な定理を用いて、数学的証明理解のためにインスタンス化する。 読者はこの証明をステップレベルの粒度で実行し、カスタム例や逆例をテストし、各ステップをブリッジする論理的依存関係をトレースすることができる。
  論文  参考訳（メタデータ） (2026-04-03T00:16:52Z)
• Statistical Parsing for Logical Information Retrieval [0.0]
  本稿では、推論、セマンティクス、構文間のギャップに対処する。 推論のために、QBBN を NEG 因子で拡張し、P(x) + P(neg x) = 1 を強制する。 意味論では、ロールラベル付き述語、モーダル量化器、およびPrawitzに続く表現性の3つの階層を持つ型付き論理言語を示す。 文法において,文を論理形式に決定的にコンパイルする型付きスロット文法を提案する。
  論文  参考訳（メタデータ） (2026-02-12T16:57:25Z)
• Are Language Models Efficient Reasoners? A Perspective from Logic Programming [109.47572890883248]
  現代言語モデル(LM)は、強い推論能力を示すが、標準的な評価は、人間のような推論の重要な側面である効率性を見越しながら、正確性を強調する。 本稿では、論理プログラミングのレンズを用いて、LM推論効率を評価するためのフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-10-29T15:30:31Z)
• Can Large Language Models Learn Formal Logic? A Data-Driven Training and Evaluation Framework [2.9334627971166336]
  本稿では,大規模言語モデル(LLM)の論理的推論能力について検討する。 訓練されたLLMは、一連の仮定とゴールを入力として受け取り、その仮定からゴールを正式に導出する証明を出力として生成する。 トレーニングにとって重要な障害は、現実世界の証明が不足していることだ。
  論文  参考訳（メタデータ） (2025-04-28T19:25:29Z)
• LP-LM: No Hallucinations in Question Answering with Logic Programming [0.30693357740321775]
  大規模言語モデル(LLM)は、ユーザクエリに対するヒューマンライクな応答を生成することができる。 本稿では,知識ベース(KB)に含まれる既知の事実の回答を基盤とするLP-LMを提案する。 DCGとタブリングを利用することで、LP-LMは十分な数の文法規則に対して入力文のサイズで線形時間で実行される。
  論文  参考訳（メタデータ） (2025-02-13T11:48:31Z)
• P-FOLIO: Evaluating and Improving Logical Reasoning with Abundant Human-Written Reasoning Chains [97.25943550933829]
  P-FOLIO(P-FOLIO)は、多種多様で複雑な推論連鎖からなる人称注釈付きデータセットである。 我々はP-FOLIOを用いて大規模言語モデル推論機能の評価と改善を行う。
  論文  参考訳（メタデータ） (2024-10-11T19:22:57Z)
• LogicBench: Towards Systematic Evaluation of Logical Reasoning Ability of Large Language Models [52.03659714625452]
  最近開発された大規模言語モデル (LLM) は、幅広い言語理解タスクにおいて非常によく機能することが示されている。 しかし、それらは自然言語に対して本当に「理性」があるのだろうか? この疑問は研究の注目を集めており、コモンセンス、数値、定性的など多くの推論技術が研究されている。
  論文  参考訳（メタデータ） (2024-04-23T21:08:49Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26: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)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  大規模言語モデル(LLM)は人間のような推論能力を示しているが、それでも複雑な論理的問題に悩まされている。 本稿では,論理問題の解法を改善するために,LLMとシンボリックソルバを統合した新しいフレームワークであるLogic-LMを紹介する。
  論文  参考訳（メタデータ） (2023-05-20T22:25:38Z)

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

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