The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Has anyone written an Ltac2 function (e.g. string -> string, or string list -> list) to query LLMs like chatgpt?

We tried to write it but ran into plugin build issues minimized here :

[abhishek@optiplex ltac2-llm]$ cat theories/llm.v
Require Import Ltac2.Ltac2.

Declare ML Module "ltac2-llm-plugin.plugin".

Module LLM.

 Ltac2 @ external query_gpt : string -> string :=
   "ltac2_llm" "guery_gpt".

End LLM.

Ltac2 Eval LLM.query_gpt "write an Inductive to define the AST of C++".


[abhishek@optiplex ltac2-llm]$ cat plugin/main.ml
open Ltac2_plugin
open Tac2ffi
open Tac2externals
open Openai

let api_key = Sys.getenv "OPENAI_API_KEY"
let client = Client.create api_key

let bytes_fn_of_string (f: string->string) (b:bytes) :bytes =
 Bytes.of_string (f (Bytes.to_string b))

let llmquery (s:string) : string =
 Lwt_main.run (Chat_completion.(
 send
   client
   ~temperature:0.0
   ~model:"gpt-4o"
   ~messages:
     [ { role = `System; content = "You are an expert in logic, formal methods, constructive type theory, dependent type theory, Coq (Gallina, Ltac, Ltac2)" }
     ; { role = `User; content = s }
     ]
   ()))

let define s =
 define Tac2expr.{ mltac_plugin = "ltac2_llm"; mltac_tactic = s }

let _ =
 define "query_gpt" (bytes @-> ret bytes) @@ fun s ->
   bytes_fn_of_string llmquery s
[abhishek@optiplex ltac2-llm]$
 

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/