論文の概要: Clarifying Before Reasoning: A Coq Prover with Structural Context

• arxiv url: http://arxiv.org/abs/2507.02541v1
• Date: Thu, 03 Jul 2025 11:35:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-04 15:37:16.183339
• Title: Clarifying Before Reasoning: A Coq Prover with Structural Context
• Title（参考訳）: 推論前を明確にする - 構造的コンテキストを備えた Coq プロバー
• Authors: Yanzhen Lu, Hanbin Yang, Xiaodie Wang, Ge Zhang, Biao Li, Chenxu Fu, Chao Li, Yang Yuan, Andrew Chi-Chih Yao,
• Abstract要約: タスクの明度を評価するための概念レベルメトリクスを導入し、構造化された意味コンテキストを追加すると、明度スコアが1.85$times$改善されることを示す。 我々は15の標準Coqパッケージからランダムにサンプリングされた1,386の定理でこれを評価した。
• 参考スコア（独自算出の注目度）: 13.273599284897411
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this work, we investigate whether improving task clarity can enhance reasoning ability of large language models, focusing on theorem proving in Coq. We introduce a concept-level metric to evaluate task clarity and show that adding structured semantic context to the standard input used by modern LLMs, leads to a 1.85$\times$ improvement in clarity score (44.5\%~$\rightarrow$~82.3\%). Using the general-purpose model \texttt{DeepSeek-V3}, our approach leads to a 2.1$\times$ improvement in proof success (21.8\%~$\rightarrow$~45.8\%) and outperforms the previous state-of-the-art \texttt{Graph2Tac} (33.2\%). We evaluate this on 1,386 theorems randomly sampled from 15 standard Coq packages, following the same evaluation protocol as \texttt{Graph2Tac}. Furthermore, fine-tuning smaller models on our structured data can achieve even higher performance (48.6\%). Our method uses selective concept unfolding to enrich task descriptions, and employs a Planner--Executor architecture. These findings highlight the value of structured task representations in bridging the gap between understanding and reasoning.
• Abstract（参考訳）: 本研究では,タスクの明瞭度向上が大規模言語モデルの推論能力を向上するかどうかを考察し,コークにおける定理証明に焦点をあてる。 タスクの明度を評価するための概念レベルメトリクスを導入し、現代のLCMが使用する標準入力に構造化意味コンテキストを加えると、明度スコア(44.5\%~$\rightarrow$~82.3\%)が1.85$\times$改善されることを示す。 汎用モデル \texttt{DeepSeek-V3} を用いることで、2.1$\times$ の証明成功率 (21.8\%~$\rightarrow$~45.8\%) が向上し、従来の最先端の \texttt{Graph2Tac} (33.2\%) を上回った。 我々はこれを15の標準 Coq パッケージからランダムにサンプリングした 1,386 の定理で評価し,その評価プロトコルは \texttt{Graph2Tac} と同じである。 さらに、構造化データ上の細調整された小さなモデルは、さらに高いパフォーマンス(48.6\%)を達成することができる。 提案手法では,タスク記述を豊かにするために展開する選択概念を用い,Planner-Executorアーキテクチャを採用している。 これらの知見は、理解と推論のギャップを埋める上で、構造化されたタスク表現の価値を強調した。

関連論文リスト

• Syntactic Control of Language Models by Posterior Inference [53.823006836309695]
  言語モデルによって生成されたテキストの構文構造を制御することは、明快さ、スタイリスティックな一貫性、解釈可能性を必要とするアプリケーションにとって重要である。 後部推論に基づくサンプリングアルゴリズムは、生成中に対象の選挙区構造を効果的に強制することができると論じる。 提案手法では,提案分布からのサンプリングにより後続分布を推定するモンテカルロ法と,各生成したトークンが所望の構文構造に整合することを保証する統語タグを併用する。
  論文  参考訳（メタデータ） (2025-06-08T14:01:34Z)
• EquiBench: Benchmarking Large Language Models' Understanding of Program Semantics via Equivalence Checking [55.81461218284736]
  EquiBenchは、大規模言語モデル(LLM)を評価するための新しいベンチマークである。 2つのプログラムが全ての可能な入力に対して同一の出力を生成するかどうかを決定する。 19の最先端LCMを評価し、最高の精度は63.8%と76.2%であり、これは50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• CLOVER: A Test Case Generation Benchmark with Coverage, Long-Context, and Verification [71.34070740261072]
  本稿では,テストケースの生成と完成におけるモデルの能力を評価するためのベンチマークCLOVERを提案する。 ベンチマークはタスク間でのコード実行のためにコンテナ化されています。
  論文  参考訳（メタデータ） (2025-02-12T21:42:56Z)
• Contextualization Distillation from Large Language Model for Knowledge Graph Completion [51.126166442122546]
  我々は、差別的かつ生成的なKGCフレームワークと互換性のあるプラグイン・アンド・プレイ方式であるContextualization Distillation戦略を導入する。 提案手法は,大規模言語モデルに対して,コンパクトで構造的な三重項を文脈に富んだセグメントに変換するように指示することから始まる。 多様なデータセットとKGC技術にわたる総合的な評価は、我々のアプローチの有効性と適応性を強調している。
  論文  参考訳（メタデータ） (2024-01-28T08:56:49Z)
• An In-Context Learning Agent for Formal Theorem-Proving [10.657173216834668]
  我々は、LeanやCoqのような環境で、形式的定理コンテキストのためのコンテキスト内学習エージェントを提示します。 COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。 我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
  論文  参考訳（メタデータ） (2023-10-06T16:21:22Z)
• KERMIT: Knowledge Graph Completion of Enhanced Relation Modeling with Inverse Transformation [19.31783654838732]
  大規模言語モデルを用いてコヒーレントな記述を生成し,クエリと回答のセマンティックなギャップを埋める。 また、逆関係を利用して対称グラフを作成し、KGCのための強化トレーニングサンプルを提供する。 提案手法は,WN18RRではHit@1が4.2%,FB15k-237ではHit@3が3.4%向上し,優れた性能を示した。
  論文  参考訳（メタデータ） (2023-09-26T09:03:25Z)
• Text Classification via Large Language Models [63.1874290788797]
  テキスト分類に関わる複雑な言語現象に対処するために、Clue And Reasoning Prompting (CARP)を導入する。 注目すべきは、CARPが5つの広く使用されているテキスト分類ベンチマークのうち4つで新しいSOTAパフォーマンスを得ることだ。 さらに重要なのは、CARPが低リソースとドメイン適応のセットアップで素晴らしい能力を提供します。
  論文  参考訳（メタデータ） (2023-05-15T06:24:45Z)
• NLP-IIS@UT at SemEval-2021 Task 4: Machine Reading Comprehension using the Long Document Transformer [8.645929825516816]
  本稿では,SemEval-2021の4番目の課題である"Reading of Abstract Meaning"に関する技術的報告を紹介する。 このタスクでは、コンテキストが与えられた質問に基づいて正しい答えを予測します。 この問題に対処するために、Longformerモデルを使い、シーケンスをよりよく処理しました。
  論文  参考訳（メタデータ） (2021-05-08T20:48:32Z)

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

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