論文の概要: Lemmas: Generation, Selection, Application
- arxiv url: http://arxiv.org/abs/2303.05854v2
- Date: Mon, 24 Jul 2023 07:21:28 GMT
- ステータス: 処理完了
- システム内更新日: 2023-07-25 23:39:53.833438
- Title: Lemmas: Generation, Selection, Application
- Title(参考訳): Lemmas: 生成、選択、適用
- Authors: Michael Rawson and Christoph Wernhard and Zsolt Zombori and Wolfgang
Bibel
- Abstract要約: 本稿では,自動定理証明器に有用な補題を生成する学習技術を含む複合システムによる実験について述べる。
凝縮分枝問題に焦点をあてることで、設定を大幅に単純化し、補題の本質と証明探索におけるそれらの役割を理解できるようになる。
- 参考スコア(独自算出の注目度): 2.0646127669654826
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Noting that lemmas are a key feature of mathematics, we engage in an
investigation of the role of lemmas in automated theorem proving. The paper
describes experiments with a combined system involving learning technology that
generates useful lemmas for automated theorem provers, demonstrating
improvement for several representative systems and solving a hard problem not
solved by any system for twenty years. By focusing on condensed detachment
problems we simplify the setting considerably, allowing us to get at the
essence of lemmas and their role in proof search.
- Abstract(参考訳): 補題が数学の重要な特徴であることに留意し、自動定理証明における補題の役割について調査を行う。
本稿では,自動定理証明器に有用な補題を生成する学習技術と,いくつかの代表的なシステムの改善を実証し,20年間,どのシステムでも解決できない難題を解くことを目的とした実験を行った。
凝縮した分断問題に焦点を当てることで、設定をかなり単純化し、補題の本質と証明探索におけるそれらの役割を把握できる。
関連論文リスト
- Learning Guided Automated Reasoning: A Brief Survey [5.607616497275423]
これまでに開発されてきたいくつかの自動推論・定理証明領域と学習・AI手法の概要について概説する。
これには、前提選択、いくつかの設定での証明ガイダンス、推論と学習を繰り返すフィードバックループ、象徴的な分類問題が含まれる。
論文 参考訳(メタデータ) (2024-03-06T19:59:17Z) - Boosting of Thoughts: Trial-and-Error Problem Solving with Large
Language Models [48.43678591317425]
Boosting of Thoughts (BoT)は、大規模言語モデルによる問題解決のための自動プロンプトフレームワークである。
我々は,BoTが他の先進的なプロンプト手法よりも高い,あるいは同等の問題解決率を達成することを示す。
論文 参考訳(メタデータ) (2024-02-17T00:13:36Z) - Solving with GeoGebra Discovery an Austrian Mathematics Olympiad
problem: Lessons Learned [0.6140969539089365]
我々は、GeoGebra Discoveryにおける自動推論ツールを通じて、オーストリア数学のOlympiad 2023の地域段階の問題に対処する。
この問題を解決しようとすると、4種類のフィードバックが生まれます。
我々は、これらの多様な問題について、GeoGebra Discoveryの利点、課題、そして現在の開発分野のいくつかを示す役割を、説明し、反映する。
論文 参考訳(メタデータ) (2024-01-22T12:51:35Z) - MacGyver: Are Large Language Models Creative Problem Solvers? [90.62345519188655]
本稿では,現代大言語モデル(LLM)の創造的問題解決能力について,制約のある環境で検討する。
私たちは1,600の現実世界の問題からなる自動生成されたデータセットであるMacGyverを作成します。
MacGyverはどちらのグループでも難しいが、ユニークで相補的な方法では難しい。
論文 参考訳(メタデータ) (2023-11-16T08:52:27Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。
提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文 参考訳(メタデータ) (2023-06-29T18:35:41Z) - Faith and Fate: Limits of Transformers on Compositionality [109.79516190693415]
3つの代表的構成課題にまたがる変圧器大言語モデルの限界について検討する。
これらのタスクは、問題をサブステップに分割し、これらのステップを正確な答えに合成する必要があります。
実験結果から,多段階合成推論を線形化部分グラフマッチングに還元することにより,トランスフォーマーLLMが構成課題を解くことが示唆された。
論文 参考訳(メタデータ) (2023-05-29T23:24:14Z) - Four Geometry Problems to Introduce Automated Deduction in Secondary
Schools [0.0]
幾何学における自動推論の主題は、特に問題に対処することで導入することができる。
この課題は4つの中等教育の幾何学的問題に対処することで論じられる。
これらの問題に対して,情報通信技術を活用した授業計画について論じる。
論文 参考訳(メタデータ) (2022-02-08T00:07:34Z) - Formal Mathematics Statement Curriculum Learning [64.45821687940946]
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。
また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
論文 参考訳(メタデータ) (2022-02-03T00:17:00Z) - Lyapunov Exponents for Diversity in Differentiable Games [19.16909724435523]
Ridge Rider (RR) はヘシアン(リッジ)の固有ベクトルに従うことによって最適化問題の多様な解を求めるアルゴリズムである。
RRは保守的な勾配系のために設計されており、サドルで分岐する。
本稿では,任意の分岐点を求める手法として,一般化リッジライダー(GRR)を提案する。
論文 参考訳(メタデータ) (2021-12-24T22:48:14Z) - Specialization in Hierarchical Learning Systems [0.0]
我々は,専門家の階層における情報制約が,正規化の原則的方法を提供するだけでなく,専門化の強制にもどの程度役立つかを検討する。
我々は,問題空間を複数のサブプロブレムに分割し,個々の専門家が解決できる情報理論に基づくオンライン学習ルールを考案する。
本稿では, 分類, 回帰, 密度推定, 強化学習問題など, 様々な問題に対するアプローチの適用性について述べる。
論文 参考訳(メタデータ) (2020-11-03T17:00:31Z) - On the Social and Technical Challenges of Web Search Autosuggestion
Moderation [118.47867428272878]
自動提案は通常、検索ログと文書表現のコーパスに基づいてトレーニングされた機械学習(ML)システムによって生成される。
現在の検索エンジンは、このような問題のある提案を抑えるのに、ますます熟練している。
問題のある提案のいくつかの側面、パイプラインに沿った困難な問題、そしてWeb検索を超えたアプリケーションの増加になぜ私たちの議論が適用されるのかについて論じる。
論文 参考訳(メタデータ) (2020-07-09T19:22:00Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。