論文の概要: Process-Driven Autoformalization in Lean 4
- arxiv url: http://arxiv.org/abs/2406.01940v2
- Date: Mon, 14 Oct 2024 03:46:00 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-10-15 15:03:46.101514
- Title: Process-Driven Autoformalization in Lean 4
- Title（参考訳）: リーン4におけるプロセス駆動の自動化
- Authors: Jianqiao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, Zhicheng Yang, Jing Tang, Zhijiang Guo,
- Abstract要約: 大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。
また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。
実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
- 参考スコア（独自算出の注目度）: 30.056591518828554
- License:
- Abstract: Autoformalization, the conversion of natural language mathematics into formal languages, offers significant potential for advancing mathematical reasoning. However, existing efforts are limited to formal languages with substantial online corpora and struggle to keep pace with rapidly evolving languages like Lean 4. To bridge this gap, we propose a new benchmark \textbf{Form}alization for \textbf{L}ean~\textbf{4} (\textbf{\name}) designed to evaluate the autoformalization capabilities of large language models (LLMs). This benchmark encompasses a comprehensive assessment of questions, answers, formal statements, and proofs. Additionally, we introduce a \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{PSV}) model that leverages the precise feedback from Lean 4 compilers to enhance autoformalization. Our experiments demonstrate that the PSV method improves autoformalization, enabling higher accuracy using less filtered training data. Furthermore, when fine-tuned with data containing detailed process information, PSV can leverage the data more effectively, leading to more significant improvements in autoformalization for Lean 4. Our dataset and code are available at \url{https://github.com/rookie-joe/PDA}.
- Abstract（参考訳）: 自然言語を形式言語に変換するオートフォーマル化は、数学的推論を前進させる大きな可能性を秘めている。
しかし、既存の取り組みは、実質的なオンラインコーパスを持つフォーマルな言語に限られており、Lean 4.0のような急速に進化する言語とペースを維持するのに苦労している。
このギャップを埋めるために,大規模言語モデル(LLM)の自動形式化機能を評価するために設計された,新しいベンチマークである \textbf{L}ean~\textbf{4} (\textbf{\name}) を提案する。
このベンチマークは、質問、回答、公式なステートメント、証明の総合的な評価を含んでいる。
さらに、リーン4コンパイラからの正確なフィードバックを活用してオートフォーマル化を強化する、 \textbf{P}rocess-\textbf{S}upervised \textbf{V}erifier (\textbf{PSV})モデルを導入する。
実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
さらに、詳細なプロセス情報を含むデータを微調整すると、PSVはより効率的にデータを活用することができ、Lean 4.0のオートフォーマライゼーションが大幅に改善される。
データセットとコードは \url{https://github.com/rookie-joe/PDA} で利用可能です。
関連論文リスト
- FormalAlign: Automated Alignment Evaluation for Autoformalization [12.674957231226871]
textscFormalAlignは、自動形式化シーケンス生成タスクと、入力と出力の間の表現アライメントの両方をトレーニングする。
textscFormalAlignは4つのベンチマークで評価され、優れたパフォーマンスを示している。
この効果的なアライメント評価は、手動検証の必要性を大幅に低減する。
論文 参考訳（メタデータ） (2024-10-14T03:58:35Z) - Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
本稿では,Mathlib4コーパス(形式言語Lean 4における数学の統一ライブラリ)を自然言語に翻訳するための新しいフレームワークを提案する。
私たちはこのパイプラインの結果をHeraldとしてMathlib4で発表します(階層とレトリバルベースのトランスレーショナルリーン)。
また,Heraldを微調整したHerald Translatorを提案する。
論文 参考訳（メタデータ） (2024-10-09T10:11:24Z) - FactAlign: Long-form Factuality Alignment of Large Language Models [35.067998820937284]
大規模言語モデルは次世代の情報アクセスエンジンとして大きな可能性を示している。
本稿では,FactAlignを提案する。FactAlignは,長文応答の現実性を高めるために設計された,新しいアライメントフレームワークである。
オープンドメインのプロンプトと情報検索に関する実験により、FactAlignはLLM応答の事実精度を大幅に向上することを示した。
論文 参考訳（メタデータ） (2024-10-02T16:03:13Z) - Boosting the Capabilities of Compact Models in Low-Data Contexts with Large Language Models and Retrieval-Augmented Generation [2.9921619703037274]
本稿では,形態素解析の言語タスクにおいて,より小さなモデルの出力を補正するために,大言語モデル(LLM)を基盤とした検索拡張生成(RAG)フレームワークを提案する。
データ不足や訓練可能なパラメータの不足を補うために,言語情報を活用するとともに,LLMを通して解釈・蒸留された記述文法からの入力を許容する。
コンパクトなRAG支援モデルがデータスカース設定に極めて有効であることを示し、このタスクとターゲット言語に対する新しい最先端技術を実現する。
論文 参考訳（メタデータ） (2024-10-01T04:20:14Z) - SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳（メタデータ） (2024-08-28T06:33:03Z) - Lean Workbook: A large-scale Lean problem set formalized from natural language math problems [50.22847430754973]
大規模な言語モデルは、リーンのような形式言語を使って証明する数学の定理が得意ではありません。
この領域で重要な課題は、これらの形式言語で利用可能なトレーニングデータの不足である。
本稿では,自然言語の数学的問題をリーン4文に変換するために,合成データを反復的に生成・フィルタリングするパイプラインを提案する。
論文 参考訳（メタデータ） (2024-06-06T08:25:43Z) - Calibrating the Confidence of Large Language Models by Eliciting Fidelity [52.47397325111864]
RLHFのようなテクニックで最適化された大規模な言語モデルは、有用で無害な点において優れた整合性を実現している。
調整後、これらの言語モデルはしばしば過剰な自信を示し、表現された自信は正確さの度合いで正確に校正しない。
本稿では,言語モデルの信頼度を推定するプラグイン・アンド・プレイ手法を提案する。
論文 参考訳（メタデータ） (2024-04-03T11:36:12Z) - RegaVAE: A Retrieval-Augmented Gaussian Mixture Variational Auto-Encoder
for Language Modeling [79.56442336234221]
可変オートエンコーダ(VAE)に基づく検索拡張言語モデルであるRegaVAEを紹介する。
テキストコーパスを潜在空間にエンコードし、ソースとターゲットの両方のテキストから現在と将来の情報をキャプチャする。
各種データセットに対する実験結果から,テキスト生成品質と幻覚除去の大幅な改善が示された。
論文 参考訳（メタデータ） (2023-10-16T16:42:01Z) - Large Language Models Meet Knowledge Graphs to Answer Factoid Questions [57.47634017738877]
本稿では,知識グラフから追加情報に富んだ事前学習されたテキスト・テキスト言語モデルを探索する手法を提案する。
抽出した部分グラフの線形化によりトランスフォーマーモデルで容易に情報を得る。
抽出された情報で回答候補を最終ランク付けすると、事前訓練されたテキスト-テキスト言語モデルのHits@1スコアが4-6%向上する。
論文 参考訳（メタデータ） (2023-10-03T15:57:00Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z) - Efficient Nearest Neighbor Language Models [114.40866461741795]
非パラメトリックニューラルネットワークモデル(NLM)は、外部データストアを用いてテキストの予測分布を学習する。
比較性能を維持しながら、推論速度の最大6倍の高速化を実現する方法を示す。
論文 参考訳（メタデータ） (2021-09-09T12:32:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。