論文の概要: Autoformalization with Large Language Models
- arxiv url: http://arxiv.org/abs/2205.12615v1
- Date: Wed, 25 May 2022 09:53:30 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-27 04:13:29.884675
- Title: Autoformalization with Large Language Models
- Title(参考訳): 大規模言語モデルによる自動生成
- Authors: Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats,
Mateja Jamnik, Christian Szegedy
- Abstract要約: 自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
- 参考スコア(独自算出の注目度): 22.86710743804944
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization is the process of automatically translating from natural
language mathematics to formal specifications and proofs. A successful
autoformalization system could advance the fields of formal verification,
program synthesis, and artificial intelligence. While the long-term goal of
autoformalization seemed elusive for a long time, we show large language models
provide new prospects towards this goal. We make the surprising observation
that LLMs can correctly translate a significant portion ($25.3\%$) of
mathematical competition problems perfectly to formal specifications in
Isabelle/HOL. We demonstrate the usefulness of this process by improving a
previously introduced neural theorem prover via training on these
autoformalized theorems. Our methodology results in a new state-of-the-art
result on the MiniF2F theorem proving benchmark, improving the proof rate from
$29.6\%$ to $35.2\%$.
- Abstract(参考訳): オートフォーマル化(Autoformalization)は、自然言語から形式仕様や証明への自動翻訳プロセスである。
オートフォルマライズシステムの成功は、形式的検証、プログラム合成、人工知能の分野を前進させる可能性がある。
オートフォーマル化の長期的な目標は長い間解明されているように思われるが、大きな言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々は, LLM が数学の競合問題の大部分 (25.3 %$) を, Isabelle/HOL の形式的な仕様に完全変換できるという驚くべき観察を行う。
自己形式化された定理のトレーニングを通じて,前回導入した神経定理証明器を改良することにより,このプロセスの有用性を実証する。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6\%から35.2\%に改善した。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - A New Approach Towards Autoformalization [8.176989532546632]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳(メタデータ) (2023-10-12T00:50:24Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳(メタデータ) (2023-02-24T03:28:46Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳(メタデータ) (2022-11-14T16:52:32Z) - Lila: A Unified Benchmark for Mathematical Reasoning [59.97570380432861]
LILAは、23の多様なタスクと4次元からなる統一的な数学的推論ベンチマークである。
我々は,Pythonプログラムの形式でタスク命令とソリューションを収集することにより,20のデータセットベンチマークを拡張してベンチマークを構築した。
LILAで訓練された汎用数学的推論モデルであるBHASKARAを紹介する。
論文 参考訳(メタデータ) (2022-10-31T17:41:26Z) - Masked Language Modeling and the Distributional Hypothesis: Order Word
Matters Pre-training for Little [74.49773960145681]
マスク言語モデル(MLM)トレーニングの印象的なパフォーマンスの可能な説明は、そのようなモデルがNLPパイプラインで広く普及している構文構造を表現することを学びました。
本稿では,先行訓練がダウンストリームタスクでほぼ完全に成功する理由として,高次単語共起統計をモデル化できることを挙げる。
以上の結果から,純粋分布情報は,事前学習の成功を主に説明し,深い言語知識を必要とする難易度評価データセットのキュレーションの重要性を強調する。
論文 参考訳(メタデータ) (2021-04-14T06:30:36Z) - Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。
我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
論文 参考訳(メタデータ) (2021-02-11T18:59:24Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - Leap-Of-Thought: Teaching Pre-Trained Models to Systematically Reason
Over Implicit Knowledge [96.92252296244233]
大規模な事前学習言語モデル(LM)は推論能力を得るが、制御は困難である。
本研究では,暗黙的,事前学習された知識と明示的な自然言語文を併用して,体系的推論を確実に行うことができることを示す。
我々の研究は、シンプルな自然言語文を追加することで、モデルを簡単に修正できるユーザと対話することで、常に改善されるオープンドメインシステムへの道を開く。
論文 参考訳(メタデータ) (2020-06-11T17:02:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。