論文の概要: Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

• arxiv url: http://arxiv.org/abs/2607.04631v1
• Date: Mon, 06 Jul 2026 03:31:14 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-07-07 22:26:30.025692
• Title: Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
• Title（参考訳）: 形式的ディスコ:形式的検証プログラムのスケーラブルなオープンエンディング生成
• Abstract要約: フォーマル・ディスコ(Formal Disco)は、LDMベースの労働者の協調のための分散システムである。 大規模なオープンエンド合成データ生成にも容易に適用できる。 合成検証プログラムの大規模なデータセットを3つの言語でリリースする。
• 参考スコア（独自算出の注目度）: 43.83836626474095
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides the strongest possible guarantees, but the ability of AI models to work with verification-aware languages is hindered by the scarcity of human-written examples of programs in those languages. To tackle this prevalent data scarcity issue, we propose Formal Disco: a distributed system for coordination of LLM-based workers that can be easily applied to open-ended synthetic data generation at scale. We use Formal Disco to share tasks and programs between three classes of workers: "initiators", which read random READMEs from open-source repositories and documentation snippets to sketch a related verified program, "fixers" which take compiler and verifier feedback and attempt to resolve issues, and "extenders" that take working programs and propose patches to expand them. Formal Disco records all agent-generated traces and uses them both for initial distillation from a stronger model as well as self-improvement. We also propose a principle of maximum entropy for synthetic program generation, and use entropy maximization via iterative supervised fine-tuning to learn to generate increasingly diverse programs over time. We release large datasets of synthetic verified programs in three languages - Dafny, Verus, and Frama-C -, and fine-tune open models for verification-relevant tasks, often matching or exceeding the performance of Claude Opus 4.5. Overall, our work offers a path to create synthetic data at scale for formal reasoning domains and overcome the long-standing data barrier.
• Abstract（参考訳）: コード生成のコストは、AIエージェントの能力向上によって急速に低下していますが、生成されたプログラムの品質保証はペースを保っていません。 形式的検証は、最強の保証を提供するが、検証対応言語を扱うAIモデルの能力は、それらの言語における人間の記述したプログラムの例が不足していることによって妨げられる。 このようなデータ不足問題に対処するために,大規模でオープンな合成データ生成に容易に適用可能な,LLMベースの作業者の協調のための分散システムであるFormal Discoを提案する。 オープンソースのリポジトリやドキュメントスニペットからランダムにREADMEを読み取って、関連する検証プログラムをスケッチする"initiator"、コンパイラと検証者からのフィードバックを受け取り、問題の解決を試みる"fixers"、作業プログラムを取り込み、それらを拡張するためのパッチを提案する"exenders"である。 フォーマル・ディスコは、全てのエージェント生成トレースを記録し、より強いモデルからの最初の蒸留と自己改善の両方に使用する。 また、合成プログラム生成のための最大エントロピーの原理を提案し、反復的教師付き微調整によるエントロピー最大化を用いて、時間とともに多様なプログラムを生成することを学ぶ。 Dafny、Verus、Frama-Cの3つの言語で合成検証プログラムの大規模なデータセットを公開し、Claude Opus 4.5のパフォーマンスにマッチまたは超過する検証関連タスクのための微調整オープンモデルをリリースする。 全体として、我々の研究は、形式的推論ドメインのために大規模に合成データを作成し、長期間にわたるデータバリアを克服する道を提供する。

関連論文リスト

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMICは、データ合成を推論するための厳密な媒体として実行可能なコードを活用するフレームワークである。 MIMICは、ナラティブ融合、コード誘導テスト合成、動的コードインスツルメンテーションを通じて、アルゴリズムを検証可能な推論軌道に変換する。 提案手法は, 一般的な推論, 複雑な数学的ベンチマーク, きめ細かい決定論的タスクにおいて, 精度を著しく向上させる。
  論文  参考訳（メタデータ） (2026-09-13T17:04:16Z)
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
  エージェントAIシステムは、驚くほどの頻度でコードを生成することができる。 生成されたコードが実際にユーザが意図した通りに動作するようにします。
  論文  参考訳（メタデータ） (2026-03-17T21:28:59Z)
• Automatic Syntax Error Repair for Discrete Controller Synthesis using Large Language Model [8.741815980649667]
  本稿では,Large Language Models (LLMs) を利用してDCSモデルの構文誤りを修復する自動手法を提案する。 LLMには形式文法規則やイラストレーション例を含むDCS固有のドメイン知識が備わっており、正確な修正を導く。 人間の開発者に比べて3.46倍のスピードアップを実現している。
  論文  参考訳（メタデータ） (2025-12-08T07:57:15Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• 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)
• GenerationPrograms: Fine-grained Attribution with Executable Programs [72.23792263905372]
  コードエージェント」アーキテクチャの最近の進歩に触発されたモジュラー生成フレームワークであるGenerationProgramsを導入する。 GenerationProgramsは、プロセスを2つの異なるステージに分解する: まず、クエリに明示的に調整されたモジュール形式のテキスト操作からなる実行可能なプログラムプランを作成し、次に、プログラムの指定した命令に従ってこれらの操作を実行し、最終的な応答を生成する。 経験的評価は、生成プログラムは文書レベルと文レベルの両方の属性品質を著しく改善することを示している。
  論文  参考訳（メタデータ） (2025-06-17T14:37:09Z)
• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs [7.087237546722617]
  ソフトウェア正当性を確立する最も強力な方法の1つは、フォーマルな方法を使用することである。 私たちの仕事は、形式モデルの作成を自動化することで、この重大な欠点に対処します。 このようにして、形式モデルを作成するのに必要な時間を大幅に削減する。
  論文  参考訳（メタデータ） (2025-01-22T15:57:29Z)
• Joint Verification and Refinement of Language Models for Safety-Constrained Planning [25.390607788572535]
  大規模言語モデルは、ロボットタスクを実行するために自然言語記述からプログラムを生成することができる。 しかしながら、これらの生成されたプログラムは、しばしば外部から与えられたタスク仕様に違反するエラーを含む。 本稿では,生成したロボットプログラムを自動表現に変換する手法を開発し,タスク関連安全仕様に対して検証する。
  論文  参考訳（メタデータ） (2024-10-18T21:16:30Z)
• Procedures as Programs: Hierarchical Control of Situated Agents through Natural Language [81.73820295186727]
  エージェント命令と制御のための階層的な手続き的知識を表現する強力な手法である,プログラムとしての手続きの形式化を提案する。 NL命令に対するIQAおよびALFREDデータセット上で、このフレームワークをインスタンス化する。
  論文  参考訳（メタデータ） (2021-09-16T20:36:21Z)

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

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