論文の概要: Twitch: Learning Abstractions for Equational Theorem Proving

• arxiv url: http://arxiv.org/abs/2603.06849v1
• Date: Fri, 06 Mar 2026 20:15:09 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-10 15:13:13.201787
• Title: Twitch: Learning Abstractions for Equational Theorem Proving
• Title（参考訳）: Twitch: 等式定理証明のための抽象化を学ぶ
• Authors: Guy Axelrod, Moa Johansson, Nicholas Smallbone,
• Abstract要約: 我々は、Stitchの助けを借りて抽象化を発見するツールTwitchを紹介する。 Twitchは、(1)予想の部分的かつ失敗的な証明から、(2)同じ領域における他の定理の証明から、という2つの方法で抽象化を生成することができる。 Twitchは12のレーティング-1の問題を証明できるだけでなく、他の多くの問題でも大幅にスピードアップできることを示す。
• 参考スコア（独自算出の注目度）: 1.5905165019585945
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.
• Abstract（参考訳）: 自動推論におけるいくつかの成功戦略は、どの用語や節の形が興味深いかという人為的なガイダンスに依存している。 本稿では,興味深い用語の形を自動的に発見することを目的としている。 具体的には、関連する証明において、繰り返し発生する用語パターンを抽象化として発見する。 プログラム合成タスクにおいて,再利用可能なライブラリ関数を発見するために開発されたツールであるStitchの助けを借りて,抽象化を発見するツールTwitchを提案する。 Twitchは、(1)予想の部分的かつ失敗的な証明から、(2)同じ領域における他の定理の証明から、という2つの方法で抽象化を生成することができる。 また、方程式定理証明器であるツイー(Twee)をこれらの抽象化を使用するように拡張した。 TwitchをTPTPから一組の単位等式(UEQ)問題で評価し、12のレーティング-1の問題を証明し、他の多くの問題に対してかなりのスピードアップが得られることを示す。

関連論文リスト

• Gödel's Poetry [0.0]
  本稿では,Lean4の証明生成に特殊言語モデルを用いるコンピュータ定理証明の新しいアプローチを提案する。 分解せずにMiniF2Fの90.4%のパスレートを達成する。 重要な技術的貢献は、抽象構文木(AST)解析機能を備えたKimina Lean Serverの拡張にあります。
  論文  参考訳（メタデータ） (2025-12-16T10:00:01Z)
• RLAD: Training LLMs to Discover Abstractions for Solving Reasoning Problems [98.98963933669751]
  問題が発生したら、複数の抽象化を提案できるモデルをトレーニングし、続いてソリューション構築のインセンティブを与えるRLを作ります。 この結果、RLトレーニングパラダイムはRLADと呼ばれ、抽象化ジェネレータとソリューションジェネレータを共同で訓練する。 我々は、大規模なテスト予算で多くのソリューションを生成するよりも、より多くのテスト時間計算を抽象化の生成に割り当てることが、パフォーマンスに有益であることを示しています。
  論文  参考訳（メタデータ） (2025-10-02T17:44:23Z)
• Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
  ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。 制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。 我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
  論文  参考訳（メタデータ） (2024-06-30T13:34:54Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• Machine learning and information theory concepts towards an AI Mathematician [77.63761356203105]
  人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。 このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。 興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
  論文  参考訳（メタデータ） (2024-03-07T15:12:06Z)
• Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry [0.0]
  我々は、幾何定理(と性質)の自動発見のための異なるアプローチを提示し、議論する。 定理証明者が興味深い定理を生成できるかどうかを判断することは、決定論的でない課題である。
  論文  参考訳（メタデータ） (2024-01-22T12:51:19Z)
• UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression [127.68780714438103]
  計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。 我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。 また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
  論文  参考訳（メタデータ） (2022-12-06T04:37:51Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)
• Automating the Generation of High School Geometry Proofs using Prolog in an Educational Context [0.0]
  我々は、Prologのエンコーディングから証明の完全なセットの生成に至るまで、我々が実装した中核的な概念を提示する。 また、私たちが直面した主な問題と、選択したソリューションも提示します。
  論文  参考訳（メタデータ） (2020-02-28T05:23:16Z)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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