論文の概要: Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
- arxiv url: http://arxiv.org/abs/2605.26017v1
- Date: Mon, 25 May 2026 16:35:36 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-05-26 19:50:20.474072
- Title: Trustworthy Software Project Generation : a Case Study with an Interactive Theorem Prover
- Title（参考訳）: 信頼できるソフトウェアプロジェクト生成 : 対話的理論による事例研究
- Authors: Jian Fang, Yingfei Xiong,
- Abstract要約: 本稿では,対話型定理証明器(ITP)が大規模ソフトウェア生成を支援するかどうかを考察する。
ITPは純粋全関数を扱うが、I/Oのような効果はないため、エージェントは実効的なコードを純粋論理から分離する。
本稿では, RISC-V RV32I ベースの47命令すべてに対して, CPU インタプリタの完全自動開発を通じて, この経路について検討する。
- 参考スコア（独自算出の注目度）: 2.6146136791093104
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Generating code from natural-language requirements has become a primary route for LLM-assisted software development. Although LLMs can successfully complete small programming tasks, generating an entire complex project remains unreliable because subtle errors may survive compilation and testing. Verified programming can reduce this risk by requiring generated implementations to satisfy machine-checked specifications. Existing explorations mostly target verification-oriented languages and toolchains such as Dafny and Frama-C, but directly generating project-scale verified code with these systems remains difficult. This paper studies whether interactive theorem provers (ITPs) can support large-scale software generation. Because ITPs handle pure total functions but not effects such as I/O, our agent separates effectful code from pure logic: it implements the effects in the target language, proves the pure logic in an ITP, and extracts it for integration into the final project. We study this route through the fully automatic development of a CPU interpreter for all 47 instructions of the unprivileged RISC-V RV32I base: after the requirements are supplied, no human intervenes in synthesis, proof repair, extraction, or integration. With Rocq as the backend, the agent completes the project within 30 minutes, producing 1,859 lines of verified Rocq and extracting 2,848 lines of C++. The resulting interpreter passes all 265 LLM-generated tests covering the 47 instructions and exhibits zero crashes and zero hangs during 12 hours of AFL++ fuzzing. Under the same configuration, a Dafny-based backend fails to complete verification. Our observation is that Rocq exposes a concrete proof state when a proof attempt fails, giving the agent actionable feedback for repair. These results provide empirical evidence that ITP-based verified programming is a feasible route for LLM-generated software projects.
- Abstract（参考訳）: 自然言語要求からコードを生成することは、LLM支援ソフトウェア開発の主要なルートとなっている。
LLMは小さなプログラミングタスクをうまくこなすことができるが、微妙なエラーがコンパイルやテストに耐えられるため、複雑なプロジェクト全体を生成することは信頼性が低い。
検証されたプログラミングは、マシンチェックされた仕様を満たすために生成された実装を必要とすることにより、このリスクを低減することができる。
既存の調査は主にDafnyやFrama-Cのような検証指向言語やツールチェーンをターゲットにしているが、これらのシステムでプロジェクト規模の検証コードを直接生成することは難しい。
本稿では,対話型定理証明器(ITP)が大規模ソフトウェア生成を支援するかどうかを考察する。
I/Oのような純粋な全関数を処理するが、I/Oのようなエフェクトは扱わないため、エージェントは、対象言語でエフェクトを実装し、IPPで純粋なロジックを証明し、最終プロジェクトに統合するために抽出する、純粋論理からエフェクトフルコードを切り離す。
本稿では, RISC-V RV32I ベースの47命令すべてに対して, CPU インタプリタの完全自動開発を通じて, この経路について検討する。
Rocqをバックエンドとして、エージェントは30分以内にプロジェクトを完了し、検証済みのRocqの1,859行を生成し、2,848行のC++を抽出する。
結果、インタプリタは47命令をカバーする265個のLCM生成テストをすべてパスし、AFL++ファジィの12時間の間にゼロクラッシュとゼロハングを示す。
同じ構成で、Dafnyベースのバックエンドは検証を完了できない。
我々の観察では、Rocqは証明試みが失敗すると具体的な証明状態を公開するので、エージェントに修復のための実用的なフィードバックを与える。
これらの結果は、ILPベースの検証プログラミングがLLM生成ソフトウェアプロジェクトにとって実現可能なルートであることを示す実証的な証拠を提供する。
関連論文リスト
- CktFormalizer: Autoformalization of Natural Language into Circuit Representations [23.44745731124114]
CktFormalizerは、Lean 4.0に組み込まれた依存型HDLを通じてハードウェア生成をリダイレクトするフレームワークである。
VerilogEval(156問題)、RTLLM(50問題)、ResBench(56問題)では、CktFormalizerは直接Verilog生成と競合するシミュレーションパスレートを達成する。
論文 参考訳（メタデータ） (2026-05-08T14:20:06Z) - SPARC: Scenario Planning and Reasoning for Automated C Unit Test Generation [1.0010193170880752]
本稿では,高レベルのプログラム意図とポインタ演算と手動メモリ管理の厳密な構文制約とのギャップを埋める,ニューロシンボリックなシナリオベースのフレームワークを提案する。
我々は、59の現実世界およびアルゴリズムの被験者で評価し、バニラプロンプト生成ベースラインを31.36%、分岐カバレッジ26.01%、突然変異スコア20.78%で上回り、シンボリック実行ツールKLEEに適合または超えている。
論文 参考訳（メタデータ） (2026-02-18T18:09:03Z) - Generative Logic: A New Computer Architecture for Deterministic Reasoning and Knowledge Generation [0.0]
Generative Logic (GL) は、ユーザの公理的定義から始まる決定論的アーキテクチャである。
GLは予想を列挙し、正規化、型、CEフィルタを適用し、機械チェック可能な証明を自動的に再構築する。
論文 参考訳（メタデータ） (2025-07-25T17:29:19Z) - PRO-V: An Efficient Program Generation Multi-Agent System for Automatic RTL Verification [6.983135183126461]
Pro-Vは、堅牢なRTL検証のためのプログラム生成マルチエージェントシステムである。
生成したテストベンチの正しさを高めるため、効率的なn個の反復サンプリング戦略が組み込まれている。
Pro-Vは、黄金のRTL実装では87.17%、RTL変異では76.28%の精度で検証されている。
論文 参考訳（メタデータ） (2025-06-13T20:06:34Z) - Towards Automated Formal Verification of Backend Systems with LLMs [9.66648456498893]
バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。
我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。
本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
論文 参考訳（メタデータ） (2025-04-13T16:49:37Z) - Get my drift? Catching LLM Task Drift with Activation Deltas [55.75645403965326]
タスクドリフトは攻撃者がデータを流出させたり、LLMの出力に影響を与えたりすることを可能にする。
そこで, 簡易線形分類器は, 分布外テストセット上で, ほぼ完全なLOC AUCでドリフトを検出することができることを示す。
このアプローチは、プロンプトインジェクション、ジェイルブレイク、悪意のある指示など、目に見えないタスクドメインに対して驚くほどうまく一般化する。
論文 参考訳（メタデータ） (2024-06-02T16:53:21Z) - ML-Bench: Evaluating Large Language Models and Agents for Machine Learning Tasks on Repository-Level Code [76.84199699772903]
ML-Benchは、既存のコードリポジトリを利用してタスクを実行する現実世界のプログラミングアプリケーションに根ざしたベンチマークである。
LLM(Large Language Model)とAIエージェントの両方を評価するために、事前に定義されたデプロイメント環境でLLMのテキスト-コード変換を評価するML-LLM-Benchと、Linuxサンドボックス環境でエンドツーエンドのタスク実行で自律エージェントをテストするML-Agent-Benchの2つの設定が採用されている。
論文 参考訳（メタデータ） (2023-11-16T12:03:21Z) - LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。
具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。
LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
論文 参考訳（メタデータ） (2023-02-16T18:23:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。