Lanyon AI 披露了1060万美元的融资，用于经过形式化验证的科学代码

位于普林斯顿的实验室将 LLM 与符号编译器配对，从同一规范生成科学代码和机器可验证的证明。

By · Published · Updated

Primary source: PR Newswire

为何重要

形式化验证可以使 AI 生成的科学软件可审计，但其价值取决于经认证的规范是否捕捉到工程师的真实意图。

Lanyon AI discloses $10.6M round for formally verified scientific code — The Princeton-based lab pairs an LLM with a symbolic compiler to generate scientific code and machine-checkable proofs from one specification.

Jonathan Gorard, Ammar Hakim, and James "Jimmy" Juno 在 8 月 17 日披露了对 Lanyon AI 的 1,060 万美元初始融资轮，支持他们尝试让 AI 生成的科学软件证明其满足规范要求的努力。…

When you purchase through links in our articles, we may earn a small commission. This doesn’t affect our editorial independence.

Reader comments

Conversation for this story loads after sign-in.