複雑な指示不要、AIの自己修正を繰り返すだけで未解決の数学難問8件を解明

研究チームは、AIによる形式的定理証明において、複雑な人間の設計手順を介さず単純な自己内省ループを回す検証環境「h1」を発表した。近年、数学の証明AIでは問題の分解や計画立案といった人間による複雑なワークフローが多用されているが、シンプルな計算量の拡大が対抗できるかを検証した。

「h1」は問題の分解や探索構造を強制せず、証明支援系「Lean 4」からの検証フィードバックとモデル自身の内省のみを繰り返す仕組みを採用した。検証の結果、「PutnamBench」や「FATE-X」などのベンチマークで最高水準の性能を記録したほか、「FormalConjectures」における未解決問題8件を解決した。

同一モデルでの比較において「Goedel-Architect」や「AlphaProof Nexus」といった専用ワークフローと同等以上の成果を収めており、1回の試行でも難問解決に達することが示された。研究チームは、複雑な手順を規定する前に実行フィードバック環境を整えるべきだと提言している。