論文の概要: Towards Automated Formal Verification of Backend Systems with LLMs
- arxiv url: http://arxiv.org/abs/2506.10998v1
- Date: Sun, 13 Apr 2025 16:49:37 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-06-22 23:32:14.450855
- Title: Towards Automated Formal Verification of Backend Systems with LLMs
- Title（参考訳）: LLMを用いたバックエンドシステムの自動形式検証に向けて
- Authors: Kangping Xu, Yifan Luo, Yang Yuan, Andrew Chi-Chih Yao,
- Abstract要約: バックエンドのコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。
我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。
本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることがわかった。
- 参考スコア（独自算出の注目度）: 9.66648456498893
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Software testing plays a critical role in ensuring that systems behave as intended. However, existing automated testing approaches struggle to match the capabilities of human engineers due to key limitations such as test locality, lack of general reliability, and business logic blindness. In this work, we propose a novel framework that leverages functional programming and type systems to translate Scala backend code into formal Lean representations. Our pipeline automatically generates theorems that specify the intended behavior of APIs and database operations, and uses LLM-based provers to verify them. When a theorem is proved, the corresponding logic is guaranteed to be correct and no further testing is needed. If the negation of a theorem is proved instead, it confirms a bug. In cases where neither can be proved, human intervention is required. We evaluate our method on realistic backend systems and find that it can formally verify over 50% of the test requirements, which suggests that half of a testing engineer's workload can be automated. Additionally, with an average cost of only $2.19 per API, LLM-based verification is significantly more cost-effective than manual testing and can be scaled easily through parallel execution. Our results indicate a promising direction for scalable, AI-powered software testing, with the potential to greatly improve engineering productivity as models continue to advance.
- Abstract（参考訳）: ソフトウェアテストは、システムが意図した通りに振る舞うことを保証する上で重要な役割を果たす。
しかし、既存の自動テストアプローチは、テストのローカリティ、一般的な信頼性の欠如、ビジネスロジックの盲点といった重要な制限のために、ヒューマンエンジニアの能力に匹敵する。
本研究では,Scalaのバックエンドコードを形式的なリーン表現に変換するために,関数型プログラミングと型システムを活用する新しいフレームワークを提案する。
我々のパイプラインは、APIやデータベース操作の意図した振る舞いを規定する定理を自動生成し、LSMベースのプロバーを用いて検証する。
定理が証明されると、対応する論理は正しいことが保証され、それ以上のテストは必要ない。
定理の否定が代わりに証明されれば、それはバグを確認する。
どちらも証明できない場合、人間の介入が必要である。
本手法を現実的なバックエンドシステム上で評価した結果,テスト要件の50%以上を正式に検証できることが確認され,テストエンジニアの作業負荷の半分が自動化可能であることが示唆された。
さらに、API当たりの平均コストは2.19ドルに過ぎず、LSMベースの検証は手動テストよりもはるかに費用対効果が高く、並列実行によって容易にスケールできる。
我々の結果は、スケーラブルでAI駆動のソフトウェアテストにおいて有望な方向性を示し、モデルが進歩し続けるにつれて、エンジニアリングの生産性が大幅に向上する可能性を示している。
関連論文リスト
- Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。
実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
論文 参考訳（メタデータ） (2025-05-28T17:57:47Z) - APE-Bench I: Towards File-level Automated Proof Engineering of Formal Math Libraries [5.227446378450704]
APE-Bench Iは、Mathlib4の実際のコミット履歴から構築された最初の現実的なベンチマークである。
Eleansticはスケーラブルな並列検証インフラストラクチャで、Mathlibの複数バージョンにわたる検証に最適化されている。
論文 参考訳（メタデータ） (2025-04-27T05:04:02Z) - Are You Getting What You Pay For? Auditing Model Substitution in LLM APIs [60.881609323604685]
ブラックボックスAPIを通じてアクセスされるLarge Language Models (LLM)は、信頼の課題をもたらす。
ユーザーは、宣伝されたモデル機能に基づいたサービスの料金を支払う。
プロバイダは、運用コストを削減するために、特定のモデルを安価で低品質の代替品に隠蔽的に置き換えることができる。
この透明性の欠如は、公正性を損なうとともに、信頼を損なうとともに、信頼性の高いベンチマークを複雑にする。
論文 参考訳（メタデータ） (2025-04-07T03:57:41Z) - SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
SOPBenchは、各サービス固有のSOPコードプログラムを実行可能な関数の有向グラフに変換する評価パイプラインである。
提案手法では,各サービス固有のSOPコードプログラムを実行可能関数の有向グラフに変換し,自然言語SOP記述に基づいてこれらの関数を呼び出しなければならない。
我々は18の先行モデルを評価し、上位モデルでさえタスクが困難であることを示す。
論文 参考訳（メタデータ） (2025-03-11T17:53:02Z) - ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis [50.020850767257095]
本稿では,LLMに様々な粒度で自動化手法を付加するProofAugを提案する。
本手法は,オープンソースのDeep-math-7bベースモデルとIsabelle証明アシスタントを用いて,MiniF2Fベンチマークで検証した。
また、ProofAugのLean 4バージョンを実装し、Kimina-Prover-seek-Distill-1.5Bのパス@1のパフォーマンスを44.3%から50.4%に改善します。
論文 参考訳（メタデータ） (2025-01-30T12:37:06Z) - The Potential of LLMs in Automating Software Testing: From Generation to Reporting [0.0]
手動テストは効果的だが、時間とコストがかかり、自動化メソッドの需要が増大する。
大規模言語モデル(LLM)の最近の進歩は、ソフトウェア工学に大きな影響を与えている。
本稿では,人間の介入を減らし,テスト効率を向上させるため,LSMを用いた自動ソフトウェアテストに対するエージェント指向アプローチについて検討する。
論文 参考訳（メタデータ） (2024-12-31T02:06:46Z) - AutoPT: How Far Are We from the End2End Automated Web Penetration Testing? [54.65079443902714]
LLMによって駆動されるPSMの原理に基づく自動浸透試験エージェントであるAutoPTを紹介する。
以上の結果から, AutoPT は GPT-4o ミニモデル上でのベースラインフレームワーク ReAct よりも優れていた。
論文 参考訳（メタデータ） (2024-11-02T13:24:30Z) - Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
リーンでLLM推論を実行するためのフレームワークであるLean Copilotを紹介します。
証明のステップを提案し、証明の目標を完了し、関連する前提を選択するツールを構築します。
人間を助ける場合、Lean Copilotは平均3.86で手動で入力された証明ステップを2.08ステップしか必要としない。
定理証明プロセスを自動化する場合、Lean Copilotの74.2%の証明ステップは平均85%がエソップ(40.1%)より優れている。
論文 参考訳（メタデータ） (2024-04-18T22:54:08Z) - Automating REST API Postman Test Cases Using LLM [0.0]
本稿では,大規模言語モデルを用いたテストケースの自動生成手法の探索と実装について述べる。
この方法論は、テストケース生成の効率性と有効性を高めるために、Open AIの使用を統合する。
この研究で開発されたモデルは、手作業で収集したポストマンテストケースやさまざまなRest APIのインスタンスを使ってトレーニングされている。
論文 参考訳（メタデータ） (2024-04-16T15:53:41Z) - Test-Driven Development for Code Generation [0.850206009406913]
大きな言語モデル(LLM)は、問題ステートメントから直接コードスニペットを生成する重要な機能を示している。
本稿では,テスト駆動開発(TDD)をAI支援コード生成プロセスに組み込む方法について検討する。
論文 参考訳（メタデータ） (2024-02-21T04:10:12Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。