Imandra 新推出的 AI 编程助手 CodeLogician 利用"推理能力"确保代码准确性

初创公司 Imandra Inc. 表示，通过推出一个全新的自动推理系统 CodeLogician，他们将人工智能驱动的代码补全技术提升到了一个新的水平。

与其他专门用于代码补全任务的大语言模型(如 GitHub Inc. 的 Copilot)不同，CodeLogician 据称基于一个称为"神经符号 AI"的新概念，这使它能够对生成的代码进行推理，大大降低了所谓的"幻觉"或不准确的可能性。

CodeLogician 由 ImandraX 驱动，这是 Imandra Core 推理引擎的最新版本，在金融服务业和政府部门广泛应用于验证、测试和审计关键任务系统，包括国家证券交易所。

通过自动将创建的代码转换为数学模型，CodeLogician 可以利用 ImandraX 引擎更好地理解、分析和验证应用层源代码。它还可以自动生成测试用例来证明代码的准确性。因此，CodeLogician 不仅是一个 AI 编程助手，还是一个验证工具，可以保证其生成代码的准确性，帮助开发者发现任何安全漏洞并证明代码按预期运行。

CodeLogician 使用 LangGraph 框架构建，其初始版本与 Python 编程语言兼容，未来的更新将增加对 Java 和 COBOL 的支持，从而能够帮助转换遗留软件应用。

据 Imandra 表示，CodeLogician 将彻底改变开发者的生产力，消除了手动验证数千行 AI 生成代码的负担。

Imandra 联合创始人兼联合首席执行官 Grant Passmore 表示，现有的生成式 AI 编码工具存在缺陷，因为尽管它们生成了大量看似合理的代码，但无法保证这些代码的准确性。

"这些代码通常会以微妙且危险的方式出错，" 他说。"CodeLogician 超越了生成式 AI，使用符号数学推理来确保代码真正按预期运行。"

Imandra 表示，CodeLogician 的核心优势在于 LangGraph 框架，它允许系统迭代优化其底层模型，解释其推理过程并提供高度保证。为此，它依赖于一个称为"状态空间探索"的独特特性，这使它能够通过符号区域分解来全面分析大语言模型的所有可能状态和行为。

这是一种新颖的技术，使其能够理解底层大语言模型在尝试解决问题时的思考过程。这有助于确保大语言模型生成的代码准确性，然后应用智能测试来证明其正确性。

CodeLogician 现已向早期测试者开放，开发者可以注册候补名单以获取访问权限。一旦正式发布，它将通过应用程序编程接口 (API) 提供程序化访问，并在 Microsoft Corp. 的 Visual Studio Code Marketplace 中作为 VS Code 扩展提供。

"比尔·盖茨曾将通用软件开发的形式化方法称为'圣杯'，" Imandra 的另一位联合首席执行官 Denis Ignatovich 说。"现在，借助神经符号 AI 的力量和自动推理的突破，我们正在逐步接近实现这一目标 — 将先进的推理工具直接交到工程师手中。"