論文の概要: Formal Methods Meets Readability: Auto-Documenting JML Java Code
- arxiv url: http://arxiv.org/abs/2506.09230v1
- Date: Tue, 10 Jun 2025 20:39:29 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-13 06:35:02.079129
- Title: Formal Methods Meets Readability: Auto-Documenting JML Java Code
- Title（参考訳）: 形式的メソッドの可読性 - JML Javaコードの自動文書化
- Authors: Juan Carlos Recio Abad, Ruben Saborido, Francisco Chicano,
- Abstract要約: 本稿では,Java モデリング言語 (JML) を用いた形式仕様が,LLM (Large Language Model) の生成する Javadocs の品質を高めることができるかどうかを検討する。
JMLアノテーションと非アノテーションJavaクラスから生成されたドキュメントを体系的に比較する。
以上の結果から,JMLはクラスレベルのドキュメンテーションを著しく改善し,メソッドレベルではより適度に向上することが示唆された。
- 参考スコア（独自算出の注目度）: 1.0650780147044159
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper investigates whether formal specifications using Java Modeling Language (JML) can enhance the quality of Large Language Model (LLM)-generated Javadocs. While LLMs excel at producing documentation from code alone, we hypothesize that incorporating formally verified invariants yields more complete and accurate results. We present a systematic comparison of documentation generated from JML-annotated and non-annotated Java classes, evaluating quality through both automated metrics and expert analysis. Our findings demonstrate that JML significantly improves class-level documentation completeness, with more moderate gains at the method level. Formal specifications prove particularly effective in capturing complex class invariants and design contracts that are frequently overlooked in code-only documentation. A threshold effect emerges, where the benefits of JML become more pronounced for classes with richer sets of invariants. While JML enhances specification coverage, its impact on core descriptive quality is limited, suggesting that formal specifications primarily ensure comprehensive coverage rather than fundamentally altering implementation descriptions. These results offer actionable insights for software teams adopting formal methods in documentation workflows, highlighting scenarios where JML provides clear advantages. The study contributes to AI-assisted software documentation research by demonstrating how formal methods and LLMs can synergistically improve documentation quality.
- Abstract（参考訳）: 本稿では,Java モデリング言語 (JML) を用いた形式仕様が,LLM (Large Language Model) の生成する Javadocs の品質を高めることができるかどうかを検討する。
LLMはコードだけでドキュメントを作成するのに優れていますが、形式的に検証された不変性を取り入れることで、より完全で正確な結果が得られるという仮説を立てています。
本稿では,JML アノテーションおよび非アノテーション Java クラスから生成されたドキュメンテーションを体系的に比較し,自動メトリクスとエキスパート分析による品質評価を行う。
以上の結果から,JMLはクラスレベルのドキュメントの完全性を大幅に改善し,メソッドレベルでは適度に向上することが示された。
形式的な仕様は、コードのみのドキュメントでしばしば見過ごされる複雑なクラス不変量や設計契約の取得に特に有効である。
閾値効果が出現し、よりリッチな不変集合を持つクラスに対して、JMLの利点がより顕著になる。
JMLは仕様カバレッジを向上させるが、コア記述品質への影響は限定的であり、形式的な仕様は実装記述を根本的に変更するのではなく、主に包括的なカバレッジを保証することを示唆している。
これらの結果は、ソフトウェアチームがドキュメントワークフローにフォーマルなメソッドを採用するための実用的な洞察を与え、JMLが明確なアドバンテージを提供するシナリオを強調します。
この研究は、形式的なメソッドとLLMがドキュメントの品質を相乗的に改善できる方法を示すことによって、AI支援のソフトウェアドキュメント研究に貢献する。
関連論文リスト
- Behavioral Augmentation of UML Class Diagrams: An Empirical Study of Large Language Models for Method Generation [0.0]
本研究では, 大規模言語モデル(LLM)を用いて, 21 の構造化廃棄物処理事例を用いて, メソドレスダイアグラム(21 クラス, 17 の関係性)を増強する。
合計90の図(3,373の方法)が6回にわたって評価された。
論文 参考訳（メタデータ） (2025-06-01T02:33:40Z) - Type-Constrained Code Generation with Language Models [51.03439021895432]
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。
そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。
提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
論文 参考訳（メタデータ） (2025-04-12T15:03:00Z) - Next Steps in LLM-Supported Java Verification [0.8057006406834466]
大きな言語モデル(LLM)はコード生成に適したツールであるだけでなく、アノテーションベースのコード仕様を生成することもできる。
本稿では、この厳密なツールセットを用いて、信頼できないLCMから正しい仕様アノテーションを確実に取り出す方法について、初期の結果を提供する。
論文 参考訳（メタデータ） (2025-02-03T17:55:50Z) - ClassEval-T: Evaluating Large Language Models in Class-Level Code Translation [19.69195067838796]
クラスレベルのコード翻訳ベンチマークであるClassEval-Tを構築し、クラスレベルのコード翻訳における最近のLLMの性能を広範囲に評価する最初の試みを行う。
完全なコードサンプルと関連するテストスイートを使って、JavaとC++への手動移行を実現するのに、私たちは360人時間を費やしました。
実験結果は,最も広く研究されているメソッドレベルのコード翻訳ベンチマークと比較して,顕著な性能低下を示した。
論文 参考訳（メタデータ） (2024-11-09T11:13:14Z) - Not All Experts are Equal: Efficient Expert Pruning and Skipping for Mixture-of-Experts Large Language Models [90.14693869269519]
MoE LLMはより少ないパラメータで高いパフォーマンスを実現することができるが、パラメータサイズが大きいためデプロイは困難である。
本稿では主に,プラグ・アンド・プレイ・エキスパートレベルのスペーシフィケーション技術を導入することで,MoE LLMの展開効率を向上させることを目的としている。
論文 参考訳（メタデータ） (2024-02-22T18:56:07Z) - AlignedCoT: Prompting Large Language Models via Native-Speaking Demonstrations [52.43593893122206]
Alignedcotは、大規模言語モデルを呼び出すためのコンテキスト内学習技術である。
ゼロショットシナリオでは、一貫した正しいステップワイズプロンプトを達成する。
数学的推論とコモンセンス推論の実験を行う。
論文 参考訳（メタデータ） (2023-11-22T17:24:21Z) - Exploring Large Language Models for Code Explanation [3.2570216147409514]
大規模言語モデル(LLM)は自然言語処理において顕著な進歩を遂げている。
本研究では,様々なLLMを用いて,コードスニペットの自然言語要約を生成するタスクについて検討する。
論文 参考訳（メタデータ） (2023-10-25T14:38:40Z) - BLESS: Benchmarking Large Language Models on Sentence Simplification [55.461555829492866]
我々は、テキスト単純化(TS)タスク上で、最新の最先端の大規模言語モデル(LLM)のパフォーマンスベンチマークであるBLESSを紹介する。
異なるドメイン(Wikipedia、ニュース、医療)の3つのテストセットに対して、サイズ、アーキテクチャ、事前学習方法、アクセシビリティの異なる44のモデルを評価する。
評価の結果,最高のLSMはTSのトレーニングを受けていないにもかかわらず,最先端のTSベースラインと相容れない性能を示した。
論文 参考訳（メタデータ） (2023-10-24T12:18:17Z) - Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting [68.19544657508509]
言語モデル(LLM)は、言語技術の基本コンポーネントとして採用されている。
いくつかの広く使われているオープンソースLLMは、数ショット設定でプロンプトフォーマットの微妙な変更に対して非常に敏感であることがわかった。
本稿では,与えられたタスクに対して有効なプロンプトフォーマットのサンプルセットを迅速に評価するアルゴリズムを提案し,モデル重み付けにアクセスせずに期待性能の間隔を報告する。
論文 参考訳（メタデータ） (2023-10-17T15:03:30Z) - How Effective are Large Language Models in Generating Software Specifications? [14.170320751508502]
大規模言語モデル(LLM)は多くのソフトウェア工学(SE)タスクにうまく適用されている。
ソフトウェアコメントやドキュメンテーションからソフトウェア仕様を生成するためのLCMの能力を評価するための、最初の実証的研究を行う。
論文 参考訳（メタデータ） (2023-06-06T00:28:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。