「形式検証」の記事一覧

• 形式的不確実性の文法：LLMによる自動推論の信頼性評価

  2025-05-27 02:27

  科学・技術

  大規模言語モデル（LLM）は形式仕様の自動生成に有望ですが、確率的出力と決定論的検証とのギャップが課題です。本論文は、LLMが形式的推論で誤る要因と、不確実性の定量化手法の効果を検証しました。SAT/SMT問題においては分野依存の精度変動が顕著で、既存のエントロピー指標などでは誤りを十分に検出できませんでした。そこで、出力を確率文脈自由文法（PCFG）でモデル化し、文法エントロピーなどの新たな指標を提案。これにより選択的検証で誤り率を最大100%削減する方法を示しました。

• ACE-RISCV: RISC-V向けの機密計算フレームワーク

  2025-05-21 20:21

  科学・技術

  IBMによるオープンソースプロジェクトACE-RISCVは、RISC-Vアーキテクチャ向けの仮想マシンベースの信頼実行環境（TEE）を提供する機密計算フレームワークです。形式検証されたセキュリティモニターを中核とし、PQC（耐量子暗号）にも対応。ローカルアテステーション機能により、ネット接続のない組み込み機器でも安全性を担保します。Linux KVMやQEMU上での動作も可能で、開発者向けの詳細な構築手順も公開されています。