論文の概要: Improving Autoformalization using Type Checking

• arxiv url: http://arxiv.org/abs/2406.07222v1
• Date: Tue, 11 Jun 2024 13:01:50 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-12 16:03:55.298998
• Title: Improving Autoformalization using Type Checking
• Title（参考訳）: 型チェックによる自動書式化の改善
• Authors: Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut,
• Abstract要約: 大規模言語モデルは、自然言語を形式言語に自動翻訳するタスクである、自動形式化の約束を示す。 前回の報告では、Lean 3のCodexを使って達成されたProofNetの公式化ベンチマークのパフォーマンスが16.1%の非公式なステートメントの形式化に成功しただけだった。 解析の結果、これらのモデルの性能は、型チェックを成功させる形式的なステートメントを生成することができないため、大きく制限されていることがわかった。
• 参考スコア（独自算出の注目度）: 15.58948808529849
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models show promise for autoformalization, the task of automatically translating natural language into formal languages. However, current autoformalization methods remain limited. The last reported state-of-the-art performance on the ProofNet formalization benchmark for the Lean proof assistant, achieved using Codex for Lean 3, only showed successful formalization of 16.1% of informal statements. Similarly, our evaluation of GPT-4o for Lean 4 only produces successful translations 34.9% of the time. Our analysis shows that the performance of these models is largely limited by their inability to generate formal statements that successfully type-check (i.e., are syntactically correct and consistent with types) - with a whopping 86.6% of GPT-4o errors starting from a type-check failure. In this work, we propose a method to fix this issue through decoding with type-check filtering, where we initially sample a diverse set of candidate formalizations for an informal statement, then use the Lean proof assistant to filter out candidates that do not type-check. Using GPT-4o as a base model, and combining our method with self-consistency, we obtain a +18.3% absolute increase in formalization accuracy, and achieve a new state-of-the-art of 53.2% on ProofNet with Lean 4.
• Abstract（参考訳）: 大規模言語モデルは、自然言語を形式言語に自動翻訳するタスクである、自動形式化の約束を示す。 しかし、現在の自己形式化法は依然として限られている。 前回の報告では、Lean 3のCodexを使って達成されたProofNetの公式化ベンチマークのパフォーマンスが16.1%の非公式なステートメントの形式化に成功しただけだった。 同様に、リーン4に対するGPT-4oの評価は34.9%しか成功していない。 我々の分析によると、これらのモデルの性能は、型チェックを成功させるフォーマルなステートメントを生成できないこと(つまり、構文的に正しく、型と整合性がある)によって大きく制限されており、GPT-4oエラーの86.6%は、型チェックの失敗から始まっている。 本稿では,型チェックによるデコードによるこの問題の解決手法を提案する。まず最初に,非公式な文に対するさまざまな候補の形式化をサンプルし,次にリーン証明アシスタントを用いて型チェックを行わない候補をフィルタリングする。 GPT-4oをベースモデルとして使用し、我々のメソッドと自己整合性を組み合わせることで、形式化の精度が+18.3%向上し、ProofNetとLean 4.0で53.2%の新しい最先端を実現する。

関連論文リスト

• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• FormalAlign: Automated Alignment Evaluation for Autoformalization [12.674957231226871]
  textscFormalAlignは、自動形式化シーケンス生成タスクと、入力と出力の間の表現アライメントの両方をトレーニングする。 textscFormalAlignは4つのベンチマークで評価され、優れたパフォーマンスを示している。 この効果的なアライメント評価は、手動検証の必要性を大幅に低減する。
  論文  参考訳（メタデータ） (2024-10-14T03:58:35Z)
• Process-Driven Autoformalization in Lean 4 [30.056591518828554]
  大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。 また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。 実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
  論文  参考訳（メタデータ） (2024-06-04T03:48:08Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Calibrating the Confidence of Large Language Models by Eliciting Fidelity [52.47397325111864]
  RLHFのようなテクニックで最適化された大規模な言語モデルは、有用で無害な点において優れた整合性を実現している。 調整後、これらの言語モデルはしばしば過剰な自信を示し、表現された自信は正確さの度合いで正確に校正しない。 本稿では,言語モデルの信頼度を推定するプラグイン・アンド・プレイ手法を提案する。
  論文  参考訳（メタデータ） (2024-04-03T11:36:12Z)
• GPT-HateCheck: Can LLMs Write Better Functional Tests for Hate Speech Detection? [50.53312866647302]
  HateCheckは、合成データに対してきめ細かいモデル機能をテストするスイートである。 GPT-HateCheckは,スクラッチからより多彩で現実的な機能テストを生成するフレームワークである。 クラウドソースのアノテーションは、生成されたテストケースが高品質であることを示しています。
  論文  参考訳（メタデータ） (2024-02-23T10:02:01Z)
• Towards AI-Assisted Synthesis of Verified Dafny Methods [1.0187122752343796]
  既存の大規模言語モデルでは、検証プログラムの習熟度が著しく低下している。 Dafny検証対応言語における2つの事前学習モデルの習熟度を改善する方法を示す。
  論文  参考訳（メタデータ） (2024-02-01T00:07:23Z)
• Benchmarking and Improving Generator-Validator Consistency of Language Models [82.73914625520686]
  言語モデル(LM)において、解答の生成と検証が一般的である矛盾 最先端のLMであるGPT-4でさえ、GVとの共存率はわずか76%である。 このアプローチはAlpaca-30BのGV一貫性を60%から93%に向上させる。
  論文  参考訳（メタデータ） (2023-10-03T07:23:22Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)
• TuringAdvice: A Generative and Dynamic Evaluation of Language Use [90.3029315711237]
  言語理解モデルのための新しい課題タスクとデータセットであるTuringAdviceを提案する。 現実の人が現在直面している記述された状況を考えると、モデルは自然言語で有益なアドバイスを生成する必要がある。 実証的な結果は、今日のモデルがTuringAdviceで苦労していることを示している。
  論文  参考訳（メタデータ） (2020-04-07T18:00:03Z)

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

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