論文の概要: Learning to Prove Trigonometric Identities
- arxiv url: http://arxiv.org/abs/2207.06679v1
- Date: Thu, 14 Jul 2022 06:16:17 GMT
- ステータス: 処理完了
- システム内更新日: 2022-07-16 02:23:31.790792
- Title: Learning to Prove Trigonometric Identities
- Title(参考訳): 三角性を証明するための学習
- Authors: Zhou Liu, Yujun Li, Zhengying Liu, Lin Li, Zhenguo Li
- Abstract要約: 我々は三角法等式の自動証明システムを構築した。
私たちのゴールは、証明を完成させるだけでなく、できるだけ少数のステップで証明を完成させることです。
強化学習によってさらなる改善が加えられたAutoTrigは、BFSと同じくらいの短いステップで、アイデンティティの証明ステップを提供することができる。
- 参考スコア(独自算出の注目度): 36.56548303496931
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Automatic theorem proving with deep learning methods has attracted attentions
recently. In this paper, we construct an automatic proof system for
trigonometric identities. We define the normalized form of trigonometric
identities, design a set of rules for the proof and put forward a method which
can generate theoretically infinite trigonometric identities. Our goal is not
only to complete the proof, but to complete the proof in as few steps as
possible. For this reason, we design a model to learn proof data generated by
random BFS (rBFS), and it is proved theoretically and experimentally that the
model can outperform rBFS after a simple imitation learning. After further
improvement through reinforcement learning, we get AutoTrig, which can give
proof steps for identities in almost as short steps as BFS (theoretically
shortest method), with a time cost of only one-thousandth. In addition,
AutoTrig also beats Sympy, Matlab and human in the synthetic dataset, and
performs well in many generalization tasks.
- Abstract(参考訳): 近年,ディープラーニング手法による自動定理証明が注目されている。
本稿では,三角法等式の自動証明システムを構築する。
三角idの正規化形式を定義し、証明のための一連のルールを設計し、理論上無限の三角idを生成できる方法を提唱する。
私たちの目標は、証明を完遂するだけでなく、可能な限り少数のステップで証明を完成させることです。
そこで我々は,ランダムなBFS(rBFS)によって生成された証明データを学習するモデルを設計し,そのモデルが単純な模倣学習後にrBFSより優れていることを理論的・実験的に証明した。
強化学習によるさらなる改善により、autotrigはbfs(理論上最も短い方法)とほぼ同等の短時間で識別の証明ステップを、わずか1分の1の時間コストで得ることができる。
さらにAutoTrigは、合成データセットでSympy、Matlab、人間を破り、多くの一般化タスクでうまく機能する。
関連論文リスト
- 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) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳(メタデータ) (2023-03-08T22:00:15Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳(メタデータ) (2022-05-25T02:22:30Z) - Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。
本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。
私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
論文 参考訳(メタデータ) (2021-03-05T17:01:34Z) - Learning to Prove from Synthetic Theorems [41.74768503409581]
自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。
このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
論文 参考訳(メタデータ) (2020-06-19T17:48:09Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。