参照実装は設計判断を保存する

SPA を一つ動かすところまでなら、React で画面を作り、HTTP API を用意し、データベースへ接続すれば形になる。しかし、業務アプリケーションとして継続利用できる状態まで進めると、画面と API の外側に別の設 … 続きを読む

カテゴリー tech

AI エージェントの安全境界は改変・探索・再利用できる経路から分離する

AI エージェントへ安全規則を与える方法として、禁止操作を定義する、実行時に監視する、操作履歴を保存する、機密情報の扱いを指示するといった仕組みがある。これらはそれぞれ異なる役割を持つ。禁止操作の定義は、どの行動を許可す … 続きを読む

AI の長期記憶は、履歴から現在状態を再構成する

長期的に利用する AI には、過去の会話や出来事から得た情報を保持し、後の判断に利用する能力が求められる。ところが、記録として正しいことと、現在の判断材料として正しいことは一致するとは限らない。勤務先、予定、役割、利用中 … 続きを読む

数学の希少資源が答えから理解へ移り始めた

数学の未解決問題には、答えへ到達するまで何年、何十年とかかるものがある。時間を要する理由は、最終的な証明を書く作業だけにあるのではなく、その証明へ至る経路を見つけるまでに大きな探索が必要になるためである。どの定理を使うか … 続きを読む

M4 Max 128GB でローカル LLM を仕事単位で評価する

ローカル LLM の性能を確認するとき、最初に目に入るのは、モデルを端末のメモリーへ読み込めるか、そして 1 秒間に何トークンを生成できるかという数字である。前者はモデルをその計算機で実行できるかを決め、後者は文章が返っ … 続きを読む

カテゴリー tech

アクチュアリー領域の AI モダナイゼーションで数理モデルの同一性を検証する

生成 AI や AI エージェントは、既存コードの読解、別言語への変換、設計資料の整理、試験コードの生成を高速化できる。モダナイゼーションで本当に難しいのは、変換そのものより、変換後のシステムを何を根拠に「同じ業務を実行 … 続きを読む

フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか

AI が正しい文章やコードを生成できることと、その成果物が正しいと確定できることは別の問題である。生成結果がもっともらしく見えること、過去より正答率が高いこと、別の AI が正しいと評価したことは、いずれも成果物そのもの … 続きを読む