Fugu-MT 論文翻訳(概要): Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

論文の概要: Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs

arxiv url: http://arxiv.org/abs/2507.04719v1
Date: Mon, 07 Jul 2025 07:27:45 GMT
ステータス: 翻訳完了
システム内更新日: 2025-07-08 15:46:35.309763
Title: Advocate for Complete Benchmarks for Formal Reasoning with Formal/Informal Statements and Formal/Informal Proofs
Title（参考訳）: 形式的/インフォーマルな文と形式的/インフォーマルな証明を用いた形式的推論のための完全ベンチマークの提唱
Authors: Roozbeh Yousefzadeh, Xuenan Cao,
Abstract要約: 私たちは、オープンコード、オープンデータ、そして、完全でエラーのないベンチマークがこの分野の進歩を加速する立場を取っています。私たちは、この分野に貢献するための障壁を生み出すプラクティスを特定し、それらを取り除く方法を提案します。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: This position paper provides a critical but constructive discussion of current practices in benchmarking and evaluative practices in the field of formal reasoning and automated theorem proving. We take the position that open code, open data, and benchmarks that are complete and error-free will accelerate progress in this field. We identify practices that create barriers to contributing to this field and suggest ways to remove them. We also discuss some of the practices that might produce misleading evaluative information. We aim to create discussions that bring together people from various groups contributing to automated theorem proving, autoformalization, and informal reasoning.
Abstract（参考訳）: 本稿では,形式的推論と自動定理証明の分野におけるベンチマークと評価の実践に関する,批判的かつ建設的な議論を提供する。オープンコード、オープンデータ、そして完全かつエラーのないベンチマークがこの分野の進歩を加速する位置にある。私たちは、この分野に貢献するための障壁を生み出すプラクティスを特定し、それらを取り除く方法を提案します。また、誤解を招く評価情報を生み出すかもしれないプラクティスについても論じる。我々は, 自動定理証明, 自己形式化, 非公式推論に寄与する様々なグループの人々を集めて議論することを目指している。

関連論文リスト

Beyond Agreement: Rethinking Ground Truth in Educational AI Annotation [1.8434042562191815]
我々は、注釈品質ハッパーのゲートキーパーとしての人間間信頼性(IRR)への過度な依存が、データの分類に進展していると論じる。本稿では,マルチラベルアノテーションスキーム,エキスパートベースアプローチ,クローズ・ザ・ループの有効性など,補完的な評価手法の5つの例を紹介する。我々は、アノテーションの品質と基礎的真実を再考し、合意のみに対する妥当性と教育的影響を優先することを求める。
論文参考訳（メタデータ） (2025-07-31T20:05:26Z)
Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning [8.135142928659546]
自動形式化タスクを評価するための,体系的かつ自動的な手法を提案する。提案手法は,論理的保存(LP),数学的整合性(MC),形式的妥当性(FV),形式的品質(FQ)を基準とした審査員のアンサンブルに基づく。全体としては,LLM審査員のEFGアンサンブルが評価に好適であることを示す。
論文参考訳（メタデータ） (2025-06-12T17:09:51Z)
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)
Improving Autoformalization using Type Checking [15.58948808529849]
我々は、現在の自己形式化手法とそれらの評価に使用されるプロセスの両方を分析し、特にLean 4の定理証明言語に注目します。 ProofNetの絶対精度は18.4%まで向上し,既存の手法上での自己整合性による型チェックフィルタリングが性能を著しく向上することを示した。我々はまた、新しい研究レベルの数学データセット RLM25、修正されたProofNet、ラベル付き正誤オートフォーマライゼーションペアでメトリクスを評価するProofNetVerifといった新しいベンチマークもリリースした。
論文参考訳（メタデータ） (2024-06-11T13:01:50Z)
DELTA: Pre-train a Discriminative Encoder for Legal Case Retrieval via Structural Word Alignment [55.91429725404988]
判例検索のための識別モデルであるDELTAを紹介する。我々は浅層デコーダを利用して情報ボトルネックを作り、表現能力の向上を目指しています。本手法は, 判例検索において, 既存の最先端手法よりも優れている。
論文参考訳（メタデータ） (2024-03-27T10:40:14Z)
A Unifying Framework for Learning Argumentation Semantics [47.84663434179473]
Inductive Logic Programmingアプローチを用いて、抽象的および構造化された議論フレームワークのアクセシビリティセマンティクスを解釈可能な方法で学習する新しいフレームワークを提案する。提案手法は既存の議論解法よりも優れており,フォーマルな議論や人間と機械の対話の領域において,新たな研究の方向性が開けることになる。
論文参考訳（メタデータ） (2023-10-18T20:18:05Z)
Abductive Commonsense Reasoning Exploiting Mutually Exclusive Explanations [118.0818807474809]
帰納的推論は、イベントのもっともらしい説明を見つけることを目的としている。自然言語処理における帰納的推論のための既存のアプローチは、しばしば監督のために手動で生成されたアノテーションに依存している。この研究は、ある文脈に対して、説明のサブセットのみが正しいという事実を活用する、帰納的コモンセンス推論のアプローチを提案する。
論文参考訳（メタデータ） (2023-05-24T01:35:10Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Probing as Quantifying the Inductive Bias of Pre-trained Representations [99.93552997506438]
本稿では,特定のタスクに対する表現の帰納的バイアスを評価することを目的とした,探索のための新しいフレームワークを提案する。トークン、アーク、文レベルの一連のタスクに我々のフレームワークを適用します。
論文参考訳（メタデータ） (2021-10-15T22:01:16Z)

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