論文の概要: 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%の新しい最先端を実現する。

関連論文リスト

• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency [22.86318578119266]
  そこで我々は,記号的同値性と意味的整合性に基づいて,k個の自己形式化候補から最良の結果をスコアし,選択する新しいフレームワークを提案する。 MATHおよびminiF2Fデータセットに対する実験により,本手法は自己形式化精度を大幅に向上させることが示された。
  論文  参考訳（メタデータ） (2024-10-28T11:37:39Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人間による証明の欠如を克服する新しいフレームワークであるSAFEを紹介します。 GPT-4oに比べて効率と精度が優れていた。 この進歩により性能が大幅に向上し、人間の専門家によるベンチマークで70.50%の精度が達成された。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• 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)
• Process-Driven Autoformalization in Lean 4 [30.056591518828554]
  大規模言語モデルの自己形式化能力を評価するためのベンチマークを開発する。 また、Lean 4コンパイラからの正確なフィードバックを利用して自動形式化を強化するモデルも導入しています。 実験の結果,PSV法ではオートフォーマライゼーションが向上し,フィルタの少ないトレーニングデータによる精度が向上した。
  論文  参考訳（メタデータ） (2024-06-04T03:48:08Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Unsupervised Pretraining for Fact Verification by Language Model Distillation [4.504050940874427]
  SFAVEL (Self-supervised Fact Verification via Language Model Distillation) は,教師なし事前学習フレームワークである。 アノテーションを必要とせずに、自己管理機能を高品質なクレーム-ファクトアライメントに分解する。 これは、特徴が高品質なクレームとエビデンスアライメントを達成することを奨励する、新しい対照的な損失関数によって実現されている。
  論文  参考訳（メタデータ） (2023-09-28T15:53:44Z)
• Autoformalization with Large Language Models [22.86710743804944]
  自動形式化システムの成功は、形式検証、プログラム合成、人工知能の分野を前進させる可能性がある。 大規模な言語モデルがこの目標に向けて新たな展望を提供することを示す。 我々の手法はMiniF2F定理証明ベンチマークで新たな最先端結果をもたらし、証明レートを29.6%から35.2%に改善した。
  論文  参考訳（メタデータ） (2022-05-25T09:53:30Z)

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

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