論文の概要: Improving Autoformalization using Type Checking

• arxiv url: http://arxiv.org/abs/2406.07222v2
• Date: Tue, 11 Feb 2025 11:02:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-12 14:05:21.842790
• Title: Improving Autoformalization using Type Checking
• Title（参考訳）: 型チェックによる自動書式化の改善
• Authors: Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut,
• Abstract要約: 我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
• 参考スコア（独自算出の注目度）: 15.58948808529849
• License:
• Abstract: Autoformalization, the automatic translation of unconstrained natural language into formal languages, has garnered significant attention due to its potential applications in theorem proving, formal verification, and LLM output checking. In this work, we analyze both current autoformalization methods and the processes used to evaluate them, focusing specifically on the Lean 4 theorem proving language. We demonstrate that scaling type-check filtering with self-consistency techniques on top of existing methods significantly improves performance, achieving absolute accuracy gains of up to +18.4\% on ProofNet. To support reproducibility and further research, we release our code, including new symbolic equivalence for Lean formulas. We also release new benchmarks: a new research-level mathematics dataset RLM25, a corrected ProofNet, and ProofNetVerif with labeled correct and incorrect autoformalization pairs for evaluating metrics.
• Abstract（参考訳）: 制約のない自然言語を形式言語に自動翻訳するオートフォーマル化は、定理証明、形式検証、LLM出力チェックの潜在的な応用により、大きな注目を集めている。 本研究では、現在の自己形式化手法と、それらを評価するために使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetでは,既存の手法上での自己整合性による型チェックフィルタのスケーリングにより性能が大幅に向上し,絶対精度が+18.4\%に達することが実証された。 再現性とさらなる研究をサポートするため、私たちは、リーンの公式に対する新しい象徴的等価性を含むコードを公開しています。 我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。

関連論文リスト

• 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)

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

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