論文の概要: ${\rm P{\small ROOF}W{\small ALA}}$: Multilingual Proof Data Synthesis and Theorem-Proving

• arxiv url: http://arxiv.org/abs/2502.04671v1
• Date: Fri, 07 Feb 2025 05:35:46 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-10 14:57:19.487569
• Title: ${\rm P{\small ROOF}W{\small ALA}}$: Multilingual Proof Data Synthesis and Theorem-Proving
• Title（参考訳）: ${\rm P{\small ROOF}W{\small ALA}}$:多言語証明データ合成と定理証明
• Authors: Amitayush Thakur, George Tsoukalas, Greg Durrett, Swarat Chaudhuri,
• Abstract要約: $rm P Small ROOFWsmall ALA$と呼ばれるフレームワークは、ニューラル定理プロデューサと2つの確立された対話的証明アシスタント間の相互作用を可能にする。 私たちは、$rm P Small ROOFWsmall ALA$生成のCoqとLeanのデータの組み合わせでトレーニングされたモデルが、標準のprov-at-k$メトリック上で、Lean-onlyとCoq-onlyのモデルを上回っていることを示します。
• 参考スコア（独自算出の注目度）: 53.67926215943612
• License:
• Abstract: Neural networks have shown substantial promise at automatic theorem-proving in interactive proof assistants (ITPs) like Lean and Coq. However, most neural theorem-proving models are restricted to specific ITPs, leaving out opportunities for cross-lingual $\textit{transfer}$ between ITPs. We address this weakness with a multilingual proof framework, ${\rm P{\small ROOF}W{\small ALA}}$, that allows a standardized form of interaction between neural theorem-provers and two established ITPs (Coq and Lean). It enables the collection of multilingual proof step data -- data recording the result of proof actions on ITP states -- for training neural provers. ${\rm P{\small ROOF}W{\small ALA}}$ allows the systematic evaluation of a model's performance across different ITPs and problem domains via efficient parallel proof search algorithms. We show that multilingual training enabled by ${\rm P{\small ROOF}W{\small ALA}}$ can lead to successful transfer across ITPs. Specifically, a model trained on a mix of ${\rm P{\small ROOF}W{\small ALA}}$-generated Coq and Lean data outperforms Lean-only and Coq-only models on the standard prove-at-$k$ metric. We open source all code including code for the $\href{https://github.com/trishullab/proof-wala}{ProofWala\; Framework}$, and the $\href{https://github.com/trishullab/itp-interface}{Multilingual\; ITP\; interaction\; framework}$.
• Abstract（参考訳）: ニューラルネットワークは、LeanやCoqのような対話型証明アシスタント(ITP)において、自動定理証明において大きな可能性を示してきた。 しかしながら、ほとんどのニューラル定理証明モデルは特定のIPPに制限されており、IPP間の相互言語的$\textit{transfer}$の機会は残されている。 この弱点を多言語証明フレームワークである${\rm P{\small ROOF}W{\small ALA}}$で解決する。 これは、神経プローバのトレーニングのための多言語証明ステップデータ(IPP状態の証明アクションの結果を記録するデータ)の収集を可能にする。 ${\rm P{\small ROOF}W{\small ALA}}$は、効率的な並列証明探索アルゴリズムを用いて、異なるIPPと問題領域にわたるモデルの性能を体系的に評価することを可能にする。 我々は,${\rm P{\small ROOF}W{\small ALA}}$によって実現された多言語学習が,IPP間の転送を成功させることを示す。 具体的には、${\rm P{\small ROOF}W{\small ALA}}$生成のCoqとLeanのデータの組み合わせでトレーニングされたモデルは、標準のprov-at-k$メトリック上で、LeanのみのモデルとCoqのみのモデルを上回ります。 私たちは$\href{https://github.com/trishullab/proof-wala}{ProofWala\; Framework}$と$\href{https://github.com/trishullab/itp-interface}{Multilingual\; ITP\; Interaction\; framework}$のコードを含むすべてのコードをオープンソースにしています。

関連論文リスト

• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• Transfer Q Star: Principled Decoding for LLM Alignment [105.89114186982972]
  Transfer $Q*$は、ベースラインモデルを通してターゲット報酬$r$の最適値関数を推定する。 提案手法は, 従来のSoTA法で観測された準最適差を著しく低減する。
  論文  参考訳（メタデータ） (2024-05-30T21:36:12Z)
• Learning (Very) Simple Generative Models Is Hard [45.13248517769758]
  我々は,$mathbbRdtobbRd'$の出力座標が$mathrmpoly(d)$ニューロンを持つ一層ReLUネットワークである場合でも,リアルタイムアルゴリズムが問題を解決可能であることを示す。 我々の証明の鍵となる要素は、コンパクトに支持されたピースワイズ線形関数$f$をニューラルネットワークで束ねたスロープで構築することであり、$mathcalN(0,1)$のプッシュフォワードは$mathcalのすべての低度モーメントと一致する。
  論文  参考訳（メタデータ） (2022-05-31T17:59:09Z)
• Distributed Sparse Feature Selection in Communication-Restricted Networks [6.9257380648471765]
  疎線形回帰と特徴選択のための新しい分散スキームを提案し,理論的に解析する。 データセット全体から因果次元を推定するために,ネットワーク内の情報共有をシンプルかつ効果的に行う手法を提案する。
  論文  参考訳（メタデータ） (2021-11-02T05:02:24Z)
• On the Power of Multitask Representation Learning in Linear MDP [61.58929164172968]
  本稿では,線形マルコフ決定過程(MDP)におけるマルチタスク表現学習の統計的メリットについて分析する。 簡単な最小二乗アルゴリズムが $tildeO(H2sqrtfrackappa MathcalC(Phi)2 kappa dNT+frackappa dn) というポリシーを学ぶことを証明した。
  論文  参考訳（メタデータ） (2021-06-15T11:21:06Z)
• RNNs can generate bounded hierarchical languages with optimal memory [113.73133308478612]
  RNNは、自然言語構文の足場を反映した境界階層言語を効率的に生成できることを示す。 Dyck-($k$,$m$)は、よくネストされた括弧($k$型)と$m$バウンドされたネスト深さの言語である。 明示的な構成により,$O(m log k)$ hidden units の RNN がメモリの指数的削減に十分であることを示す。
  論文  参考訳（メタデータ） (2020-10-15T04:42:29Z)
• Improving Robustness and Generality of NLP Models Using Disentangled Representations [62.08794500431367]
  スーパービジョンニューラルネットワークはまず入力$x$を単一の表現$z$にマップし、次に出力ラベル$y$にマッピングする。 本研究では,非交叉表現学習の観点から,NLPモデルの堅牢性と汎用性を改善する手法を提案する。 提案した基準でトレーニングしたモデルは、広範囲の教師付き学習タスクにおいて、より堅牢性とドメイン適応性を向上することを示す。
  論文  参考訳（メタデータ） (2020-09-21T02:48:46Z)

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

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