その現実を前に、シリコンバレーの一部のスタートアップ企業は、AIによって生成されたコードの精度を検証するための技術開発を模索しています。
ChatGPTのようなAIチャットボットや、現在のプログラミングサポートシステムは、わずか数秒でコンピューターコードを作成できます。それでも、専門家は、これらのシステムは時々エラーが発生したり、不正確な情報を生成したりすることさえあると述べています。
カーネギーメロン大学(米国)の研究者によって1月に発表された研究によると、コード生成AIツールはソフトウェア開発プロセスを加速するのに役立つ可能性があります。ただし、コードの品質を低下させ、長期的にプロジェクトに問題を引き起こす可能性もあります。
この課題に直面して、シリコンバレーの多くのスタートアップ企業は、コンピューターコードを検証するための技術を開発しています。
Axiom MathやHarmonic(カリフォルニア州パロアルト)、Logical Intelligence(サンフランシスコ)などの人工知能分野のテクノロジースタートアップは、数学者が問題を証明するのと同様の方法でコードを検証できるAIシステムを構築しています。
Axiom Mathの創設者兼CEOであるカリーナ・ホン氏は、コード認証はAI技術開発の次のステップになる可能性があると述べています。
最近、同社はメンロー・ベンチャーズ、グレイクロフト、マドローナを含むベンチャーキャピタルファンドから2億米ドルの資金調達に成功したと発表しました。
設立から約1年で従業員はわずか約20人ですが、Axiom Mathは16億米ドルの評価を受けています。投資家は、同社の技術がCodexやClaude CodeなどのAIシステムによって生成されたコードの品質を向上させるのに役立つと信じています。
マット・クラニング(テクノロジー分野のベンチャー投資家であり、メンロー・ベンチャーズのパートナー)によると、現在AIを使用してコードを作成する際の最大の問題は、ユーザーがコードにエラーがあるかどうかを確認できないことです。
マット・クラニング氏は、Axiomのようなコード検証技術は、この問題をある程度解決するのに役立つ可能性があると述べています。
当初、Axiomは複雑な数学の問題を解決するための技術を開発しました。同社のシステムであるAxiomProverは、パットナム数学コンテスト(米国とカナダで最も優秀な大学生コンテストの1つ)で満点を獲得しました。
この技術は、10年以上前に数学的命題を証明するために開発されたリーンプログラミング言語を使用して動作します。
数学における正誤を明確に特定する能力のおかげで、システムは問題を解決する過程で論理的なエラーを排除できます。
研究者たちは、同じ方法をコンピューターコードを検証するために適用できることを期待しています。これは、「移行学習」の例であり、AIシステムがある分野でスキルを習得し、他のタスクに成功裏に適用する場合です。
それにもかかわらず、一部の専門家は、この方法には依然として制限があると警告しています。カーネギーメロン大学のコンピュータサイエンス教授であるボグダン・ヴァシレスク氏によると、「正しい」コンピュータコードとは何かを常に明確に特定できるわけではありません。
実際には、多くのソフトウェア、特に何百万人ものユーザーにサービスを提供するオンラインサービスは、複雑で予測不可能な動作環境になるだろう。
したがって、AIはいくつかのエラーをチェックするのに役立ちますが、この技術はコンピューターコード内のすべての問題を完全に排除することは困難です。
