論文の概要: Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents

• arxiv url: http://arxiv.org/abs/2603.17150v1
• Date: Tue, 17 Mar 2026 21:28:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-03-19 18:32:57.401361
• Title: Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents
• Title（参考訳）: Intent Formalization:AIエージェント時代における信頼性の高いコーディングのグランドチャレンジ
• Authors: Shuvendu K. Lahiri,
• Abstract要約: エージェントAIシステムは、驚くほどの頻度でコードを生成することができる。 生成されたコードが実際にユーザが意図した通りに動作するようにします。
• 参考スコア（独自算出の注目度）: 7.228124845671868
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Agentic AI systems can now generate code with remarkable fluency, but a fundamental question remains: \emph{does the generated code actually do what the user intended?} The gap between informal natural language requirements and precise program behavior -- the \emph{intent gap} -- has always plagued software engineering, but AI-generated code amplifies it to an unprecedented scale. This article argues that \textbf{intent formalization} -- the translation of informal user intent into a set of checkable formal specifications -- is the key challenge that will determine whether AI makes software more reliable or merely more abundant. Intent formalization offers a tradeoff spectrum suitable to the reliability needs of different contexts: from lightweight tests that disambiguate likely misinterpretations, through full functional specifications for formal verification, to domain-specific languages from which correct code is synthesized automatically. The central bottleneck is \emph{validating specifications}: since there is no oracle for specification correctness other than the user, we need semi-automated metrics that can assess specification quality with or without code, through lightweight user interaction and proxy artifacts such as tests. We survey early research that demonstrates the \emph{potential} of this approach: interactive test-driven formalization that improves program correctness, AI-generated postconditions that catch real-world bugs missed by prior methods, and end-to-end verified pipelines that produce provably correct code from informal specifications. We outline the open research challenges -- scaling beyond benchmarks, achieving compositionality over changes, metrics for validating specifications, handling rich logics, designing human-AI specification interactions -- that define a research agenda spanning AI, programming languages, formal methods, and human-computer interaction.
• Abstract（参考訳）: エージェントAIシステムは、驚くほどの頻度でコードを生成することができるが、根本的な疑問は残る: \emph{does the generated code really do the user intended? } 非公式な自然言語要件と正確なプログラム動作のギャップ -- emph{intent gap} -- は常にソフトウェアエンジニアリングに悩まされてきたが、AI生成コードはそれを前例のない規模に増幅している。 この記事では、'textbf{intent formalization} -- 非公式なユーザインテントをチェック可能な形式仕様のセットに翻訳する -- が、AIがソフトウェアをより信頼性を高めたり、単に豊富なものにするかどうかを決定する重要な課題である、と論じる。 直観的形式化(Intent formalization)は、さまざまなコンテキストの信頼性要件に適したトレードオフスペクトルを提供する。形式検証の完全な機能仕様から、正しいコードが自動的に合成されるドメイン固有言語まで、おそらく誤解を曖昧にする可能性のある軽量テストである。 ユーザ以外の仕様の正確性に関するオラクルは存在しないので、テストのような軽量なユーザインタラクションやプロキシアーティファクトを通じて、コードの有無に関わらず仕様の品質を評価できる半自動化されたメトリクスが必要です。 プログラムの正確性を改善するインタラクティブなテスト駆動形式化、事前の方法で見逃された実世界のバグをキャッチするAI生成の事後条件、非公式な仕様から確実に正しいコードを生成するエンドツーエンドの検証パイプライン。 我々は、AI、プログラミング言語、フォーマルなメソッド、人間とコンピュータのインタラクションにまたがる研究課題を定義するオープンな研究課題 - ベンチマークを越えてのスケーリング、変更に対する構成性の達成、仕様の検証のためのメトリクス、リッチなロジックの処理、ヒューマンとAIの仕様のインタラクションの設計 -- の概要を説明した。

関連論文リスト

• Enhancing Formal Software Specification with Artificial Intelligence [1.4217721366366873]
  形式的ソフトウェア仕様は、早期エラー検出と明示的な不変性を可能にすることが知られている。 表記のオーバーヘッドが高く、伝統的な形式言語を使うのに必要な専門知識があるため、工業的採用が限られている。 近年の人工知能の進歩は、これらのコストを大幅に削減しつつ、形式仕様の利点の多くを維持することができる。
  論文  参考訳（メタデータ） (2026-01-11T13:53:22Z)
• Position: Intelligent Coding Systems Should Write Programs with Justifications [9.304020701255093]
  これらのシステムは、コードを生成するだけでなく、モデル推論とユーザ理解を橋渡しする明確な一貫性のある正当化も生み出すべきだ、と私たちは主張する。 我々は, 正当性生成のためのニューロシンボリックなアプローチを提唱し, トレーニング中の行動とプログラムセマンティクスが神経表現によって豊かになるように, 象徴的制約を導出する。
  論文  参考訳（メタデータ） (2025-08-08T05:04:47Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• Leveraging LLMs for Formal Software Requirements -- Challenges and Prospects [0.0]
  VERIFAI1は、このギャップを埋めるための自動化および半自動化アプローチを調査することを目的としている。 本論文では, 課題の繰り返しと今後の研究方向性を明らかにするために, 関連文献の予備的な合成について述べる。
  論文  参考訳（メタデータ） (2025-07-18T19:15:50Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。 トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
  論文  参考訳（メタデータ） (2023-02-14T18:43:34Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  大きな言語モデル(LLM)は、非公式な自然言語(NL)の意図からコードを生成する。 自然言語は曖昧であり、形式的な意味論が欠けているため、正確性の概念を定義するのは難しい。 言語に依存しない抽象アルゴリズムと具体的な実装TiCoderについて述べる。
  論文  参考訳（メタデータ） (2022-08-11T17:41:08Z)

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

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