論文の概要: 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にある。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Automata-based constraints for language model decoding [9.137697105669142]
  言語モデル(LM)は、いくつかの形式言語で文字列を生成することがしばしば期待されている。 チューニングにはかなりのリソースが必要で、一般的でない、あるいはタスク固有のフォーマットでは実用的ではない。 我々はこれらの問題をオートマトン理論を適用して解決する。 我々のシステムは、7000倍高速に制約をコンパイルし、確実に正確であり、モジュール方式で拡張することができる。
  論文  参考訳（メタデータ） (2024-07-11T00:25:01Z)
• LLM Critics Help Catch Bugs in Mathematics: Towards a Better Mathematical Verifier with Natural Language Feedback [71.95402654982095]
  本研究では,自然言語フィードバック型検証器Math-Minosを提案する。 実験の結果,少量の自然言語フィードバックが検証器の性能を大幅に向上させることがわかった。
  論文  参考訳（メタデータ） (2024-06-20T06:42:27Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。 1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。 このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
  論文  参考訳（メタデータ） (2024-02-29T15:26:14Z)
• Large Language Models are Better Reasoners with Self-Verification [48.534270563880845]
  大規模言語モデル(LLM)は、いくつかの自然言語処理タスクにおいて強力な推論能力を示している。 思考の連鎖(CoT)を促進させるLLMは、個別のミスに非常に敏感な、多段階のプロンプトと多段階の予測を必要とする。 また,LLMにも同様な自己検証能力があることを示す。
  論文  参考訳（メタデータ） (2022-12-19T15:51:52Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

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

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