論文の概要: Can Large Language Models Model Programs Formally?

• arxiv url: http://arxiv.org/abs/2604.01851v1
• Date: Thu, 02 Apr 2026 10:06:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-03 14:21:10.670789
• Title: Can Large Language Models Model Programs Formally?
• Title（参考訳）: 大規模言語モデルはプログラムを形式的にモデル化できるか?
• Authors: Zhiyong Chen, Jialun Cao, Jiarong Wu, Chang Xu, Shing-Chi Cheung,
• Abstract要約: Model-BenchはLLMのプログラムモデリング機能の評価と改善のためのベンチマークとパイプラインである。 有名な3つのベンチマークから派生した400のPythonプログラムで構成されている。 実験の結果,LLMのプログラムモデリングにおける限界が明らかとなった。
• 参考スコア（独自算出の注目度）: 26.12584614197935
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In the digital age, ensuring the correctness, safety, and reliability of software through formal verification is paramount, particularly as software increasingly underpins critical infrastructure. Formal verification, split into theorem proving and model checking, provides a feasible and reliable path. Unlike theorem proving, which yields notable advances, model checking has been less focused due to the difficulty of automatic program modeling. To fill this gap, we introduce Model-Bench, a benchmark and an accompanying pipeline for evaluating and improving LLMs' program modeling capability by modeling Python programs into verification-ready model checking specifications checkable by its accompanying model checker. Model-Bench comprises 400 Python programs derived from three well-known benchmarks (HumanEval, MBPP, and LiveCodeBench). Our extensive experiments reveal significant limitations in LLMs' program modeling and further provide inspiring directions.
• Abstract（参考訳）: デジタル時代には、ソフトウェアの正当性、安全性、信頼性を形式的検証を通じて保証することが最重要であり、特にソフトウェアが重要な基盤を担っている。 形式的検証は、定理証明とモデル検査に分割され、実現可能で信頼性の高い経路を提供する。 顕著な進歩をもたらす定理証明とは異なり、自動プログラムモデリングの難しさから、モデル検査は焦点を絞ってはいない。 このギャップを埋めるために、Pythonプログラムをモデルチェッカーでチェック可能な検証可能なモデルチェック仕様にモデル化することで、LLMのプログラムモデリング機能の評価と改善のためのベンチマークと付随パイプラインであるModel-Benchを紹介する。 Model-Benchは、よく知られた3つのベンチマーク(HumanEval、MBPP、LiveCodeBench)から派生した400のPythonプログラムで構成されている。 LLMのプログラムモデリングには大きな制限があり、さらに刺激的な方向を提供する。

関連論文リスト

• Can Large Language Models Implement Agent-Based Models? An ODD-based Replication Study [0.6821122205224714]
  大規模言語モデル(LLM)は、テキスト記述から非自明な実行可能なコードを合成できるようになった。 LLMは、複製、検証、検証をサポートする方法で、標準化された仕様からエージェントベースのモデルを確実に実装できますか? 制御されたODD-to-code翻訳タスクにおいて17の現代LLMを評価する。
  論文  参考訳（メタデータ） (2026-02-08T19:56:20Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  本稿では,dLLMの復号化機構をモデル属性の強力なツールとして利用できることを示す。 本稿では、デコードステップ間の構造的関係を捉え、モデル固有の振る舞いをよりよく明らかにする、DDM(Directed Decoding Map)と呼ばれる新しい情報抽出手法を提案する。
  論文  参考訳（メタデータ） (2025-10-02T06:25:10Z)
• 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)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• Learning Program Behavioral Models from Synthesized Input-Output Pairs [70.9524884086882]
  本稿では,ニューラルマシン翻訳アルゴリズムを用いて,入力/出力動作からモデルを学習するフレームワークであるModelizerを紹介する。 Modelizerはオリジナルのプログラムをモックし、95.4%の精度でBLEUスコアは0.98で、現実世界のアプリケーションのモックには0.04の標準エラーがある。 プログラムの出力がプログラムの振舞いのあらゆる側面となるため、これらのモデルのいくつかの応用を予想する。
  論文  参考訳（メタデータ） (2024-07-11T15:25:02Z)
• Arithmetic in Transformers Explained [1.8434042562191815]
  我々は、加算、減算、または両方で訓練された44個の自己回帰トランスモデルを解析する。 加算モデルが共通論理アルゴリズムに収束し、ほとんどのモデルが99.999%の精度で予測できることを示す。 我々は,これらのアルゴリズム回路を定義し,発見し,視覚化するために,機械的解釈可能性ツールの再利用ライブラリを導入する。
  論文  参考訳（メタデータ） (2024-02-04T21:33:18Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  ショッピング・バスケット・アプリケーション・モデルにおけるPrism Model Checkerを用いたシミュレーションの結果を示す。 目的は、買い物客が買い物プロセスの多くの定義された状態を通過するときの行動をシミュレートすることである。
  論文  参考訳（メタデータ） (2023-07-16T00:14:40Z)
• Self-Checker: Plug-and-Play Modules for Fact-Checking with Large Language Models [75.75038268227554]
  Self-Checkerはファクトチェックを容易にするプラグインとプレイモジュールからなるフレームワークである。 このフレームワークは、低リソース環境でファクトチェックシステムを構築するための、高速で効率的な方法を提供する。
  論文  参考訳（メタデータ） (2023-05-24T01:46:07Z)

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

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