論文の概要: Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
- arxiv url: http://arxiv.org/abs/2608.21516v2
- Date: Wed, 26 Aug 2026 05:46:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-27 14:15:14.90582
- Title: Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
- Title（参考訳）: Neuro-Formal Verification: Agentic Language-Agnostic Formal Program Reasoning
- Abstract要約: ニューロフォーマル検証(NFV)は、主流プログラミング言語の開発者の自動化を活用する。
AI符号化エージェントが翻訳し、確立された検証者が決定し、機械チェックされた証明により、音質よりも経験的精度で、主流言語で提起された質問にプッシュボタンで回答する。
正誤のPython問題のデータセットの結果は、llm-as-judgeベースラインと比較して推奨されている。
- 参考スコア（独自算出の注目度）: 7.228124845671868
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Formal verification offers the strongest assurance available for software, and verification-aware languages have made its automation real. Yet the benefits reach few mainstream developers, most of whose languages have no verification support. Besides, specifying properties and modeling the environment require expertise in formal methods. Proof is therefore reserved for a few celebrated artifacts, while the production code that ships is attested only through review and testing. We introduce neuro-formal verification (NFV), which harnesses that automation for developers of mainstream programming languages: an AI coding agent translates, an established verifier decides, and a question posed in a mainstream language is answered push-button, at empirical accuracy rather than soundness, with a machine-checked proof. Results on a dataset of correct and incorrect solutions to Python programming problems are encouraging compared to an {llm-as-judge} baseline: NFV returns a Dafny proof of correctness or of a bug on 57% of the entries at 92% precision, and a CBMC counterexample for 63% of the buggy programs at 90% precision.
- Abstract（参考訳）: 形式的検証は、ソフトウェアで利用可能な最強の保証を提供する。
しかし、その利点は主流の開発者にはほとんど及ばず、ほとんどの言語は検証サポートを持っていません。
さらに、プロパティの指定と環境のモデリングには形式的な手法の専門知識が必要である。
したがって、Proofはいくつかの有名なアーティファクトに予約されており、出荷されるプロダクションコードはレビューとテストによってのみ検証される。
我々は、AIコーディングエージェントが翻訳し、確立された検証器が決定し、メインストリーム言語で提起された質問が、機械チェックされた証明を用いて、音質よりも経験的精度でプッシュボタンで答えられるという、主流プログラミング言語の開発者の自動化を活用する神経形式検証(NFV)を導入する。
NFVは、92%の精度でエントリの57%でDafnyの正当性またはバグの証明を返し、90%の精度でバグギープログラムの63%に対してCBMCの反例を返します。
関連論文リスト
- Programmers Are Poor and Overconfident Judges of LLM-Generated Assertions [12.758916403043207]
生成したアサーションの正確性と完全性を評価する開発者の能力を評価するため,86人のPythonプログラマによる制御実験を行った。
一般的な仮定に反して、AIアシストはコードの理解とレビューの信頼性を向上しない可能性がある。
論文 参考訳（メタデータ） (2026-07-09T19:22:35Z) - Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization [26.123396123145415]
LLMエージェントが非公式なプログラミング問題を忠実な形式仕様に変換することができるかどうか、仕様自動書式化について検討する。
Codeforces問題から派生した581の仕様記述タスクのベンチマークであるVerus-SpecBenchを紹介する。
フェールモードの解析は、モデル生成仕様が重要な入力仮定を受け入れ、誤った出力を受け入れ、有効な仕様を拒否できることを示している。
論文 参考訳（メタデータ） (2026-05-26T02:12:48Z) - From Natural Language to Verified Code: Toward AI Assisted Problem-to-Code Generation with Dafny-Based Formal Verification [0.30915521808748864]
大規模な言語モデルは、自動化されたソフトウェア工学における約束を示すが、その正しさの保証は、誤ったコードや幻覚的なコードによってしばしば損なわれる。
NaturalLanguage2VerifiedCodeデータセット:60の複雑なアルゴリズム問題の集合を提供する。
7個のオープンウェイト LLM でランダムに選択された11個の問題集合をタイレッドプロンプト戦略を用いて評価した。
以上の結果から,コンテキストレスなプロンプトがほぼユニバーサルの失敗につながる一方で,構造的アンカーと反復的自己修復が劇的なパフォーマンスの転換を促進することが示唆された。
論文 参考訳（メタデータ） (2026-04-24T14:28:10Z) - Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
エージェントAIシステムは、驚くほどの頻度でコードを生成することができる。
生成されたコードが実際にユーザが意図した通りに動作するようにします。
論文 参考訳（メタデータ） (2026-03-17T21:28:59Z) - Propose, Solve, Verify: Self-Play Through Formal Verification [75.44204610186587]
形式的検証が信頼性の高い正当性信号を提供する検証コード生成設定における自己再生について検討する。
本稿では,PSV(Propose, Solve, Verify)という,難易度の高い合成問題を生成可能なプロジェクタと,専門家の反復によって訓練された解決器を作成するための,形式的検証信号を用いた簡単なセルフプレイフレームワークを紹介する。
そこで本研究では,生成した質問数とトレーニングの繰り返し数によるパフォーマンスの尺度を示し,形式的検証と難易度を考慮した提案を,自己再生を成功させる上で不可欠な要素として同定する。
論文 参考訳（メタデータ） (2025-12-20T00:56:35Z) - 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) - Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。
プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。
また, GPT-4o miniが74.18%と高い修理成功率を示した。
論文 参考訳（メタデータ） (2025-07-04T15:36:12Z) - Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。
SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。
我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
論文 参考訳（メタデータ） (2024-10-21T08:15:45Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Teaching Large Language Models to Self-Debug [62.424077000154945]
大規模言語モデル(LLM)は、コード生成において素晴らしいパフォーマンスを達成した。
本稿では,大規模言語モデルで予測プログラムを数発のデモでデバッグする自己デバッグを提案する。
論文 参考訳（メタデータ） (2023-04-11T10:43:43Z) - AVATAR: A Parallel Corpus for Java-Python Program Translation [77.86173793901139]
プログラム翻訳とは、ある言語から別の言語へソースコードを移行することを指す。
AVATARは9,515のプログラミング問題とそのソリューションをJavaとPythonという2つの人気のある言語で記述したものです。
論文 参考訳（メタデータ） (2021-08-26T05:44:20Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。