論文の概要: Formal Mathematics Statement Curriculum Learning
- arxiv url: http://arxiv.org/abs/2202.01344v1
- Date: Thu, 3 Feb 2022 00:17:00 GMT
- ステータス: 処理完了
- システム内更新日: 2022-02-04 13:30:40.157786
- Title: Formal Mathematics Statement Curriculum Learning
- Title(参考訳): 形式数学文のカリキュラム学習
- Authors: Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor
Babuschkin, Ilya Sutskever
- Abstract要約: 同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。
また, 難易度が十分に異なる形式文の集合に適用した場合, 専門家の反復により, ますます困難な問題に対するカリキュラムの発見と解決が可能であることも観察した。
- 参考スコア(独自算出の注目度): 64.45821687940946
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We explore the use of expert iteration in the context of language modeling
applied to formal mathematics. We show that at same compute budget, expert
iteration, by which we mean proof search interleaved with learning,
dramatically outperforms proof search only. We also observe that when applied
to a collection of formal statements of sufficiently varied difficulty, expert
iteration is capable of finding and solving a curriculum of increasingly
difficult problems, without the need for associated ground-truth proofs.
Finally, by applying this expert iteration to a manually curated set of problem
statements, we achieve state-of-the-art on the miniF2F benchmark, automatically
solving multiple challenging problems drawn from high school olympiads.
- Abstract(参考訳): 形式数学に適用される言語モデリングの文脈において,専門家によるイテレーションの利用について検討する。
同じ計算予算、専門家の反復、つまり、学習にインターリーブされた証明検索が、証明検索のみを劇的に上回っていることを示す。
また, 十分な難易度を持つ形式文の収集に適用した場合, 専門家の反復は, 関連する基礎的真理証明を必要とせず, ますます困難な問題のカリキュラムを見つけ, 解決することができる。
最後に、このエキスパートイテレーションを手作業でキュレートされた問題ステートメントに適用することにより、miniF2Fベンチマークの最先端を達成し、高校のオリンピック選手が引き起こした複数の課題を自動的に解決する。
関連論文リスト
- Context Matters: Data-Efficient Augmentation of Large Language Models
for Scientific Applications [15.893290942177112]
GPT-4のような大規模言語モデル(LLM)に固有の課題について検討する。
一貫性と意味論的に厳密な方法で誤った回答を提示するLLMの能力は、事実の不正確さの検出を複雑にする。
本研究の目的は,このような誤りの理解と軽減を図り,LCMの精度と信頼性の向上に寄与することである。
論文 参考訳(メタデータ) (2023-12-12T08:43:20Z) - Fusing Models with Complementary Expertise [44.60955450789187]
データ分布の相補的な知識で専門家モデルの出力を融合させるFoE(Fusion of Experts)問題を考える。
我々の方法は差別的タスクと生成的タスクの両方に当てはまる。
論文 参考訳(メタデータ) (2023-10-02T18:31:35Z) - Knowledge Crosswords: Geometric Reasoning over Structured Knowledge with
Large Language Models [51.35398315130094]
構造的知識に対する幾何学的推論を提案し、そこでは知識の一部がグラフ構造に連結され、モデルは不足した情報を埋める必要がある。
このような幾何学的知識推論は、構造化された知識、不確実性のある推論、事実の検証、エラーが発生した時のバックトラックを扱う能力を必要とする。
本稿では,不完全なエンティティネットワークの幾何学的制約を表す自然言語質問からなるマルチブランクQAデータセットであるKnowledge Crosswordsを提案する。
論文 参考訳(メタデータ) (2023-10-02T15:43:53Z) - FIMO: A Challenge Formal Dataset for Automated Theorem Proving [31.695624833932577]
FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。
公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
論文 参考訳(メタデータ) (2023-09-08T12:34:28Z) - Causal Discovery with Language Models as Imperfect Experts [119.22928856942292]
専門知識を用いて因果グラフの同定を改善する方法について検討する。
整合性に基づく専門家の知識を改良するための戦略を提案する。
本稿では,不完全な専門家として大規模言語モデルを用いる実データを用いたケーススタディについて報告する。
論文 参考訳(メタデータ) (2023-07-05T16:01:38Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。
提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文 参考訳(メタデータ) (2023-06-29T18:35:41Z) - Towards a Holistic Understanding of Mathematical Questions with
Contrastive Pre-training [65.10741459705739]
本稿では,数学的問題表現,すなわち QuesCo に対する対照的な事前学習手法を提案する。
まず、コンテンツレベルと構造レベルを含む2段階の質問強化を設計し、類似した目的で文字通り多様な質問ペアを生成する。
そこで我々は,知識概念の階層的情報を完全に活用するために,知識階層を意識したランク戦略を提案する。
論文 参考訳(メタデータ) (2023-01-18T14:23:29Z) - Learning to Find Proofs and Theorems by Learning to Refine Search
Strategies [0.9137554315375919]
AlphaZeroスタイルのエージェントは、非決定論的プログラムとして表される高度な専門家戦略を洗練するために自己学習を行っている。
類似教師エージェントは、学習者にとって適切な関連性と難易度のあるタスクを生成するための自己学習を行う。
論文 参考訳(メタデータ) (2022-05-27T20:48:40Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。