AutoVerus爆誕！Rustコードを自動で証明しちゃう最強ツール✨
- Rustコードの証明（しょうめい）を自動生成するAutoVerusってスゴくない？😍
- LLM（大規模言語モデル）がRustコードの正しさを証明する注釈（アノテーション）を生成するんだって！✍️
- 形式検証（けいしきけんしょう）のハードルを下げて、みんなが安心してコード書けるようになるって最高じゃん？🥳
● 背景：ソフトウェアのバグを減らして、セキュリティを強化したいって課題があったの！ ● 方法：LLMを使って、Rustコードの正しさを証明する注釈を自動で作っちゃう！ ● 結果：開発者は専門知識（せんもんちしき）なしでコードの正しさを確認できるようになったの！ ● 意義（ここがヤバい♡ポイント）：ソフトウェアの品質（ひんしつ）が爆上がりして、IT業界がもっと発展（はってん）するかも！
AutoVerus は、Rustコードを安全にしたい企業とか開発者（かいはつしゃ）に超オススメ💖 バグ減るし、セキュリティも上がるし、最高じゃん？👏 形式検証（けいしきけんしょう）の知識がなくても使えるから、初心者（しょしんしゃ）でも安心だよ！👍
💡 リアルでの使いみち
- クラウドサービスとかAIプラットフォームで、セキュリティレベルを爆上げ！🚀
- Webアプリとかモバイルアプリで、ユーザーのデータとかを守る！🛡️
続きは「らくらく論文」アプリで
AutoVerus: Automated Proof Generation for Rust Code
Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.