Fugu-MT 論文翻訳(概要): Lemmas: Generation, Selection, Application

論文の概要: Lemmas: Generation, Selection, Application

arxiv url: http://arxiv.org/abs/2303.05854v1
Date: Fri, 10 Mar 2023 11:06:43 GMT
ステータス: 処理完了
システム内更新日: 2023-03-13 15:22:21.395758
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年間,どのシステムでも解決できない難題を解くことを目的とした実験を行った。凝縮した分断問題に焦点を当てることで、設定をかなり単純化し、補題の本質と証明探索におけるそれらの役割を把握できる。

関連論文リスト

Global Lyapunov functions: a long-standing open problem in mathematics, with symbolic transformers [7.953947994427209]
我々は、Lyapunov関数を発見し、システムのグローバルな安定性を保証するという、数学における長年のオープンな問題を考える。この問題には既知の一般解はなく、いくつかの小さなアルゴリズム系にのみ存在する。そこで本研究では,システム上でのシーケンス・ツー・シーケンス・トランスフォーマが,解法や人間よりも優れた性能を示すことを示す。
論文参考訳（メタデータ） (2024-10-10T18:50:10Z)
Solving Zebra Puzzles Using Constraint-Guided Multi-Agent Systems [25.0042181817455]
本稿では,大言語モデルとオフ・ザ・シェルフ定理証明器を統合したマルチエージェントシステムZPSを紹介する。このシステムは、問題をより小さく管理可能な部分に分割することで、複雑なパズル解決作業に取り組む。また,問題解の正当性を評価するための自動グリッドパズルグレーダを導入し,ユーザスタディで評価することで,自動グレーダが信頼性が高いことを示す。
論文参考訳（メタデータ） (2024-07-04T14:22:25Z)
Automatic question generation for propositional logical equivalences [6.221146613622175]
そこで我々は,各学生に対して適切な質問を生成できる手法を開発し,実装する。従来の研究では、妥当性、ユーザ定義の困難さ、パーソナライズされた問題生成を含む、教育におけるAQGフレームワークについて研究されてきた。我々の新しいAQGアプローチは、一年生のコンピュータサイエンス学生にとってコアコースである離散数学に論理的等価性問題をもたらす。
論文参考訳（メタデータ） (2024-05-09T02:44:42Z)
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)
MacGyver: Are Large Language Models Creative Problem Solvers? [87.70522322728581]
本稿では, 現代LLMの創造的問題解決能力について, 制約付き環境下で検討する。我々は1,600以上の実世界の問題からなる自動生成データセットであるMACGYVERを作成する。我々はLLMと人間の両方にコレクションを提示し、それらの問題解決能力を比較して比較する。
論文参考訳（メタデータ） (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)
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)
On the Social and Technical Challenges of Web Search Autosuggestion Moderation [118.47867428272878]
自動提案は通常、検索ログと文書表現のコーパスに基づいてトレーニングされた機械学習(ML)システムによって生成される。現在の検索エンジンは、このような問題のある提案を抑えるのに、ますます熟練している。問題のある提案のいくつかの側面、パイプラインに沿った困難な問題、そしてWeb検索を超えたアプリケーションの増加になぜ私たちの議論が適用されるのかについて論じる。
論文参考訳（メタデータ） (2020-07-09T19:22:00Z)

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