論文の概要: FormalAlign: Automated Alignment Evaluation for Autoformalization
- arxiv url: http://arxiv.org/abs/2410.10135v1
- Date: Mon, 14 Oct 2024 03:58:35 GMT
- ステータス: 処理完了
- システム内更新日: 2024-10-30 02:54:14.432419
- Title: FormalAlign: Automated Alignment Evaluation for Autoformalization
- Title（参考訳）: FormalAlign: オートフォーマル化のための自動アライメント評価
- Authors: Jianqiao Lu, Yingjia Wan, Yinya Huang, Jing Xiong, Zhengying Liu, Zhijiang Guo,
- Abstract要約: textscFormalAlignは、自動形式化シーケンス生成タスクと、入力と出力の間の表現アライメントの両方をトレーニングする。
textscFormalAlignは4つのベンチマークで評価され、優れたパフォーマンスを示している。
この効果的なアライメント評価は、手動検証の必要性を大幅に低減する。
- 参考スコア（独自算出の注目度）: 12.674957231226871
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Autoformalization aims to convert informal mathematical proofs into machine-verifiable formats, bridging the gap between natural and formal languages. However, ensuring semantic alignment between the informal and formalized statements remains challenging. Existing approaches heavily rely on manual verification, hindering scalability. To address this, we introduce \textsc{FormalAlign}, the first automated framework designed for evaluating the alignment between natural and formal languages in autoformalization. \textsc{FormalAlign} trains on both the autoformalization sequence generation task and the representational alignment between input and output, employing a dual loss that combines a pair of mutually enhancing autoformalization and alignment tasks. Evaluated across four benchmarks augmented by our proposed misalignment strategies, \textsc{FormalAlign} demonstrates superior performance. In our experiments, \textsc{FormalAlign} outperforms GPT-4, achieving an Alignment-Selection Score 11.58\% higher on \forml-Basic (99.21\% vs. 88.91\%) and 3.19\% higher on MiniF2F-Valid (66.39\% vs. 64.34\%). This effective alignment evaluation significantly reduces the need for manual verification. Both the dataset and code can be accessed via~\url{https://github.com/rookie-joe/FormalAlign}.
- Abstract（参考訳）: オートフォーマル化は、非公式な数学的証明を機械で検証可能な形式に変換し、自然言語と形式言語のギャップを埋めることを目的としている。
しかし、非公式な文と形式化された文のセマンティックアライメントを確保することは依然として困難である。
既存のアプローチは手動による検証に大きく依存しており、スケーラビリティを妨げる。
これを解決するために,自然言語と形式言語のアライメントを評価するために設計された最初の自動フレームワークである \textsc{FormalAlign} を紹介する。
\textsc{FormalAlign} は、オートフォーマル化シーケンス生成タスクと入力と出力の間の表現的アライメントの両方をトレーニングし、相互に強化されたオートフォーマル化とアライメントタスクのペアを組み合わせた二重損失を使用する。
提案手法によって強化された4つのベンチマークから評価し,より優れた性能を示す。
我々の実験では、textsc{FormalAlign} は GPT-4 より優れ、 \forml-Basic では 11.58 %、MiniF2F-Valid では 3.19 %(66.39 % 対 64.34 %) である。
この効果的なアライメント評価は、手動検証の必要性を大幅に低減する。
データセットとコードは、~\url{https://github.com/rookie-joe/FormalAlign}を介してアクセスすることができる。
関連論文リスト
- Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。
MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
論文 参考訳（メタデータ） (2024-10-28T11:37:39Z) - Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。
まず,人間のアノテーションに対するQASemConsistency法の有効性を示す。
そこで我々は,局所的な事実の不整合を自動的に検出するいくつかの手法を実装した。
論文 参考訳（メタデータ） (2024-10-09T22:53:48Z) - 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) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Improving Autoformalization using Type Checking [15.58948808529849]
大規模言語モデルは、自然言語を形式言語に自動翻訳するタスクである、自動形式化の約束を示す。
前回の報告では、Lean 3のCodexを使って達成されたProofNetの公式化ベンチマークのパフォーマンスが16.1%の非公式なステートメントの形式化に成功しただけだった。
解析の結果、これらのモデルの性能は、型チェックを成功させる形式的なステートメントを生成することができないため、大きく制限されていることがわかった。
論文 参考訳（メタデータ） (2024-06-11T13:01:50Z) - Process-Driven Autoformalization in Lean 4 [30.056591518828554]
大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。
また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。
実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
論文 参考訳（メタデータ） (2024-06-04T03:48:08Z) - Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。
1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。
自己形式化定理文の自動意味評価を行う。
論文 参考訳（メタデータ） (2024-05-27T14:35:10Z) - Autoformalization with Large Language Models [22.86710743804944]
自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。
大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。
我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
論文 参考訳（メタデータ） (2022-05-25T09:53:30Z) - Bi-level Alignment for Cross-Domain Crowd Counting [113.78303285148041]
現在の手法は、補助的なタスクを訓練したり、高価な粗大な見積もりを適用したりするための外部データに依存している。
そこで我々は, 簡易かつ効率的に適用可能な, 逆学習に基づく新しい手法を開発した。
実世界の5つのクラウドカウントベンチマークに対するアプローチを評価し、既存のアプローチを大きなマージンで上回ります。
論文 参考訳（メタデータ） (2022-05-12T02:23:25Z) - Text Revision by On-the-Fly Representation Optimization [76.11035270753757]
現在の最先端手法は、これらのタスクをシーケンスからシーケンスまでの学習問題として定式化している。
並列データを必要としないテキストリビジョンのための反復的なインプレース編集手法を提案する。
テキストの単純化に関する最先端の教師付き手法よりも、競争力があり、パフォーマンスも向上する。
論文 参考訳（メタデータ） (2022-04-15T07:38:08Z) - Automatic Extraction of Rules Governing Morphological Agreement [103.78033184221373]
原文から第一パス文法仕様を抽出する自動フレームワークを開発する。
我々は、世界の多くの言語の文法の中核にあるモルフォシンタクティックな現象である合意を記述する規則の抽出に焦点をあてる。
我々のフレームワークはUniversal Dependenciesプロジェクトに含まれるすべての言語に適用され、有望な結果が得られます。
論文 参考訳（メタデータ） (2020-10-02T18:31:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。