論文の概要: Viverra: Text-to-Code with Guarantees

• arxiv url: http://arxiv.org/abs/2605.14972v1
• Date: Thu, 14 May 2026 15:36:44 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-15 21:45:34.91645
• Title: Viverra: Text-to-Code with Guarantees
• Title（参考訳）: Viverra: 保証付きテキストからコーディング
• Authors: Haoze Wu, Rocky Klopfenstein, Keith Farkas, Nina Narodytska,
• Abstract要約: Viverraは、ユーザが生成したプログラムを理解するのを助けるために、生成したコードと一緒に、正式に認証されたアノテーションを自動的に生成するシステムである。 V Viverraは、認証されたアサーションで効率的にコードを生成することができ、これらのアサーションは、コード理解タスクにおけるユーザのパフォーマンスを改善する。
• 参考スコア（独自算出の注目度）: 5.566349423527438
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: A fundamental limitation of Text-to-Code is that no guarantee can be obtained about the correctness of the generated code. Therefore, to ensure its correctness, the generated code still has to be reviewed, tested, and maintained by developers. However, parsing through LLM-generated code can be tedious and time-consuming, potentially negating the productivity gains promised by AI-coding tools. To address this challenge, we present Viverra, a system that automatically produces formally verified annotations alongside generated code to aid user's understanding of the generated program. Given a natural-language task description, Viverra prompts an LLM to synthesize a C program together with candidate assertions expressing safety and correctness properties. It then verifies those assertions in a compositional and best-effort manner via a portfolio of bounded model checkers. Evaluation on 18 diverse programming tasks suggests that Viverra can efficiently generate code with verified assertions, and that these assertions improve users' performance on code-comprehension tasks in a user study with more than 400 participants.
• Abstract（参考訳）: Text-to-Codeの基本的な制限は、生成されたコードの正確性に関して保証が得られないことである。 したがって、その正確性を保証するために、生成したコードは、開発者によってレビュー、テスト、保守されなければならない。 しかし、LLM生成コードによる解析は面倒で時間がかかり、AIコーディングツールが約束する生産性向上を否定する可能性がある。 この課題に対処するために、ユーザが生成したプログラムの理解を支援するために、生成したコードと並行して、正式に検証されたアノテーションを自動生成するシステムViverraを提案する。 自然言語によるタスク記述が与えられた後、Viverra は LLM に安全性と正当性を表す候補アサーションと共に C プログラムを合成するよう促す。 次に、境界モデルチェッカーのポートフォリオを通じて、これらのアサーションを構成的かつベストプラクティスで検証する。 18の多様なプログラミングタスクの評価は、Viverraが証明されたアサーションで効率的にコードを生成することができ、400人以上の参加者を持つユーザスタディにおいて、コード理解タスクにおけるユーザのパフォーマンスを向上させることを示唆している。

関連論文リスト

• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• Towards Formal Verification of LLM-Generated Code from Natural Language Prompts [17.130884318613944]
  LLM生成したコードに対して、正式な正当性を保証することを目指している。 本稿では,ユーザの意図を形式的に定義されているが,自然言語的な方法で表現できる形式的なクエリ言語を提案する。 83%のケースで正しいコードを検証でき、92%で間違ったコードを識別できます。
  論文  参考訳（メタデータ） (2025-07-17T16:54:42Z)
• Ensuring Functional Correctness of Large Code Models with Selective Generation [13.517414451760635]
  コード生成モデルの幻覚は、より高い安全性基準を必要とするシステムへの適用性を妨げます。 生成した単体テストによって評価された機能的正当性に基づいて,不確実な世代から退避する固有コード生成器を提案する。 本手法の有効性を,コード幻覚の制御性と適切な選択効率とともに示す。
  論文  参考訳（メタデータ） (2025-05-19T06:29:16Z)
• Chain of Targeted Verification Questions to Improve the Reliability of Code Generated by LLMs [10.510325069289324]
  LLMが生成するコードの信頼性向上を目的とした自己補充手法を提案する。 当社のアプローチは,初期コード内の潜在的なバグを特定するために,対象とする検証質問(VQ)に基づいています。 本手法は,LLMをターゲットとするVQと初期コードで再プロンプトすることで,潜在的なバグの修復を試みる。
  論文  参考訳（メタデータ） (2024-05-22T19:02:50Z)
• Iterative Refinement of Project-Level Code Context for Precise Code Generation with Compiler Feedback [29.136378191436396]
  我々は,コンパイラフィードバックを用いてLLM生成コードを改善する新しいコード生成手法であるCoCoGenを提案する。 CoCoGenは、まず静的解析を利用して、生成されたコードとプロジェクトのコンテキストのミスマッチを特定する。 その後、コードリポジトリから抽出された情報を使用して、識別されたエラーを反復的に調整し、修正する。
  論文  参考訳（メタデータ） (2024-03-25T14:07:27Z)
• Code Prompting Elicits Conditional Reasoning Abilities in Text+Code LLMs [65.2379940117181]
  自然言語の問題をコードに変換する一連のプロンプトであるコードプロンプトを導入します。 コードプロンプトは複数のLLMに対して高速に向上することがわかった。 GPT 3.5を解析した結果,入力問題のコードフォーマッティングが性能向上に不可欠であることが判明した。
  論文  参考訳（メタデータ） (2024-01-18T15:32:24Z)
• Python Code Generation by Asking Clarification Questions [57.63906360576212]
  本稿では,この課題に対して,より斬新で現実的なセットアップを導入する。 我々は、自然言語記述の過小評価は、明確化を問うことで解決できると仮定する。 我々は、生成した合成明確化質問と回答を含む自然言語記述とコードのペアを含む、CodeClarQAという新しいデータセットを収集し、導入する。
  論文  参考訳（メタデータ） (2022-12-19T22:08:36Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

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

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