FormalScience：Leanにおけるエージェント的コード生成による、スケーラブルな人間参加型オートフォーマライゼーション
arXiv cs.AI / 2026/4/28
📰 ニュースDeveloper Stack & InfrastructureTools & Practical UsageModels & Research
要点
- この論文は、専門分野に依存しない人間参加型のエージェント的パイプライン「FormalScience」を提案し、非形式的な科学・数学的推論をLean上で構文的に正しく、かつ意味的にも整合する形式証明へと低コストで変換できるようにします。
- その手法を物理で実証するために、「FormalPhysics」として200件の大学レベルの物理問題と解答（主に量子力学と電磁気学）と、それらのLean4による形式化を収録したデータセットを構築しています。
- 著者らは、ゼロショット・プロンプト、誤りフィードバック付きの自己改善、さらに新しい多段階のエージェント手法を用いて、このデータセット上でステートメントのオートフォーマライゼーションを行う際の性能を、オープンソースモデルとプロプライエタリシステムの両方で評価します。
- 物理分野における「意味ドリフト」を、表記の崩壊（notational collapse）や抽象化の持ち上げ（abstraction elevation）といった概念で体系的に特徴付け、意味を完全に保存できない場合に形式言語が何を検証しているのかを説明します。
- 本研究では、コードベースとUI付きのインタラクティブなFormalScienceシステムを公開し、物理以外の科学分野でもオートフォーマライゼーションと定理証明を支援します。
