論文の概要: claimcheck: Measuring and Improving Specification Faithfulness

• arxiv url: http://arxiv.org/abs/2610.17358v1
• Date: Mon, 12 Oct 2026 20:14:51 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-15 21:06:15.449394
• Title: claimcheck: Measuring and Improving Specification Faithfulness
• Title（参考訳）: クレームチェック:仕様の忠実度の測定と改善
• Abstract要約: 自然言語の要件と形式的なアーティファクトのギャップを計測する。 行の3分の1は、忠実なラベルを保持するアーティファクトの意味保存の書き直しである。 不正な形式化を検出するツールであるクレームチェックを導入する。
• 参考スコア（独自算出の注目度）: 35.18016233072556
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Formal verification proves that a program satisfies its specification, but says nothing about whether the specification captures what the author meant. As LLMs increasingly write both code and specifications, a gap between the author's natural-language requirement and the specification becomes a live risk. A machine-checked proof of a property narrower than the one requested is worthless but passes every check. Closing this gap is solving the spec formalization problem: given a natural-language requirement, produce a formal artifact whose meaning matches it. To measure the gap, we curate an end-to-end benchmark for spec formalization spanning four formal languages: Dafny contracts and Lean 4, Isabelle and Rocq theorem statements. Each of its 3,234 rows pairs a natural-language requirement with a formal artifact and a label established by execution, by proof, or by the benchmark it is drawn from. A third of the rows are meaning-preserving rewrites of the artifact that keep the faithful label, so a judge cannot score by detecting that a row was edited. We introduce claimcheck, a tool that detects incorrect formalizations: the formal artifact is translated back into plain English by a model that never sees the requirement, and a separate model, the judge, decides whether the informalization and the requirement express the same guarantee. On all four languages it gains 8.2 to 9.8 points of macro recall over a single call shown the requirement and the artifact, and 4.2 to 6.0 over that call handed the same list of meaning-preserving rewrites. Showing the judge the artifact as well costs 1.4 to 4.5 points. Across four judges that also see the artifact, the gain shrinks as the judge gets stronger, to within a point of the informed single call for the strongest.
• Abstract（参考訳）: 形式的検証は、プログラムが仕様を満たすことを証明しますが、仕様が著者が意味するところを捉えているかどうかについては何も述べていません。 LLMがコードと仕様の両方を書くようになると、著者の自然言語要求と仕様とのギャップが生のリスクとなる。 要求されたものよりも狭いプロパティのマシンチェックによる証明は価値がないが、すべてのチェックをパスする。 このギャップを埋めることによって仕様の形式化が解決される: 自然言語の要件が与えられたら、その意味が一致する形式的なアーティファクトを生成する。 このギャップを測定するために、Dafny契約とLean 4、Isabelle、Rocqの4つの形式言語にまたがる仕様の形式化のためのエンドツーエンドのベンチマークをキュレートする。 それぞれの3,234行は、形式的なアーティファクトと、実行、証明、ベンチマークによって確立されたラベルと、自然言語要件をペアリングする。 行の3分の1は、忠実なラベルを保持するアーティファクトの意味保存の書き直しであるので、審査員は行が編集されたことを検知して得点することができない。 形式的アーティファクトは、要求を決して見ないモデルによって平易な英語に変換され、裁判官は、非公式化と要件が同じ保証を表現しているかどうかを判断する。 4つの言語で1回の呼び出しで8.2から9.8ポイントのマクロリコールが得られ、その呼び出しの4.2から6.0が同じ意味保存リライトのリストを渡した。 審査員にそのアーティファクトを見せるのにも1.4から4.5ポイントかかる。 アーティファクトも見る4人の審査員のうち、審査員が強くなるにつれて利得は減少し、最も強い1つの呼び出しのポイント内に入る。

関連論文リスト

• Aligning Faithfulness for Theory-Scale Autoformalization [17.298425520643438]
  最初の理論スケールの忠実度ベンチマークであるFaithAlignを紹介する。 また、非公式な文脈と仮定が持たない146項目からなる同伴集合であるFaithAlign-Gapを提示する。 8モデル全体では、GPT-6 Astra は 47.8% で最大の欠陥 F1 を達成し、2つ以上の欠陥を持つ項目の4.5% で全ての欠陥を識別する。
  論文  参考訳（メタデータ） (2026-10-13T14:53:04Z)
• SWE-Proof: Can Language Models Resolve Real-World Issues with Machine-Checked Proofs? [39.004582663385364]
  Benchprooferは、既知の正しいパッチでコーディングタスクを正式に認証されたパイプラインに変換するパイプラインです。 SWE-bench Verified に適用すると SWE-Proof が得られる。
  論文  参考訳（メタデータ） (2026-09-18T01:16:53Z)
• IdeaAMBIG: Benchmarking Implementation-Critical Gaps in Research-Idea Specifications [52.570108663867046]
  研究のアイデアは、新しく、一貫性があり、科学的に妥当であるが、その提案された手法は、忠実な実装のために不十分に指定されている。 提案手法は,実装を対象とする研究手法仕様の体系化の可否を,有能な実装者やコーディングエージェントに十分な方法論的情報を提供して,前提条件を満たさずに目的とする手法を構築することができるかを検討する。 IdeaAMBIGは660のエビデンス基底インスタンスのベンチマークで、レポートとGitHubの問題から163の現実世界のギャップと、コーディフィケーション対応のリファレンスに注入される合成ギャップを497のコントロールで管理する。
  論文  参考訳（メタデータ） (2026-09-09T17:59:04Z)
• ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers [77.95933562142014]
  ITPEvalは、4つの主要なIPP間で自動形式証明翻訳を評価するための最初のベンチマークである。 itpevalは、状態が分離されたウォームバックエンドを備えた、統合されたマルチITP認証インフラストラクチャです。
  論文  参考訳（メタデータ） (2026-07-07T22:05:55Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• 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)
• GERE: Generative Evidence Retrieval for Fact Verification [57.78768817972026]
  本稿では,ジェネレーション方式で証拠を検索する最初のシステムであるGEREを提案する。 FEVERデータセットの実験結果は、GEREが最先端のベースラインよりも大幅に改善されていることを示している。
  論文  参考訳（メタデータ） (2022-04-12T03:49:35Z)
• AmbiFC: Fact-Checking Ambiguous Claims with Evidence [57.7091560922174]
  実世界の情報ニーズから10kクレームを抽出したファクトチェックデータセットであるAmbiFCを提示する。 アンビFCの証拠に対する主張を比較する際に,曖昧さから生じる不一致を分析した。 我々は,このあいまいさをソフトラベルで予測するモデルを開発した。
  論文  参考訳（メタデータ） (2021-04-01T17:40:08Z)

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

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