論文の概要: Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries

• arxiv url: http://arxiv.org/abs/2610.33094v1
• Date: Thu, 22 Oct 2026 07:42:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-27 22:27:13.242313
• Title: Beyond Correctness: Attribution of Natural-Language Documentation for Formal Libraries
• Title（参考訳）: 正確性を超えて:形式ライブラリーの自然言語文書化の貢献
• Abstract要約: ドキュメンテーションステートメントが確実に真実であることを示し、関数の振舞いが変わった後も保持する。 我々は帰属を利用して、確認可能な証拠とともに、出版された各文に何を公開するかを決め、それから回収された形式的財産を添付します。 結果は、証明可能な真実は、ドキュメントが関数が実際に何をしているかを反映していることを保証するものではないことを示している。
• 参考スコア（独自算出の注目度）: 20.202284634250546
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal languages are widely used in software engineering to specify and verify program properties. Because their mathematical notation and logic are hard to read, developers often rely on natural-language documentation to understand the functions in formal libraries. Yet a documentation statement can be provably true and still hold after the function's behavior changes. We call a statement's dependence on the function's specific behavior attribution, and we give a method to check it. We design and implement DocAuth, a documentation-generation method that uses attribution to decide what to publish and attaches to each published sentence the formal property recovered from it, together with checkable evidence. On 150 functions from the Community Books library of the ACL2 theorem prover, three large language models produce proved but non-attributable properties for about a third of the functions. DocAuth matches or exceeds the attribution rate of a mutation-based filter while delivering 37% more attributable sentences. Compared with a pipeline that checks truth alone, it raises the share of published sentences that a second model confirms as attributable from 82.9% to 94.7%. These results show that provable truth does not guarantee that documentation reflects what a function actually does. Attribution complements truth as a criterion for generating and evaluating documentation for formal libraries.
• Abstract（参考訳）: フォーマル言語は、プログラムの特性を特定し検証するために、ソフトウェア工学で広く使われている。 数学的表記法や論理は読みにくいため、開発者は形式ライブラリの関数を理解するために自然言語のドキュメントを使うことが多い。 しかし、ドキュメントのステートメントは確実に真実であり、関数の振舞いが変わった後も保持される。 我々は、関数の特定の振舞いへの依存をステートメントと呼び、それをチェックする方法を与えます。 ドキュメント生成手法であるDocAuthを設計、実装し、属性を使って、公開する各文に何を公開するかを決め、それから取り出した形式的プロパティを、チェック可能な証拠とともにアタッチする。 ACL2定理証明器のCommunity Booksライブラリから150の関数に対して、3つの大きな言語モデルが証明されたが、約3分の1の関数に対して帰属しない性質を証明した。 DocAuthは、突然変異ベースのフィルタの帰属率と一致し、さらに帰属可能な文を37%提供します。 真実のみをチェックするパイプラインと比較して、第2のモデルが属性を82.9%から94.7%と確認する文のシェアを上昇させる。 これらの結果は、証明可能な真実は、ドキュメントが関数が実際に何をしているかを反映していることを保証するものではないことを示している。 属性は、形式ライブラリのドキュメントの生成と評価の基準として真実を補完する。

関連論文リスト

• LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software [0.9023847175654603]
  本稿では,Large Language Models (LLMs) を用いた合金仕様作成のための探索的研究について述べる。 Flipperは機能フラグ管理システムであり、Cerberusはデータ検証ライブラリである。
  論文  参考訳（メタデータ） (2026-07-20T22:41:55Z)
• Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization [10.775710068605006]
  本稿では,評価問題とボトルネック帰属問題の両方として,忠実な文の形式化について検討する。 ツール拡張されたエージェントは89.5%のコンパイルに到達したが、コンセンサスの忠実度は60.5%に過ぎず、29.0ポイントのコンパイルパスを持つが、コンセンサスに反するギャップを露呈する。
  論文  参考訳（メタデータ） (2026-06-30T00:27:53Z)
• Natural Language-Focused Software Engineering via Code-Documentation Equivalence [17.47344940875897]
  与えられたコードスニペットに等価なドキュメントを自動的に生成する、Documentaryと呼ばれる新しいアプローチを提案する。 提案手法により,LCMは関数の出力を12.8～24.5%高い精度で予測できることがわかった。 人間の開発者は、Documentaryが生成したドキュメントは、オリジナルの人間によるドキュメントよりも、コードの理解と編集に有用だと考えている。
  論文  参考訳（メタデータ） (2026-06-20T22:19:00Z)
• Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
  ツール拡張言語モデルでは、中間表現と実行機構の両方を変えるため、自然言語推論とコード実行パイプラインを比較することは困難である。 モデルは、その推論を実行可能なコードとして表現し、言語モデルは、そのコードを文脈でシミュレートして、回答を生成する。 中間介入は自然言語の推論と有意に異なるものではない(+0.15pp)。
  論文  参考訳（メタデータ） (2026-06-14T04:17:21Z)
• BRIDGE: Building Representations In Domain Guided Program Verification [67.36686119518441]
  BRIDGEは、検証をコード、仕様、証明の3つの相互接続ドメインに分解する。 提案手法は, 標準誤差フィードバック法よりも精度と効率を著しく向上することを示す。
  論文  参考訳（メタデータ） (2025-11-26T06:39:19Z)
• Cite Pretrain: Retrieval-Free Knowledge Attribution for Large Language Models [44.31597857713689]
  最初の段階でActive Indexingを導入し、一般化可能なソースアンコールバインディングを作成します。 Qwen-2.5-7B&3Bの実験は、アクティブインデックスがパッシブインデックスのベースラインを一貫して上回っていることを示している。 内部の引用は、モデルを検索ノイズに対してより堅牢にすることで、外部の引用を補完する。
  論文  参考訳（メタデータ） (2025-06-21T04:48:05Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Same or Different? Diff-Vectors for Authorship Analysis [78.83284164605473]
  古典的な著作物分析において、特徴ベクトルは文書を表し、特徴の値は文書中の特徴の相対周波数(関数の増大)を表し、クラスラベルは文書の著者を表す。 筆者らの実験は共著者検証,著者検証,クローズドセットの著者帰属に取り組んでおり,DVは自然に第1の問題を解くのに向いているが,第2と第3の問題を解くための2つの新しい方法も提供している。
  論文  参考訳（メタデータ） (2023-01-24T08:48:12Z)
• DocCoder: Generating Code by Retrieving and Reading Docs [87.88474546826913]
  コードマニュアルとドキュメントを明示的に活用するアプローチであるDocCoderを紹介します。 我々のアプローチは一般的に、どんなプログラミング言語にも適用でき、基礎となるニューラルモデルとは無関係です。
  論文  参考訳（メタデータ） (2022-07-13T06:47:51Z)

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

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