論文の概要: Case study: solving P-99 with LPTP and an LLM

• arxiv url: http://arxiv.org/abs/2607.21196v1
• Date: Thu, 23 Jul 2026 11:17:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-24 18:26:25.38593
• Title: Case study: solving P-99 with LPTP and an LLM
• Title（参考訳）: ケーススタディ:LPTPとLPLMによるP-99の解決
• Abstract要約: 9つのProlog Problems (P-99) は有名なPrologのエクササイズである。 我々は、LLM(Large Language Model)の推進だけで、最初の30を解決した。 解決すれば、Prologコードとテストファイルを生成し、テストを実行して、パスしたかどうかを確認し、次に、形式、基底性、終了性、ユニーク性、存在、時には機能的正当性を正式に証明します。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ninety-Nine Prolog Problems (P-99) is a famous set of Prolog exercises. We solved the first thirty three just by prompting an LLM (Large Language Model). We used Claude from Anthropic. By solved we mean: generate the Prolog code and a test file, run the tests and check whether they pass, then formally prove types, groundness, termination, uniqueness, existence and also sometimes functional correctness with LPTP (Logic Program Theorem Prover). Hence our approach is an experiment in vibe-coding/vericoding of P-99. It is a vibe-coding experiment because we started from informal specifications written in English and let Claude generate the Prolog code. It also fits within vericoding because the LLM proved reliability guarantees on the generated Prolog code. Claude wrote 58 logic procedures, 508 tests, 257 lemmas for a total of 11800 proof lines. We manually checked each file generated by the LLM. We checked the Prolog code, ran the tests, examined the logical statements generated by Claude and proof-checked Claude's proofs with LPTP. This paper describes this experiment and provides the main details so that it can be reproduced by the interested reader.
• Abstract（参考訳）: 9つのProlog Problems (P-99) は有名なPrologのエクササイズである。 我々は LLM (Large Language Model) を推し進めて最初の30の問題を解いた。 人類学からクロードを使った。 解決すれば、Prologコードとテストファイルを生成し、テストを実行して、彼らがパスしたかどうかを正式に証明し、型、基底性、終了性、ユニーク性、存在、そして時々LPTP(Logic Program Theorem Prover)で機能的正当性を証明します。 したがって,本手法はP-99のバイブコーディング/ベリコーディング実験である。 英語で書かれた非公式仕様から始まり、ClaudeがPrologコードを生成するようにしました。 LLM が生成した Prolog コードに対して信頼性を保証することを証明したため、検証コードにも適合する。 クロードは58の論理手順、508の試験、257の補題、合計11800の証明ラインを書いた。 LLMで生成された各ファイルを手動でチェックした。 我々はPrologのコードをチェックし、テストを実行し、Claudeが生成した論理文を調べ、LPTPでClaudeの証明を検証した。 本稿では,本実験について述べるとともに,興味ある読者が再現できるように,本実験について解説する。

関連論文リスト

• Case study: proving sqrt(2) irrational with LPTP and an LLM [0.0]
  2の平方根が論理プログラミングの文脈における有理数ではないことを示すことを目的としたLLM(Large Language Model)との相互作用を示す。 我々は、論理プログラムに関する特性を記述し証明するために、LPTP(Logic Program Theorem Prover)システムに依存している。
  論文  参考訳（メタデータ） (2026-07-23T11:15:38Z)
• Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover [2.6146136791093104]
  本稿では,対話型定理証明器(ITP)が大規模ソフトウェア生成を支援するかどうかを考察する。 ITPは純粋全関数を扱うが、I/Oのような効果はないため、エージェントは実効的なコードを純粋論理から分離する。 本稿では, RISC-V RV32I ベースの47命令すべてに対して, CPU インタプリタの完全自動開発を通じて, この経路について検討する。
  論文  参考訳（メタデータ） (2026-05-25T16:35:36Z)
• DuET: Dual Execution for Test Output Prediction with Generated Code and Pseudocode [56.14374797825548]
  よりエラー耐性の高い擬似コードに基づいて予測を行うLLMベースの擬似コード実行を提案する。 両手法を機能的多数決で組み合わせた二重実行フレームワークであるDuETを提案する。 LiveCodeBenchでは、DuETは最先端のパフォーマンスを実現し、Pass@1を13.6ppで改善した。
  論文  参考訳（メタデータ） (2026-04-13T14:18:58Z)
• CLEVER: A Curated Benchmark for Formally Verified Code Generation [53.5486188696892]
  $rm Csmall LEVER$は、リーンにおけるエンドツーエンドのコード生成のための161の問題を、高品質でキュレートしたベンチマークである。 それぞれの問題は、(1)堅実な仕様と一致する仕様を生成するタスク、(2)この仕様を確実に満足するリーン実装を生成するタスクで構成されています。
  論文  参考訳（メタデータ） (2025-05-20T05:15:47Z)
• APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning [16.8655558789989]
  本稿では,自動定理証明のためのモデルに依存しないエージェントフレームワークであるAPOLLO (Automated PrOof repair viaLLM and Lean cOllaboration)を提案する。 エージェントのセットは、証明を分析し、シンタックスのエラーを修正し、リーンを使って証明の誤りを特定し、失敗するサブレムマを分離し、自動化されたソルバを利用し、残りの目標に対してLLMを呼び出す。 この結果から,LLM出力を目標としたコンパイラ誘導型修復は,効率と正確性の両方において劇的に向上することが示された。
  論文  参考訳（メタデータ） (2025-05-09T03:38:31Z)
• Insights from Verification: Training a Verilog Generation LLM with Reinforcement Learning with Testbench Feedback [36.69082579950107]
  大規模言語モデル(LLM)は、自然言語記述からVerilog生成において強力な性能を示している。 本稿では,テストベンチからの検証洞察をVerilog 生成 LLM のトレーニングに統合する手法を提案する。
  論文  参考訳（メタデータ） (2025-04-22T11:38:14Z)
• LP-LM: No Hallucinations in Question Answering with Logic Programming [0.30693357740321775]
  大規模言語モデル(LLM)は、ユーザクエリに対するヒューマンライクな応答を生成することができる。 本稿では,知識ベース(KB)に含まれる既知の事実の回答を基盤とするLP-LMを提案する。 DCGとタブリングを利用することで、LP-LMは十分な数の文法規則に対して入力文のサイズで線形時間で実行される。
  論文  参考訳（メタデータ） (2025-02-13T11:48:31Z)
• Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。 人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。 定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• 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)
• Benchmarking Large Language Models for Automated Verilog RTL Code Generation [21.747037230069854]
  有用なVerilogを生成するために,大規模言語モデル(LLM)を特徴付ける。 機能解析のためのテストベンチと,Verilogコードの構文をテストするフローからなる評価フレームワークを構築した。 その結果,LLMの微調整結果は,構文的に正しいコードを生成する能力が高いことがわかった。
  論文  参考訳（メタデータ） (2022-12-13T16:34:39Z)
• Self-Supervised Log Parsing [59.04636530383049]
  大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。 既存のアプローチは、ログ特化や手動ルール抽出に依存している。 本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
  論文  参考訳（メタデータ） (2020-03-17T19:25:25Z)

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

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