論文の概要: Gödel's Poetry

• arxiv url: http://arxiv.org/abs/2512.14252v1
• Date: Tue, 16 Dec 2025 10:00:01 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-17 16:49:26.675469
• Title: Gödel's Poetry
• Title（参考訳）: ゲーデルの詩
• Authors: Kelly J. Davis,
• Abstract要約: 本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal, automated theorem proving has long been viewed as a challenge to artificial intelligence. We introduce here a new approach to computer theorem proving, one that employs specialized language models for Lean4 proof generation combined with recursive decomposition of difficult theorems into simpler entailing propositions. These models are coordinated through a multi-agent architecture that orchestrates autoformalization (if required), proof generation, decomposition of difficult theorems into simpler entailing propositions, and recursive proof (and/or decomposition) of these propositions. Without decomposition, we achieve a 90.4% pass rate on miniF2F. With decomposition, this is significantly improved. A key technical contribution lies in our extension of the Kimina Lean Server with abstract syntax tree (AST) parsing capabilities to facilitate automated, recursive proof decomposition. The system is made available on PyPI as goedels-poetry (at https://pypi.org/project/goedels-poetry ), and the open-source implementation KellyJDavis/goedels-poetry (at https://github.com/KellyJDavis/goedels-poetry ) facilitates both adaptation to alternative language models and extension with custom functionality.
• Abstract（参考訳）: 形式的で自動化された定理証明は、人工知能への挑戦と見なされてきた。 本稿では,Lean4の証明生成のための特殊言語モデルと,難解な定理の再帰的分解を組み合わせ,より単純な補足命題に組み合わせたコンピュータ定理証明の新しいアプローチを紹介する。 これらのモデルは、自動形式化(必要であれば)、証明生成、難解定理のより単純な命題への分解、およびこれらの命題の再帰的証明(および/または分解)をオーケストレーションするマルチエージェントアーキテクチャを通してコーディネートされる。 分解がなければ、MiniF2Fの90.4%のパスレートを達成する。 分解により、これは大幅に改善される。 重要な技術的貢献は、自動化された再帰的な証明分解を容易にする抽象構文ツリー(AST)解析機能を備えたKimina Lean Serverの拡張にあります。 システムは、goedels-poetry (https://pypi.org/project/goedels-poetry )としてPyPI上で利用可能であり、オープンソース実装である KellyJDavis/goedels-poetry (https://github.com/KellyJDavis/goedels-poetry )は、代替言語モデルへの適応と、カスタム機能の拡張の両方を容易にする。

関連論文リスト

• Neuro-Symbolic Query Compiler [57.78201019000895]
  本稿では,このギャップを埋めるために,言語文法規則とコンパイラ設計に触発されたニューラルシンボリックなフレームワークQCompilerを提案する。 理論上は、複雑なクエリを形式化するのに最小でも十分なバックス・ナウアー形式(BNF)の文法を$G[q]$で設計する。 葉のサブクエリの原子性は、より正確な文書検索と応答生成を保証し、複雑なクエリに対処するRAGシステムの能力を大幅に改善する。
  論文  参考訳（メタデータ） (2025-05-17T09:36:03Z)
• Hierarchical Attention Generates Better Proofs [8.676187819105298]
  注意機構を数学的推論構造に整合させる正規化手法であるtextbfHierarchical Attention を導入する。 提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。
  論文  参考訳（メタデータ） (2025-04-27T10:35:05Z)
• ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
  本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。 本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。 また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
  論文  参考訳（メタデータ） (2025-01-30T12:37:06Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• PE: A Poincare Explanation Method for Fast Text Hierarchy Generation [16.059322030238384]
  本稿では,双曲空間との特徴的相互作用をモデル化するための新しい手法であるPoincare Explanation(PE)を提案する。 具体的には、テキスト階層の構築を、双曲空間に散在する木を見つけるものとして捉えている。
  論文  参考訳（メタデータ） (2024-03-25T09:04:14Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
  PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。 我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
  論文  参考訳（メタデータ） (2021-02-11T18:59:24Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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