Imandra CodeLogician：将大型语言模型引入形式化验证的全新框架

Imandra CodeLogician 是 Imandra 团队推出的一个原型系统，旨在把大规模语言模型（LLM）与成熟的形式化方法相结合，实现 自然语言到可验证代码 的闭环。系统整体架构分为三层：

1. 前端 LLM 接口 – 采用 OpenAI GPT‑4（或本地部署的 LLaMA）解析用户的自然语言需求，自动生成 Imandra DSL（类似 Python 的函数式语言）代码片段以及对应的规范说明。
2. 中间转换层 – 将 LLM 输出的 DSL 代码映射为 Imandra 的内部抽象语法树（AST），并注入 自动化证明策略（如 induction、SMT 求解器）
3. 后端形式化引擎 – 利用 Imandra 的交互式定理证明器对生成的规范进行 自动化验证，若验证失败会把错误信息回传给 LLM，进行迭代修正。

关键特性

• 自然语言到证明的端到端流水线：用户只需描述“函数 sort 必须返回升序列表”，系统即可生成实现、规范以及完整的归纳证明。
• 可插拔的 LLM：支持 OpenAI、Anthropic、Claude、以及本地模型（通过 ollama run）
• 即时反馈循环：验证失败时，LLM 会基于错误提示自动重写代码或补充前置条件。

示例代码

# 用户自然语言需求
# “实现一个函数 `max_pair`，返回列表中最大的两个数，并证明返回值始终是列表中最大的两个元素”。

# LLM 生成的 Imandra DSL
let max_pair (xs: list[int]) : (int * int) =
  match xs with
  | [] -> (0,0)
  | [x] -> (x,0)
  | x::y::rest ->
      let (a,b) = max_pair (y::rest) in
      if x > a then (x,a) else (a,x)

# 自动生成的定理
theorem max_pair_correct:
  forall xs.
    let (m1,m2) = max_pair xs in
    m1 >= m2 /\
    (forall y in xs. y <= m1) /\
    (forall y in xs. y = m1 -> y <= m2)

上述代码在 Imandra REPL 中执行 prove max_pair_correct，系统会自动选择归纳策略并给出 QED。若证明卡住，LLM 会收到类似 “归纳基不完整” 的提示，重新生成更强的前置条件。

适用场景

• 安全关键代码审计：快速生成形式化规范并验证现有实现。
• 教学与科研：帮助学生理解归纳证明的思路，降低学习门槛。
• 原型快速迭代：在需求变更时，仅需修改自然语言描述，系统自动同步代码与证明。

开源实现

项目代码已在 GitHub 上公开，采用 MIT 许可证，支持 Docker 一键部署。

# 拉取并启动
git clone https://github.com/imandra-ai/codelogician.git
cd codelogician
pip install -r requirements.txt
docker compose up -d   # 启动 Imandra 后端 + LLM 接口

通过 RESTful API（POST /generate）即可提交自然语言需求，返回完整的 DSL 与证明状态。