論文の概要: Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
- arxiv url: http://arxiv.org/abs/2403.18120v1
- Date: Tue, 26 Mar 2024 22:01:13 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-28 20:55:22.669846
- Title: Don't Trust: Verify -- Grounding LLM Quantitative Reasoning with Autoformalization
- Title(参考訳): Don't Trust: Verify -- オートフォーマライゼーションによるLLM定量推論の根拠
- Authors: Jin Peng Zhou, Charles Staats, Wenda Li, Christian Szegedy, Kilian Q. Weinberger, Yuhuai Wu,
- Abstract要約: 大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。
LLMのトレーニングコーパスが十分に多くの形式数学の例を含むなら、それらが形式的イザベル符号に翻訳するように促すことができるという事実を活用する。
これは、形式化されたバージョンが内部や形式化された問題ステートメントと矛盾するソリューションを自動的に拒否するメカニズムを提供する。
- 参考スコア(独自算出の注目度): 45.439933713342256
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLM), such as Google's Minerva and OpenAI's GPT families, are becoming increasingly capable of solving mathematical quantitative reasoning problems. However, they still make unjustified logical and computational errors in their reasoning steps and answers. In this paper, we leverage the fact that if the training corpus of LLMs contained sufficiently many examples of formal mathematics (e.g. in Isabelle, a formal theorem proving environment), they can be prompted to translate i.e. autoformalize informal mathematical statements into formal Isabelle code -- which can be verified automatically for internal consistency. This provides a mechanism to automatically reject solutions whose formalized versions are inconsistent within themselves or with the formalized problem statement. We evaluate our method on GSM8K, MATH and MultiArith datasets and demonstrate that our approach provides a consistently better heuristic than vanilla majority voting -- the previously best method to identify correct answers, by more than 12% on GSM8K. In our experiments it improves results consistently across all datasets and LLM model sizes. The code can be found at https://github.com/jinpz/dtv.
- Abstract(参考訳): GoogleのMinervaやOpenAIのGPTファミリーのような大規模言語モデル(LLM)は、数学的な量的推論問題を解く能力がますます高まっている。
しかし、彼らは推論ステップや解答において、不正確な論理的および計算的誤りを犯している。
本稿では, LLM のトレーニングコーパスが形式数学の例を十分に多く含んでいれば(例えば,Isabelle の形式的定理証明環境),形式的数学的文を形式的イザベル符号に自動変換し, 内部整合性のために自動的に検証することができる。これにより, 形式化されたバージョンが内部あるいは形式化された問題文と矛盾する解を自動的に除去する機構が提供される。我々は, GSM8K , MATH および MultiArith のデータセット上で本手法を評価し,本手法がバニラの多数決投票よりも一貫したヒューリスティックな手法であることを示す。
我々の実験では、すべてのデータセットとLLMモデルサイズで結果が一貫して改善されます。
コードはhttps://github.com/jinpz/dtv.comにある。
関連論文リスト
- Evaluating Mathematical Reasoning Beyond Accuracy [50.09931172314218]
推論ステップの品質を評価するための新しい方法論であるReasonEvalを紹介します。
我々は、ReasonEvalが人間のラベル付きデータセット上で最先端のパフォーマンスを達成することを示す。
我々は、ReasonEvalがデータ選択において重要な役割を果たすことを観察する。
論文 参考訳(メタデータ) (2024-04-08T17:18:04Z) - GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of
LLMs as Mathematical Problem Solvers [73.78371810664319]
大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。
1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。
このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
論文 参考訳(メタデータ) (2024-02-29T15:26:14Z) - A New Approach Towards Autoformalization [8.176989532546632]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳(メタデータ) (2023-10-12T00:50:24Z) - GRACE: Discriminator-Guided Chain-of-Thought Reasoning [75.35436025709049]
本稿では, 正しい推論手順を導出するために, GRACE (CorrectnEss Discriminator) を用いたチェーン・オブ・シークレット・リAsoningを提案する。
GRACEは、正しいステップと間違ったステップに対して対照的な損失で訓練された判別器を採用しており、復号時に次のステップ候補を採点するために使用される。
論文 参考訳(メタデータ) (2023-05-24T09:16:51Z) - MathPrompter: Mathematical Reasoning using Large Language Models [7.953723258038284]
大規模言語モデル (LLM) は算術的推論タスクを解く際の性能に制限がある。
MathPrompterはZero-shot-of- Thoughtプロンプト技術を使って複数の代数式やPython関数を生成し、異なる方法で同じ数学問題を解く。
論文 参考訳(メタデータ) (2023-03-04T04:43:49Z) - Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。
思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。
また,LLMにも同様な自己検証能力があることを示す。
論文 参考訳(メタデータ) (2022-12-19T15:51:52Z) - PAL: Program-aided Language Models [112.94785609781503]
自然言語問題を理解するために,プログラム支援言語モデル(PaL)を提案する。
PaLはソリューションステップをPythonインタプリタのようなプログラムランタイムにオフロードする。
私たちは12のベンチマークで新しい最先端の結果を設定しました。
論文 参考訳(メタデータ) (2022-11-18T18:56:13Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳(メタデータ) (2022-05-25T09:53:30Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。