検証条件のためのニューラル定理証明：実世界ベンチマーク
TL;DRプログラム検証におけるボトルネックである「検証条件（VC）」の自動証明に特化した、初の実世界・多言語ベンチマーク「NTP4VC」が提案されました。Linux等の実プロジェクトから生成されたデータを用い、Isabelle、Lean、Rocqに対応。LLMの可能性と現状の課題を浮き彫りにしています。
Cog AI Archive
最新の記事
人気記事ピックアップ
RedSage: サイバーセキュリティに特化した汎用LLM
TL;DRRedSageは、プライバシーリスクを回避しつつ多様なセキュリティ業務を支援するために開発された、オープンソースのサイバーセキュリティ特化型LLMである。118億トークンの専門データによる事前学習と、エージェントベースのパイプラインで生成された26.6万件の指示データによる調整を経て、既存モデルを上回る性能を実現した。
EvolVE：LLMベースのVerilog生成と最適化のための進化的探索
TL;DR大規模言語モデル（LLM）を用いたVerilog生成において、厳密な論理や並行性の扱いに課題がある中、本研究は進化的探索を用いた新フレームワーク「EvolVE」を提案します。モンテカルロ木探索とIdea-Guided Refinementを組み合わせ、機能的正当性と最適化性能を向上させました。
保存済みの記事がまだありません。
読み込み中…